CVC3
2.4.1
|
#include <arith_theorem_producer_old.h>
Public Member Functions | |
ArithTheoremProducerOld (TheoremManager *tm, TheoryArithOld *theoryArith) | |
Constructor. More... | |
Expr | rat (Rational r) |
Create Expr from Rational (for convenience) More... | |
Type | realType () |
Type | intType () |
Expr | darkShadow (const Expr &lhs, const Expr &rhs) |
Construct the dark shadow expression representing lhs <= rhs. More... | |
Expr | grayShadow (const Expr &v, const Expr &e, const Rational &c1, const Rational &c2) |
Construct the gray shadow expression representing c1 <= v - e <= c2. More... | |
virtual Theorem | varToMult (const Expr &e) |
==> e = 1 * e More... | |
virtual Theorem | uMinusToMult (const Expr &e) |
==> -(e) = (-1) * e More... | |
virtual Theorem | minusToPlus (const Expr &x, const Expr &y) |
==> x - y = x + (-1) * y More... | |
virtual Theorem | canonUMinusToDivide (const Expr &e) |
-(e) ==> e / (-1); takes 'e' More... | |
virtual Theorem | canonDivideConst (const Expr &c, const Expr &d) |
(c) / d ==> (c/d), takes c and d More... | |
virtual Theorem | canonDivideMult (const Expr &cx, const Expr &d) |
(c * x) / d ==> (c/d) * x, takes (c*x) and d More... | |
virtual Theorem | canonDividePlus (const Expr &e, const Expr &d) |
(+ c ...)/d ==> push division to all the coefficients. More... | |
virtual Theorem | canonDivideVar (const Expr &e1, const Expr &e2) |
x / d ==> (1/d) * x, takes x and d More... | |
virtual Expr | simplifiedMultExpr (std::vector< Expr > &mulKids) |
virtual Expr | canonMultConstMult (const Expr &c, const Expr &e) |
virtual Expr | canonMultConstPlus (const Expr &e1, const Expr &e2) |
virtual Expr | canonMultPowPow (const Expr &e1, const Expr &e2) |
virtual Expr | canonMultPowLeaf (const Expr &e1, const Expr &e2) |
virtual Expr | canonMultLeafLeaf (const Expr &e1, const Expr &e2) |
virtual Expr | canonMultLeafOrPowMult (const Expr &e1, const Expr &e2) |
virtual Expr | canonCombineLikeTerms (const std::vector< Expr > &sumExprs) |
virtual Expr | canonMultLeafOrPowOrMultPlus (const Expr &e1, const Expr &e2) |
virtual Expr | canonMultPlusPlus (const Expr &e1, const Expr &e2) |
virtual Theorem | canonMultMtermMterm (const Expr &e) |
virtual Theorem | canonPlus (const Expr &e) |
Canonize (PLUS t1 ... tn) More... | |
virtual Theorem | canonInvertConst (const Expr &e) |
virtual Theorem | canonInvertLeaf (const Expr &e) |
virtual Theorem | canonInvertPow (const Expr &e) |
virtual Theorem | canonInvertMult (const Expr &e) |
virtual Theorem | canonInvert (const Expr &e) |
==> 1/e = e' where e' is canonical; takes e. More... | |
virtual Theorem | moveSumConstantRight (const Expr &e) |
virtual Theorem | canonDivide (const Expr &e) |
virtual Theorem | canonMult (const Expr &e) |
virtual Theorem | canonMultTermConst (const Expr &c, const Expr &t) |
t*c ==> c*t, takes constant c and term t More... | |
virtual Theorem | canonMultTerm1Term2 (const Expr &t1, const Expr &t2) |
t1*t2 ==> Error, takes t1 and t2 where both are non-constants More... | |
virtual Theorem | canonMultZero (const Expr &e) |
0*t ==> 0, takes 0*t More... | |
virtual Theorem | canonMultOne (const Expr &e) |
1*t ==> t, takes 1*t More... | |
virtual Theorem | canonMultConstConst (const Expr &c1, const Expr &c2) |
c1*c2 ==> c', takes constant c1*c2 More... | |
virtual Theorem | canonMultConstTerm (const Expr &c1, const Expr &c2, const Expr &t) |
c1*(c2*t) ==> c'*t, takes c1 and c2 and t More... | |
virtual Theorem | canonMultConstSum (const Expr &c1, const Expr &sum) |
c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum More... | |
virtual Theorem | canonPowConst (const Expr &pow) |
c^n = c' (compute the constant power expression) More... | |
virtual Theorem | canonFlattenSum (const Expr &e) |
flattens the input. accepts a PLUS expr More... | |
virtual Theorem | canonComboLikeTerms (const Expr &e) |
combine like terms. accepts a flattened PLUS expr More... | |
virtual Theorem | multEqZero (const Expr &expr) |
virtual Theorem | powEqZero (const Expr &expr) |
virtual Theorem | elimPower (const Expr &expr) |
virtual Theorem | elimPowerConst (const Expr &expr, const Rational &root) |
virtual Theorem | evenPowerEqNegConst (const Expr &expr) |
virtual Theorem | intEqIrrational (const Expr &expr, const Theorem &isInt) |
virtual Theorem | constPredicate (const Expr &e) |
e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=} More... | |
virtual Theorem | rightMinusLeft (const Expr &e) |
e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=} More... | |
virtual Theorem | leftMinusRight (const Expr &e) |
e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=} More... | |
virtual Theorem | plusPredicate (const Expr &x, const Expr &y, const Expr &z, int kind) |
x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind') More... | |
virtual Theorem | multEqn (const Expr &x, const Expr &y, const Expr &z) |
x = y <==> x * z = y * z, where z is a non-zero constant More... | |
virtual Theorem | divideEqnNonConst (const Expr &x, const Expr &y, const Expr &z) |
virtual Theorem | multIneqn (const Expr &e, const Expr &z) |
Multiplying inequation by a non-zero constant. More... | |
virtual Theorem | eqToIneq (const Expr &e) |
x = y ==> x <= y and x >= y More... | |
virtual Theorem | flipInequality (const Expr &e) |
"op1 GE|GT op2" <==> op2 LE|LT op1 More... | |
Theorem | negatedInequality (const Expr &e) |
Propagating negation over <,<=,>,>=. More... | |
Theorem | realShadow (const Theorem &alphaLTt, const Theorem &tLTbeta) |
Real shadow: a <(=) t, t <(=) b ==> a <(=) b. More... | |
Theorem | realShadowEq (const Theorem &alphaLEt, const Theorem &tLEalpha) |
alpha <= t <= alpha ==> t = alpha More... | |
Theorem | finiteInterval (const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt) |
Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c) More... | |
Theorem | darkGrayShadow2ab (const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx) |
Dark & Gray shadows when a <= b. More... | |
Theorem | darkGrayShadow2ba (const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx) |
Dark & Gray shadows when b <= a. More... | |
Theorem | expandDarkShadow (const Theorem &darkShadow) |
Theorem | expandGrayShadow0 (const Theorem &grayShadow) |
GRAY_SHADOW(v, e, c, c) ==> v=e+c. More... | |
Theorem | splitGrayShadow (const Theorem &grayShadow) |
G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2) More... | |
Theorem | splitGrayShadowSmall (const Theorem &grayShadow) |
Theorem | expandGrayShadow (const Theorem &grayShadow) |
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2. More... | |
Theorem | expandGrayShadowConst (const Theorem &grayShadow) |
Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion]. More... | |
Theorem | grayShadowConst (const Theorem &g) |
|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a)) More... | |
Rational | constRHSGrayShadow (const Rational &c, const Rational &b, const Rational &a) |
Implements j(c,b,a) More... | |
Theorem | lessThanToLE (const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight) |
Theorem | lessThanToLERewrite (const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight) |
Theorem | intVarEqnConst (const Expr &eqn, const Theorem &isIntx) |
Theorem | IsIntegerElim (const Theorem &isIntx) |
Theorem | eqElimIntRule (const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars) |
Equality elimination rule for integers:
See the detailed description for explanations. More... | |
Theorem | isIntConst (const Expr &e) |
return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant More... | |
Theorem | equalLeaves1 (const Theorem &e) |
Theorem | equalLeaves2 (const Theorem &e) |
Theorem | equalLeaves3 (const Theorem &e) |
Theorem | equalLeaves4 (const Theorem &e) |
Theorem | diseqToIneq (const Theorem &diseq) |
x /= y ==> (x < y) OR (x > y) More... | |
Theorem | dummyTheorem (const Expr &e) |
Theorem | oneElimination (const Expr &x) |
Theorem | clashingBounds (const Theorem &lowerBound, const Theorem &upperBound) |
Theorem | addInequalities (const Theorem &thm1, const Theorem &thm2) |
Theorem | addInequalities (const std::vector< Theorem > &thms) |
Theorem | implyWeakerInequality (const Expr &expr1, const Expr &expr2) |
Theorem | implyNegatedInequality (const Expr &expr1, const Expr &expr2) |
Theorem | integerSplit (const Expr &intVar, const Rational &intPoint) |
Theorem | trustedRewrite (const Expr &expr1, const Expr &expr2) |
Theorem | rafineStrictInteger (const Theorem &isIntConstrThm, const Expr &constr) |
Theorem | simpleIneqInt (const Expr &ineq, const Theorem &isIntRHS) |
Theorem | intEqualityRationalConstant (const Theorem &isIntConstrThm, const Expr &constr) |
Theorem | cycleConflict (const std::vector< Theorem > &inequalitites) |
Theorem | implyEqualities (const std::vector< Theorem > &inequalities) |
Theorem | implyWeakerInequalityDiffLogic (const std::vector< Theorem > &antecedentThms, const Expr &implied) |
Theorem | implyNegatedInequalityDiffLogic (const std::vector< Theorem > &antecedentThms, const Expr &implied) |
Theorem | expandGrayShadowRewrite (const Expr &theShadow) |
Theorem | compactNonLinearTerm (const Expr &nonLinear) |
Theorem | nonLinearIneqSignSplit (const Theorem &ineqThm) |
Theorem | implyDiffLogicBothBounds (const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2) |
Theorem | powerOfOne (const Expr &e) |
Theorem | rewriteLeavesConst (const Expr &e) |
![]() | |
virtual | ~ArithProofRules () |
![]() | |
TheoremProducer (TheoremManager *tm) | |
virtual | ~TheoremProducer () |
bool | withProof () |
Testing whether to generate proofs. More... | |
bool | withAssumptions () |
Testing whether to generate assumptions. More... | |
Proof | newLabel (const Expr &e) |
Create a new proof label (bound variable) for an assumption (formula) More... | |
Proof | newPf (const std::string &name) |
Proof | newPf (const std::string &name, const Expr &e) |
Proof | newPf (const std::string &name, const Proof &pf) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2) |
Proof | newPf (const std::string &name, const Expr &e, const Proof &pf) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf) |
Proof | newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end) |
Proof | newPf (const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end) |
Proof | newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const std::vector< Expr > &args) |
Proof | newPf (const std::string &name, const Expr &e, const std::vector< Expr > &args) |
Proof | newPf (const std::string &name, const Expr &e, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const std::vector< Proof > &pfs) |
Proof | newPf (const std::string &name, const std::vector< Expr > &args, const Proof &pf) |
Proof | newPf (const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs) |
Proof | newPf (const Proof &label, const Expr &frm, const Proof &pf) |
Creating LAMBDA-abstraction (LAMBDA label formula proof) More... | |
Proof | newPf (const Proof &label, const Proof &pf) |
Creating LAMBDA-abstraction (LAMBDA label proof). More... | |
Proof | newPf (const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf) |
Similarly, multi-argument lambda-abstractions: (LAMBDA (u1,...,un): (f1,...,fn). pf) More... | |
Proof | newPf (const std::vector< Proof > &labels, const Proof &pf) |
Static Public Member Functions | |
static bool | greaterthan (const Expr &, const Expr &) |
Private Member Functions | |
Auxiliary functions for eqElimIntRule() | |
Methods that compute the subterms used in eqElimIntRule() | |
Rational | modEq (const Rational &i, const Rational &m) |
Compute the special modulus: i - m*floor(i/m+1/2) More... | |
Expr | create_t (const Expr &eqn) |
Create the term 't'. See eqElimIntRule(). More... | |
Expr | create_t2 (const Expr &lhs, const Expr &rhs, const Expr &t) |
Create the term 't2'. See eqElimIntRule(). More... | |
Expr | create_t3 (const Expr &lhs, const Expr &rhs, const Expr &t) |
Create the term 't3'. See eqElimIntRule(). More... | |
void | sumModM (std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor) |
Takes sum = a_0 + a_1*x_1+...+a_n*x_n and returns the vector of similar monomials (in 'summands') with coefficients mod(a_i, m). If divide flag is true, the coefficients will be mod(a_i,m)/m. More... | |
Expr | monomialModM (const Expr &e, const Rational &m, const Rational &divisor) |
Compute the special modulus: i - m*floor(i/m+1/2) More... | |
void | sumMulF (std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor) |
Compute the special modulus: i - m*floor(i/m+1/2) More... | |
Expr | monomialMulF (const Expr &e, const Rational &m, const Rational &divisor) |
Compute the special modulus: i - m*floor(i/m+1/2) More... | |
Rational | f (const Rational &i, const Rational &m) |
Compute floor(i/m+1/2) + mod(i,m) More... | |
Expr | substitute (const Expr &term, ExprMap< Expr > &eMap) |
Compute the special modulus: i - m*floor(i/m+1/2) More... | |
void | getLeaves (const Expr &e, std::set< Rational > &s, ExprHashMap< bool > &cache) |
Compute the special modulus: i - m*floor(i/m+1/2) More... | |
Private Attributes | |
TheoryArithOld * | d_theoryArith |
Additional Inherited Members | |
![]() | |
Theorem | newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf) |
Create a new theorem. See also newRWTheorem() and newReflTheorem() More... | |
Theorem | newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) |
Create a rewrite theorem: lhs = rhs. More... | |
Theorem | newReflTheorem (const Expr &e) |
Create a reflexivity theorem. More... | |
Theorem | newAssumption (const Expr &thm, const Proof &pf, int scope=-1) |
Theorem3 | newTheorem3 (const Expr &thm, const Assumptions &assump, const Proof &pf) |
Theorem3 | newRWTheorem3 (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) |
void | soundError (const std::string &file, int line, const std::string &cond, const std::string &msg) |
![]() | |
TheoremManager * | d_tm |
ExprManager * | d_em |
const bool * | d_checkProofs |
Op | d_pfOp |
Expr | d_hole |
Definition at line 31 of file arith_theorem_producer_old.h.
|
inline |
Constructor.
Definition at line 66 of file arith_theorem_producer_old.h.
Compute the special modulus: i - m*floor(i/m+1/2)
Definition at line 2429 of file arith_theorem_producer_old.cpp.
References DebugAssert, CVC3::Rational::toString(), and TRACE.
Create the term 't'. See eqElimIntRule().
Definition at line 2369 of file arith_theorem_producer_old.cpp.
References CLASS_NAME, DebugAssert, CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isPlus(), CVC3::multExpr(), CVC3::plusExpr(), CVC3::Rational::toString(), and CVC3::Expr::toString().
|
private |
Create the term 't2'. See eqElimIntRule().
Definition at line 2388 of file arith_theorem_producer_old.cpp.
References DebugAssert, CVC3::Expr::getRational(), CVC3::isPlus(), CVC3::Expr::isRational(), CVC3::plusExpr(), and CVC3::Rational::toString().
|
private |
Create the term 't3'. See eqElimIntRule().
Definition at line 2408 of file arith_theorem_producer_old.cpp.
References DebugAssert, CVC3::Expr::getRational(), CVC3::isPlus(), CVC3::Expr::isRational(), CVC3::plusExpr(), and CVC3::Rational::toString().
|
private |
Takes sum = a_0 + a_1*x_1+...+a_n*x_n and returns the vector of similar monomials (in 'summands') with coefficients mod(a_i, m). If divide flag is true, the coefficients will be mod(a_i,m)/m.
Definition at line 2445 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::begin(), CLASS_NAME, DebugAssert, CVC3::Expr::end(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), and CVC3::Rational::toString().
|
private |
Compute the special modulus: i - m*floor(i/m+1/2)
Definition at line 2465 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getKids(), CVC3::Expr::getRational(), CVC3::isMult(), CVC3::multExpr(), CVC3::Rational::toString(), CVC3::Expr::toString(), and TRACE.
|
private |
Compute the special modulus: i - m*floor(i/m+1/2)
Definition at line 2493 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::begin(), CLASS_NAME, DebugAssert, CVC3::Expr::end(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), and CVC3::Rational::toString().
|
private |
Compute the special modulus: i - m*floor(i/m+1/2)
Definition at line 2513 of file arith_theorem_producer_old.cpp.
References DebugAssert, CVC3::isMult(), CVC3::multExpr(), and CVC3::Rational::toString().
Compute floor(i/m+1/2) + mod(i,m)
Definition at line 2438 of file arith_theorem_producer_old.cpp.
References DebugAssert, and CVC3::Rational::toString().
Compute the special modulus: i - m*floor(i/m+1/2)
Definition at line 2530 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::begin(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::ExprMap< Data >::find(), CVC3::isMult(), CVC3::isPlus(), and CVC3::plusExpr().
|
private |
Compute the special modulus: i - m*floor(i/m+1/2)
Definition at line 3838 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), DebugAssert, CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), CVC3::Expr::getRational(), CVC3::Expr::isAtomic(), CVC3::Expr::isITE(), and CVC3::Expr::isRational().
Create Expr from Rational (for convenience)
Definition at line 70 of file arith_theorem_producer_old.h.
References CVC3::TheoremProducer::d_em, and CVC3::ExprManager::newRatExpr().
|
inline |
Definition at line 71 of file arith_theorem_producer_old.h.
References CVC3::TheoryArith::realType().
|
inline |
Definition at line 72 of file arith_theorem_producer_old.h.
References CVC3::TheoryArith::intType().
Construct the dark shadow expression representing lhs <= rhs.
Definition at line 74 of file arith_theorem_producer_old.h.
References CVC3::TheoryArith::darkShadow().
|
inline |
Construct the gray shadow expression representing c1 <= v - e <= c2.
Alternatively, v = e + i for some i s.t. c1 <= i <= c2
Definition at line 80 of file arith_theorem_producer_old.h.
References CVC3::TheoryArith::grayShadow().
==> e = 1 * e
Implements CVC3::ArithProofRules.
Definition at line 57 of file arith_theorem_producer_old.cpp.
==> -(e) = (-1) * e
Implements CVC3::ArithProofRules.
Definition at line 65 of file arith_theorem_producer_old.cpp.
==> x - y = x + (-1) * y
Implements CVC3::ArithProofRules.
Definition at line 73 of file arith_theorem_producer_old.cpp.
-(e) ==> e / (-1); takes 'e'
Canon Rule for unary minus: it just converts it to division by -1, the result is not yet canonical:
Implements CVC3::ArithProofRules.
Definition at line 83 of file arith_theorem_producer_old.cpp.
(c) / d ==> (c/d), takes c and d
Canon Rules for division by constant 'd'
Implements CVC3::ArithProofRules.
Definition at line 92 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::getRational(), CVC3::isRational(), and CVC3::Expr::toString().
(c * x) / d ==> (c/d) * x, takes (c*x) and d
Implements CVC3::ArithProofRules.
Definition at line 111 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isRational(), and CVC3::Expr::toString().
(+ c ...)/d ==> push division to all the coefficients.
The result is not canonical, but canonizing the summands will make it canonical. Takes (+ c ...) and d
Implements CVC3::ArithProofRules.
Definition at line 139 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::end(), CVC3::isPlus(), CVC3::isRational(), CVC3::plusExpr(), and CVC3::Expr::toString().
x / d ==> (1/d) * x, takes x and d
Implements CVC3::ArithProofRules.
Definition at line 162 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::getRational(), CVC3::isRational(), and CVC3::Expr::toString().
Definition at line 2556 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), CVC3::MULT, CVC3::PLUS, CVC3::POW, and RATIONAL_EXPR.
Definition at line 197 of file arith_theorem_producer_old.cpp.
References DebugAssert, and CVC3::multExpr().
Definition at line 210 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::Expr::isRational(), CVC3::MULT, and CVC3::Expr::toString().
Definition at line 232 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Theorem::getRHS(), CVC3::Expr::isRational(), and CVC3::PLUS.
Definition at line 251 of file arith_theorem_producer_old.cpp.
References DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::POW, and CVC3::powExpr().
Definition at line 291 of file arith_theorem_producer_old.cpp.
References DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::POW, and CVC3::powExpr().
Definition at line 330 of file arith_theorem_producer_old.cpp.
References CVC3::powExpr().
Definition at line 358 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::MULT, CVC3::POW, and CVC3::powExpr().
Definition at line 430 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), CVC3::MULT, CVC3::multExpr(), and CVC3::plusExpr().
|
virtual |
Definition at line 511 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::PLUS.
Definition at line 530 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::PLUS.
Implements CVC3::ArithProofRules.
Definition at line 554 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, FatalAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::isMult(), CVC3::Expr::isRational(), CVC3::MULT, CVC3::PLUS, CVC3::POW, RATIONAL_EXPR, and CVC3::Expr::toString().
Canonize (PLUS t1 ... tn)
Implements CVC3::ArithProofRules.
Definition at line 719 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::PLUS.
Definition at line 819 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::isRational(), and CVC3::Expr::toString().
Definition at line 835 of file arith_theorem_producer_old.cpp.
References CVC3::powExpr().
Definition at line 847 of file arith_theorem_producer_old.cpp.
References DebugAssert, CVC3::Expr::getKind(), CVC3::POW, CVC3::powExpr(), and CVC3::Expr::toString().
Definition at line 866 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getKind(), CVC3::MULT, and CVC3::Expr::toString().
==> 1/e = e' where e' is canonical; takes e.
Implements CVC3::ArithProofRules.
Definition at line 889 of file arith_theorem_producer_old.cpp.
References DebugAssert, CVC3::Expr::getKind(), CVC3::MULT, CVC3::PLUS, CVC3::POW, RATIONAL_EXPR, and CVC3::Expr::toString().
Transform e = (SUM r t1 ... tn) @ 0 into (SUM t1 ... tn) @ -r. The first sum term (r) must be a rational and t1 ... tn terms must be canonised.
e | the expression to transform |
Implements CVC3::ArithProofRules.
Definition at line 911 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::isEq(), CVC3::isIneq(), CVC3::isPlus(), CVC3::isRational(), CVC3::Expr::isRational(), CVC3::plusExpr(), MiniSat::right(), and CVC3::Expr::toString().
e[0]/e[1] ==> e[0]*(e[1])^-1
Implements CVC3::ArithProofRules.
Definition at line 957 of file arith_theorem_producer_old.cpp.
References DebugAssert, CVC3::DIVIDE, CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), and CVC3::Expr::toString().
Multiply out the operands of the multiplication (each of them is expected to be canonised
Implements CVC3::ArithProofRules.
Definition at line 752 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::andExpr(), CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::eqExpr(), CVC3::geExpr(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Expr::iffExpr(), CVC3::Expr::impExpr(), CVC3::isPlus(), CVC3::isPow(), CVC3::Expr::isRational(), CVC3::leExpr(), CVC3::ltExpr(), CVC3::MULT, CVC3::orExpr(), CVC3::Expr::toString(), TRACE, and XOR.
t*c ==> c*t, takes constant c and term t
Implements CVC3::ArithProofRules.
Definition at line 975 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::isRational(), and CVC3::Expr::toString().
t1*t2 ==> Error, takes t1 and t2 where both are non-constants
Implements CVC3::ArithProofRules.
Definition at line 989 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, and CVC3::Expr::toString().
0*t ==> 0, takes 0*t
Implements CVC3::ArithProofRules.
Definition at line 1002 of file arith_theorem_producer_old.cpp.
1*t ==> t, takes 1*t
Implements CVC3::ArithProofRules.
Definition at line 1010 of file arith_theorem_producer_old.cpp.
c1*c2 ==> c', takes constant c1*c2
Implements CVC3::ArithProofRules.
Definition at line 1019 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::getRational(), CVC3::isRational(), and CVC3::Expr::toString().
|
virtual |
c1*(c2*t) ==> c'*t, takes c1 and c2 and t
Implements CVC3::ArithProofRules.
Definition at line 1037 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::getRational(), CVC3::isRational(), and CVC3::Expr::toString().
c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
Implements CVC3::ArithProofRules.
Definition at line 1057 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::isRational(), CVC3::PLUS, CVC3::plusExpr(), and CVC3::Expr::toString().
c^n = c' (compute the constant power expression)
Implements CVC3::ArithProofRules.
Definition at line 1080 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Rational::isInteger(), CVC3::Expr::isRational(), CVC3::POW, CVC3::pow(), and CVC3::Expr::toString().
flattens the input. accepts a PLUS expr
Implements CVC3::ArithProofRules.
Definition at line 1107 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::PLUS, CVC3::plusExpr(), and CVC3::Expr::toString().
combine like terms. accepts a flattened PLUS expr
Implements CVC3::ArithProofRules.
Definition at line 1134 of file arith_theorem_producer_old.cpp.
References CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::ExprMap< Data >::count(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isPlus(), CVC3::Expr::isRational(), CVC3::plusExpr(), and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 1192 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::begin(), CHECK_SOUND, CVC3::Expr::end(), CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::isPow(), CVC3::Expr::isRational(), and OR.
Implements CVC3::ArithProofRules.
Definition at line 1239 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isPow(), CVC3::Expr::isRational(), and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 1266 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::orExpr(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 1285 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::Expr::orExpr(), CVC3::pow(), and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 1310 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::isEq(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 1330 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isEq(), CVC3::isIntPred(), CVC3::ratRoot(), and CVC3::Expr::toString().
e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=}
e | takes e is (e0@e1) where e0 and e1 are constants |
Implements CVC3::ArithProofRules.
Definition at line 1355 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, EQ, CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::GT, CVC3::isRational(), CVC3::LE, CVC3::LT, and CVC3::Expr::toString().
e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}
Implements CVC3::ArithProofRules.
Definition at line 1394 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, EQ, CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::GT, CVC3::LE, and CVC3::LT.
e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=}
Implements CVC3::ArithProofRules.
Definition at line 1412 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, EQ, CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::GT, CVC3::LE, and CVC3::LT.
|
virtual |
x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind')
Implements CVC3::ArithProofRules.
Definition at line 1430 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, EQ, CVC3::GE, CVC3::GT, CVC3::LE, MiniSat::left(), CVC3::LT, and MiniSat::right().
x = y <==> x * z = y * z, where z is a non-zero constant
Implements CVC3::ArithProofRules.
Definition at line 1449 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), and CVC3::Expr::isRational().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 1462 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::eqExpr(), and CVC3::orExpr().
Multiplying inequation by a non-zero constant.
z>0 ==> e[0] @ e[1] <==> e[0]*z @ e[1]*z
z<0 ==> e[0] @ e[1] <==> e[1]*z @ e[0]*z
for @ in {<,<=,>,>=}:
Implements CVC3::ArithProofRules.
Definition at line 1474 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Expr::getRational(), CVC3::GT, CVC3::Expr::isRational(), CVC3::LE, CVC3::LT, and CVC3::Expr::toString().
x = y ==> x <= y and x >= y
Implements CVC3::ArithProofRules.
Definition at line 1631 of file arith_theorem_producer_old.cpp.
References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::geExpr(), CVC3::Expr::isEq(), CVC3::leExpr(), and CVC3::Expr::toString().
"op1 GE|GT op2" <==> op2 LE|LT op1
Implements CVC3::ArithProofRules.
Definition at line 1653 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::isGE(), CVC3::isGT(), CVC3::LE, CVC3::LT, and CVC3::Expr::toString().
Propagating negation over <,<=,>,>=.
NOT (op1 < op2) <==> (op1 >= op2)
NOT (op1 <= op2) <==> (op1 > op2)
NOT (op1 > op2) <==> (op1 <= op2)
NOT (op1 >= op2) <==> (op1 < op2)
Implements CVC3::ArithProofRules.
Definition at line 1673 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::GE, CVC3::GT, CVC3::isGT(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::Expr::isNot(), CVC3::LE, CVC3::LT, and CVC3::Expr::toString().
|
virtual |
Real shadow: a <(=) t, t <(=) b ==> a <(=) b.
Implements CVC3::ArithProofRules.
Definition at line 1702 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::isLE(), CVC3::isLT(), CVC3::LT, and CVC3::Theorem::toString().
|
virtual |
alpha <= t <= alpha ==> t = alpha
takes two ineqs "|- alpha LE t" and "|- t LE alpha" and returns "|- t = alpha"
Implements CVC3::ArithProofRules.
Definition at line 1737 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isLE(), and CVC3::Theorem::toString().
|
virtual |
Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c)
Implements CVC3::ArithProofRules.
Definition at line 1769 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isIntPred(), CVC3::isLE(), CVC3::isPlus(), CVC3::isRational(), and CVC3::Expr::toString().
|
virtual |
Dark & Gray shadows when a <= b.
takes two integer ineqs (i.e. all vars are ints) "|- beta <= b.x" and "|- a.x <= alpha" and checks if "1 <= a <= b" and returns (D or G) and (!D or !G), where D = Dark_Shadow(ab-1, b.alpha - a.beta), G = Gray_Shadow(a.x, alpha, -(a-1), 0).
Implements CVC3::ArithProofRules.
Definition at line 1833 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::geExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::isIntPred(), CVC3::isLE(), CVC3::minusExpr(), CVC3::multExpr(), CVC3::Theorem::toString(), and CVC3::Expr::toString().
|
virtual |
Dark & Gray shadows when b <= a.
takes two integer ineqs (i.e. all vars are ints) "|- beta <= b.x" and "|- a.x <= alpha" and checks if "1 <= b < a" and returns (D or G) and (!D or !G), where D = Dark_Shadow(ab-1, b.alpha - a.beta), G = Gray_Shadow(b.x, beta, 0, b-1).
Implements CVC3::ArithProofRules.
Definition at line 1926 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::geExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::isIntPred(), CVC3::isLE(), CVC3::minusExpr(), CVC3::multExpr(), CVC3::Theorem::toString(), and CVC3::Expr::toString().
takes a dark shadow and expands it into an inequality.
Implements CVC3::ArithProofRules.
Definition at line 2014 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isDarkShadow(), CVC3::leExpr(), and CVC3::Expr::toString().
GRAY_SHADOW(v, e, c, c) ==> v=e+c.
Implements CVC3::ArithProofRules.
Definition at line 2029 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isGrayShadow(), and CVC3::Expr::toString().
G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2)
Here G1 = G(x,e,c1,c), G2 = G(x,e,c+1,c2), and c = floor((c1+c2)/2).
Implements CVC3::ArithProofRules.
Definition at line 2054 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 3456 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Rational::getInt(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::orExpr(), and CVC3::Expr::toString().
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2.
Implements CVC3::ArithProofRules.
Definition at line 2091 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::leExpr(), and CVC3::Expr::toString().
Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion].
Implements three versions of the rule:
where the conclusion may become FALSE or without the GRAY_SHADOW part, depending on the values of a, c and i.
Implements CVC3::ArithProofRules.
Definition at line 2122 of file arith_theorem_producer_old.cpp.
References CVC3::abs(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::GRAY_SHADOW, CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::isMult(), CVC3::isRational(), CVC3::Expr::isRational(), CVC3::Expr::orExpr(), and CVC3::Expr::toString().
|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a))
In the case the new c1 > c2, return |- FALSE
Implements CVC3::ArithProofRules.
Definition at line 2187 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::Expr::isRational(), and CVC3::Expr::toString().
Rational ArithTheoremProducerOld::constRHSGrayShadow | ( | const Rational & | c, |
const Rational & | b, | ||
const Rational & | a | ||
) |
Implements j(c,b,a)
accepts 3 integers a,b,c and returns (b > 0)? (c+b) mod a : (a - (c+b)) mod a
Definition at line 2227 of file arith_theorem_producer_old.cpp.
References DebugAssert, and CVC3::Rational::isInteger().
|
virtual |
Takes a Theorem(\alpha < \beta) and returns Theorem(\alpha < \beta <==> \alpha <= \beta -1) where \alpha and \beta are integer expressions
Implements CVC3::ArithProofRules.
Definition at line 2245 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isIntPred(), CVC3::isLT(), CVC3::leExpr(), and CVC3::Expr::toString().
|
virtual |
Takes a Theorem(\alpha < \beta) and returns Theorem(\alpha < \beta <==> \alpha <= \beta -1) where \alpha and \beta are integer expressions
Implements CVC3::ArithProofRules.
Definition at line 3416 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isIntPred(), CVC3::isLT(), CVC3::leExpr(), and CVC3::Expr::toString().
|
virtual |
eqn | is an equation 0 = a.x or 0 = c + a.x |
isIntx | is a proof of IS_INTEGER(x) |
It also handles the special case of 0 = a.x <==> x = 0
Implements CVC3::ArithProofRules.
Definition at line 2297 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::Rational::isInteger(), CVC3::isIntPred(), CVC3::isMult(), CVC3::isPlus(), CVC3::isRational(), CVC3::Expr::isRational(), MiniSat::left(), MiniSat::right(), and CVC3::Expr::toString().
IS_INTEGER(x) |= EXISTS (y : INT) y = x where x is not already known to be an integer.
Implements CVC3::ArithProofRules.
Definition at line 2682 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Expr::eqExpr(), EXISTS, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), and CVC3::IS_INTEGER.
|
virtual |
Equality elimination rule for integers:
See the detailed description for explanations.
This rule implements a step in the iterative algorithm for eliminating integer equality. The terms in the rule are defined as follows:
All the variables and coefficients are integer, and a >= 2.
eqn | is the equation
|
See detailed docs for more information.
This rule implements a step in the iterative algorithm for eliminating integer equality. The terms in the rule are defined as follows:
All the variables and coefficients are integer, and a >= 2.
eqn | is the equation ax=t:
|
isIntx | is a Theorem deriving the integrality of the LHS variable: IS_INTEGER(x) |
isIntVars | is a vector of Theorems deriving the integrality of all variables on the RHS |
Implements CVC3::ArithProofRules.
Definition at line 2708 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), EXISTS, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::int2string(), CVC3::isDivide(), CVC3::isInt(), CVC3::Rational::isInteger(), CVC3::isIntPred(), CVC3::isPlus(), CVC3::isRational(), CVC3::Theorem::isRewrite(), CVC3::Expr::setType(), CVC3::Rational::toString(), CVC3::Theorem::toString(), CVC3::Expr::toString(), and TRACE.
return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant
e | is a predicate IS_INTEGER(c) where c is a rational constant |
Implements CVC3::ArithProofRules.
Definition at line 2800 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::isInt(), CVC3::Rational::isInteger(), CVC3::isIntPred(), CVC3::isRational(), and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 2816 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::PLUS, and RATIONAL_EXPR.
Implements CVC3::ArithProofRules.
Definition at line 2845 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::PLUS, and RATIONAL_EXPR.
Implements CVC3::ArithProofRules.
Definition at line 2874 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::PLUS, and RATIONAL_EXPR.
Implements CVC3::ArithProofRules.
Definition at line 2903 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::PLUS, and RATIONAL_EXPR.
x /= y ==> (x < y) OR (x > y)
Used in concrete model generation
Implements CVC3::ArithProofRules.
Definition at line 2931 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::gtExpr(), CVC3::Expr::isEq(), CVC3::Expr::isNot(), CVC3::ltExpr(), CVC3::orExpr(), and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 2950 of file arith_theorem_producer_old.cpp.
Implements CVC3::ArithProofRules.
Definition at line 2955 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::isMult(), CVC3::Expr::isRational(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 2976 of file arith_theorem_producer_old.cpp.
References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Expr::getRational(), CVC3::isGE(), CVC3::isGT(), CVC3::isLE(), CVC3::isLT(), CVC3::isRational(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3016 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::GT, CVC3::isGE(), CVC3::isGT(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::LT, CVC3::plusExpr(), and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 3775 of file arith_theorem_producer_old.cpp.
References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::LE, CVC3::LT, CVC3::plusExpr(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3065 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Expr::impExpr(), CVC3::isIneq(), CVC3::isPlus(), CVC3::isRational(), CVC3::LE, CVC3::LT, CVC3::plusExpr(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3131 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Expr::impExpr(), CVC3::isIneq(), CVC3::isMult(), CVC3::isPlus(), CVC3::isRational(), CVC3::LT, CVC3::Expr::negate(), CVC3::plusExpr(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3230 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::geExpr(), CVC3::Expr::impExpr(), CVC3::IS_INTEGER, CVC3::Rational::isInteger(), CVC3::leExpr(), CVC3::orExpr(), and CVC3::Rational::toString().
Implements CVC3::ArithProofRules.
Definition at line 3217 of file arith_theorem_producer_old.cpp.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3253 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::GE, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::Expr::getString(), CVC3::GT, CVC3::isIneq(), CVC3::Rational::isInteger(), CVC3::isPlus(), CVC3::isRational(), CVC3::Expr::isRational(), CVC3::LE, CVC3::LT, CVC3::plusExpr(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 1508 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::GE, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::GT, CVC3::isIntPred(), CVC3::isMult(), CVC3::isPlus(), CVC3::Expr::isRational(), CVC3::Expr::isVar(), CVC3::LE, and CVC3::LT.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3332 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, EQ, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::Expr::getString(), CVC3::isPlus(), CVC3::isRational(), CVC3::Expr::isRational(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3369 of file arith_theorem_producer_old.cpp.
References CVC3::Assumptions::add().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3388 of file arith_theorem_producer_old.cpp.
References CVC3::Assumptions::add(), CVC3::andExpr(), CVC3::Expr::eqExpr(), and RAW_LIST.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3494 of file arith_theorem_producer_old.cpp.
References CVC3::Assumptions::add(), and RAW_LIST.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3516 of file arith_theorem_producer_old.cpp.
References CVC3::Assumptions::add(), CVC3::Expr::notExpr(), and RAW_LIST.
Implements CVC3::ArithProofRules.
Definition at line 3539 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::leExpr(), and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 3567 of file arith_theorem_producer_old.cpp.
References CVC3::Expr::arity(), CVC3::Rational::getInt(), CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isPow(), CVC3::isRational(), CVC3::multExpr(), and CVC3::plusExpr().
Implements CVC3::ArithProofRules.
Definition at line 3697 of file arith_theorem_producer_old.cpp.
References CVC3::Assumptions::add(), CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isPlus(), CVC3::isPow(), CVC3::LE, CVC3::ltExpr(), CVC3::Expr::orExpr(), CVC3::POW, CVC3::Expr::toString(), and XOR.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3742 of file arith_theorem_producer_old.cpp.
References CVC3::Assumptions::add().
Implements CVC3::ArithProofRules.
Definition at line 3823 of file arith_theorem_producer_old.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::isPow(), CVC3::isRational(), and CVC3::Expr::toString().
Reimplemented from CVC3::ArithProofRules.
Definition at line 3867 of file arith_theorem_producer_old.cpp.
References CVC3::ExprHashMap< Data >::clear(), DebugAssert, EQ, CVC3::GE, CVC3::Expr::getKind(), CVC3::GT, CVC3::Expr::isNull(), CVC3::Expr::isPropAtom(), CVC3::LE, and CVC3::LT.
|
private |
Definition at line 32 of file arith_theorem_producer_old.h.