21 #ifndef _cvc3__include__theory_arith3_h_
22 #define _cvc3__include__theory_arith3_h_
46 friend std::ostream&
operator<<(std::ostream& os,
const FreeConst& fc);
72 friend std::ostream&
operator<<(std::ostream& os,
const Ineq& ineq);
125 void selectLargest(
const std::vector<Expr>& v1, std::vector<Expr>& v2);
128 void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
244 bool isStale(
const Ineq& ineq);
275 std::set<Expr>& cache);
311 bool enumerate,
bool computeSize);
Theorem substAndCanonize(const Expr &t, ExprMap< Theorem > &subst)
Substitute all vars in term 't' according to the substitution 'subst' and canonize the result...
Theorem processRealEq(const Theorem &eqn)
processes equalities with 1 or more vars of type REAL
void refineCounterExample()
Process disequalities from the arrangement for model generation.
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
CDMap< Expr, Rational > fixedMaxCoefficient
void checkType(const Expr &e)
Check that e is a valid Type expr.
Theorem isolateVariable(const Theorem &inputThm, bool &e1)
Take an inequality and isolate a variable.
Theorem d_ineq
The inequality.
ArithProofRules * d_rules
Data structure of expressions in CVC3.
Theorem isIntegerDerive(const Expr &isIntE, const Theorem &thm)
A helper method for isIntegerThm()
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
TheoryArith3(TheoryCore *core)
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Theorem processSimpleIntEq(const Theorem &eqn)
One step of INT equality processing (aux. method for processIntEq())
void computeType(const Expr &e)
Compute and store the type of e.
void setupRec(const Expr &e)
Recursive setup for isolated inequalities (and other new expressions)
bool varOnLHS() const
Flag whether var is isolated on the LHS.
Data class for the strongest free constant in separation inqualities.
This theory handles basic linear arithmetic.
Theorem doSolve(const Theorem &e)
Solve an equation and return an equivalent Theorem in the solved form.
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
Theorem canon(const Expr &e)
Canonize the expression e, assuming all children are canonical.
MS C++ specific settings.
CDO< size_t > d_bufferIdx
Buffer index of the next unprocessed inequality.
bool lessThan(const Expr &e1, const Expr &e2)
bool varOnRHS() const
Flag whether var is isolated on the RHS.
void processFiniteIntervals(const Expr &x)
For an integer var 'x', find and process all constraints A <= ax <= A+c.
const FreeConst * d_const
ExprMap< CDList< Ineq > * > d_inequalitiesLeftDB
Database of inequalities with a variable isolated on the left.
void selectLargest(const std::vector< Expr > &v1, std::vector< Expr > &v2)
void assignVariables(std::vector< Expr > &v)
Theorem canonPredEquiv(const Theorem &thm)
Theorem canonConjunctionEquiv(const Theorem &thm)
takes in a conjunction equivalence Thm and canonizes it.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
void separateMonomial(const Expr &e, Expr &c, Expr &var)
Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.
void projectInequalities(const Theorem &theInequality, bool isolatedVarOnRHS)
ExprMap< CDList< Ineq > * > d_inequalitiesRightDB
Database of inequalities with a variable isolated on the right.
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
const Theorem & ineq() const
Get the inequality.
Ineq(const Theorem &ineq, bool varOnRHS, const FreeConst &c)
Initial constructor. 'r' is taken from the subsumption database.
void selectSmallest(std::vector< Expr > &v1, std::vector< Expr > &v2)
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
void getFactors(const Expr &e, std::set< Expr > &factors)
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
bool findBounds(const Expr &e, Rational &lub, Rational &glb)
CDList< Theorem > d_buffer
Buffer of input inequalities.
CDMap< Expr, Rational > maxCoefficientRight
ArithProofRules * createProofRules3()
bool kidsCanonical(const Expr &e)
Check if the kids of e are fully simplified and canonized (for debugging)
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Theorem processIntEq(const Theorem &eqn)
processes equalities whose vars are all of type INT
Rational currentMaxCoefficient(Expr var)
bool isInteger(const Expr &e)
Check the term t for integrality (return bool)
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
void updateStats(const Rational &c, const Expr &var)
Update the statistics counters for the variable with a coeff. c.
const Rational & getConst() const
const Expr & getRHS() const
CDList< Theorem > d_diseq
CDMap< Expr, bool > d_sharedTerms
Set of shared terms (for counterexample generation)
const int * d_bufferThres
Threshold when the buffer must be processed.
Ineq()
Default constructor is disabled.
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Theorem normalizeProjectIneqs(const Theorem &ineqThm1, const Theorem &ineqThm2)
const Rational & freeConstIneq(const Expr &ineq, bool varOnRHS)
Extract the free constant from an inequality.
CDMap< Expr, int > d_countRight
Mapping of a variable to the number of inequalities where the variable would be isolated on the right...
CDMap< Expr, FreeConst > d_freeConstDB
Mapping of inequalities to the largest/smallest free constant.
bool lessThanVar(const Expr &isolatedVar, const Expr &var2)
bool pickIntEqMonomial(const Expr &right, Expr &isolated, bool &nonlin)
picks the monomial with the smallest abs(coeff) from the input
void collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache)
Traverse 'e' and push all the i-leaves into 'vars' vector.
void findRationalBound(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
bool isStale(const Expr &e)
Check if the term expression is "stale".
Private class for an inequality in the Fourier-Motzkin database.
const FreeConst & getConst() const
Get the max/min constant.
Expr computeNormalFactor(const Expr &rhs)
Given a canonized term, compute a factor to make all coefficients integer and relatively prime...
void selectSmallestByCoefficient(std::vector< Expr > input, std::vector< Expr > &output)
friend std::ostream & operator<<(std::ostream &os, const FreeConst &fc)
Printing.
Theorem canonSimplify(const Theorem &thm)
Composition of canonSimplify(const Expr&) by transitivity: take e0 = e1, canonize and simplify e1 to ...
void checkAssertEqInvariant(const Theorem &e)
A debug check used by the primary solver.
void addEdge(const Expr &e1, const Expr &e2)
void processBuffer()
Process inequalities in the buffer.
void processFiniteInterval(const Theorem &alphaLEax, const Theorem &bxLEbeta)
Check if alpha <= ax & bx <= beta is a finite interval for integer var 'x', and assert the corresponding ...
bool d_rhs
Var is isolated on the RHS.
CDMap< Expr, Rational > maxCoefficientLeft
Theorem normalize(const Expr &e)
Normalize an equation (make all coefficients rel. prime integers)
Cardinality
Enum for cardinality of types.
void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
Theorem solve(const Theorem &e)
An optional solver.
CDO< bool > d_inModelCreation
Theorem isIntegerThm(const Expr &e)
Check the term t for integrality.
void fixCurrentMaxCoefficient(Expr variable, Rational max)
Expr pickMonomial(const Expr &right)
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Theorem canonPred(const Theorem &thm)
Canonize predicate (x = y, x < y, etc.)
void addToBuffer(const Theorem &thm)
Add an inequality to the input buffer. See also d_buffer.
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Theorem solvedForm(const std::vector< Theorem > &solvedEqs)
Take a system of equations and turn it into a solved form.
ExprMap< std::vector< Expr > > d_edges
bool dfs(const Expr &e1, const Expr &e2)
Theorem canonSimplify(const Expr &e)
Canonize and reduce e w.r.t. union-find database; assume all children are canonical.
const FreeConst & updateSubsumptionDB(const Expr &ineq, bool varOnRHS, bool &subsumed)
Update the free constant subsumption database with new inequality.
FreeConst(const Rational &r, bool strict)
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
CDMap< Expr, int > d_countLeft
Mapping of a variable to the number of inequalities where the variable would be isolated on the left...
CDMap< Expr, bool > d_sharedVars
Set of shared integer variables (i-leaves)