21 #ifndef _cvc3__include__theory_arith_new_h_
22 #define _cvc3__include__theory_arith_new_h_
62 friend std::ostream&
operator<<(std::ostream& os,
const FreeConst& fc);
74 d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { }
87 friend std::ostream&
operator<<(std::ostream& os,
const Ineq& ineq);
128 void selectLargest(
const std::vector<Expr>& v1, std::vector<Expr>& v2);
131 void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
195 bool isStale(
const Ineq& ineq);
218 std::set<Expr>& cache);
251 bool enumerate,
bool computeSize);
327 if (k >= 0)
return q;
379 DebugAssert(type ==
FINITE,
"EpsRational::operator +, adding to infinite number");
391 DebugAssert(type ==
FINITE,
"EpsRational::operator +, adding to infinite number");
404 DebugAssert(type ==
FINITE,
"EpsRational::operator -, subtracting from infinite number");
416 DebugAssert(type ==
FINITE,
"EpsRational::operator *, multiplying an infinite number");
427 DebugAssert(type ==
FINITE,
"EpsRational::operator *, dividing an infinite number");
444 return (q < r.
q || (q == r.
q && k <= r.
k));
456 FatalAssert(
false,
"EpsRational::operator <=, what kind of number is this????");
485 FatalAssert(
false,
"EpsRational::toString, what kind of number is this????");
487 return "hm, what am I?";
555 std::cout << expr1 <<
" @ " << expr2 <<
std::endl;
558 if (expr1[1] == expr2[1])
563 return bound < bI.
bound;
566 return expr1[1] < expr2[1];
597 return bound < bI.
bound;
600 return e[1] < bI.
e[1];
void projectInequalities(const Theorem &theInequality, bool isolatedVarOnRHS)
EpsRational getLowerBound(const Expr &x) const
CDMap< Expr, bool > d_sharedVars
Set of shared integer variables (i-leaves)
_hash_table::iterator iterator
Data structure of expressions in CVC3.
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
void updateValue(const Expr &var, const Expr &e)
Theorem solvedForm(const std::vector< Theorem > &solvedEqs)
Take a system of equations and turn it into a solved form.
void processFiniteIntervals(const Expr &x)
For an integer var 'x', find and process all constraints A <= ax <= A+c.
bool operator>(const EpsRational &r) const
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Theorem d_ineq
The inequality.
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
EpsRational(const EpsRational &r)
bool operator<(const ExprBoundInfo &bI) const
Ineq()
Default constructor is disabled.
Theorem processSimpleIntEq(const Theorem &eqn)
One step of INT equality processing (aux. method for processIntEq())
Theorem processRealEq(const Theorem &eqn)
processes equalities with 1 or more vars of type REAL
void updateStats(const Rational &c, const Expr &var)
Update the statistics counters for the variable with a coeff. c.
Theorem isIntegerThm(const Expr &e)
Check the term t for integrality.
BoundInfo(const EpsRational &bound, const Theorem &thm)
Theorem normalizeProjectIneqs(const Theorem &ineqThm1, const Theorem &ineqThm2)
void checkAssertEqInvariant(const Theorem &e)
A debug check used by the primary solver.
const int * d_bufferThres
Threshold when the buffer must be processed.
This theory handles basic linear arithmetic.
const FreeConst & getConst() const
Get the max/min constant.
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
bool lessThan(const Expr &e1, const Expr &e2)
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
bool operator<(const EpsRational &r) const
MS C++ specific settings.
bool d_rhs
Var is isolated on the RHS.
ExprMap< CDList< Ineq > * > d_inequalitiesRightDB
Database of inequalities with a variable isolated on the right.
bool kidsCanonical(const Expr &e)
Check if the kids of e are fully simplified and canonized (for debugging)
bool findBounds(const Expr &e, Rational &lub, Rational &glb)
EpsRational operator*(const Rational &a) const
const Rational & findCoefficient(const Expr &var, const Expr &expr)
void registerAtom(const Expr &e)
static const EpsRational MinusInfinity
std::string toString(int base=10) const
bool operator<=(const EpsRational &r) const
Theorem pivotRule(const Theorem &eq, const Expr &var)
Theorem doSolve(const Theorem &e)
Solve an equation and return an equivalent Theorem in the solved form.
Theorem canonConjunctionEquiv(const Theorem &thm)
takes in a conjunction equivalence Thm and canonizes it.
std::set< Expr > SetOfVariables
QueryResult checkSatSimplex()
CDMap< Expr, int > d_countLeft
Mapping of a variable to the number of inequalities where the variable would be isolated on the left...
#define DebugAssert(cond, str)
enumerated type for result of queries
bool isInteger(const Expr &e)
Check the term t for integrality (return bool)
ExprBoundInfo(const EpsRational &bound, const Expr &e)
TebleauxMap freshVariables
Theorem canonPred(const Theorem &thm)
Canonize predicate (x = y, x < y, etc.)
ArithProofRules * d_rules
Rational getTableauxEntry(const Expr &x_i, const Expr &x_j)
Theorem processIntEq(const Theorem &eqn)
processes equalities whose vars are all of type INT
Hash::hash_map< Expr, Theorem > TebleauxMap
CDMap< Expr, BoundInfo > lowerBound
QueryResult assertEqual(const Expr &x_i, const EpsRational &c, const Theorem &thm)
std::string tableauxAsString() const
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void computeType(const Expr &e)
Compute and store the type of e.
ArithProofRules * createProofRules()
EpsRational operator/(const Rational &a) const
EpsRational & operator+=(const EpsRational &r)
void separateMonomial(const Expr &e, Expr &c, Expr &var)
Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.
TheoryArithNew(TheoryCore *core)
std::vector< Expr > assertedExpr
void propagateTheory(const Expr &assertExpr, const EpsRational &bound, const EpsRational &oldBound)
CDMap< Expr, BoundInfo > upperBound
static const EpsRational Zero
void addSharedTerm(const Expr &e)
Theorem substAndCanonizeModTableaux(const Theorem &eq)
CDList< Theorem > d_diseq
bool lessThanVar(const Expr &isolatedVar, const Expr &var2)
Theorem canonSimplify(const Expr &e)
Canonize and reduce e w.r.t. union-find database; assume all children are canonical.
Hash::hash_map< Expr, SetOfVariables > DependenciesMap
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
CDMap< Expr, EpsRational > beta
Theorem isIntegerDerive(const Expr &isIntE, const Theorem &thm)
A helper method for isIntegerThm()
void collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache)
Traverse 'e' and push all the i-leaves into 'vars' vector.
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
bool isStale(const Expr &e)
Check if the term expression is "stale".
void substAndCanonizeTableaux(const Theorem &eq)
DependenciesMap dependenciesMap
std::set< Expr > intVariables
Theorem canonSimplify(const Theorem &thm)
Composition of canonSimplify(const Expr&) by transitivity: take e0 = e1, canonize and simplify e1 to ...
CDList< Theorem > d_buffer
Buffer of input inequalities.
Private class for an inequality in the Fourier-Motzkin database.
const Rational & getConst() const
Theorem normalize(const Expr &e, NormalizationType type=NORMALIZE_GCD)
EpsRational(RationalType type)
CDO< bool > d_inModelCreation
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
EpsRational operator-(const EpsRational &r) const
CDMap< Expr, FreeConst > d_freeConstDB
Mapping of inequalities to the largest/smallest free constant.
QueryResult assertLower(const Expr &x_i, const EpsRational &c, const Theorem &thm)
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
const Expr & getRHS() const
bool varOnLHS() const
Flag whether var is isolated on the LHS.
Expr computeNormalFactor(const Expr &rhs, NormalizationType type=NORMALIZE_GCD)
std::string toString() const
Theorem addInequalities(const Theorem &le_1, const Theorem &le_2)
Theorem substAndCanonize(const Expr &t, ExprMap< Theorem > &subst)
Substitute all vars in term 't' according to the substitution 'subst' and canonize the result...
Theorem getVariableIntroThm(const Expr &leftSide)
FreeConst(const Rational &r, bool strict)
Theorem rafineIntegerConstraints(const Theorem &thm)
CDMap< Expr, bool > d_sharedTerms
Set of shared terms (for counterexample generation)
Ineq(const Theorem &ineq, bool varOnRHS, const FreeConst &c)
Initial constructor. 'r' is taken from the subsumption database.
Theorem getUpperBoundThm(const Expr &x) const
void checkType(const Expr &e)
Check that e is a valid Type expr.
Rational getRational() const
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 ...
ExprMap< CDList< Ineq > * > d_inequalitiesLeftDB
Database of inequalities with a variable isolated on the left.
Rational getFloor() const
EpsRational operator+(const EpsRational &r) const
static const EpsRational PlusInfinity
EpsRational getBeta(const Expr &x)
const Theorem & ineq() const
Get the inequality.
CDO< size_t > d_bufferIdx
Buffer index of the next unprocessed inequality.
void updateFreshVariables()
Theorem solve(const Theorem &e)
An optional solver.
CDO< QueryResult > consistent
bool operator==(const EpsRational &r) const
void pivotAndUpdate(const Expr &x_i, const Expr &x_j, const EpsRational &v)
std::set< Expr > unsatBasicVariables
Theorem getLowerBoundThm(const Expr &x) const
void addToBuffer(const Theorem &thm)
Add an inequality to the input buffer. See also d_buffer.
void findRationalBound(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)
Expr pickIntEqMonomial(const Expr &right)
picks the monomial with the smallest abs(coeff) from the input
void addEdge(const Expr &e1, const Expr &e2)
Theorem getLowerBoundExplanation(const TebleauxMap::iterator &var_it)
QueryResult checkSatInteger()
bool varOnRHS() const
Flag whether var is isolated on the RHS.
CDMap< Expr, int > d_countRight
Mapping of a variable to the number of inequalities where the variable would be isolated on the right...
EpsRational getUpperBound(const Expr &x) const
Theorem isolateVariable(const Theorem &inputThm, bool &e1)
Take an inequality and isolate a variable.
std::string unsatAsString() const
CDO< Theorem > integer_lemma
friend std::ostream & operator<<(std::ostream &os, const FreeConst &fc)
Printing.
void updateDependenciesAdd(const Expr &var, const Expr &sum)
std::set< ExprBoundInfo > BoundInfoSet
const FreeConst * d_const
Expr pickMonomial(const Expr &right)
Cardinality
Enum for cardinality of types.
Theorem getUpperBoundExplanation(const TebleauxMap::iterator &var_it)
Theorem canon(const Expr &e)
Canonize the expression e, assuming all children are canonical.
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Theorem deriveGomoryCut(const Expr &x_i)
void updateDependencies(const Expr &oldExpr, const Expr &newExpr, const Expr &var, const Expr &skipVar)
EpsRational(const Rational q)
CDO< unsigned int > assertedExprCount
bool dfs(const Expr &e1, const Expr &e2)
void selectSmallest(std::vector< Expr > &v1, std::vector< Expr > &v2)
void assignVariables(std::vector< Expr > &v)
void selectLargest(const std::vector< Expr > &v1, std::vector< Expr > &v2)
void pivot(const Expr &x_r, const Expr &x_s)
void refineCounterExample()
Process disequalities from the arrangement for model generation.
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
bool isBasic(const Expr &x) const
QueryResult assertUpper(const Expr &x_i, const EpsRational &c, const Theorem &thm)
std::string boundsAsString()
ExprMap< std::vector< Expr > > d_edges
Theorem canonPredEquiv(const Theorem &thm)
bool operator<(const BoundInfo &bI) const
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
EpsRational(const Rational q, const Rational k)
void setupRec(const Expr &e)
Recursive setup for isolated inequalities (and other new expressions)
void updateDependenciesRemove(const Expr &var, const Expr &sum)