10 template<
typename Pol>
13 template<
typename Pol>
17 template<
typename Poly>
19 template<
typename Poly>
21 template<
typename Poly>
84 CARL_LOG_ERROR(
"carl.formula",
"Unknown formula type " <<
unsigned(_type));
95 template<
typename Pol>
124 template<
typename Pol>
146 template<
typename Pol>
184 mutable std::mutex mActivityMutex;
186 mutable std::mutex mVariablesMutex;
264 std::size_t
id()
const {
300 template<
typename Pol>
308 return os << std::get<carl::Variable>(f.
mContent);
310 return os << std::get<Constraint<Pol>>(f.
mContent);
312 return os << std::get<VariableAssignment<Pol>>(f.
mContent);
314 return os << std::get<VariableComparison<Pol>>(f.
mContent);
316 return os << std::get<BVConstraint>(f.
mContent);
318 return os << std::get<UEquality>(f.
mContent);
320 return os <<
"!(" << std::get<Formula<Pol>>(f.
mContent) <<
")";
324 return os <<
")(" << std::get<QuantifierContent<Pol>>(f.
mContent).mFormula <<
")";
332 return os <<
")(" << std::get<QuantifierContent<Pol>>(f.
mContent).mFormula <<
")";
339 template<
typename Pol>
341 assert(fc !=
nullptr);
A small wrapper that configures logging for carl.
#define CARL_LOG_ERROR(channel, msg)
MultivariatePolynomial< Rational > Pol
carl is the main namespace for the library.
FormulaType
Represent the type of a formula to allow faster/specialized processing.
std::set< Formula< Poly > > FormulaSet
std::ostream & operator<<(std::ostream &os, const BasicConstraint< Poly > &c)
Prints the given constraint on the given stream.
std::vector< Formula< Poly > > Formulas
std::string formulaTypeToString(FormulaType _type)
auto stream_joined(const std::string &glue, const T &v)
Allows to easily output some container with all elements separated by some string.
std::multiset< Formula< Poly > > FormulasMulti
std::set< Variable > Variables
auto & get(const std::string &name)
A Variable represents an algebraic variable that can be used throughout carl.
Represent a sum type/variant of an (in)equality between a variable on the left-hand side and multivar...
Represent a polynomial (in)equality against zero.
Represent an SMT formula, which can be an atom for some background theory or a boolean combination of...
Stores the variables and the formula bound by a quantifier.
Formula< Pol > mFormula
The formula bound by this quantifier.
QuantifierContent(std::vector< carl::Variable > &&_vars, Formula< Pol > &&_formula)
Constructs the content of a quantified formula.
bool operator==(const QuantifierContent &_qc) const
Checks this content of a quantified formula and the given content of a quantified formula is equal.
std::vector< carl::Variable > mVariables
The quantified variables.
Formula< Pol > mFormula
The formula bound by this quantifier.
Formula< Pol > mAuxFormula
The guard.
AuxQuantifierContent(std::vector< carl::Variable > &&_vars, Formula< Pol > &&_aux_formula, Formula< Pol > &&_formula)
std::vector< carl::Variable > mVariables
The quantified variables.
bool operator==(const AuxQuantifierContent &_qc) const
FormulaContent(const FormulaContent &)=delete
~FormulaContent()
Destructor.
Variables * mpVariables
Container collecting the variables which occur in this formula.
bool operator==(const FormulaContent &_content) const
friend std::ostream & operator<<(std::ostream &os, const FormulaContent< P > &f)
double mActivity
The activity for this formula, which means, how much is this formula involved in the solving procedur...
FormulaContent(FormulaType _type, Formulas< Pol > &&_subformula)
FormulaContent(FormulaType _type, std::size_t _id=0)
Constructs the formula (true), if the given bool is true and the formula (false) otherwise.
FormulaContent(FormulaType _type, const std::initializer_list< Formula< Pol >> &_subformula)
FormulaType mType
The type of this formula.
FormulaContent(FormulaContent &&o)
FormulaContent(VariableAssignment< Pol > &&_variableAssignment)
FormulaContent(FormulaType _type, std::vector< carl::Variable > &&_vars, const Formula< Pol > &_term)
Constructs a quantifier expression: (exists (vars) term) or (forall (vars) term)
size_t mUsages
The number of formulas existing with this content.
FormulaContent(FormulaType _type, Formula< Pol > &&_subformula)
Constructs a formula of the given type with a single subformula.
FormulaContent(UEquality &&_ueq)
Constructs a formula being an uninterpreted equality.
const FormulaContent< Pol > * mNegation
The negation.
Condition mProperties
The propositions of this formula.
FormulaContent(Constraint< Pol > &&_constraint)
Constructs a formula being a constraint.
FormulaContent(Variable _variable)
Constructs a formula being a variable.
FormulaContent(BVConstraint &&_constraint)
Constructs a formula being a bitvector constraint.
FormulaContent(FormulaType _type, std::vector< carl::Variable > &&_vars, const Formula< Pol > &_aux_term, const Formula< Pol > &_term)
std::variant< carl::Variable, Constraint< Pol >, VariableComparison< Pol >, VariableAssignment< Pol >, BVConstraint, UEquality, Formula< Pol >, Formulas< Pol >, QuantifierContent< Pol >, AuxQuantifierContent< Pol > > mContent
The content of this formula.
FormulaContent(VariableComparison< Pol > &&_variableComparison)
size_t mHash
The hash value.
Implements an uninterpreted equality, that is an equality of either two uninterpreted function instan...