CVC3  2.4.1
Classes | Public Member Functions | Private Types | Private Member Functions | Private Attributes | Friends
CVC3::TheoryArithNew Class Reference

#include <theory_arith_new.h>

Inheritance diagram for CVC3::TheoryArithNew:
CVC3::TheoryArith CVC3::Theory

List of all members.

Classes

struct  BoundInfo
class  EpsRational
struct  ExprBoundInfo
class  FreeConst
class  Ineq
 Private class for an inequality in the Fourier-Motzkin database. More...
class  VarOrderGraph

Public Member Functions

void separateMonomial (const Expr &e, Expr &c, Expr &var)
 Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.
bool isInteger (const Expr &e)
 Check the term t for integrality (return bool)
 TheoryArithNew (TheoryCore *core)
 ~TheoryArithNew ()
ArithProofRulescreateProofRules ()
void addSharedTerm (const Expr &e)
void assertFact (const Theorem &e)
 Assert a new fact to the decision procedure.
void refineCounterExample ()
 Process disequalities from the arrangement for model generation.
void computeModelBasic (const std::vector< Expr > &v)
 Assign concrete values to basic-type variables in v.
void computeModel (const Expr &e, std::vector< Expr > &vars)
 Compute the value of a compound variable from the more primitive ones.
void checkSat (bool fullEffort)
 Check for satisfiability in the theory.
Theorem rewrite (const Expr &e)
 Theory-specific rewrite rules.
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 solve (const Theorem &e)
 An optional solver.
void checkAssertEqInvariant (const Theorem &e)
 A debug check used by the primary solver.
void checkType (const Expr &e)
 Check that e is a valid Type expr.
Cardinality finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize)
 Compute information related to finiteness of types.
void computeType (const Expr &e)
 Compute and store the type of e.
Type computeBaseType (const Type &t)
 Compute the base type of the top-level operator of an arbitrary type.
void computeModelTerm (const Expr &e, std::vector< Expr > &v)
 Add variables from 'e' to 'v' for constructing a concrete model.
Expr computeTypePred (const Type &t, const Expr &e)
 Theory specific computation of the subtyping predicate for type t applied to the expression e.
Expr computeTCC (const Expr &e)
 Compute and cache the TCC of e.
ExprStreamprint (ExprStream &os, const Expr &e)
 Theory-specific pretty-printing.
virtual Expr parseExprOp (const Expr &e)
 Theory-specific parsing implemented by the DP.
void registerAtom (const Expr &e)
EpsRational getLowerBound (const Expr &x) const
EpsRational getUpperBound (const Expr &x) const
Theorem getLowerBoundThm (const Expr &x) const
Theorem getUpperBoundThm (const Expr &x) const
EpsRational getBeta (const Expr &x)
- Public Member Functions inherited from CVC3::TheoryArith
 TheoryArith (TheoryCore *core, const std::string &name)
 ~TheoryArith ()
virtual void addMultiplicativeSignSplit (const Theorem &case_split_thm)
virtual bool addPairToArithOrder (const Expr &smaller, const Expr &bigger)
bool isSyntacticRational (const Expr &e, Rational &r)
 Return whether e is syntactically identical to a rational constant.
bool isAtomicArithFormula (const Expr &e)
 Whether any ite's appear in the arithmetic part of the formula e.
Expr rewriteToDiff (const Expr &e)
 Rewrite an atom to look like x - y op c if possible–for smtlib translation.
Theorem canonThm (const Theorem &thm)
 Composition of canon(const Expr&) by transitivity: take e0 = e1, canonize e1 to e2, return e0 = e2.
Type realType ()
Type intType ()
Type subrangeType (const Expr &l, const Expr &r)
Expr rat (Rational r)
Expr darkShadow (const Expr &lhs, const Expr &rhs)
 Construct the dark shadow expression representing lhs <= rhs.
Expr grayShadow (const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)
 Construct the gray shadow expression representing c1 <= v - e <= c2.
bool leavesAreNumConst (const Expr &e)
- Public Member Functions inherited from CVC3::Theory
 Theory (TheoryCore *theoryCore, const std::string &name)
 Whether theory has been used (for smtlib translator)
virtual ~Theory (void)
 Destructor.
ExprManagergetEM ()
 Access to ExprManager.
TheoryCoretheoryCore ()
 Get a pointer to theoryCore.
CommonProofRulesgetCommonRules ()
 Get a pointer to common proof rules.
const std::string & getName () const
 Get the name of the theory (for debugging purposes)
virtual void setUsed ()
 Set the "used" flag on this theory (for smtlib translator)
virtual bool theoryUsed ()
 Get whether theory has been used (for smtlib translator)
virtual Theorem theoryPreprocess (const Expr &e)
 Theory-specific preprocessing.
virtual Theorem simplifyOp (const Expr &e)
 Recursive simplification step.
virtual void assertTypePred (const Expr &e, const Theorem &pred)
 Receives all the type predicates for the types of the given theory.
virtual Theorem rewriteAtomic (const Expr &e)
 Theory-specific rewrites for atomic formulas.
virtual void notifyInconsistent (const Theorem &thm)
 Notification of conflict.
virtual void registerAtom (const Expr &e, const Theorem &thm)
virtual bool inconsistent ()
 Check if the current context is inconsistent.
virtual void setInconsistent (const Theorem &e)
 Make the context inconsistent; The formula proved by e must FALSE.
virtual void setIncomplete (const std::string &reason)
 Mark the current decision branch as possibly incomplete.
virtual Theorem simplify (const Expr &e)
 Simplify a term e and return a Theorem(e==e')
Expr simplifyExpr (const Expr &e)
 Simplify a term e w.r.t. the current context.
virtual void enqueueFact (const Theorem &e)
 Submit a derived fact to the core from a decision procedure.
virtual void enqueueSE (const Theorem &e)
 Check if the current context is inconsistent.
virtual void assertEqualities (const Theorem &e)
 Handle new equalities (usually asserted through addFact)
virtual Expr parseExpr (const Expr &e)
 Parse the generic expression.
virtual void assignValue (const Expr &t, const Expr &val)
 Assigns t a concrete value val. Used in model generation.
virtual void assignValue (const Theorem &thm)
 Record a derived assignment to a variable (LHS).
void registerKinds (Theory *theory, std::vector< int > &kinds)
 Register new kinds with the given theory.
void unregisterKinds (Theory *theory, std::vector< int > &kinds)
 Unregister kinds for a theory.
void registerTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
 Register a new theory.
void unregisterTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver)
 Unregister a theory.
int getNumTheories ()
 Return the number of registered theories.
bool hasTheory (int kind)
 Test whether a kind maps to any theory.
TheorytheoryOf (int kind)
 Return the theory associated with a kind.
TheorytheoryOf (const Type &e)
 Return the theory associated with a type.
TheorytheoryOf (const Expr &e)
 Return the theory associated with an Expr.
Theorem find (const Expr &e)
 Return the theorem that e is equal to its find.
const TheoremfindRef (const Expr &e)
 Return the find as a reference: expr must have a find.
Theorem findReduce (const Expr &e)
 Return find-reduced version of e.
bool findReduced (const Expr &e)
 Return true iff e is find-reduced.
Expr findExpr (const Expr &e)
 Return the find of e, or e if it has no find.
Expr getTCC (const Expr &e)
 Compute the TCC of e, or the subtyping predicate, if e is a type.
Type getBaseType (const Expr &e)
 Compute (or look up in cache) the base type of e and return the result.
Type getBaseType (const Type &tp)
 Compute the base type from an arbitrary type.
Expr getTypePred (const Type &t, const Expr &e)
 Calls the correct theory to compute a type predicate.
Theorem updateHelper (const Expr &e)
 Update the children of the term e.
void setupCC (const Expr &e)
 Setup a term for congruence closure (must have sig and rep attributes)
void updateCC (const Theorem &e, const Expr &d)
 Update a term w.r.t. congruence closure (must be setup with setupCC())
Theorem rewriteCC (const Expr &e)
 Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
void getModelTerm (const Expr &e, std::vector< Expr > &v)
 Calls the correct theory to get all of the terms that need to be assigned values in the concrete model.
Theorem getModelValue (const Expr &e)
 Fetch the concrete assignment to the variable during model generation.
void addSplitter (const Expr &e, int priority=0)
 Suggest a splitter to the SearchEngine.
void addGlobalLemma (const Theorem &thm, int priority=0)
 Add a global lemma.
bool isLeaf (const Expr &e)
 Test if e is an i-leaf term for the current theory.
bool isLeafIn (const Expr &e1, const Expr &e2)
 Test if e1 is an i-leaf in e2.
bool leavesAreSimp (const Expr &e)
 Test if all i-leaves of e are simplified.
Type boolType ()
 Return BOOLEAN type.
const ExprfalseExpr ()
 Return FALSE Expr.
const ExprtrueExpr ()
 Return TRUE Expr.
Expr newVar (const std::string &name, const Type &type)
 Create a new variable given its name and type.
Expr newVar (const std::string &name, const Type &type, const Expr &def)
 Create a new named expression given its name, type, and definition.
Op newFunction (const std::string &name, const Type &type, bool computeTransClosure)
 Create a new uninterpreted function.
Op lookupFunction (const std::string &name, Type *type)
 Look up a function by name.
Op newFunction (const std::string &name, const Type &type, const Expr &def)
 Create a new defined function.
Expr addBoundVar (const std::string &name, const Type &type)
 Create and add a new bound variable to the stack, for parseExprOp().
