Represent an SMT formula, which can be an atom for some background theory or a boolean combination of (sub)formulas.
More...
|
| Formula (FormulaType _type=FALSE) |
|
| Formula (Variable::Arg _booleanVar) |
|
| Formula (const Pol &_pol, Relation _rel) |
|
| Formula (const Constraint< Pol > &_constraint) |
|
| Formula (const VariableComparison< Pol > &_variableComparison) |
|
| Formula (const VariableAssignment< Pol > &_variableAssignment) |
|
| Formula (const BVConstraint &_constraint) |
|
| Formula (FormulaType _type, Formula &&_subformula) |
|
| Formula (FormulaType _type, const Formula &_subformula) |
|
| Formula (FormulaType _type, const Formula &_subformulaA, const Formula &_subformulaB) |
|
| Formula (FormulaType _type, const Formula &_subformulaA, const Formula &_subformulaB, const Formula &_subformulaC) |
|
| Formula (FormulaType _type, const FormulasMulti< Pol > &_subformulas) |
|
| Formula (FormulaType _type, const Formulas< Pol > &_subasts) |
|
| Formula (FormulaType _type, Formulas< Pol > &&_subasts) |
|
| Formula (FormulaType _type, const std::initializer_list< Formula< Pol >> &_subasts) |
|
| Formula (FormulaType _type, const FormulaSet< Pol > &_subasts) |
|
| Formula (FormulaType _type, FormulaSet< Pol > &&_subasts) |
|
| Formula (FormulaType _type, std::vector< Variable > &&_vars, const Formula &_term) |
|
| Formula (FormulaType _type, const std::vector< Variable > &_vars, const Formula &_term) |
|
| Formula (FormulaType _type, std::vector< Variable > &&_vars, const Formula &_aux_term, const Formula &_term) |
|
| Formula (FormulaType _type, const std::vector< Variable > &_vars, const Formula &_aux_term, const Formula &_term) |
|
| Formula (const UTerm &_lhs, const UTerm &_rhs, bool _negated) |
|
| Formula (UEquality &&_eq) |
|
| Formula (const UEquality &_eq) |
|
| Formula (const Formula &_formula) |
|
| Formula (Formula &&_formula) noexcept |
|
| ~Formula () |
|
Formula & | operator= (const Formula &_formula) |
|
Formula & | operator= (Formula &&_formula) |
|
double | activity () const |
|
void | set_activity (double _activity) const |
| Sets the activity to the given value. More...
|
|
FormulaType | type () const |
|
std::size_t | hash () const |
|
std::size_t | id () const |
|
bool | is_true () const |
|
bool | is_false () const |
|
const Condition & | properties () const |
|
const Variables & | variables () const |
|
Formula | negated () const |
|
Formula | base_formula () const |
|
const Formula & | remove_negations () const |
|
const Formula & | subformula () const |
|
const Formula & | premise () const |
|
const Formula & | conclusion () const |
|
const Formula & | condition () const |
|
const Formula & | first_case () const |
|
const Formula & | second_case () const |
|
const std::vector< carl::Variable > & | quantified_variables () const |
|
const Formula & | quantified_formula () const |
|
const Formula & | quantified_aux_formula () const |
|
const Formulas< Pol > & | subformulas () const |
|
const Constraint< Pol > & | constraint () const |
|
const VariableComparison< Pol > & | variable_comparison () const |
|
const VariableAssignment< Pol > & | variable_assignment () const |
|
const BVConstraint & | bv_constraint () const |
|
carl::Variable::Arg | boolean () const |
|
const UEquality & | u_equality () const |
|
size_t | size () const |
|
bool | empty () const |
|
const_iterator | begin () const |
|
const_iterator | end () const |
|
const_reverse_iterator | rbegin () const |
|
const_reverse_iterator | rend () const |
|
const Formula & | back () const |
|
bool | property_holds (const Condition &_property) const |
| Checks if the given property holds for this formula. More...
|
|
bool | is_atom () const |
|
bool | is_literal () const |
|
bool | is_boolean_combination () const |
|
bool | is_bound () const |
|
bool | is_nary () const |
|
bool | is_constraint_conjunction () const |
|
bool | is_real_constraint_conjunction () const |
|
bool | is_integer_constraint_conjunction () const |
|
bool | is_only_propositional () const |
|
Logic | logic () const |
|
bool | contains (const Formula &_formula) const |
|
bool | operator== (const Formula &_formula) const |
|
bool | operator!= (const Formula &_formula) const |
|
bool | operator< (const Formula &_formula) const |
|
bool | operator> (const Formula &_formula) const |
|
bool | operator<= (const Formula &_formula) const |
|
bool | operator>= (const Formula &_formula) const |
|
Formula | operator! () const |
|
template<typename Pol>
class carl::Formula< Pol >
Represent an SMT formula, which can be an atom for some background theory or a boolean combination of (sub)formulas.
Definition at line 46 of file Formula.h.