21 #ifndef _cvc3__include__theory_arith_h_
22 #define _cvc3__include__theory_arith_h_
29 class ArithProofRules;
86 bool printAsReal =
false);
134 virtual void checkSat(
bool fullEffort) = 0;
142 bool enumerate,
bool computeSize) = 0;
217 {
return Expr(
POW, pow, base);}
222 {
return Expr(
LT, left, right); }
224 {
return Expr(
LE, left, right); }
226 {
return Expr(
GT, left, right); }
228 {
return Expr(
GE, left, right); }
Expr minusExpr(const Expr &left, const Expr &right)
virtual void assertFact(const Theorem &e)=0
Assert a new fact to the decision procedure.
Expr ltExpr(const Expr &left, const Expr &right)
Data structure of expressions in CVC3.
virtual void computeModel(const Expr &e, std::vector< Expr > &vars)=0
Compute the value of a compound variable from the more primitive ones.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
virtual Theorem rewrite(const Expr &e)=0
Theory-specific rewrite rules.
virtual void update(const Theorem &e, const Expr &d)=0
Notify a theory of a new equality.
bool isIntPred(const Expr &e)
Expr grayShadow(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)
Construct the gray shadow expression representing c1 <= v - e <= c2.
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
Expr operator+(const Expr &left, const Expr &right)
virtual Type computeBaseType(const Type &t)=0
Compute the base type of the top-level operator of an arbitrary type.
This theory handles basic linear arithmetic.
virtual Theorem canon(const Expr &e)=0
Canonize the expression e, assuming all children are canonical.
bool isAtomicArithTerm(const Expr &e)
Whether any ite's appear in the arithmetic part of the term e.
MS C++ specific settings.
void printRational(ExprStream &os, const Rational &r, bool printAsReal=false)
Print a rational in SMT-LIB format.
Expr operator/(const Expr &left, const Expr &right)
virtual void checkType(const Expr &e)=0
Check that e is a valid Type expr.
Expr gtExpr(const Expr &left, const Expr &right)
#define DebugAssert(cond, str)
virtual void refineCounterExample()=0
Process disequalities from the arrangement for model generation.
virtual void addMultiplicativeSignSplit(const Theorem &case_split_thm)
virtual Expr computeTypePred(const Type &t, const Expr &e)=0
Theory specific computation of the subtyping predicate for type t applied to the expression e...
bool isAtomicArithFormula(const Expr &e)
Whether any ite's appear in the arithmetic part of the formula e.
Expr operator-(const Expr &child)
bool isPlus(const Expr &e)
bool isMinus(const Expr &e)
bool isRational(const Expr &e)
virtual void separateMonomial(const Expr &e, Expr &c, Expr &var)=0
Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.
virtual Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)=0
Compute information related to finiteness of types.
virtual void computeModelBasic(const std::vector< Expr > &v)=0
Assign concrete values to basic-type variables in v.
const Expr & getExpr() const
TheoryArith(TheoryCore *core, const std::string &name)
virtual bool addPairToArithOrder(const Expr &smaller, const Expr &bigger)
Expr operator*(const Expr &left, const Expr &right)
bool isSyntacticRational(const Expr &e, Rational &r)
Return whether e is syntactically identical to a rational constant.
virtual Expr parseExprOp(const Expr &e)=0
Theory-specific parsing implemented by the DP.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
virtual void computeType(const Expr &e)=0
Compute and store the type of e.
const Expr & getRHS() const
Expr powExpr(const Expr &pow, const Expr &base)
Power (x^n, or base^{pow}) expressions.
bool isIntegerConst(const Expr &e)
Expr newRatExpr(const Rational &r)
bool isIneq(const Expr &e)
ExprManager * getEM()
Access to ExprManager.
Expr rewriteToDiff(const Expr &e)
Rewrite an atom to look like x - y op c if possible–for smtlib translation.
bool leavesAreNumConst(const Expr &e)
virtual void addSharedTerm(const Expr &e)=0
Notify theory of a new shared term.
bool isDarkShadow(const Expr &e)
virtual void computeModelTerm(const Expr &e, std::vector< Expr > &v)=0
Add variables from 'e' to 'v' for constructing a concrete model.
Expr darkShadow(const Expr &lhs, const Expr &rhs)
Construct the dark shadow expression representing lhs <= rhs.
Generic API for Theories plus methods commonly used by theories.
Theorem canonRec(const Expr &e)
Canonize the expression e recursively.
bool isDivide(const Expr &e)
virtual ExprStream & print(ExprStream &os, const Expr &e)=0
Theory-specific pretty-printing.
virtual void checkAssertEqInvariant(const Theorem &e)=0
A debug check used by the primary solver.
bool isUMinus(const Expr &e)
Expr plusExpr(const Expr &left, const Expr &right)
bool isGrayShadow(const Expr &e)
Expr geExpr(const Expr &left, const Expr &right)
std::vector< int > d_kinds
bool recursiveCanonSimpCheck(const Expr &e)
helper for checkAssertEqInvariant
Cardinality
Enum for cardinality of types.
Theorem canonThm(const Theorem &thm)
Composition of canon(const Expr&) by transitivity: take e0 = e1, canonize e1 to e2, return e0 = e2.
Rational pow(Rational pow, const Rational &base)
Raise 'base' into the power of 'pow' (pow must be an integer)
bool isPow(const Expr &e)
Expr uminusExpr(const Expr &child)
virtual void setup(const Expr &e)=0
Set up the term e for call-backs when e or its children change.
Expr leExpr(const Expr &left, const Expr &right)
bool isMult(const Expr &e)
Expr divideExpr(const Expr &left, const Expr &right)
Theorem canonSimp(const Expr &e)
simplify leaves and then canonize
virtual Theorem solve(const Theorem &e)=0
An optional solver.
Type subrangeType(const Expr &l, const Expr &r)
virtual Expr computeTCC(const Expr &e)=0
Compute and cache the TCC of e.
Expr multExpr(const Expr &left, const Expr &right)
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
virtual void checkSat(bool fullEffort)=0
Check for satisfiability in the theory.