Expr addBoundVar (const std::string &name, const Type &type, const Expr &def)
 Create and add a new bound named def to the stack, for parseExprOp().
Expr lookupVar (const std::string &name, Type *type)
 Lookup variable and return it and its type. Return NULL Expr if it doesn't exist yet.
Type newTypeExpr (const std::string &name)
 Create a new uninterpreted type with the given name.
Type lookupTypeExpr (const std::string &name)
 Lookup type by name. Return Null if no such type exists.
Type newTypeExpr (const std::string &name, const Type &def)
 Create a new type abbreviation with the given name.
Type newSubtypeExpr (const Expr &pred, const Expr &witness)
 Create a new subtype expression.
Expr resolveID (const std::string &name)
 Resolve an identifier, for use in parseExprOp()
void installID (const std::string &name, const Expr &e)
 Install name as a new identifier associated with Expr e.
Theorem typePred (const Expr &e)
 Return BOOLEAN type.
Theorem reflexivityRule (const Expr &a)
 ==> a == a
Theorem symmetryRule (const Theorem &a1_eq_a2)
 a1 == a2 ==> a2 == a1
Theorem transitivityRule (const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
 (a1 == a2) & (a2 == a3) ==> (a1 == a3)
Theorem substitutivityRule (const Op &op, const std::vector< Theorem > &thms)
 (c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Theorem substitutivityRule (const Expr &e, const Theorem &t)
 Special case for unary operators.
Theorem substitutivityRule (const Expr &e, const Theorem &t1, const Theorem &t2)
 Special case for binary operators.
Theorem substitutivityRule (const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)
 Optimized: only positions which changed are included.
Theorem substitutivityRule (const Expr &e, int changed, const Theorem &thm)
 Optimized: only a single position changed.
Theorem iffMP (const Theorem &e1, const Theorem &e1_iff_e2)
 e1 AND (e1 IFF e2) ==> e2
Theorem rewriteAnd (const Expr &e)
 ==> AND(e1,e2) IFF [simplified expr]
Theorem rewriteOr (const Expr &e)
 ==> OR(e1,...,en) IFF [simplified expr]
Theorem rewriteIte (const Expr &e)
 Derived rule for rewriting ITE.
Theorem renameExpr (const Expr &e)
 Derived rule to create a new name for an expression.

Private Types

enum  NormalizationType { NORMALIZE_GCD, NORMALIZE_UNIT }
typedef Hash::hash_map< Expr,
Theorem
TebleauxMap
typedef std::set< ExprSetOfVariables
typedef Hash::hash_map< Expr,
SetOfVariables
DependenciesMap
typedef std::set< ExprBoundInfoBoundInfoSet

Private Member Functions

Theorem isIntegerThm (const Expr &e)
 Check the term t for integrality.
Theorem isIntegerDerive (const Expr &isIntE, const Theorem &thm)
 A helper method for isIntegerThm()
bool kidsCanonical (const Expr &e)
 Check if the kids of e are fully simplified and canonized (for debugging)
Theorem canon (const Expr &e)
 Canonize the expression e, assuming all children are canonical.
Theorem canonSimplify (const Expr &e)
 Canonize and reduce e w.r.t. union-find database; assume all children are canonical.
Theorem canonSimplify (const Theorem &thm)
 Composition of canonSimplify(const Expr&) by transitivity: take e0 = e1, canonize and simplify e1 to e2, return e0 = e2.
Theorem canonPred (const Theorem &thm)
 Canonize predicate (x = y, x < y, etc.)
Theorem canonPredEquiv (const Theorem &thm)
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.
Expr pickIntEqMonomial (const Expr &right)
 picks the monomial with the smallest abs(coeff) from the input
Theorem processRealEq (const Theorem &eqn)
 processes equalities with 1 or more vars of type REAL
Theorem processIntEq (const Theorem &eqn)
 processes equalities whose vars are all of type INT
Theorem processSimpleIntEq (const Theorem &eqn)
 One step of INT equality processing (aux. method for processIntEq())
Theorem isolateVariable (const Theorem &inputThm, bool &e1)
 Take an inequality and isolate a variable.
void updateStats (const Rational &c, const Expr &var)
 Update the statistics counters for the variable with a coeff. c.
void updateStats (const Expr &monomial)
 Update the statistics counters for the monomial.
void addToBuffer (const Theorem &thm)
 Add an inequality to the input buffer. See also d_buffer.
Expr pickMonomial (const Expr &right)
bool lessThanVar (const Expr &isolatedVar, const Expr &var2)
bool isStale (const Expr &e)
 Check if the term expression is "stale".
bool isStale (const Ineq &ineq)
 Check if the inequality is "stale" or subsumed.
void projectInequalities (const Theorem &theInequality, bool isolatedVarOnRHS)
void assignVariables (std::vector< Expr > &v)
void findRationalBound (const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)
bool findBounds (const Expr &e, Rational &lub, Rational &glb)
Theorem normalizeProjectIneqs (const Theorem &ineqThm1, const Theorem &ineqThm2)
Theorem solvedForm (const std::vector< Theorem > &solvedEqs)
 Take a system of equations and turn it into a solved form.
Theorem substAndCanonize (const Expr &t, ExprMap< Theorem > &subst)
 Substitute all vars in term 't' according to the substitution 'subst' and canonize the result.
Theorem substAndCanonize (const Theorem &eq, ExprMap< Theorem > &subst)
 Substitute all vars in the RHS of the equation 'eq' of the form (x = t) according to the substitution 'subst', and canonize the result.
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 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 constraint.
void processFiniteIntervals (const Expr &x)
 For an integer var 'x', find and process all constraints A <= ax <= A+c.
void setupRec (const Expr &e)
 Recursive setup for isolated inequalities (and other new expressions)
Theorem deriveGomoryCut (const Expr &x_i)
Theorem rafineIntegerConstraints (const Theorem &thm)
void propagateTheory (const Expr &assertExpr, const EpsRational &bound, const EpsRational &oldBound)
void updateDependenciesAdd (const Expr &var, const Expr &sum)
void updateDependenciesRemove (const Expr &var, const Expr &sum)
void updateDependencies (const Expr &oldExpr, const Expr &newExpr, const Expr &var, const Expr &skipVar)
void updateFreshVariables ()
void updateValue (const Expr &var, const Expr &e)
std::string tableauxAsString () const
std::string unsatAsString () const
std::string boundsAsString ()
Theorem getVariableIntroThm (const Expr &leftSide)
const RationalfindCoefficient (const Expr &var, const Expr &expr)
bool isBasic (const Expr &x) const
Rational getTableauxEntry (const Expr &x_i, const Expr &x_j)
void pivot (const Expr &x_r, const Expr &x_s)
void update (const Expr &x_i, const EpsRational &v)
void pivotAndUpdate (const Expr &x_i, const Expr &x_j, const EpsRational &v)
QueryResult assertUpper (const Expr &x_i, const EpsRational &c, const Theorem &thm)
QueryResult assertLower (const Expr &x_i, const EpsRational &c, const Theorem &thm)
QueryResult assertEqual (const Expr &x_i, const EpsRational &c, const Theorem &thm)
Expr computeNormalFactor (const Expr &rhs, NormalizationType type=NORMALIZE_GCD)
Theorem normalize (const Expr &e, NormalizationType type=NORMALIZE_GCD)
Theorem normalize (const Theorem &thm, NormalizationType type=NORMALIZE_GCD)
Theorem substAndCanonizeModTableaux (const Theorem &eq)
Theorem substAndCanonizeModTableaux (const Expr &sum)
void substAndCanonizeTableaux (const Theorem &eq)
Theorem pivotRule (const Theorem &eq, const Expr &var)
Theorem getLowerBoundExplanation (const TebleauxMap::iterator &var_it)
Theorem getUpperBoundExplanation (const TebleauxMap::iterator &var_it)
Theorem addInequalities (const Theorem &le_1, const Theorem &le_2)
QueryResult checkSatSimplex ()
QueryResult checkSatInteger ()

Private Attributes

CDList< Theoremd_diseq
CDO< size_t > d_diseqIdx
ArithProofRulesd_rules
CDO< bool > d_inModelCreation
ExprMap< CDList< Ineq > * > d_inequalitiesRightDB
 Database of inequalities with a variable isolated on the right.
ExprMap< CDList< Ineq > * > d_inequalitiesLeftDB
 Database of inequalities with a variable isolated on the left.
CDMap< Expr, FreeConstd_freeConstDB
 Mapping of inequalities to the largest/smallest free constant.
CDList< Theoremd_buffer
 Buffer of input inequalities.
CDO< size_t > d_bufferIdx
 Buffer index of the next unprocessed inequality.
const int * d_bufferThres
 Threshold when the buffer must be processed.
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, 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_sharedTerms
 Set of shared terms (for counterexample generation)
CDMap< Expr, bool > d_sharedVars
 Set of shared integer variables (i-leaves)
VarOrderGraph d_graph
std::set< ExprintVariables
CDO< QueryResultconsistent
Theorem explanation
CDMap< Expr, BoundInfolowerBound
CDMap< Expr, BoundInfoupperBound
CDMap< Expr, EpsRationalbeta
DependenciesMap dependenciesMap
TebleauxMap tableaux
TebleauxMap freshVariables
std::set< ExprunsatBasicVariables
std::vector< ExprassertedExpr
CDO< unsigned int > assertedExprCount
bool propagate
BoundInfoSet allBounds
CDO< Theoreminteger_lemma

Friends

std::ostream & operator<< (std::ostream &os, const FreeConst &fc)
 Printing.
std::ostream & operator<< (std::ostream &os, const Ineq &ineq)
 Printing.

Additional Inherited Members

- Protected Member Functions inherited from CVC3::TheoryArith
Theorem canonRec (const Expr &e)
 Canonize the expression e recursively.
void printRational (ExprStream &os, const Rational &r, bool printAsReal=false)
 Print a rational in SMT-LIB format.
bool isAtomicArithTerm (const Expr &e)
 Whether any ite's appear in the arithmetic part of the term e.
Theorem canonSimp (const Expr &e)
 simplify leaves and then canonize
bool recursiveCanonSimpCheck (const Expr &e)
 helper for checkAssertEqInvariant
- Protected Attributes inherited from CVC3::TheoryArith
Type d_realType
Type d_intType
std::vector< int > d_kinds
- Protected Attributes inherited from CVC3::Theory
bool d_theoryUsed

Detailed Description

This theory handles basic linear arithmetic.

Author:
Clark Barrett
Since:
Sat Feb 8 14:44:32 2003

Definition at line 41 of file theory_arith_new.h.


Member Typedef Documentation

Definition at line 611 of file theory_arith_new.h.

typedef std::set<Expr> CVC3::TheoryArithNew::SetOfVariables
private

Definition at line 615 of file theory_arith_new.h.

Definition at line 616 of file theory_arith_new.h.

A set of BoundInfo objects

Definition at line 636 of file theory_arith_new.h.


Member Enumeration Documentation

Type of noramlization GCD = 1 or just first coefficient 1

Enumerator:
NORMALIZE_GCD 
NORMALIZE_UNIT 

Definition at line 813 of file theory_arith_new.h.


Constructor & Destructor Documentation

TheoryArithNew::TheoryArithNew ( TheoryCore core)
TheoryArithNew::~TheoryArithNew ( )

Member Function Documentation

Theorem TheoryArithNew::isIntegerThm ( const Expr e)
private

Check the term t for integrality.

Returns:
a theorem of IS_INTEGER(t) or Null.

Definition at line 68 of file theory_arith_new.cpp.

References CVC3::Expr::getType(), CVC3::IS_INTEGER, and CVC3::isReal().

Referenced by isInteger(), processFiniteInterval(), and rafineIntegerConstraints().

Theorem TheoryArithNew::isIntegerDerive ( const Expr isIntE,
const Theorem thm 
)
private

A helper method for isIntegerThm()

Check if IS_INTEGER(e) is easily derivable from the given 'thm'

Definition at line 76 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), CVC3::Theorem::getExpr(), CVC3::Expr::isAnd(), and CVC3::Theorem::isNull().

bool TheoryArithNew::kidsCanonical ( const Expr e)
private

Check if the kids of e are fully simplified and canonized (for debugging)

Definition at line 94 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), std::endl(), and IF_DEBUG.

