ModelEvaluation_Bitvector.h File Reference

#include "../Model.h"
#include <carl-formula/bitvector/BVConstraint.h>
#include <carl-formula/bitvector/BVTerm.h>

Include dependency graph for ModelEvaluation_Bitvector.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces
	carl
	carl is the main namespace for the library.

Functions
template<typename Rational , typename Poly >
void	carl::substitute_inplace (BVTerm &bvt, const Model< Rational, Poly > &m)
	Substitutes all variables from a model within a bitvector term. More...
template<typename Rational , typename Poly >
void	carl::substitute_inplace (BVConstraint &bvc, const Model< Rational, Poly > &m)
	Substitutes all variables from a model within a bitvector constraint. More...
template<typename Rational , typename Poly >
void	carl::evaluate_inplace (ModelValue< Rational, Poly > &res, BVTerm &bvt, const Model< Rational, Poly > &m)
	Evaluates a bitvector term to a ModelValue over a Model. More...
template<typename Rational , typename Poly >
void	carl::evaluate_inplace (ModelValue< Rational, Poly > &res, BVConstraint &bvc, const Model< Rational, Poly > &m)
	Evaluates a bitvector constraint to a ModelValue over a Model. More...