carl  24.04
Computer ARithmetic Library
Public Member Functions | Static Public Member Functions | Protected Member Functions | Private Types | Private Member Functions | Private Attributes
carl::FormulaPool< Pol > Class Template Reference

#include <FormulaPool.h>

Inheritance diagram for carl::FormulaPool< Pol >:
Inheritance graph
[legend]
Collaboration diagram for carl::FormulaPool< Pol >:
Collaboration graph
[legend]

Public Member Functions

std::size_t size () const
 
void print () const
 
Formula< Pol > getTseitinVar (const Formula< Pol > &_formula)
 
Formula< Pol > createTseitinVar (const Formula< Pol > &_formula)
 
template<typename ArgType >
void forallDo (void(*_func)(ArgType *, const Formula< Pol > &), ArgType *_arg) const
 
bool formulasInverse (const Formula< Pol > &_subformulaA, const Formula< Pol > &_subformulaB)
 

Static Public Member Functions

static FormulaPool< Pol > & getInstance ()
 Returns the single instance of this class by reference. More...
 

Protected Member Functions

 FormulaPool (unsigned _capacity=10000)
 Constructor of the formula pool. More...
 
 ~FormulaPool ()
 
const FormulaContent< Pol > * trueFormula () const
 
const FormulaContent< Pol > * falseFormula () const
 

Private Types

using underlying_set = boost::intrusive::unordered_set< FormulaContent< Pol > >
 

Private Member Functions

bool isBaseFormula (const Constraint< Pol > &c) const
 
bool isBaseFormula (const UEquality &ueq) const
 
bool isBaseFormula (const VariableComparison< Pol > &vc) const
 
bool isBaseFormula (const VariableAssignment< Pol > &va) const
 
bool isBaseFormula (const FormulaContent< Pol > *f) const
 
const FormulaContent< Pol > * getBaseFormula (const FormulaContent< Pol > *f) const
 
FormulaContent< Pol > * createNegatedContent (const FormulaContent< Pol > *f) const
 
const FormulaContent< Pol > * create (FormulaType _type)
 Create formula representing a boolean value. More...
 
const FormulaContent< Pol > * create (Variable _variable)
 Create formula representing a boolean variable. More...
 
const FormulaContent< Pol > * create (Constraint< Pol > &&_constraint)
 
const FormulaContent< Pol > * create (const Constraint< Pol > &_constraint)
 
const FormulaContent< Pol > * create (VariableComparison< Pol > &&_variableComparison)
 
const FormulaContent< Pol > * create (const VariableComparison< Pol > &_variableComparison)
 
const FormulaContent< Pol > * create (VariableAssignment< Pol > &&_variableAssignment)
 
const FormulaContent< Pol > * create (const VariableAssignment< Pol > &_variableAssignment)
 
const FormulaContent< Pol > * create (BVConstraint &&_constraint)
 
const FormulaContent< Pol > * create (const BVConstraint &_constraint)
 
const FormulaContent< Pol > * create (FormulaType _type, Formula< Pol > &&_subFormula)
 Create formula representing a unary function. More...
 
const FormulaContent< Pol > * create (FormulaType _type, const Formulas< Pol > &_subformulas)
 Create formula representing a nary function. More...
 
const FormulaContent< Pol > * create (FormulaType _type, const std::initializer_list< Formula< Pol >> &_subformulas)
 
const FormulaContent< Pol > * create (FormulaType _type, Formulas< Pol > &&_subformulas)
 
const FormulaContent< Pol > * createImplication (Formulas< Pol > &&_subformulas)
 Create formula representing an implication. More...
 
const FormulaContent< Pol > * createNAry (FormulaType _type, Formulas< Pol > &&_subformulas)
 
const FormulaContent< Pol > * createITE (Formulas< Pol > &&_subformulas)
 
const FormulaContent< Pol > * create (FormulaType _type, std::vector< Variable > &&_vars, const Formula< Pol > &_term)
 
const FormulaContent< Pol > * create (const FormulasMulti< Pol > &_subformulas)
 
const FormulaContent< Pol > * create (const UTerm &_lhs, const UTerm &_rhs, bool _negated)
 
const FormulaContent< Pol > * create (UEquality &&eq)
 
void free (const FormulaContent< Pol > *_elem)
 