Theorem TheoryArithNew::canon ( const Expr e)
privatevirtual

Canonize the expression e, assuming all children are canonical.

Compute a canonical form for expression e and return a theorem that e is equal to its canonical form. Note that canonical form for arith expressions is of the following form:

b + a_1 x_1 + a_2 x_2 + ... + a_n x_n (ONE SUM EXPRESION)

or just a rational b (RATIONAL EXPRESSION)

where a_i and b are rationals and x_i are arithmetical leaves (i.e. variables or non arithmetic terms)

Author:
Clark Barrett
Vijay Ganesh
Since:
Sat Feb 8 14:46:32 2003

Implements CVC3::TheoryArith.

Definition at line 123 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), DebugAssert, CVC3::DIVIDE, CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::isRational(), CVC3::MINUS, CVC3::MULT, CVC3::PLUS, CVC3::POW, CVC3::Expr::toString(), TRACE, and CVC3::UMINUS.

Referenced by pivotRule(), processFiniteInterval(), and rewrite().

Theorem TheoryArithNew::canonSimplify ( const Expr e)
private

Canonize and reduce e w.r.t. union-find database; assume all children are canonical.

Definition at line 246 of file theory_arith_new.cpp.

References DebugAssert, CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), CVC3::Expr::toString(), and TRACE.

Referenced by canonSimplify().

Theorem CVC3::TheoryArithNew::canonSimplify ( const Theorem thm)
inlineprivate

Composition of canonSimplify(const Expr&) by transitivity: take e0 = e1, canonize and simplify e1 to e2, return e0 = e2.

Definition at line 155 of file theory_arith_new.h.

References canonSimplify(), CVC3::Theorem::getRHS(), and CVC3::Theory::transitivityRule().

Theorem TheoryArithNew::canonPred ( const Theorem thm)
private

Canonize predicate (x = y, x < y, etc.)

accepts a theorem, canonizes it, applies iffMP and substituvity to derive the canonized thm

Definition at line 279 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::getOp(), and CVC3::Theorem::toString().

Referenced by processFiniteInterval().

Theorem TheoryArithNew::canonPredEquiv ( const Theorem thm)
private

Canonize predicate like canonPred except that the input theorem is an equivalent transformation.

Accepts an equivalence theorem, canonizes the subexpressions, applies transitivity and substituvity to derive the canonized theorem.

Parameters:
thmequivalence theorem
Returns:
the canonised expression theorem

Definition at line 295 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getOp(), CVC3::Theorem::getRHS(), and CVC3::Theorem::toString().

Referenced by normalize(), and rewrite().

Theorem TheoryArithNew::doSolve ( const Theorem thm)
private

Solve an equation and return an equivalent Theorem in the solved form.

Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)

  1. translate e to the form e' = 0
  2. if (e'.isRational()) then {if e' != 0 return false else true}
  3. a for loop checks if all the variables are integers.
    • if not isolate a suitable real variable and call processRealEq().
    • if all variables are integers then isolate suitable variable and call processIntEq().

Definition at line 331 of file theory_arith_new.cpp.

References DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::getRational(), IF_DEBUG, CVC3::isRational(), CVC3::Expr::isRational(), CVC3::Theorem::isRewrite(), MiniSat::right(), CVC3::Theorem::toString(), and TRACE.

Referenced by solve().

Theorem TheoryArithNew::canonConjunctionEquiv ( const Theorem thm)
private

takes in a conjunction equivalence Thm and canonizes it.

accepts an equivalence theorem whose RHS is a conjunction, canonizes it, applies iffMP and substituvity to derive the canonized thm

Definition at line 318 of file theory_arith_new.cpp.

Expr TheoryArithNew::pickIntEqMonomial ( const Expr right)
private

picks the monomial with the smallest abs(coeff) from the input

pick a monomial for the input equation. This function is used only if the equation is an integer equation. Choose the monomial with the smallest absolute value of coefficient.

Definition at line 388 of file theory_arith_new.cpp.

References CVC3::abs(), CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::isMult(), CVC3::isPlus(), CVC3::isRational(), MiniSat::min(), and CVC3::Expr::toString().

Theorem TheoryArithNew::processRealEq ( const Theorem eqn)
private

processes equalities with 1 or more vars of type REAL

input is e1=e2<==>0=e' Theorem and some of the vars in e' are of type REAL. isolate one of them and send back to framework. output is "e1=e2 <==> var = e''" Theorem.

