CVC3
|
#include <arith_theorem_producer3.h>
Inherits CVC3::ArithProofRules, and CVC3::TheoremProducer.
Public Member Functions | |
ArithTheoremProducer3 (TheoremManager *tm, TheoryArith3 *theoryArith) | |
Constructor. | |
Expr | rat (Rational r) |
Create Expr from Rational (for convenience) | |
Type | realType () |
Type | intType () |
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. | |
virtual Theorem | varToMult (const Expr &e) |
==> e = 1 * e | |
virtual Theorem | uMinusToMult (const Expr &e) |
==> -(e) = (-1) * e | |
virtual Theorem | minusToPlus (const Expr &x, const Expr &y) |
==> x - y = x + (-1) * y | |
virtual Theorem | canonUMinusToDivide (const Expr &e) |
-(e) ==> e / (-1); takes 'e' | |
virtual Theorem | canonDivideConst (const Expr &c, const Expr &d) |
(c) / d ==> (c/d), takes c and d | |
virtual Theorem | canonDivideMult (const Expr &cx, const Expr &d) |
(c * x) / d ==> (c/d) * x, takes (c*x) and d | |
virtual Theorem | canonDividePlus (const Expr &e, const Expr &d) |
(+ c ...)/d ==> push division to all the coefficients. | |
virtual Theorem | canonDivideVar (const Expr &e1, const Expr &e2) |
x / d ==> (1/d) * x, takes x and d | |
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) | |
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. | |
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 | |
virtual Theorem | canonMultTerm1Term2 (const Expr &t1, const Expr &t2) |
t1*t2 ==> Error, takes t1 and t2 where both are non-constants | |
virtual Theorem | canonMultZero (const Expr &e) |
0*t ==> 0, takes 0*t | |
virtual Theorem | canonMultOne (const Expr &e) |
1*t ==> t, takes 1*t | |
virtual Theorem | canonMultConstConst (const Expr &c1, const Expr &c2) |
c1*c2 ==> c', takes constant c1*c2 | |
virtual Theorem | canonMultConstTerm (const Expr &c1, const Expr &c2, const Expr &t) |
c1*(c2*t) ==> c'*t, takes c1 and c2 and t | |
virtual Theorem | canonMultConstSum (const Expr &c1, const Expr &sum) |
c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum | |
virtual Theorem | canonPowConst (const Expr &pow) |
c^n = c' (compute the constant power expression) | |
virtual Theorem | canonFlattenSum (const Expr &e) |
flattens the input. accepts a PLUS expr | |
virtual Theorem | canonComboLikeTerms (const Expr &e) |
combine like terms. accepts a flattened PLUS expr | |
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 {=,<,<=,>,>=} | |
virtual Theorem | rightMinusLeft (const Expr &e) |
e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=} | |
virtual Theorem | leftMinusRight (const Expr &e) |
e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=} | |
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') | |
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 | |
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. | |
virtual Theorem | eqToIneq (const Expr &e) |
x = y ==> x <= y and x >= y | |
virtual Theorem | flipInequality (const Expr &e) |
"op1 GE|GT op2" <==> op2 LE|LT op1 | |
Theorem | negatedInequality (const Expr &e) |
Propagating negation over <,<=,>,>=. | |
Theorem | realShadow (const Theorem &alphaLTt, const Theorem &tLTbeta) |
Real shadow: a <(=) t, t <(=) b ==> a <(=) b. | |
Theorem | realShadowEq (const Theorem &alphaLEt, const Theorem &tLEalpha) |
alpha <= t <= alpha ==> t = alpha | |
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) | |
Theorem | darkGrayShadow2ab (const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx) |
Dark & Gray shadows when a <= b. | |
Theorem | darkGrayShadow2ba (const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx) |
Dark & Gray shadows when b <= a. | |
Theorem | expandDarkShadow (const Theorem &darkShadow) |
Theorem | expandGrayShadow0 (const Theorem &grayShadow) |
GRAY_SHADOW(v, e, c, c) ==> v=e+c. | |
Theorem | splitGrayShadow (const Theorem &grayShadow) |
G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2) | |
Theorem | splitGrayShadowSmall (const Theorem &grayShadow) |
Theorem | expandGrayShadow (const Theorem &grayShadow) |
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2. | |
Theorem | expandGrayShadowConst (const Theorem &grayShadow) |
Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion]. | |
Theorem | grayShadowConst (const Theorem &g) |
|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a)) | |
Rational | constRHSGrayShadow (const Rational &c, const Rational &b, const Rational &a) |
Implements j(c,b,a) | |
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:
| |
Theorem | isIntConst (const Expr &e) |
return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant | |
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) | |
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) |
![]() | |
virtual | ~ArithProofRules () |
virtual Theorem | rewriteLeavesConst (const Expr &e) |
![]() | |
TheoremProducer (TheoremManager *tm) | |
virtual | ~TheoremProducer () |
bool | withProof () |
Testing whether to generate proofs. | |
bool | withAssumptions () |
Testing whether to generate assumptions. | |
Proof | newLabel (const Expr &e) |
Create a new proof label (bound variable) for an assumption (formula) | |
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) | |
Proof | newPf (const Proof &label, const Proof &pf) |
Creating LAMBDA-abstraction (LAMBDA label proof). | |
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) | |
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) | |
Expr | create_t (const Expr &eqn) |
Create the term 't'. See eqElimIntRule(). | |
Expr | create_t2 (const Expr &lhs, const Expr &rhs, const Expr &t) |
Create the term 't2'. See eqElimIntRule(). | |
Expr | create_t3 (const Expr &lhs, const Expr &rhs, const Expr &t) |
Create the term 't3'. See eqElimIntRule(). | |
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. | |
Expr | monomialModM (const Expr &e, const Rational &m, const Rational &divisor) |
Compute the special modulus: i - m*floor(i/m+1/2) | |
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) | |
Expr | monomialMulF (const Expr &e, const Rational &m, const Rational &divisor) |
Compute the special modulus: i - m*floor(i/m+1/2) | |
Rational | f (const Rational &i, const Rational &m) |
Compute floor(i/m+1/2) + mod(i,m) | |
Expr | substitute (const Expr &term, ExprMap< Expr > &eMap) |
Compute the special modulus: i - m*floor(i/m+1/2) | |
Private Attributes | |
TheoryArith3 * | 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() | |
Theorem | newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) |
Create a rewrite theorem: lhs = rhs. | |
Theorem | newReflTheorem (const Expr &e) |
Create a reflexivity theorem. | |
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 32 of file arith_theorem_producer3.h.
|
inline |
Constructor.
Definition at line 66 of file arith_theorem_producer3.h.
Compute the special modulus: i - m*floor(i/m+1/2)
Definition at line 2227 of file arith_theorem_producer3.cpp.
References DebugAssert, CVC3::Rational::toString(), and TRACE.
Create the term 't'. See eqElimIntRule().
Definition at line 2167 of file arith_theorem_producer3.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 2186 of file arith_theorem_producer3.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 2206 of file arith_theorem_producer3.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 2243 of file arith_theorem_producer3.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 2263 of file arith_theorem_producer3.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 2291 of file arith_theorem_producer3.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 2311 of file arith_theorem_producer3.cpp.
References DebugAssert, CVC3::isMult(), CVC3::multExpr(), and CVC3::Rational::toString().
Compute floor(i/m+1/2) + mod(i,m)
Definition at line 2236 of file arith_theorem_producer3.cpp.
References DebugAssert, and CVC3::Rational::toString().
Compute the special modulus: i - m*floor(i/m+1/2)
Definition at line 2328 of file arith_theorem_producer3.cpp.
References CVC3::Expr::begin(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::ExprMap< Data >::find(), CVC3::isMult(), CVC3::isPlus(), and CVC3::plusExpr().
Create Expr from Rational (for convenience)
Definition at line 70 of file arith_theorem_producer3.h.
References CVC3::TheoremProducer::d_em, and CVC3::ExprManager::newRatExpr().
|
inline |
Definition at line 71 of file arith_theorem_producer3.h.
References d_theoryArith, and CVC3::TheoryArith::realType().
|
inline |
Definition at line 72 of file arith_theorem_producer3.h.
References d_theoryArith, and CVC3::TheoryArith::intType().
Construct the dark shadow expression representing lhs <= rhs.
Definition at line 74 of file arith_theorem_producer3.h.
References d_theoryArith, and 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_producer3.h.
References d_theoryArith, and CVC3::TheoryArith::grayShadow().
==> e = 1 * e
Implements CVC3::ArithProofRules.
Definition at line 56 of file arith_theorem_producer3.cpp.
==> -(e) = (-1) * e
Implements CVC3::ArithProofRules.
Definition at line 64 of file arith_theorem_producer3.cpp.
==> x - y = x + (-1) * y
Implements CVC3::ArithProofRules.
Definition at line 72 of file arith_theorem_producer3.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 82 of file arith_theorem_producer3.cpp.
(c) / d ==> (c/d), takes c and d
Canon Rules for division by constant 'd'
Implements CVC3::ArithProofRules.
Definition at line 91 of file arith_theorem_producer3.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 110 of file arith_theorem_producer3.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 138 of file arith_theorem_producer3.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 161 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::getRational(), CVC3::isRational(), and CVC3::Expr::toString().
Definition at line 2354 of file arith_theorem_producer3.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 196 of file arith_theorem_producer3.cpp.
References DebugAssert, and CVC3::multExpr().
Definition at line 209 of file arith_theorem_producer3.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 231 of file arith_theorem_producer3.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 250 of file arith_theorem_producer3.cpp.
References DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::POW, and CVC3::powExpr().
Definition at line 290 of file arith_theorem_producer3.cpp.
References DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::POW, and CVC3::powExpr().
Definition at line 329 of file arith_theorem_producer3.cpp.
References CVC3::powExpr().
Definition at line 357 of file arith_theorem_producer3.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 429 of file arith_theorem_producer3.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 510 of file arith_theorem_producer3.cpp.
References CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::PLUS.
Definition at line 529 of file arith_theorem_producer3.cpp.
References CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::PLUS.
Implements CVC3::ArithProofRules.
Definition at line 553 of file arith_theorem_producer3.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 718 of file arith_theorem_producer3.cpp.
References CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::PLUS.
Definition at line 769 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::isRational(), and CVC3::Expr::toString().
Definition at line 785 of file arith_theorem_producer3.cpp.
References CVC3::powExpr().
Definition at line 797 of file arith_theorem_producer3.cpp.
References DebugAssert, CVC3::Expr::getKind(), CVC3::POW, CVC3::powExpr(), and CVC3::Expr::toString().
Definition at line 816 of file arith_theorem_producer3.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 839 of file arith_theorem_producer3.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 861 of file arith_theorem_producer3.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 907 of file arith_theorem_producer3.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 751 of file arith_theorem_producer3.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::MULT.
t*c ==> c*t, takes constant c and term t
Implements CVC3::ArithProofRules.
Definition at line 925 of file arith_theorem_producer3.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 939 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, and CVC3::Expr::toString().
0*t ==> 0, takes 0*t
Implements CVC3::ArithProofRules.
Definition at line 952 of file arith_theorem_producer3.cpp.
1*t ==> t, takes 1*t
Implements CVC3::ArithProofRules.
Definition at line 960 of file arith_theorem_producer3.cpp.
c1*c2 ==> c', takes constant c1*c2
Implements CVC3::ArithProofRules.
Definition at line 969 of file arith_theorem_producer3.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 987 of file arith_theorem_producer3.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 1007 of file arith_theorem_producer3.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 1030 of file arith_theorem_producer3.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 1057 of file arith_theorem_producer3.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 1084 of file arith_theorem_producer3.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 1142 of file arith_theorem_producer3.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::end(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isMult(), CVC3::Expr::isRational(), OR, and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 1165 of file arith_theorem_producer3.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 1192 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isPow(), CVC3::Expr::orExpr(), and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 1217 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isPow(), CVC3::Expr::isRational(), CVC3::Expr::orExpr(), CVC3::pow(), and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 1241 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isPow(), CVC3::Expr::isRational(), and CVC3::Expr::toString().
Implements CVC3::ArithProofRules.
Definition at line 1260 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isIntPred(), CVC3::isPow(), CVC3::Expr::isRational(), 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 1287 of file arith_theorem_producer3.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 1326 of file arith_theorem_producer3.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 1344 of file arith_theorem_producer3.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 1362 of file arith_theorem_producer3.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 1381 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), and CVC3::Expr::isRational().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 1394 of file arith_theorem_producer3.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 1406 of file arith_theorem_producer3.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 1433 of file arith_theorem_producer3.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 1455 of file arith_theorem_producer3.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 1475 of file arith_theorem_producer3.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 1504 of file arith_theorem_producer3.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 1539 of file arith_theorem_producer3.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 1571 of file arith_theorem_producer3.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 1635 of file arith_theorem_producer3.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::isIntPred(), CVC3::isLE(), CVC3::isMult(), 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 1726 of file arith_theorem_producer3.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::isIntPred(), CVC3::isLE(), CVC3::isMult(), 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 1811 of file arith_theorem_producer3.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 1826 of file arith_theorem_producer3.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 1852 of file arith_theorem_producer3.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 3024 of file arith_theorem_producer3.cpp.
References DebugAssert.
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2.
Implements CVC3::ArithProofRules.
Definition at line 1889 of file arith_theorem_producer3.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 1920 of file arith_theorem_producer3.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 1985 of file arith_theorem_producer3.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 ArithTheoremProducer3::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 2025 of file arith_theorem_producer3.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 2043 of file arith_theorem_producer3.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 3103 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isIntPred(), CVC3::isLT(), CVC3::leExpr(), and CVC3::Expr::toString().
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 2095 of file arith_theorem_producer3.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 2480 of file arith_theorem_producer3.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. \param 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. \param eqn is the equation ax=t:
\param isIntx is a Theorem deriving the integrality of the LHS variable: IS_INTEGER(x) \param isIntVars is a vector of Theorems deriving the integrality of all variables on the RHS
Implements CVC3::ArithProofRules.
Definition at line 2506 of file arith_theorem_producer3.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 2598 of file arith_theorem_producer3.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 2614 of file arith_theorem_producer3.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 2643 of file arith_theorem_producer3.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 2672 of file arith_theorem_producer3.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 2701 of file arith_theorem_producer3.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 2729 of file arith_theorem_producer3.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 2748 of file arith_theorem_producer3.cpp.
Implements CVC3::ArithProofRules.
Definition at line 2753 of file arith_theorem_producer3.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 2774 of file arith_theorem_producer3.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 2814 of file arith_theorem_producer3.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 3061 of file arith_theorem_producer3.cpp.
References DebugAssert.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 2859 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::Expr::impExpr(), CVC3::isGE(), CVC3::isGT(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::isRational(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 2906 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::Expr::impExpr(), CVC3::isGE(), CVC3::isGT(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::isRational(), CVC3::Expr::negate(), and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 2951 of file arith_theorem_producer3.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 2938 of file arith_theorem_producer3.cpp.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 2970 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::GE, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::GT, CVC3::isIneq(), CVC3::Rational::isInteger(), CVC3::isRational(), CVC3::LE, CVC3::LT, and CVC3::Expr::toString().
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3073 of file arith_theorem_producer3.cpp.
References DebugAssert.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3083 of file arith_theorem_producer3.cpp.
References DebugAssert.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3088 of file arith_theorem_producer3.cpp.
References DebugAssert.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3093 of file arith_theorem_producer3.cpp.
References DebugAssert.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3029 of file arith_theorem_producer3.cpp.
References DebugAssert.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3034 of file arith_theorem_producer3.cpp.
References DebugAssert.
Implements CVC3::ArithProofRules.
Definition at line 3039 of file arith_theorem_producer3.cpp.
References DebugAssert.
Implements CVC3::ArithProofRules.
Definition at line 3044 of file arith_theorem_producer3.cpp.
References DebugAssert.
Implements CVC3::ArithProofRules.
Definition at line 3049 of file arith_theorem_producer3.cpp.
References DebugAssert.
|
virtual |
Implements CVC3::ArithProofRules.
Definition at line 3054 of file arith_theorem_producer3.cpp.
References DebugAssert.
Implements CVC3::ArithProofRules.
Definition at line 3066 of file arith_theorem_producer3.cpp.
References DebugAssert.
|
private |
Definition at line 33 of file arith_theorem_producer3.h.
Referenced by darkShadow(), grayShadow(), intType(), and realType().