bool freeTseitinVariable (const FormulaContent< Pol > *_toDelete)
 
void reg (const FormulaContent< Pol > *_elem) const
 
const FormulaContent< Pol > * add (FormulaContent< Pol > &&_formula)
 Adds the given formula to the pool, if it does not yet occur in there. More...
 
void check_rehash ()
 

Private Attributes

friend Singleton< FormulaPool >
 
friend Formula< Pol >
 
unsigned mIdAllocator
 id allocator More...
 
FormulaContent< Pol > * mpTrue
 The unique formula representing true. More...
 
FormulaContent< Pol > * mpFalse
 The unique formula representing false. More...
 
pool::RehashPolicy mRehashPolicy
 
std::unique_ptr< typename underlying_set::bucket_type[]> mPoolBuckets
 
underlying_set mPool
 The formula pool. More...
 
FastPointerMap< FormulaContent< Pol >, const FormulaContent< Pol > * > mTseitinVars
 
FastPointerMap< FormulaContent< Pol >, typename FastPointerMap< FormulaContent< Pol >, const FormulaContent< Pol > * >::iterator > mTseitinVarToFormula
 

Detailed Description

template<typename Pol>
class carl::FormulaPool< Pol >

Definition at line 32 of file FormulaPool.h.

Member Typedef Documentation

◆ underlying_set

template<typename Pol >
using carl::FormulaPool< Pol >::underlying_set = boost::intrusive::unordered_set<FormulaContent<Pol> >
private

Definition at line 48 of file FormulaPool.h.

Constructor & Destructor Documentation

◆ FormulaPool()

template<typename Pol >
carl::FormulaPool< Pol >::FormulaPool ( unsigned  _capacity = 10000)
protected

Constructor of the formula pool.

Parameters
_capacityExpected necessary capacity of the pool.

◆ ~FormulaPool()

template<typename Pol >
carl::FormulaPool< Pol >::~FormulaPool ( )
protected

Member Function Documentation

◆ add()

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::add ( FormulaContent< Pol > &&  _formula)
private

Adds the given formula to the pool, if it does not yet occur in there.

Note, that this method uses the allocator which is locked before calling.

Parameters
_formulaThe formula to add to the pool.
Returns
The given formula, if it did not yet occur in the pool; The equivalent formula already occurring in the pool, otherwise.
Here is the caller graph for this function:

◆ check_rehash()

template<typename Pol >
void carl::FormulaPool< Pol >::check_rehash ( )
inlineprivate