Definition at line 420 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), DebugAssert, EQ, CVC3::Theorem::getLHS(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::isMult(), CVC3::isPlus(), CVC3::isRational(), CVC3::isReal(), MiniSat::left(), MiniSat::right(), CVC3::Theorem::toString(), CVC3::Expr::toString(), and TRACE.

Theorem TheoryArithNew::processIntEq ( const Theorem eqn)
private

processes equalities whose vars are all of type INT

input is e1=e2<==>0=e' Theorem and all of the vars in e' are of type INT. isolate one of them and send back to framework. output is "e1=e2 <==> var = e''" Theorem and some associated equations in solved form.

Definition at line 642 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::isAnd(), CVC3::Expr::isFalse(), CVC3::Theorem::isRewrite(), CVC3::Expr::toString(), and TRACE.

Theorem TheoryArithNew::processSimpleIntEq ( const Theorem eqn)
private
Theorem CVC3::TheoryArithNew::isolateVariable ( const Theorem inputThm,
bool &  e1 
)
private

Take an inequality and isolate a variable.

void TheoryArithNew::updateStats ( const Rational c,
const Expr var 
)
private

Update the statistics counters for the variable with a coeff. c.

Definition at line 808 of file theory_arith_new.cpp.

References CVC3::Rational::toString(), and TRACE.

void TheoryArithNew::updateStats ( const Expr monomial)
private

Update the statistics counters for the monomial.

Definition at line 821 of file theory_arith_new.cpp.

References CVC3::Expr::getRational().

void TheoryArithNew::addToBuffer ( const Theorem thm)
private

Add an inequality to the input buffer. See also d_buffer.

Definition at line 829 of file theory_arith_new.cpp.

References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Theorem::getExpr(), CVC3::isPlus(), CVC3::isRational(), and TRACE.

Expr CVC3::TheoryArithNew::pickMonomial ( const Expr right)
private
void TheoryArithNew::separateMonomial ( const Expr e,
Expr c,
Expr var 
)
virtual

Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.

Implements CVC3::TheoryArith.

Definition at line 944 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getKids(), CVC3::isMult(), CVC3::isPlus(), CVC3::isRational(), CVC3::Expr::isRational(), CVC3::multExpr(), CVC3::Expr::toString(), and TRACE.

Referenced by findRationalBound().

bool CVC3::TheoryArithNew::isInteger ( const Expr e)
inline

Check the term t for integrality (return bool)

Definition at line 189 of file theory_arith_new.h.

References isIntegerThm(), and CVC3::Theorem::isNull().

Referenced by assertFact(), assignVariables(), checkSatInteger(), computeType(), print(), processFiniteInterval(), processFiniteIntervals(), and solve().

bool TheoryArithNew::lessThanVar ( const Expr isolatedVar,
const Expr var2 
)
private

Definition at line 932 of file theory_arith_new.cpp.

References DebugAssert, CVC3::isRational(), and CVC3::Expr::toString().

bool CVC3::TheoryArithNew::isStale ( const Expr e)
private

Check if the term expression is "stale".

bool CVC3::TheoryArithNew::isStale ( const Ineq ineq)
private

Check if the inequality is "stale" or subsumed.

void CVC3::TheoryArithNew::projectInequalities ( const Theorem theInequality,
bool  isolatedVarOnRHS 
)
private
void TheoryArithNew::assignVariables ( std::vector< Expr > &  v)
private
void TheoryArithNew::findRationalBound ( const Expr varSide,
const Expr ratSide,
const Expr var,
Rational r 
)
private
bool TheoryArithNew::findBounds ( const Expr e,
Rational lub,
Rational glb 
)
private
Theorem CVC3::TheoryArithNew::normalizeProjectIneqs ( const Theorem ineqThm1,
const Theorem ineqThm2 
)
private
Theorem TheoryArithNew::solvedForm ( const std::vector< Theorem > &  solvedEqs)
private

Take a system of equations and turn it into a solved form.

Takes a vector of equations and for every equation x_i=t_i substitutes t_j for x_j in t_i for all j>i. This turns the system of equations into a solved form.

Assumption: variables x_j may appear in the RHS terms t_i ONLY for i<j, but not for i>=j.

Definition at line 681 of file theory_arith_new.cpp.

References CVC3::ExprMap< Data >::begin(), DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::Theorem::getExpr(), IF_DEBUG, TRACE, and TRACE_MSG.

Theorem TheoryArithNew::substAndCanonize ( const Expr t,
ExprMap< Theorem > &  subst 
)
private

Substitute all vars in term 't' according to the substitution 'subst' and canonize the result.

ASSUMPTION: 't' is a fully canonized arithmetic term, and every element of subst is a fully canonized equation of the form x=e, indexed by the LHS variable.

Definition at line 736 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), CVC3::ExprMap< Data >::empty(), CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Theorem::getRHS(), and TRACE.

Theorem TheoryArithNew::substAndCanonize ( const Theorem eq,
ExprMap< Theorem > &  subst 
)
private

Substitute all vars in the RHS of the equation 'eq' of the form (x = t) according to the substitution 'subst', and canonize the result.

ASSUMPTION: 't' is a fully canonized equation of the form x = t, and so is every element of subst, indexed by the LHS variable.

Definition at line 787 of file theory_arith_new.cpp.

References DebugAssert, CVC3::ExprMap< Data >::empty(), CVC3::Theorem::getExpr(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), and CVC3::Expr::toString().

void TheoryArithNew::collectVars ( const Expr e,
std::vector< Expr > &  vars,
std::set< Expr > &  cache 
)
private

Traverse 'e' and push all the i-leaves into 'vars' vector.

Definition at line 1155 of file theory_arith_new.cpp.

References CVC3::Expr::begin(), CVC3::Expr::end(), and CVC3::Theory::isLeaf().

void TheoryArithNew::processFiniteInterval ( const Theorem alphaLEax,
const Theorem bxLEbeta 
)
private
void TheoryArithNew::processFiniteIntervals ( const Expr x)
private

For an integer var 'x', find and process all constraints A <= ax <= A+c.

Definition at line 1226 of file theory_arith_new.cpp.

References d_inequalitiesLeftDB, d_inequalitiesRightDB, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), isInteger(), processFiniteInterval(), and CVC3::CDList< T >::size().

void TheoryArithNew::setupRec ( const Expr e)
private

Recursive setup for isolated inequalities (and other new expressions)

This function recursively decends expression tree without caching until it hits a node that is already setup. Be careful on what expressions you are calling it.

Definition at line 1252 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), CVC3::Expr::hasFind(), CVC3::Theory::reflexivityRule(), CVC3::Expr::setEqNext(), CVC3::Expr::setFind(), and setup().

ArithProofRules * TheoryArithNew::createProofRules ( )

Definition at line 43 of file arith_theorem_producer.cpp.

Referenced by TheoryArithNew().

void TheoryArithNew::addSharedTerm ( const Expr e)
virtual

Keep track of all finitely bounded integer variables in shared terms.

When a new shared term t is reported, all of its variables x1...xn are added to the set d_sharedVars.

For each newly added variable x, check all of its opposing inequalities, find out all the finite bounds and assert the corresponding GRAY_SHADOW constraints.

When projecting integer inequalities, the database d_sharedVars is consulted, and if the variable is in it, check the shadows for being a finite interval, and produce the additional GRAY_SHADOW constraints.

Implements CVC3::TheoryArith.

Definition at line 1282 of file theory_arith_new.cpp.

References d_sharedTerms.

void TheoryArithNew::assertFact ( const Theorem e)
virtual
void TheoryArithNew::refineCounterExample ( )
virtual
void TheoryArithNew::computeModelBasic ( const std::vector< Expr > &  v)
virtual

Assign concrete values to basic-type variables in v.

Implements CVC3::TheoryArith.

Definition at line 1433 of file theory_arith_new.cpp.

References assignVariables(), d_inModelCreation, CVC3::Theory::findExpr(), and TRACE.

void TheoryArithNew::computeModel ( const Expr e,
std::vector< Expr > &  vars 
)
virtual

Compute the value of a compound variable from the more primitive ones.

The more primitive variables for e are already assigned concrete values, and are available through getModelValue().

The new value for e must be assigned using assignValue() method.

Parameters:
eis the compound type expression to assign a value;
varsare the variables actually assigned. Normally, 'e' is the only element of vars. However, e.g. in the case of uninterpreted functions, assigning 'f' means assigning all relevant applications of 'f' to constant values (f(0), f(5), etc.). Such applications might not be known before the model is constructed (they may be of the form f(x), f(y+z), etc., where x,y,z are still unassigned).

Populating 'vars' is an opportunity for a DP to change the set of top-level "variables" to assign, if needed. In particular, it may drop 'e' from the model entirely, if it is already a concrete value by itself.

Implements CVC3::TheoryArith.

Definition at line 1456 of file theory_arith_new.cpp.

References CVC3::Theory::assignValue(), DebugAssert, CVC3::Theory::findExpr(), CVC3::isRational(), CVC3::Theory::simplify(), and CVC3::Expr::toString().

void TheoryArithNew::checkSat ( bool  fullEffort)
virtual

Check for satisfiability in the theory.

Parameters:
fullEffortwhen it is false, checkSat can do as much or as little work as it likes, though simple inferences and checks for consistency should be done to increase efficiency. If fullEffort is true, checkSat must check whether the set of facts given by assertFact together with the arrangement of shared terms (provided by addSharedTerm) induced by the global find database equivalence relation are satisfiable. If satisfiable, checkSat does nothing.

If satisfiability can be acheived by merging some of the shared terms, a new fact must be enqueued using enqueueFact (this fact need not be a literal). If there is no way to make things satisfiable, setInconsistent must be called.

Implements CVC3::TheoryArith.

Definition at line 2830 of file theory_arith_new.cpp.

References assertedExpr, assertedExprCount, checkSatSimplex(), consistent, DebugAssert, explanation, CVC3::SATISFIABLE, CVC3::Theory::setInconsistent(), TRACE, CVC3::UNSATISFIABLE, and updateFreshVariables().

Theorem TheoryArithNew::rewrite ( const Expr e)
virtual

Theory-specific rewrite rules.

By default, rewrite just returns a reflexive theorem stating that the input expression is equivalent to itself. However, rewrite is allowed to return any theorem which describes how the input expression is equivalent to some new expression. rewrite should be used to perform simplifications, normalization, and any other preprocessing on theory-specific expressions that needs to be done.

Implements CVC3::TheoryArith.

Definition at line 1570 of file theory_arith_new.cpp.

References CVC3::andExpr(), canon(), CVC3::ArithProofRules::canonPlus(), canonPredEquiv(), CVC3::ArithProofRules::constPredicate(), d_rules, DebugAssert, CVC3::ArithProofRules::dummyTheorem(), EQ, CVC3::ArithProofRules::eqToIneq(), FatalAssert, CVC3::GE, CVC3::geExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::GT, CVC3::IS_INTEGER, CVC3::Expr::isAbsLiteral(), CVC3::Expr::isAtomic(), CVC3::isPlus(), CVC3::isRational(), CVC3::Expr::isTerm(), CVC3::LE, CVC3::leExpr(), CVC3::LT, CVC3::ArithProofRules::negatedInequality(), normalize(), NORMALIZE_UNIT, NOT, CVC3::ArithProofRules::plusPredicate(), CVC3::TheoryArith::rat(), CVC3::Theory::reflexivityRule(), CVC3::ArithProofRules::rightMinusLeft(), CVC3::Expr::setRewriteNormal(), CVC3::Theory::simplify(), CVC3::Theory::substitutivityRule(), CVC3::Theory::theoryOf(), CVC3::Expr::toString(), TRACE, and CVC3::Theory::transitivityRule().

