Assignment.h File Reference
#include "Model.h"#include <carl-formula/formula/Formula.h>#include <carl-arith/ran/ran.h>#include <carl-arith/vs/SqrtEx.h>#include <carl-formula/uninterpreted/SortValue.h>#include <carl-formula/uninterpreted/UFModel.h>#include <map>#include "Assignment.tpp"
Include dependency graph for Assignment.h:
Go to the source code of this file.
Namespaces | |
| carl | |
| carl is the main namespace for the library. | |
Functions | |
| template<typename Rational , typename Poly > | |
| bool | carl::getRationalAssignmentsFromModel (const Model< Rational, Poly > &_model, std::map< Variable, Rational > &_rationalAssigns) |
| Obtains all assignments which can be transformed to rationals and stores them in the passed map. More... | |
| template<typename Rational , typename Poly > | |
| unsigned | carl::satisfies (const Model< Rational, Poly > &_assignment, const Formula< Poly > &_formula) |
| template<typename Rational , typename Poly > | |
| bool | carl::isPartOf (const std::map< Variable, Rational > &_assignment, const Model< Rational, Poly > &_model) |
| template<typename Rational , typename Poly > | |
| unsigned | carl::satisfies (const Model< Rational, Poly > &_model, const std::map< Variable, Rational > &_assignment, const std::map< BVVariable, BVTerm > &bvAssigns, const Formula< Poly > &_formula) |
| template<typename Rational , typename Poly > | |
| void | carl::getDefaultModel (Model< Rational, Poly > &_defaultModel, const UEquality &_constraint, bool _overwrite=true, size_t _seed=0) |
| template<typename Rational , typename Poly > | |
| void | carl::getDefaultModel (Model< Rational, Poly > &_defaultModel, const BVTerm &_constraint, bool _overwrite=true, size_t _seed=0) |
| template<typename Rational , typename Poly > | |
| void | carl::getDefaultModel (Model< Rational, Poly > &_defaultModel, const Constraint< Poly > &_constraint, bool _overwrite=true, size_t _seed=0) |
| template<typename Rational , typename Poly > | |
| void | carl::getDefaultModel (Model< Rational, Poly > &_defaultModel, const Formula< Poly > &_formula, bool _overwrite=true, size_t _seed=0) |
| template<typename Rational , typename Poly > | |
| Formula< Poly > | carl::representingFormula (const ModelVariable &mv, const Model< Rational, Poly > &model) |
| template<typename Rational , typename Poly > | |
| std::optional< Assignment< typename Poly::RootType > > | carl::get_ran_assignment (const carlVariables &vars, const Model< Rational, Poly > &model) |
| template<typename Rational , typename Poly > | |
| Assignment< typename Poly::RootType > | carl::get_ran_assignment (const Model< Rational, Poly > &model) |
