CVC3
2.4.1
|
#include <arith_proof_rules.h>
Public Member Functions | |
virtual | ~ArithProofRules () |
virtual Theorem | varToMult (const Expr &e)=0 |
==> e = 1 * e More... | |
virtual Theorem | uMinusToMult (const Expr &e)=0 |
==> -(e) = (-1) * e More... | |
virtual Theorem | minusToPlus (const Expr &x, const Expr &y)=0 |
==> x - y = x + (-1) * y More... | |
virtual Theorem | canonUMinusToDivide (const Expr &e)=0 |
-(e) ==> e / (-1); takes 'e' More... | |
virtual Theorem | moveSumConstantRight (const Expr &e)=0 |
virtual Theorem | canonDivideConst (const Expr &c, const Expr &d)=0 |
(c) / d ==> (c/d), takes c and d More... | |
virtual Theorem | canonDivideMult (const Expr &cx, const Expr &d)=0 |
(c * x) / d ==> (c/d) * x, takes (c*x) and d More... | |
virtual Theorem | canonDividePlus (const Expr &e, const Expr &d)=0 |
(+ c ...)/d ==> push division to all the coefficients. More... | |
virtual Theorem | canonDivideVar (const Expr &e, const Expr &d)=0 |
x / d ==> (1/d) * x, takes x and d More... | |
virtual Theorem | canonMultMtermMterm (const Expr &e)=0 |
virtual Theorem | canonPlus (const Expr &e)=0 |
Canonize (PLUS t1 ... tn) More... | |
virtual Theorem | canonMult (const Expr &e)=0 |
Canonize (MULT t1 ... tn) More... | |
virtual Theorem | canonInvert (const Expr &e)=0 |
==> 1/e = e' where e' is canonical; takes e. More... | |
virtual Theorem | canonDivide (const Expr &e)=0 |
Canonize t1/t2. More... | |
virtual Theorem | canonMultTermConst (const Expr &c, const Expr &t)=0 |
t*c ==> c*t, takes constant c and term t More... | |
virtual Theorem | canonMultTerm1Term2 (const Expr &t1, const Expr &t2)=0 |
t1*t2 ==> Error, takes t1 and t2 where both are non-constants More... | |
virtual Theorem | canonMultZero (const Expr &e)=0 |
0*t ==> 0, takes 0*t More... | |
virtual Theorem | canonMultOne (const Expr &e)=0 |
1*t ==> t, takes 1*t More... | |
virtual Theorem | canonMultConstConst (const Expr &c1, const Expr &c2)=0 |
c1*c2 ==> c', takes constant c1*c2 More... | |
virtual Theorem | canonMultConstTerm (const Expr &c1, const Expr &c2, const Expr &t)=0 |
c1*(c2*t) ==> c'*t, takes c1 and c2 and t More... | |
virtual Theorem | canonMultConstSum (const Expr &c1, const Expr &sum)=0 |
c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum More... | |
virtual Theorem | canonPowConst (const Expr &pow)=0 |
c^n = c' (compute the constant power expression) More... | |
virtual Theorem | canonFlattenSum (const Expr &e)=0 |
flattens the input. accepts a PLUS expr More... | |
virtual Theorem | canonComboLikeTerms (const Expr &e)=0 |
combine like terms. accepts a flattened PLUS expr More... | |
virtual Theorem | multEqZero (const Expr &expr)=0 |
virtual Theorem | powEqZero (const Expr &expr)=0 |
virtual Theorem | elimPower (const Expr &expr)=0 |
virtual Theorem | elimPowerConst (const Expr &expr, const Rational &root)=0 |
virtual Theorem | evenPowerEqNegConst (const Expr &expr)=0 |
virtual Theorem | intEqIrrational (const Expr &expr, const Theorem &isInt)=0 |
virtual Theorem | constPredicate (const Expr &e)=0 |
e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=} More... | |
virtual Theorem | rightMinusLeft (const Expr &e)=0 |
e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=} More... | |
virtual Theorem | leftMinusRight (const Expr &e)=0 |
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)=0 |
x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind') More... | |
virtual Theorem | multEqn (const Expr &x, const Expr &y, const Expr &z)=0 |
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)=0 |
virtual Theorem | multIneqn (const Expr &e, const Expr &z)=0 |
Multiplying inequation by a non-zero constant. More... | |
virtual Theorem | eqToIneq (const Expr &e)=0 |
x = y ==> x <= y and x >= y More... | |
virtual Theorem | flipInequality (const Expr &e)=0 |
"op1 GE|GT op2" <==> op2 LE|LT op1 More... | |
virtual Theorem | negatedInequality (const Expr &e)=0 |
Propagating negation over <,<=,>,>=. More... | |
virtual Theorem | realShadow (const Theorem &alphaLTt, const Theorem &tLTbeta)=0 |
Real shadow: a <(=) t, t <(=) b ==> a <(=) b. More... | |
virtual Theorem | realShadowEq (const Theorem &alphaLEt, const Theorem &tLEalpha)=0 |
Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha. More... | |
virtual Theorem | finiteInterval (const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt)=0 |
Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c) More... | |
virtual Theorem | darkGrayShadow2ab (const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0 |
Dark & Gray shadows when a <= b. More... | |
virtual Theorem | darkGrayShadow2ba (const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0 |
Dark & Gray shadows when b <= a. More... | |
virtual Theorem | expandDarkShadow (const Theorem &darkShadow)=0 |
DARK_SHADOW(t1, t2) ==> t1 <= t2. More... | |
virtual Theorem | expandGrayShadow0 (const Theorem &g)=0 |
GRAY_SHADOW(v, e, c, c) ==> v=e+c. More... | |
virtual Theorem | splitGrayShadow (const Theorem &g)=0 |
G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2) More... | |
virtual Theorem | splitGrayShadowSmall (const Theorem &g)=0 |
virtual Theorem | expandGrayShadow (const Theorem &g)=0 |
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2. More... | |
virtual Theorem | expandGrayShadowConst (const Theorem &g)=0 |
Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion]. More... | |
virtual Theorem | grayShadowConst (const Theorem &g)=0 |
|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a)) More... | |
virtual Theorem | lessThanToLE (const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)=0 |
a,b: INT; a < b ==> a <= b-1 [or a+1 <= b] More... | |
virtual Theorem | lessThanToLERewrite (const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)=0 |
virtual Theorem | intVarEqnConst (const Expr &eqn, const Theorem &isIntx)=0 |
virtual Theorem | IsIntegerElim (const Theorem &isIntx)=0 |
virtual Theorem | eqElimIntRule (const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars)=0 |
Equality elimination rule for integers:
See the detailed description for explanations. More... | |
virtual Theorem | isIntConst (const Expr &e)=0 |
return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant More... | |
virtual Theorem | equalLeaves1 (const Theorem &thm)=0 |
virtual Theorem | equalLeaves2 (const Theorem &thm)=0 |
virtual Theorem | equalLeaves3 (const Theorem &thm)=0 |
virtual Theorem | equalLeaves4 (const Theorem &thm)=0 |
virtual Theorem | diseqToIneq (const Theorem &diseq)=0 |
x /= y ==> (x < y) OR (x > y) More... | |
virtual Theorem | dummyTheorem (const Expr &e)=0 |
virtual Theorem | oneElimination (const Expr &x)=0 |
virtual Theorem | clashingBounds (const Theorem &lowerBound, const Theorem &upperBound)=0 |
virtual Theorem | addInequalities (const Theorem &thm1, const Theorem &thm2)=0 |
virtual Theorem | addInequalities (const std::vector< Theorem > &thms)=0 |
virtual Theorem | implyWeakerInequality (const Expr &expr1, const Expr &expr2)=0 |
virtual Theorem | implyNegatedInequality (const Expr &expr1, const Expr &expr2)=0 |
virtual Theorem | integerSplit (const Expr &intVar, const Rational &intPoint)=0 |
virtual Theorem | trustedRewrite (const Expr &expr1, const Expr &expr2)=0 |
virtual Theorem | rafineStrictInteger (const Theorem &isIntConstrThm, const Expr &constr)=0 |
virtual Theorem | simpleIneqInt (const Expr &ineq, const Theorem &isIntRHS)=0 |
virtual Theorem | intEqualityRationalConstant (const Theorem &isIntConstrThm, const Expr &constr)=0 |
virtual Theorem | cycleConflict (const std::vector< Theorem > &inequalitites)=0 |
virtual Theorem | implyEqualities (const std::vector< Theorem > &inequalities)=0 |
virtual Theorem | implyWeakerInequalityDiffLogic (const std::vector< Theorem > &antecedentThms, const Expr &implied)=0 |
virtual Theorem | implyNegatedInequalityDiffLogic (const std::vector< Theorem > &antecedentThms, const Expr &implied)=0 |
virtual Theorem | expandGrayShadowRewrite (const Expr &theShadow)=0 |
virtual Theorem | compactNonLinearTerm (const Expr &nonLinear)=0 |
virtual Theorem | nonLinearIneqSignSplit (const Theorem &ineqThm)=0 |
virtual Theorem | implyDiffLogicBothBounds (const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2)=0 |
virtual Theorem | powerOfOne (const Expr &e)=0 |
virtual Theorem | rewriteLeavesConst (const Expr &e) |
Definition at line 33 of file arith_proof_rules.h.
|
inlinevirtual |
Definition at line 36 of file arith_proof_rules.h.
==> e = 1 * e
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
==> -(e) = (-1) * e
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
==> x - y = x + (-1) * y
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
-(e) ==> e / (-1); takes 'e'
Canon Rule for unary minus: it just converts it to division by -1, the result is not yet canonical:
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
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 |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure virtual |
(c) / d ==> (c/d), takes c and d
Canon Rules for division by constant 'd'
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure virtual |
(c * x) / d ==> (c/d) * x, takes (c*x) and d
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure virtual |
(+ 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
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure virtual |
x / d ==> (1/d) * x, takes x and d
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Canonize (PLUS t1 ... tn)
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::TheoryArithNew::getUpperBoundExplanation(), and CVC3::TheoryArithNew::rewrite().
Canonize (MULT t1 ... tn)
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
==> 1/e = e' where e' is canonical; takes e.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Canonize t1/t2.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure virtual |
t*c ==> c*t, takes constant c and term t
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithNew::getLowerBoundExplanation(), and CVC3::TheoryArithNew::getUpperBoundExplanation().
|
pure virtual |
t1*t2 ==> Error, takes t1 and t2 where both are non-constants
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
0*t ==> 0, takes 0*t
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
1*t ==> t, takes 1*t
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure virtual |
c1*c2 ==> c', takes constant c1*c2
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithNew::getLowerBoundExplanation(), and CVC3::TheoryArithNew::getUpperBoundExplanation().
|
pure virtual |
c1*(c2*t) ==> c'*t, takes c1 and c2 and t
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure virtual |
c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
c^n = c' (compute the constant power expression)
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
flattens the input. accepts a PLUS expr
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
combine like terms. accepts a flattened PLUS expr
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithOld::rewrite().
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithOld::rewrite().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithOld::rewrite().
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithOld::rewrite().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithOld::rewrite().
e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=}
e | takes e is (e0@e1) where e0 and e1 are constants |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), and CVC3::TheoryArithOld::rewrite().
e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), and CVC3::TheoryArithOld::rewrite().
e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=}
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure virtual |
x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind')
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithNew::pivotRule(), and CVC3::TheoryArithNew::rewrite().
|
pure virtual |
x = y <==> x * z = y * z, where z is a non-zero constant
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalize(), and CVC3::TheoryArithNew::pivotRule().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithOld::rewrite().
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 {<,<=,>,>=}:
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithNew::processFiniteInterval(), and CVC3::TheoryArith3::processFiniteInterval().
x = y ==> x <= y and x >= y
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithNew::rewrite(), and CVC3::TheoryArithOld::rewrite().
"op1 GE|GT op2" <==> op2 LE|LT op1
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArith3::rewrite(), and CVC3::TheoryArithOld::rewrite().
Propagating negation over <,<=,>,>=.
NOT (op1 < op2) <==> (op1 >= op2)
NOT (op1 <= op2) <==> (op1 > op2)
NOT (op1 > op2) <==> (op1 <= op2)
NOT (op1 >= op2) <==> (op1 < op2)
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), and CVC3::TheoryArithOld::rewrite().
|
pure virtual |
Real shadow: a <(=) t, t <(=) b ==> a <(=) b.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure virtual |
Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure virtual |
Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c)
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithNew::processFiniteInterval(), and CVC3::TheoryArith3::processFiniteInterval().
|
pure 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).
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure 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).
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
DARK_SHADOW(t1, t2) ==> t1 <= t2.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArith3::assertFact(), and CVC3::TheoryArithOld::assertFact().
GRAY_SHADOW(v, e, c, c) ==> v=e+c.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArith3::assertFact(), and CVC3::TheoryArithOld::assertFact().
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).
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArith3::assertFact(), and CVC3::TheoryArithOld::assertFact().
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithOld::assertFact().
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArith3::assertFact(), and CVC3::TheoryArithOld::assertFact().
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.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|- 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
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArith3::assertFact(), and CVC3::TheoryArithOld::assertFact().
|
pure virtual |
a,b: INT; a < b ==> a <= b-1 [or a+1 <= b]
Takes a Theorem(\alpha < \beta) and returns Theorem(\alpha < \beta <==> \alpha <= \beta -1) or Theorem(\alpha < \beta <==> \alpha + 1 <= \beta), depending on which side must be changed (changeRight flag)
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.
Referenced by CVC3::TheoryArithOld::rewrite().
|
pure virtual |
eqn | is an equation 0 = a.x or 0 = c + a.x, where x is integer |
isIntx | is a proof of IS_INTEGER(x) |
It also handles the special case of 0 = a.x <==> x = 0
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
IS_INTEGER(x) <=> EXISTS (y : INT) y = x where x is not already known to be an integer.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArithOld::assertFact().
|
pure 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 |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
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 |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
x /= y ==> (x < y) OR (x > y)
Used in concrete model generation
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArith3::checkSat(), and CVC3::TheoryArithOld::checkSat().
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArithNew::rewrite().
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArithNew::assertFact(), and CVC3::TheoryArithNew::pivotRule().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArithNew::getLowerBoundExplanation(), and CVC3::TheoryArithNew::getUpperBoundExplanation().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArithNew::propagateTheory(), and CVC3::TheoryArithOld::registerAtom().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArithNew::propagateTheory(), and CVC3::TheoryArithOld::registerAtom().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArithNew::checkSatInteger().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArithOld::rafineInequalityToInteger(), and CVC3::TheoryArithNew::rafineIntegerConstraints().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArithOld::checkIntegerEquality().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArithOld::tryPropagate().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Referenced by CVC3::TheoryArithOld::tryPropagate().
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
|
pure virtual |
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducerOld, and CVC3::ArithTheoremProducer3.
Reimplemented in CVC3::ArithTheoremProducerOld.
Definition at line 3243 of file arith_theorem_producer.cpp.
References DebugAssert.
Referenced by CVC3::TheoryArithOld::rewrite().