Referenced by update().

void TheoryArithNew::setup ( const Expr e)
virtual

Set up the term e for call-backs when e or its children change.

setup is called once for each expression associated with the theory. It is typically used to setup theory-specific data for an expression and to add call-back information for use with update.

See also:
update

Implements CVC3::TheoryArith.

Definition at line 1734 of file theory_arith_new.cpp.

References CVC3::Expr::addToNotify(), CVC3::Expr::arity(), DebugAssert, CVC3::int2string(), CVC3::Expr::isEq(), CVC3::isIneq(), CVC3::isIntPred(), CVC3::Expr::isNot(), CVC3::isRational(), CVC3::Expr::isTerm(), CVC3::Expr::toString(), and TRACE.

Referenced by setupRec().

void TheoryArithNew::update ( const Theorem e,
const Expr d 
)
virtual

Notify a theory of a new equality.

update is a call-back used by the notify mechanism of the core theory. It works as follows. When an equation t1 = t2 makes it into the core framework, the two find equivalence classes for t1 and t2 are merged. The result is that t2 is the new equivalence class representative and t1 is no longer an equivalence class representative. When this happens, the notify list of t1 is traversed. Notify list entries consist of a theory and an expression d. For each entry (i,d), i->update(e, d) is called, where e is the theorem corresponding to the equality t1=t2.

To add the entry (i,d) to a term t1's notify list, a call must be made to t1.addNotify(i,d). This is typically done in setup.

See also:
setup

Implements CVC3::TheoryArith.

Definition at line 1769 of file theory_arith_new.cpp.

References CVC3::Theory::assertEqualities(), CVC3::TheoryArith::canonSimp(), DebugAssert, CVC3::Theory::enqueueFact(), CVC3::Theory::find(), CVC3::Theory::getCommonRules(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Theory::iffMP(), CVC3::Theory::inconsistent(), CVC3::isIneq(), CVC3::Theory::leavesAreSimp(), rewrite(), CVC3::Theory::substitutivityRule(), CVC3::Theory::symmetryRule(), CVC3::Expr::toString(), TRACE, CVC3::Theory::transitivityRule(), and CVC3::Theory::trueExpr().

Referenced by assertLower(), and assertUpper().

Theorem TheoryArithNew::solve ( const Theorem e)
virtual

An optional solver.

The solve method can be used to implement a Shostak-style solver. Since solvers do not in general combine, the following technique is used. One theory is designated as the primary solver (in our case, it is the theory of arithmetic). For each equation that enters the core framework, the primary solver is called to ensure that the equation is in solved form with respect to the primary theory.

After the primary solver, the solver for the theory associated with the equation is called. This solver can do whatever it likes, as long as the result is still in solved form with respect to the primary solver. This is a slight generalization of what is described in my (Clark)'s PhD thesis.

Implements CVC3::TheoryArith.

Definition at line 1805 of file theory_arith_new.cpp.

References DebugAssert, doSolve(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::TheoryArith::intType(), isInteger(), CVC3::Theory::isLeaf(), CVC3::Theory::isLeafIn(), CVC3::Theorem::isRewrite(), CVC3::Expr::isTerm(), and CVC3::Theory::symmetryRule().

void TheoryArithNew::checkAssertEqInvariant ( const Theorem e)
virtual

A debug check used by the primary solver.

Implements CVC3::TheoryArith.

Definition at line 1878 of file theory_arith_new.cpp.

void TheoryArithNew::checkType ( const Expr e)
virtual
Cardinality TheoryArithNew::finiteTypeInfo ( Expr e,
Unsigned n,
bool  enumerate,
bool  computeSize 
)
virtual

Compute information related to finiteness of types.

Used by the TypeComputer defined in TheoryCore (theories should not call this funtion directly – they should use the methods in Type instead). Each theory should implement this if it contains any types that could be non-infinite.

  1. Returns Cardinality of the type (finite, infinite, or unknown)
  2. If cardinality = finite and enumerate is true, sets e to the nth element of the type if it can sets e to NULL if n is out of bounds or if unable to compute nth element
  3. If cardinality = finite and computeSize is true, sets n to the size of the type if it can sets n to 0 otherwise

Implements CVC3::TheoryArith.

Definition at line 1908 of file theory_arith_new.cpp.

References CVC3::CARD_FINITE, CVC3::CARD_INFINITE, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Rational::getUnsigned(), CVC3::TheoryArith::rat(), and CVC3::SUBRANGE.

void TheoryArithNew::computeType ( const Expr e)
virtual
Type TheoryArithNew::computeBaseType ( const Type tp)
virtual

Compute the base type of the top-level operator of an arbitrary type.

Implements CVC3::TheoryArith.

Definition at line 2018 of file theory_arith_new.cpp.

References DebugAssert, CVC3::Type::getExpr(), CVC3::Expr::getKind(), IF_DEBUG, CVC3::INT, CVC3::REAL, CVC3::TheoryArith::realType(), CVC3::SUBRANGE, and CVC3::Type::toString().

void TheoryArithNew::computeModelTerm ( const Expr e,
std::vector< Expr > &  v 
)
virtual

Add variables from 'e' to 'v' for constructing a concrete model.

If e is already of primitive type, do NOT add it to v.

Implements CVC3::TheoryArith.

Definition at line 1833 of file theory_arith_new.cpp.

References CVC3::Expr::begin(), CVC3::DIVIDE, CVC3::Expr::end(), CVC3::Theory::findExpr(), CVC3::Expr::getKind(), CVC3::MULT, CVC3::PLUS, CVC3::POW, RATIONAL_EXPR, CVC3::Expr::toString(), and TRACE.

Expr TheoryArithNew::computeTypePred ( const Type t,
const Expr e 
)
virtual

Theory specific computation of the subtyping predicate for type t applied to the expression e.

By default returns true. Each theory needs to compute subtype predicates for the types associated with it. So, for example, the theory of records will take a record type [# f1: T1, f2: T2 #] and an expression e and will return the subtyping predicate for e, namely: computeTypePred(T1, e.f1) AND computeTypePred(T2, e.f2)

Implements CVC3::TheoryArith.

Definition at line 1860 of file theory_arith_new.cpp.

References CVC3::andExpr(), CVC3::Expr::getEM(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::INT, CVC3::IS_INTEGER, CVC3::leExpr(), CVC3::SUBRANGE, and CVC3::ExprManager::trueExpr().

Expr TheoryArithNew::computeTCC ( const Expr e)
virtual

Compute and cache the TCC of e.

Parameters:
eis an expression (term or formula). This function computes the TCC of e which is true iff the expression is defined.

This function computes the TCC or predicate of the top-level operator of e, and recurses into children using getTCC(), if necessary.

The default implementation is to compute TCCs recursively for all children, and return their conjunction.

Implements CVC3::TheoryArith.

Definition at line 2025 of file theory_arith_new.cpp.

References CVC3::Expr::andExpr(), CVC3::Expr::arity(), CVC3::Theory::computeTCC(), DebugAssert, CVC3::DIVIDE, CVC3::Expr::getKind(), and CVC3::TheoryArith::rat().

ExprStream & TheoryArithNew::print ( ExprStream os,
const Expr e 
)
virtual

Theory-specific pretty-printing.

By default, print the top node in AST, and resume pretty-printing the children. The same call e.print(os) can be used in DP-specific printers to use AST printing for the given node. In fact, it is strongly recommended to add e.print(os) as the default for all the cases/kinds that are not handled by the particular pretty-printer.

Implements CVC3::TheoryArith.

Definition at line 2150 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::DARK_SHADOW, CVC3::DIVIDE, CVC3::Expr::end(), CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::GRAY_SHADOW, CVC3::GT, CVC3::INT, CVC3::IS_INTEGER, CVC3::isInt(), isInteger(), CVC3::ExprStream::lang(), CVC3::LE, CVC3::LISP_LANG, CVC3::LT, CVC3::MINUS, CVC3::MULT, CVC3::NEGINF, CVC3::PLUS, CVC3::POSINF, CVC3::POW, CVC3::PRESENTATION_LANG, CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::TheoryArith::printRational(), CVC3::push(), RATIONAL_EXPR, CVC3::REAL, CVC3::REAL_CONST, CVC3::SIMPLIFY_LANG, CVC3::SMTLIB_LANG, CVC3::SMTLIB_V2_LANG, CVC3::space(), CVC3::SUBRANGE, CVC3::TPTP_LANG, and CVC3::UMINUS.

Expr TheoryArithNew::parseExprOp ( const Expr e)
virtual
void TheoryArithNew::registerAtom ( const Expr e)
virtual

Registers the atom given from the core. This atoms are stored so that they can be used for theory propagation.

Parameters:
ethe expression (atom) that is part of the input formula

Reimplemented from CVC3::Theory.

Definition at line 3953 of file theory_arith_new.cpp.

References allBounds, FatalAssert, CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::GT, CVC3::Expr::isAbsAtomicFormula(), CVC3::LE, CVC3::LT, CVC3::Expr::toString(), and TRACE.

Theorem TheoryArithNew::deriveGomoryCut ( const Expr x_i)
private

Return a Gomory cut plane derivation of the variable $x_i$. Mixed integer Gomory cut can be constructed if

  • $x_i$ is a integer basic variable with a non-integer value
  • all non-basic variables in the row of $x_i$ are assigned to their upper or lower bounds
  • all the values on the right side of the row have rational values (non eps-rational values)

Definition at line 4105 of file theory_arith_new.cpp.

References DebugAssert, getBeta(), CVC3::TheoryArithNew::EpsRational::getRational(), intVariables, isBasic(), and CVC3::Expr::toString().

Theorem TheoryArithNew::rafineIntegerConstraints ( const Theorem thm)
private

Tries to rafine the integer constraint of the theorem. For example, x < 1 is rewritten as x <= 0, and x <(=) 1.5 is rewritten as x <= 1. The constraint should be in the normal form.

Parameters:
thmthe derivation of the constraint

Definition at line 1541 of file theory_arith_new.cpp.

References d_rules, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::GT, CVC3::Rational::isInteger(), isIntegerThm(), CVC3::Theorem::isNull(), CVC3::LT, CVC3::ArithProofRules::rafineStrictInteger(), TRACE, and CVC3::Theory::transitivityRule().

void TheoryArithNew::propagateTheory ( const Expr assertExpr,
const EpsRational bound,
const EpsRational oldBound 
)
private
void TheoryArithNew::updateDependenciesAdd ( const Expr var,
const Expr sum 
)
private

Adds var to the dependencies sets of all the variables in the sum.

Parameters:
varthe variable on the left side
sumthe sum that defines the variable

Definition at line 3873 of file theory_arith_new.cpp.

References CVC3::Expr::begin(), dependenciesMap, CVC3::Expr::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::insert(), CVC3::Expr::toString(), and TRACE.

Referenced by getVariableIntroThm(), and pivot().

void TheoryArithNew::updateDependenciesRemove ( const Expr var,
const Expr sum 
)
private

Remove var from the dependencies sets of all the variables in the sum.

Parameters:
varthe variable on the left side
sumthe sum that defines the variable

Definition at line 3886 of file theory_arith_new.cpp.

References CVC3::Expr::begin(), dependenciesMap, CVC3::Expr::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::erase(), CVC3::Expr::toString(), and TRACE.

Referenced by pivot().

void TheoryArithNew::updateDependencies ( const Expr oldExpr,
const Expr newExpr,
const Expr var,
const Expr skipVar 
)
private

Updates the dependencies if a right side of an expression in the tableaux is changed. For example, if oldExpr is x + y and newExpr is y + z, var will be added to the dependency list of z, and removed from the dependency list of x.

Parameters:
oldExprthe old right side of the tableaux
newExprthe new right side of the tableaux
varthe variable that is defined by these two expressions
skipVara variable to skip when going through the expressions

Definition at line 3899 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), dependenciesMap, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::erase(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::insert(), CVC3::Theory::newVar(), CVC3::Expr::toString(), and TRACE.

Referenced by substAndCanonizeTableaux().

void TheoryArithNew::updateFreshVariables ( )
private

Update the values of variables that have appeared in the tableaux due to backtracking.

Definition at line 3859 of file theory_arith_new.cpp.

References assertedExpr, assertedExprCount, and updateValue().

Referenced by assertFact(), and checkSat().

void TheoryArithNew::updateValue ( const Expr var,
const Expr e 
)
private

Updates the value of variable var by computing the value of expression e.

Parameters:
varthe variable to update
ethe expression to compute

Definition at line 3323 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), beta, getBeta(), getLowerBound(), CVC3::Expr::getRational(), getUpperBound(), and unsatBasicVariables.

Referenced by getVariableIntroThm(), and updateFreshVariables().

string TheoryArithNew::tableauxAsString ( ) const
private

Returns a string representation of the tableaux.

Returns:
tableaux as string

Definition at line 3343 of file theory_arith_new.cpp.

References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::begin(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), and tableaux.

Referenced by assertFact(), and checkSatSimplex().

string TheoryArithNew::unsatAsString ( ) const
private

Returns a string representation of the unsat variables.

Returns:
unsat as string

Definition at line 3365 of file theory_arith_new.cpp.

References unsatBasicVariables.

Referenced by assertFact(), and checkSatSimplex().

string TheoryArithNew::boundsAsString ( )
private
Theorem TheoryArithNew::getVariableIntroThm ( const Expr leftSide)
private

Gets the equality of the fresh variable tableaux variable corresponding to this expression. If the expression has already been asserted, the coresponding variable is returned, othervise a fresh variable is created and the theorem is returned.

Parameters:
leftSidethe left side of the asserted constraint
Returns:
the equality theorem s = leftSide

Definition at line 3273 of file theory_arith_new.cpp.

References assertedExpr, assertedExprCount, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), EQ, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), CVC3::Theory::find(), freshVariables, CVC3::Theory::getCommonRules(), CVC3::Theorem::getExpr(), CVC3::CommonProofRules::iffMP(), CVC3::CommonProofRules::skolemizeRewrite(), substAndCanonizeModTableaux(), CVC3::Theory::symmetryRule(), tableaux, updateDependenciesAdd(), updateValue(), and CVC3::CommonProofRules::varIntroRule().

Referenced by assertFact().

const Rational & TheoryArithNew::findCoefficient ( const Expr var,
const Expr expr 
)
private

Find the coefficient standing by the variable var in the expression expr. Expresion is expected to be in canonical form, i.e either a rational constant, an arithmetic leaf (i.e. variable or term from some other theory), (MULT rat leaf) where rat is a non-zero rational constant, leaf is an arithmetic leaf or (PLUS $const term_0 term_1 ... term_n$) where each $term_i$ is either a leaf or (MULT $rat leaf$) and each leaf in $term_i$ must be strictly greater than the leaf in $term_{i+1}$.

Parameters:
varthe variable
exprthe expression to search in

Definition at line 3043 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), CVC3::compare(), DebugAssert, CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isPlus(), CVC3::isRational(), MiniSat::left(), MiniSat::right(), and CVC3::Expr::toString().