Definition at line 600 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [1/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( BVConstraint &&  _constraint)
inlineprivate

Definition at line 276 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [2/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( const BVConstraint &  _constraint)
inlineprivate

Definition at line 283 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [3/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( const Constraint< Pol > &  _constraint)
inlineprivate

Definition at line 250 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [4/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( const FormulasMulti< Pol > &  _subformulas)
inlineprivate
Parameters
_subformulasThe sub-formulas of the formula to create.
Returns
A formula with the given operator and sub-formulas.

Definition at line 406 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [5/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( const UTerm &  _lhs,
const UTerm &  _rhs,
bool  _negated 
)
inlineprivate

Definition at line 442 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [6/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( const VariableAssignment< Pol > &  _variableAssignment)
inlineprivate

Definition at line 272 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [7/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( const VariableComparison< Pol > &  _variableComparison)
inlineprivate

Definition at line 260 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [8/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( Constraint< Pol > &&  _constraint)
inlineprivate
Parameters
_constraintThe constraint wrapped by this formula.
Returns
A formula with wrapping the given constraint.

Definition at line 236 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [9/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( FormulaType  _type)
inlineprivate

Create formula representing a boolean value.

Parameters
_typeFormula type, may be either TRUE or FALSE.
Returns
A formula representing the given bool.

Definition at line 218 of file FormulaPool.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ create() [10/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( FormulaType  _type,
const Formulas< Pol > &  _subformulas 
)
inlineprivate

Create formula representing a nary function.

Parameters
_typeFormula type specifying the function.
_subformulasFormula representing the function arguments.
Returns
A formula representing the given function call.

Definition at line 336 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [11/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( FormulaType  _type,
const std::initializer_list< Formula< Pol >> &  _subformulas 
)
inlineprivate

Definition at line 339 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [12/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( FormulaType  _type,
Formula< Pol > &&  _subFormula 
)
inlineprivate

Create formula representing a unary function.

Parameters
_typeFormula type specifying the function.
_subFormulaFormula representing the function argument.
Returns
A formula representing the given function call.

Definition at line 294 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [13/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( FormulaType  _type,
Formulas< Pol > &&  _subformulas 
)
inlineprivate

Definition at line 342 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [14/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( FormulaType  _type,
std::vector< Variable > &&  _vars,
const Formula< Pol > &  _term 
)
inlineprivate
Parameters
_type
_vars
_term
Returns

Definition at line 393 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [15/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( UEquality &&  eq)
inlineprivate

Definition at line 453 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [16/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( Variable  _variable)
inlineprivate

Create formula representing a boolean variable.

Parameters
_variableThe Boolean variable wrapped by this formula.
Returns
A formula with wrapping the given Boolean variable.

Definition at line 228 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [17/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( VariableAssignment< Pol > &&  _variableAssignment)
inlineprivate

Definition at line 265 of file FormulaPool.h.

Here is the call graph for this function:

◆ create() [18/18]

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::create ( VariableComparison< Pol > &&  _variableComparison)
inlineprivate

Definition at line 253 of file FormulaPool.h.

Here is the call graph for this function:

◆ createImplication()

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::createImplication ( Formulas< Pol > &&  _subformulas)
private

Create formula representing an implication.

Parameters
_subformulas
Returns
Here is the caller graph for this function:

◆ createITE()

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::createITE ( Formulas< Pol > &&  _subformulas)
private
Here is the caller graph for this function:

◆ createNAry()

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::createNAry ( FormulaType  _type,
Formulas< Pol > &&  _subformulas 
)
private
Here is the caller graph for this function:

◆ createNegatedContent()

template<typename Pol >
FormulaContent<Pol>* carl::FormulaPool< Pol >::createNegatedContent ( const FormulaContent< Pol > *  f) const
inlineprivate

Definition at line 194 of file FormulaPool.h.

Here is the call graph for this function:

◆ createTseitinVar()

template<typename Pol >
Formula<Pol> carl::FormulaPool< Pol >::createTseitinVar ( const Formula< Pol > &  _formula)
inline

Definition at line 134 of file FormulaPool.h.

Here is the call graph for this function:

◆ falseFormula()

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::falseFormula ( ) const
inlineprotected

Definition at line 87 of file FormulaPool.h.

Here is the caller graph for this function:

◆ forallDo()

template<typename Pol >
template<typename ArgType >
void carl::FormulaPool< Pol >::forallDo ( void(*)(ArgType *, const Formula< Pol > &)  _func,
ArgType *  _arg 
) const
inline

Definition at line 561 of file FormulaPool.h.

◆ formulasInverse()

template<typename Pol >
bool carl::FormulaPool< Pol >::formulasInverse ( const Formula< Pol > &  _subformulaA,
const Formula< Pol > &  _subformulaB 
)

◆ free()

template<typename Pol >
void carl::FormulaPool< Pol >::free ( const FormulaContent< Pol > *  _elem)
inlineprivate

Definition at line 462 of file FormulaPool.h.

Here is the call graph for this function:

◆ freeTseitinVariable()

template<typename Pol >
bool carl::FormulaPool< Pol >::freeTseitinVariable ( const FormulaContent< Pol > *  _toDelete)
inlineprivate

Definition at line 496 of file FormulaPool.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getBaseFormula()

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::getBaseFormula ( const FormulaContent< Pol > *  f) const
inlineprivate

Definition at line 175 of file FormulaPool.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getInstance()

static FormulaPool< Pol > & carl::Singleton< FormulaPool< Pol > >::getInstance ( )
inlinestaticinherited

Returns the single instance of this class by reference.

If there is no instance yet, a new one is created.

Definition at line 45 of file Singleton.h.

◆ getTseitinVar()

template<typename Pol >
Formula<Pol> carl::FormulaPool< Pol >::getTseitinVar ( const Formula< Pol > &  _formula)
inline

Definition at line 124 of file FormulaPool.h.

Here is the call graph for this function:

◆ isBaseFormula() [1/5]

template<typename Pol >
bool carl::FormulaPool< Pol >::isBaseFormula ( const Constraint< Pol > &  c) const
inlineprivate

Definition at line 147 of file FormulaPool.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isBaseFormula() [2/5]

template<typename Pol >
bool carl::FormulaPool< Pol >::isBaseFormula ( const FormulaContent< Pol > *  f) const
inlineprivate

Definition at line 159 of file FormulaPool.h.

Here is the call graph for this function:

◆ isBaseFormula() [3/5]

template<typename Pol >
bool carl::FormulaPool< Pol >::isBaseFormula ( const UEquality &  ueq) const
inlineprivate

Definition at line 150 of file FormulaPool.h.

Here is the call graph for this function:

◆ isBaseFormula() [4/5]

template<typename Pol >
bool carl::FormulaPool< Pol >::isBaseFormula ( const VariableAssignment< Pol > &  va) const
inlineprivate

Definition at line 156 of file FormulaPool.h.

Here is the call graph for this function:

◆ isBaseFormula() [5/5]

template<typename Pol >
bool carl::FormulaPool< Pol >::isBaseFormula ( const VariableComparison< Pol > &  vc) const
inlineprivate

Definition at line 153 of file FormulaPool.h.

Here is the call graph for this function:

◆ print()

template<typename Pol >
void carl::FormulaPool< Pol >::print ( ) const
inline

Definition at line 97 of file FormulaPool.h.

◆ reg()

template<typename Pol >
void carl::FormulaPool< Pol >::reg ( const FormulaContent< Pol > *  _elem) const
inlineprivate

Definition at line 544 of file FormulaPool.h.

Here is the call graph for this function:

◆ size()

template<typename Pol >
std::size_t carl::FormulaPool< Pol >::size ( ) const
inline

Definition at line 93 of file FormulaPool.h.

◆ trueFormula()

template<typename Pol >
const FormulaContent<Pol>* carl::FormulaPool< Pol >::trueFormula ( ) const
inlineprotected

Definition at line 82 of file FormulaPool.h.

Here is the caller graph for this function:

Field Documentation

◆ Formula< Pol >

template<typename Pol >
friend carl::FormulaPool< Pol >::Formula< Pol >
private

Definition at line 35 of file FormulaPool.h.

◆ mIdAllocator

template<typename Pol >
unsigned carl::FormulaPool< Pol >::mIdAllocator
private

id allocator

Definition at line 41 of file FormulaPool.h.

◆ mpFalse

template<typename Pol >
FormulaContent<Pol>* carl::FormulaPool< Pol >::mpFalse
private

The unique formula representing false.

Definition at line 45 of file FormulaPool.h.

◆ mPool

template<typename Pol >
underlying_set carl::FormulaPool< Pol >::mPool
private

The formula pool.

Definition at line 51 of file FormulaPool.h.

◆ mPoolBuckets

template<typename Pol >
std::unique_ptr<typename underlying_set::bucket_type[]> carl::FormulaPool< Pol >::mPoolBuckets
private

Definition at line 49 of file FormulaPool.h.

◆ mpTrue

template<typename Pol >
FormulaContent<Pol>* carl::FormulaPool< Pol >::mpTrue
private

The unique formula representing true.

Definition at line 43 of file FormulaPool.h.

◆ mRehashPolicy

template<typename Pol >
pool::RehashPolicy carl::FormulaPool< Pol >::mRehashPolicy
private

Definition at line 47 of file FormulaPool.h.

◆ mTseitinVars

template<typename Pol >
FastPointerMap<FormulaContent<Pol>,const FormulaContent<Pol>*> carl::FormulaPool< Pol >::mTseitinVars
private

Definition at line 58 of file FormulaPool.h.

◆ mTseitinVarToFormula

template<typename Pol >
FastPointerMap<FormulaContent<Pol>,typename FastPointerMap<FormulaContent<Pol>,const FormulaContent<Pol>*>::iterator> carl::FormulaPool< Pol >::mTseitinVarToFormula
private

Definition at line 60 of file FormulaPool.h.

◆ Singleton< FormulaPool >

template<typename Pol >
friend carl::FormulaPool< Pol >::Singleton< FormulaPool >
private

Definition at line 34 of file FormulaPool.h.

The documentation for this class was generated from the following files: