21 #ifndef _cvc3__include__theory_arith_old_h_
22 #define _cvc3__include__theory_arith_old_h_
49 friend std::ostream&
operator<<(std::ostream& os,
const FreeConst& fc);
75 friend std::ostream&
operator<<(std::ostream& os,
const Ineq& ineq);
140 void dfs(
const Expr& e1, std::vector<Expr>& output_list);
147 void selectLargest(
const std::vector<Expr>& v1, std::vector<Expr>& v2);
150 void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
271 bool isStale(
const Ineq& ineq);
302 std::set<Expr>& cache);
338 bool enumerate,
bool computeSize);
528 if (
k >= 0)
return q;
663 return (
q < r.
q || (
q == r.
q &&
k <= r.
k));
675 FatalAssert(
false,
"EpsRational::operator <=, what kind of number is this????");
704 FatalAssert(
false,
"EpsRational::toString, what kind of number is this????");
706 return "hm, what am I?";
730 void getEdgeTheorems(
const Expr& x,
const Expr& y,
const EdgeInfo& edgeInfo, std::vector<Theorem>& outputTheorems);
953 void tryPropagate(
const Expr& x,
const Expr& y,
const DifferenceLogicGraph::EdgeInfo& x_y_edge,
int kind);
EpsRational operator*(const Rational &a) const
Theorem d_ineq
The inequality.
ArithProofRules * createProofRulesOld()
CDMap< Expr, bool > d_varConstrainedMinus
bool lessThanVar(const Expr &isolatedVar, const Expr &var2)
Theorem isolateVariable(const Theorem &inputThm, bool &e1)
Take an inequality and isolate a variable.
bool kidsCanonical(const Expr &e)
Check if the kids of e are fully simplified and canonized (for debugging)
void processFiniteIntervals(const Expr &x)
For an integer var 'x', find and process all constraints A <= ax <= A+c.
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Data structure of expressions in CVC3.
bool operator<(const EpsRational &r) const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
ExprMap< CDList< Expr > * > EdgesList
void separateMonomial(const Expr &e, Expr &c, Expr &var)
Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.
CDO< bool > d_inModelCreation
std::string toString() const
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
ExprMap< Rational > maxCoefficientRight
ExprMap< CDList< Ineq > * > d_inequalitiesLeftDB
Database of inequalities with a variable isolated on the left.
void updateConstrained(const Expr &t)
void setArith(TheoryArithOld *arith)
const FreeConst * d_const
void addEdge(const Expr &x, const Expr &y, const Rational &c, const Theorem &edge_thm)
void registerAtom(const Expr &e)
Theory-specific registration of atoms.
friend std::ostream & operator<<(std::ostream &os, const FreeConst &fc)
Printing.
DifferenceLogicGraph::EpsRational getLowerBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
bool addToBuffer(const Theorem &thm, bool priority=false)
Add an inequality to the input buffer. See also d_buffer.
void fixCurrentMaxCoefficient(Expr variable, Rational max)
bool isNonlinearEq(const Expr &e)
This theory handles basic linear arithmetic.
DifferenceLogicGraph diffLogicGraph
CDMap< Expr, int > d_countRight
Mapping of a variable to the number of inequalities where the variable would be isolated on the right...
const FreeConst & updateSubsumptionDB(const Expr &ineq, bool varOnRHS, bool &subsumed)
Update the free constant subsumption database with new inequality.
bool isConstrainedAbove(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
bool isStale(const Expr &e)
Check if the term expression is "stale".
const Theorem ineq() const
Get the inequality.
Theorem solve(const Theorem &e)
An optional solver.
MS C++ specific settings.
bool hasLowerBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
const int * d_bufferThres
Threshold when the buffer must be processed.
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
CDMap< Expr, EdgeInfo > Graph
CDMap< Expr, FreeConst > d_freeConstDB
Mapping of inequalities to the largest/smallest free constant.
ExprMap< Rational > fixedMaxCoefficient
AtomsMap formulaAtomUpperBound
CDMap< Expr, DifferenceLogicGraph::EpsRational > termLowerBounded
CDO< Rational > biggestEpsilon
CDList< Theorem > d_buffer_1
Buffer of input inequalities (one variable)
std::string toString(int base=10) const
Graph::ElementReference getEdge(const Expr &x, const Expr &y)
CDMap< Expr, Rational > termUpperBound
const Rational & freeConstIneq(const Expr &ineq, bool varOnRHS)
Extract the free constant from an inequality.
EpsRational & operator+=(const EpsRational &r)
#define DebugAssert(cond, str)
CDList< Theorem > d_diseq
CDO< unsigned > shared_index_2
DifferenceLogicGraph::EpsRational getUpperBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
Theorem substAndCanonize(const Expr &t, ExprMap< Theorem > &subst)
Substitute all vars in term 't' according to the substitution 'subst' and canonize the result...
bool dfs(const Expr &e1, const Expr &e2)
CDMap< Expr, bool > d_sharedVars
Set of shared integer variables (i-leaves)
Expr computeNormalFactor(const Expr &rhs, bool normalizeConstants)
Given a canonized term, compute a factor to make all coefficients integer and relatively prime...
CDMap< Expr, Expr > alreadyProjected
Theorem inequalityToFind(const Theorem &inequalityThm, bool normalizeRHS)
Theorem normalizeProjectIneqs(const Theorem &ineqThm1, const Theorem &ineqThm2)
Theorem checkIntegerEquality(const Theorem &thm)
CDO< Theorem > unsat_theorem
CDMap< Expr, bool > varInCycle
bool hasUpperBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
Theorem canonSimplify(const Theorem &thm)
Composition of canonSimplify(const Expr&) by transitivity: take e0 = e1, canonize and simplify e1 to ...
Theorem canon(const Expr &e)
Canonize the expression e, assuming, all children are canonical.
Private class for an inequality in the Fourier-Motzkin database.
void updateStats(const Rational &c, const Expr &var)
Update the statistics counters for the variable with a coeff. c.
Rational getEpsilon() const
bool varOnRHS() const
Flag whether var is isolated on the RHS.
CDMap< Expr, bool > termConstrainedAbove
Rational getRational() const
const FreeConst & getConst() const
Get the max/min constant.
bool addPairToArithOrder(const Expr &smaller, const Expr &bigger)
EpsRational getEdgeWeight(const Expr &x, const Expr &y)
CDO< bool > diffLogicOnly
void computeType(const Expr &e)
Compute and store the type of e.
void assignVariables(std::vector< Expr > &v)
EpsRational(RationalType type)
static const EpsRational MinusInfinity
CDO< size_t > diff_logic_size
Number of queries that are just difference logic.
bool varOnLHS() const
Flag whether var is isolated on the LHS.
void selectSmallestByCoefficient(const std::vector< Expr > &input, std::vector< Expr > &output)
CDMap< Expr, DifferenceLogicGraph::EpsRational > termUpperBounded
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
void refineCounterExample()
Process disequalities from the arrangement for model generation.
std::vector< Theorem > multiplicativeSignSplits
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
EpsRational(const EpsRational &r)
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Theorem isIntegerDerive(const Expr &isIntE, const Theorem &thm)
A helper method for isIntegerThm()
CDMap< Expr, Theorem > termLowerBoundThm
Theorem canonPredEquiv(const Theorem &thm)
EpsRational(const Rational &q)
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
int termDegree(const Expr &e)
CDMap< Expr, Theorem > bufferedInequalities
CDMap< Expr, bool > diseqSplitAlready
void getFactors(const Expr &e, std::set< Expr > &factors)
bool isPowersEquality(const Expr &nonlinearEq, Expr &power1, Expr &power2)
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
bool isConstrainedBelow(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
Theorem isIntegerThm(const Expr &e)
Check the term t for integrality.
const int * d_pathLenghtThres
const Expr & getRHS() const
void getEdgeTheorems(const Expr &x, const Expr &y, const EdgeInfo &edgeInfo, std::vector< Theorem > &outputTheorems)
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
bool tryUpdate(const Expr &x, const Expr &y, const Expr &z)
void selectSmallest(std::vector< Expr > &v1, std::vector< Expr > &v2)
TheoryArithOld(TheoryCore *core)
AtomsMap formulaAtomLowerBound
bool isInteger(const Expr &e)
Check the term t for integrality (return bool)
CDO< unsigned > shared_index_1
bool d_rhs
Var is isolated on the RHS.
Theorem doSolve(const Theorem &e)
Solve an equation and return an equivalent Theorem in the solved form.
void collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache)
Traverse 'e' and push all the i-leaves into 'vars' vector.
bool nonlinearSignSplit() const
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
ArithProofRules * d_rules
bool isUnconstrained(const Expr &t)
ExprMap< std::vector< Expr > > d_edges
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 ...
CDMap< Expr, Rational > termLowerBound
CDMap< Expr, bool > termConstrainedBelow
void checkType(const Expr &e)
Check that e is a valid Type expr.
Theorem processRealEq(const Theorem &eqn)
processes equalities with 1 or more vars of type REAL
Theorem processSimpleIntEq(const Theorem &eqn)
One step of INT equality processing (aux. method for processIntEq())
CDO< Rational > smallestPathDifference
bool existsEdge(const Expr &x, const Expr &y)
void writeGraph(std::ostream &out)
bool isPowerEquality(const Expr &nonlinearEq, Rational &constant, Expr &power1)
ExprMap< Rational > maxCoefficientLeft
void addEdge(const Expr &e1, const Expr &e2)
Theorem canonPred(const Theorem &thm)
Canonize predicate (x = y, x < y, etc.)
static const EpsRational PlusInfinity
void projectInequalities(const Theorem &theInequality, bool isolatedVarOnRHS)
Theorem normalize(const Expr &e)
Normalize an equation (make all coefficients rel. prime integers)
bool lessThan(const Expr &e1, const Expr &e2)
CDMap< Expr, bool > d_varConstrainedPlus
void setupRec(const Expr &e)
Recursive setup for isolated inequalities (and other new expressions)
Theorem rafineInequalityToInteger(const Theorem &thm)
bool canPickEqMonomial(const Expr &right)
Ineq(const Theorem &ineq, bool varOnRHS, const FreeConst &c)
Initial constructor. 'r' is taken from the subsumption database.
static const EpsRational Zero
bool isNonlinearSumTerm(const Expr &term)
EpsRational operator/(const Rational &a) const
CDList< Theorem > d_buffer_0
Buffer of input inequalities (high priority)
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
void addMultiplicativeSignSplit(const Theorem &case_split_thm)
bool pickIntEqMonomial(const Expr &right, Expr &isolated, bool &nonlin)
picks the monomial with the smallest abs(coeff) from the input
void analyseConflict(const Expr &x, int kind)
void findRationalBound(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)
void selectLargest(const std::vector< Expr > &v1, std::vector< Expr > &v2)
CDO< size_t > d_bufferIdx_2
Buffer index of the next unprocessed inequality.
CDO< size_t > d_bufferIdx_1
Buffer index of the next unprocessed inequality.
Theorem processIntEq(const Theorem &eqn)
processes equalities whose vars are all of type INT
bool isBounded(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
CDO< size_t > d_bufferIdx_3
Buffer index of the next unprocessed inequality.
CDList< Expr > d_sharedTermsList
const int * d_grayShadowThres
Threshold on gray shadow size (ignore it and set incomplete)
void expandSharedTerm(const Expr &x)
bool findBounds(const Expr &e, Rational &lub, Rational &glb)
CDMap< Expr, int > d_countLeft
Mapping of a variable to the number of inequalities where the variable would be isolated on the left...
ExprMap< CDList< Ineq > * > d_inequalitiesRightDB
Database of inequalities with a variable isolated on the right.
CDO< size_t > d_bufferIdx_0
Buffer index of the next unprocessed inequality.
Theorem getUnsatTheorem()
ExprMap< std::set< std::pair< Rational, Expr > > > AtomsMap
const Rational & getConst() const
void setRules(ArithProofRules *rules)
Cardinality
Enum for cardinality of types.
CDMap< Expr, bool > dontBuffer
CDMap< Expr, Theorem > termUpperBoundThm
FreeConst(const Rational &r, bool strict)
bool operator>(const EpsRational &r) const
bool inCycle(const Expr &x)
bool isConstrained(const Expr &t, bool intOnly=true, BoundsQueryType queryType=QueryWithCacheLeaves)
Data class for the strongest free constant in separation inqualities.
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Theorem canonSimplify(const Expr &e)
Canonize and reduce e w.r.t. union-find database; assume all children are canonical.
Type getType() const
Get the type. Recursively compute if necessary.
Rational getValuation(const Expr &x)
CDList< Theorem > d_buffer_3
Buffer of input inequalities (big constraint)
Ineq()
Default constructor is disabled.
Rational getFloor() const
void getVerticesTopological(std::vector< Expr > &output_list)
Theorem canonConjunctionEquiv(const Theorem &thm)
takes in a conjunction equivalence Thm and canonizes it.
void tryPropagate(const Expr &x, const Expr &y, const DifferenceLogicGraph::EdgeInfo &x_y_edge, int kind)
Theorem solvedForm(const std::vector< Theorem > &solvedEqs)
Take a system of equations and turn it into a solved form.
bool hasOutgoing(const Expr &x)
int extractTermsFromInequality(const Expr &inequality, Rational &c1, Expr &t1, Rational &c2, Expr &t2)
Rational currentMaxCoefficient(Expr var)
EpsRational operator+(const EpsRational &r) const
bool operator==(const EpsRational &r) const
void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
bool hasIncoming(const Expr &x)
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
void getVariables(std::vector< Expr > &variables)
DifferenceLogicGraph(TheoryArithOld *arith, TheoryCore *core, ArithProofRules *rules, Context *context)
bool operator<=(const EpsRational &r) const
ExprMap< bool > formulaAtoms
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Expr pickMonomial(const Expr &right)
CDList< Theorem > d_buffer_2
Buffer of input inequalities (small constraints)
void checkAssertEqInvariant(const Theorem &e)
A debug check used by the primary solver.
EpsRational(const Rational &q, const Rational &k)
void processBuffer()
Process inequalities in the buffer.
CDMap< Expr, bool > d_sharedTerms
Set of shared terms (for counterexample generation)