Referenced by getTableauxEntry().

bool TheoryArithNew::isBasic ( const Expr x) const
private

Return true iof the given variable is basic in the tableaux, i.e. it is on the left side, expressed in terms of the non-basic variables.

Parameters:
xthe variable to be checked
Returns:
true if the variable is basic, false if the variable is non-basic

Definition at line 2589 of file theory_arith_new.cpp.

References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), and tableaux.

Referenced by assertLower(), assertUpper(), deriveGomoryCut(), and pivot().

Rational TheoryArithNew::getTableauxEntry ( const Expr x_i,
const Expr x_j 
)
private

Returns the coefficient at a_ij in the current tableaux, i.e. the coefficient at x_j in the row of x_i.

Parameters:
x_ia basic variable
x_ja non-basic variable
Returns:
the reational coefficient

Definition at line 3038 of file theory_arith_new.cpp.

References findCoefficient(), and tableaux.

Referenced by pivotAndUpdate(), and update().

void TheoryArithNew::pivot ( const Expr x_r,
const Expr x_s 
)
private
    Swaps a basic variable \form#271 and a non-basic variable \form#272 such
    that ars \form#273. After pivoting, \form#272 becomes basic and \form#271 becomes non-basic. 
    The tableau is updated by replacing equation \form#274 with

\[x_s = \frac{x_r}{a_{rs}} - \sum_{x_j \in N }{\frac{a_{rj}}{a_rs}x_j}\]

and this equation is used to eliminate $x_s$ from the rest of the tableau by substitution.

Parameters:
x_ra basic variable
x_sa non-basic variable

Definition at line 2594 of file theory_arith_new.cpp.

References DebugAssert, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::erase(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), CVC3::Theorem::getExpr(), isBasic(), pivotRule(), substAndCanonizeTableaux(), tableaux, CVC3::Expr::toString(), TRACE, updateDependenciesAdd(), and updateDependenciesRemove().

Referenced by pivotAndUpdate().

void TheoryArithNew::update ( const Expr x_i,
const EpsRational v 
)
private

Sets the value of a non-basic variable $x_i$ to $v$ and adjusts the value of all the basic variables so that all equations remain satisfied.

Parameters:
x_ia non-basic variable
vthe value to set the variable $x_i$ to

Definition at line 2628 of file theory_arith_new.cpp.

References beta, DebugAssert, dependenciesMap, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), CVC3::Theory::find(), getBeta(), getLowerBound(), getTableauxEntry(), getUpperBound(), tableaux, CVC3::TheoryArithNew::EpsRational::toString(), CVC3::Expr::toString(), TRACE, and unsatBasicVariables.

void TheoryArithNew::pivotAndUpdate ( const Expr x_i,
const Expr x_j,
const EpsRational v 
)
private

Pivots the basic variable $x_i$ and the non-basic variable $x_j$. It also sets $x_i$ to $v$ and adjusts all basic variables to keep the equations satisfied.

Parameters:
x_ia basic variable
x_ja non-basic variable
vthe valie to assign to x_i

Definition at line 2675 of file theory_arith_new.cpp.

References beta, DebugAssert, dependenciesMap, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), getBeta(), getLowerBound(), getTableauxEntry(), getUpperBound(), pivot(), tableaux, CVC3::TheoryArithNew::EpsRational::toString(), CVC3::Expr::toString(), TRACE, and unsatBasicVariables.

Referenced by checkSatSimplex().

QueryResult TheoryArithNew::assertUpper ( const Expr x_i,
const EpsRational c,
const Theorem thm 
)
private

Asserts a new upper bound constraint on a variable and performs a simple check for consistency (not complete).

Parameters:
x_ithe variable to assert the bound on
cthe bound to assert

Definition at line 2740 of file theory_arith_new.cpp.

References CVC3::ArithProofRules::clashingBounds(), consistent, d_rules, DebugAssert, explanation, getBeta(), getLowerBound(), getLowerBoundThm(), getUpperBound(), isBasic(), CVC3::Theory::isLeaf(), propagate, CVC3::SATISFIABLE, CVC3::TheoryArithNew::EpsRational::toString(), CVC3::Expr::toString(), TRACE, CVC3::UNKNOWN, unsatBasicVariables, CVC3::UNSATISFIABLE, update(), and upperBound.

Referenced by assertEqual(), and assertFact().

QueryResult TheoryArithNew::assertLower ( const Expr x_i,
const EpsRational c,
const Theorem thm 
)
private

Asserts a new lower bound constraint on a variable and performs a simple check for consistency (not complete).

Parameters:
x_ithe variable to assert the bound on
cthe bound to assert

Definition at line 2777 of file theory_arith_new.cpp.

References CVC3::ArithProofRules::clashingBounds(), consistent, d_rules, DebugAssert, explanation, getBeta(), getLowerBound(), getUpperBound(), getUpperBoundThm(), isBasic(), CVC3::Theory::isLeaf(), lowerBound, propagate, CVC3::SATISFIABLE, CVC3::TheoryArithNew::EpsRational::toString(), CVC3::Expr::toString(), TRACE, CVC3::UNKNOWN, unsatBasicVariables, CVC3::UNSATISFIABLE, and update().

Referenced by assertEqual(), and assertFact().

QueryResult TheoryArithNew::assertEqual ( const Expr x_i,
const EpsRational c,
const Theorem thm 
)
private

Asserts a new equality constraint on a variable by asserting both upper and lower bounds.

Parameters:
x_ithe variable to assert the bound on
cthe bound to assert

Definition at line 2814 of file theory_arith_new.cpp.

References assertLower(), assertUpper(), consistent, and CVC3::UNSATISFIABLE.

Referenced by assertFact().

Expr TheoryArithNew::computeNormalFactor ( const Expr rhs,
NormalizationType  type = NORMALIZE_GCD 
)
private

Given a canonized term, compute a factor to make all coefficients integer and relatively prime

Definition at line 853 of file theory_arith_new.cpp.

References CVC3::abs(), CVC3::Expr::arity(), DebugAssert, CVC3::Rational::getDenominator(), CVC3::Rational::getNumerator(), CVC3::Expr::getRational(), CVC3::isPlus(), CVC3::isRational(), CVC3::MULT, RATIONAL_EXPR, and CVC3::Expr::toString().

Referenced by normalize().

Theorem TheoryArithNew::normalize ( const Expr e,
NormalizationType  type = NORMALIZE_GCD 
)
private

Normalize an equation (make all coefficients rel. prime integers)

accepts a rewrite theorem over eqn|ineqn and normalizes it and returns a theorem to that effect. assumes e is non-trivial i.e. e is not '0=const' or 'const=0' or '0 <= const' etc.

Definition at line 1468 of file theory_arith_new.cpp.

References canonPredEquiv(), computeNormalFactor(), d_rules, DebugAssert, FatalAssert, CVC3::GE, CVC3::Expr::getKind(), CVC3::GT, CVC3::isIneq(), CVC3::isMult(), CVC3::isPlus(), CVC3::isRational(), CVC3::LE, CVC3::LT, CVC3::ArithProofRules::multIneqn(), CVC3::TheoryArith::rat(), CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), and TRACE.

Referenced by normalize(), and rewrite().

Theorem TheoryArithNew::normalize ( const Theorem thm,
NormalizationType  type = NORMALIZE_GCD 
)
private

Normalize an equation (make all coefficients rel. prime integers) accepts a rewrite theorem over eqn|ineqn and normalizes it and returns a theorem to that effect.

Definition at line 1537 of file theory_arith_new.cpp.

References CVC3::Theorem::getRHS(), normalize(), and CVC3::Theory::transitivityRule().

Theorem TheoryArithNew::substAndCanonizeModTableaux ( const Theorem eq)
private

Canonise the equation using the tebleaux equations, i.e. replace all the tableaux right sides with the corresponding left sides and canonise the result.

Parameters:
eqthe equation to canonise
Returns:
the explaining theorem

Definition at line 3447 of file theory_arith_new.cpp.

References DebugAssert, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::empty(), EQ, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Theory::iffMP(), CVC3::Theory::substitutivityRule(), tableaux, and CVC3::Expr::toString().

Referenced by getVariableIntroThm().

Theorem TheoryArithNew::substAndCanonizeModTableaux ( const Expr sum)
private

Canonise the sum using the tebleaux equations, i.e. replace all the tableaux right sides with the corresponding left sides and canonise the result.

Parameters:
sumthe canonised sum to canonise
Returns:
the explaining theorem

Definition at line 3471 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), CVC3::TheoryArith::canonThm(), DebugAssert, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), CVC3::Theory::find(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::PLUS, CVC3::Theory::reflexivityRule(), CVC3::Theory::substitutivityRule(), tableaux, CVC3::Expr::toString(), and TRACE.

void TheoryArithNew::substAndCanonizeTableaux ( const Theorem eq)
private
Theorem TheoryArithNew::pivotRule ( const Theorem eq,
const Expr var 
)
private

Given an equality eq: $\sum a_i x_i = y$ and a variable $var$ that appears in on the left hand side, pivots $y$ and $var$ so that $y$ comes to the right-hand side.

Parameters:
eqthe proof of the equality
varthe variable to move to the right-hand side

Definition at line 3600 of file theory_arith_new.cpp.

References CVC3::Expr::arity(), canon(), d_rules, DebugAssert, EQ, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Theory::iffMP(), CVC3::Theory::isLeaf(), CVC3::ArithProofRules::multEqn(), CVC3::multExpr(), CVC3::ArithProofRules::oneElimination(), CVC3::PLUS, CVC3::plusExpr(), CVC3::ArithProofRules::plusPredicate(), CVC3::TheoryArith::rat(), CVC3::Theory::symmetryRule(), CVC3::Expr::toString(), TRACE, and CVC3::Theory::transitivityRule().

Referenced by pivot().

Theorem TheoryArithNew::getLowerBoundExplanation ( const TebleauxMap::iterator var_it)
private
    Knowing that the tableaux row for \form#180 is the problematic one, generate the
    explanation clause. The variables in the row of \form#278 are separated to
    <ul>
    <li> \form#279
  <li> \form#280 
    </ul>
    Then, the explanation clause to be returned is 

\[\Gamma = \left\lbrace x_j \leq u_j \; | \; x_j \in \mathcal{N}^+\right\rbrace \cup \left\lbrace l_j \leq x_j \; | \; x_j \in \mathcal{N}^-\right\rbrace \cup \left\lbrace l_i \leq x_i \right\rbrace\]

    @param var_it the variable that caused the clash
    @return the theorem explainang the clash

Definition at line 3662 of file theory_arith_new.cpp.

References CVC3::ArithProofRules::addInequalities(), CVC3::Expr::arity(), CVC3::ArithProofRules::canonMultConstConst(), CVC3::ArithProofRules::canonMultTermConst(), CVC3::ArithProofRules::canonPlus(), CVC3::ArithProofRules::clashingBounds(), d_rules, CVC3::Theorem::getExpr(), getLowerBoundThm(), CVC3::Expr::getRational(), getUpperBoundThm(), CVC3::Theory::iffMP(), CVC3::ArithProofRules::multIneqn(), CVC3::Theory::substitutivityRule(), and CVC3::Theory::symmetryRule().

Referenced by checkSatSimplex().

Theorem TheoryArithNew::getUpperBoundExplanation ( const TebleauxMap::iterator var_it)
private
    Knowing that the tableaux row for \form#180 is the problematic one, generate the
    explanation clause. The variables in the row of \form#278 are separated to
    <ul>
    <li> \form#279
  <li> \form#280 
    </ul>
    Then, the explanation clause to be returned is 

\[\Gamma = \left\lbrace x_j \leq u_j \; | \; x_j \in \mathcal{N}^-\right\rbrace \cup \left\lbrace l_j \leq x_j \; | \; x_j \in \mathcal{N}^+\right\rbrace \cup \left\lbrace x_i \leq u_i \right\rbrace\]

    @param var_it the variable that caused the clash
    @return the theorem explainang the clash

Definition at line 3749 of file theory_arith_new.cpp.

References CVC3::ArithProofRules::addInequalities(), CVC3::Expr::arity(), CVC3::ArithProofRules::canonMultConstConst(), CVC3::ArithProofRules::canonMultTermConst(), CVC3::ArithProofRules::canonPlus(), CVC3::ArithProofRules::clashingBounds(), d_rules, getBeta(), CVC3::Theorem::getExpr(), getLowerBoundThm(), CVC3::Expr::getRational(), getUpperBoundThm(), CVC3::Theory::iffMP(), CVC3::ArithProofRules::multIneqn(), CVC3::Theory::substitutivityRule(), CVC3::Theory::symmetryRule(), and TRACE.

Referenced by checkSatSimplex().

Theorem CVC3::TheoryArithNew::addInequalities ( const Theorem le_1,
const Theorem le_2 
)
private
QueryResult TheoryArithNew::checkSatSimplex ( )
private
QueryResult TheoryArithNew::checkSatInteger ( )
private
TheoryArithNew::EpsRational TheoryArithNew::getLowerBound ( const Expr x) const
TheoryArithNew::EpsRational TheoryArithNew::getUpperBound ( const Expr x) const
Theorem TheoryArithNew::getLowerBoundThm ( const Expr x) const

Gets the theorem of the current lower bound on variable x.

Parameters:
xthe variable
Returns:
the current lower bound on x

Definition at line 3098 of file theory_arith_new.cpp.

References DebugAssert, CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::Theory::find(), lowerBound, and CVC3::Expr::toString().

Referenced by assertUpper(), getLowerBoundExplanation(), and getUpperBoundExplanation().

Theorem TheoryArithNew::getUpperBoundThm ( const Expr x) const

Get the theorem of the current upper bound on variable x.

Parameters:
xthe variable
Returns:
the current upper bound on x

Definition at line 3107 of file theory_arith_new.cpp.

References DebugAssert, CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::Theory::find(), CVC3::Expr::toString(), and upperBound.

Referenced by assertLower(), getLowerBoundExplanation(), and getUpperBoundExplanation().

TheoryArithNew::EpsRational TheoryArithNew::getBeta ( const Expr x)

Friends And Related Function Documentation

std::ostream& operator<< ( std::ostream &  os,
const FreeConst fc 
)
friend

Printing.

Definition at line 44 of file theory_arith_new.cpp.

std::ostream& operator<< ( std::ostream &  os,
const Ineq ineq 
)
friend

Printing.

Definition at line 54 of file theory_arith_new.cpp.


Member Data Documentation

CDList<Theorem> CVC3::TheoryArithNew::d_diseq
private

For concrete model generation

Definition at line 44 of file theory_arith_new.h.

Referenced by TheoryArithNew().

CDO<size_t> CVC3::TheoryArithNew::d_diseqIdx
private

Index to the next unprocessed disequality

Definition at line 46 of file theory_arith_new.h.

ArithProofRules* CVC3::TheoryArithNew::d_rules
private
CDO<bool> CVC3::TheoryArithNew::d_inModelCreation
private

Definition at line 48 of file theory_arith_new.h.

Referenced by computeModelBasic(), and refineCounterExample().

ExprMap<CDList<Ineq> *> CVC3::TheoryArithNew::d_inequalitiesRightDB
private

Database of inequalities with a variable isolated on the right.

Definition at line 89 of file theory_arith_new.h.

Referenced by findBounds(), processFiniteIntervals(), and ~TheoryArithNew().

ExprMap<CDList<Ineq> *> CVC3::TheoryArithNew::d_inequalitiesLeftDB
private

Database of inequalities with a variable isolated on the left.

Definition at line 91 of file theory_arith_new.h.

Referenced by findBounds(), processFiniteIntervals(), and ~TheoryArithNew().

CDMap<Expr, FreeConst> CVC3::TheoryArithNew::d_freeConstDB
private

Mapping of inequalities to the largest/smallest free constant.

The Expr is the original inequality with the free constant removed and inequality converted to non-strict (for indexing purposes). I.e. ax<c+t becomes ax<=t. This inequality is mapped to a pair<c,strict>, the smallest (largest for c+t<ax) constant among inequalities with the same 'a', 'x', and 't', and a boolean flag indicating whether the strongest inequality is strict.

Definition at line 100 of file theory_arith_new.h.

CDList<Theorem> CVC3::TheoryArithNew::d_buffer
private

Buffer of input inequalities.

Definition at line 102 of file theory_arith_new.h.

Referenced by TheoryArithNew().

CDO<size_t> CVC3::TheoryArithNew::d_bufferIdx
private

Buffer index of the next unprocessed inequality.

Definition at line 103 of file theory_arith_new.h.

Referenced by TheoryArithNew().

const int* CVC3::TheoryArithNew::d_bufferThres
private

Threshold when the buffer must be processed.

Definition at line 104 of file theory_arith_new.h.

CDMap<Expr, int> CVC3::TheoryArithNew::d_countRight
private

Mapping of a variable to the number of inequalities where the variable would be isolated on the right.

Definition at line 108 of file theory_arith_new.h.

CDMap<Expr, int> CVC3::TheoryArithNew::d_countLeft
private

Mapping of a variable to the number of inequalities where the variable would be isolated on the left.

Definition at line 111 of file theory_arith_new.h.

CDMap<Expr, bool> CVC3::TheoryArithNew::d_sharedTerms
private

Set of shared terms (for counterexample generation)

Definition at line 113 of file theory_arith_new.h.

Referenced by addSharedTerm(), and refineCounterExample().

CDMap<Expr, bool> CVC3::TheoryArithNew::d_sharedVars
private

Set of shared integer variables (i-leaves)

Definition at line 115 of file theory_arith_new.h.

VarOrderGraph CVC3::TheoryArithNew::d_graph
private

Definition at line 135 of file theory_arith_new.h.

Referenced by assignVariables().

std::set<Expr> CVC3::TheoryArithNew::intVariables
private

A set of all integer variables

Definition at line 502 of file theory_arith_new.h.

Referenced by assertFact(), checkSatInteger(), and deriveGomoryCut().

CDO<QueryResult> CVC3::TheoryArithNew::consistent
private

Are we consistent or not

Definition at line 527 of file theory_arith_new.h.

Referenced by assertEqual(), assertFact(), assertLower(), assertUpper(), checkSat(), and TheoryArithNew().

Theorem CVC3::TheoryArithNew::explanation
private

The theorem explaining the inconsistency

Definition at line 530 of file theory_arith_new.h.

Referenced by assertFact(), assertLower(), assertUpper(), checkSat(), and checkSatSimplex().

CDMap<Expr, BoundInfo> CVC3::TheoryArithNew::lowerBound
private

The map from variables to lower bounds (these must be backtrackable)

Definition at line 605 of file theory_arith_new.h.

Referenced by assertLower(), boundsAsString(), getLowerBound(), and getLowerBoundThm().

CDMap<Expr, BoundInfo> CVC3::TheoryArithNew::upperBound
private

The map from variables to upper bounds (these must be backtrackable)

Definition at line 607 of file theory_arith_new.h.

Referenced by assertUpper(), boundsAsString(), getUpperBound(), and getUpperBoundThm().

CDMap<Expr, EpsRational> CVC3::TheoryArithNew::beta
private

The current real valuation of the variables (these must be backtrackable for the last succesefull checkSAT!!!)

Definition at line 609 of file theory_arith_new.h.

Referenced by checkSatInteger(), getBeta(), pivotAndUpdate(), processFiniteInterval(), update(), and updateValue().

DependenciesMap CVC3::TheoryArithNew::dependenciesMap
private

Maps variables to sets of variables that depend on it in the tableaux

Definition at line 619 of file theory_arith_new.h.

Referenced by pivotAndUpdate(), substAndCanonizeTableaux(), update(), updateDependencies(), updateDependenciesAdd(), and updateDependenciesRemove().

TebleauxMap CVC3::TheoryArithNew::tableaux
private

The tableaux, a map from basic variables to the expressions over the non-basic ones (theorems that explain them how we got there)

Definition at line 622 of file theory_arith_new.h.

Referenced by boundsAsString(), checkSatSimplex(), getTableauxEntry(), getVariableIntroThm(), isBasic(), pivot(), pivotAndUpdate(), substAndCanonizeModTableaux(), substAndCanonizeTableaux(), tableauxAsString(), and update().

TebleauxMap CVC3::TheoryArithNew::freshVariables
private

Additional tableaux map from expressions asserted to the corresponding theorems explaining the introduction of the new variables

Definition at line 625 of file theory_arith_new.h.

Referenced by getVariableIntroThm().

std::set<Expr> CVC3::TheoryArithNew::unsatBasicVariables
private

A set containing all the unsatisfied basic variables

Definition at line 628 of file theory_arith_new.h.

Referenced by assertLower(), assertUpper(), checkSatSimplex(), getBeta(), pivotAndUpdate(), unsatAsString(), update(), and updateValue().

std::vector<Expr> CVC3::TheoryArithNew::assertedExpr
private

The vector to keep the assignments from fresh variables to expressions they represent

Definition at line 631 of file theory_arith_new.h.

Referenced by assertFact(), checkSat(), getVariableIntroThm(), and updateFreshVariables().

CDO<unsigned int> CVC3::TheoryArithNew::assertedExprCount
private

The backtrackable number of fresh variables asserted so far

Definition at line 633 of file theory_arith_new.h.

Referenced by assertFact(), checkSat(), getVariableIntroThm(), TheoryArithNew(), and updateFreshVariables().

bool CVC3::TheoryArithNew::propagate
private

Internal variable to see wheather to propagate or not

Definition at line 639 of file theory_arith_new.h.

Referenced by assertFact(), assertLower(), and assertUpper().

BoundInfoSet CVC3::TheoryArithNew::allBounds
private

Store all the atoms from the formula in this set. It is searchable by an expression and the bound. To get all the implied atoms, one just has to go up (down) and check if the atom or it's negation are implied.

Definition at line 651 of file theory_arith_new.h.

Referenced by propagateTheory(), and registerAtom().

CDO<Theorem> CVC3::TheoryArithNew::integer_lemma
private

The last lemma that we asserted to check the integer satisfiability. We don't do checksat until the lemma split has been asserted.

Definition at line 914 of file theory_arith_new.h.

Referenced by checkSatInteger().


The documentation for this class was generated from the following files: