22 #ifndef _cvc3__arith_proof_rules_h_
23 #define _cvc3__arith_proof_rules_h_
159 const Expr& y,
const Expr& z,
int kind) = 0;
283 const Theorem& isIntRHS,
bool changeRight) = 0;
343 virtual Theorem cANDaIffcANDb(const Theorem& thm,
344 const Expr& solvedEq) = 0;
345 virtual Theorem substSolvedFormRule(const Expr& e1,
346 ExprMap<Expr>& eMap) = 0;
347 virtual Theorem aANDcIffbANDc(const Theorem& thm, const Expr& newEq) = 0;
396 const std::vector<Theorem>& isIntVars) = 0;
453 std::vector<Theorem>& x_le_c2,
Rational c2) = 0;
virtual Theorem eqToIneq(const Expr &e)=0
x = y ==> x <= y and x >= y
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
virtual Theorem implyNegatedInequality(const Expr &expr1, const Expr &expr2)=0
virtual Theorem expandGrayShadowConst(const Theorem &g)=0
Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion].
virtual Theorem IsIntegerElim(const Theorem &isIntx)=0
virtual Theorem elimPower(const Expr &expr)=0
virtual Theorem uMinusToMult(const Expr &e)=0
==> -(e) = (-1) * e
virtual Theorem implyEqualities(const std::vector< Theorem > &inequalities)=0
virtual Theorem equalLeaves1(const Theorem &thm)=0
Data structure of expressions in CVC3.
virtual Theorem canonDivideConst(const Expr &c, const Expr &d)=0
(c) / d ==> (c/d), takes c and d
virtual Theorem splitGrayShadowSmall(const Theorem &g)=0
virtual Theorem canonMultOne(const Expr &e)=0
1*t ==> t, takes 1*t
virtual Theorem canonMultConstSum(const Expr &c1, const Expr &sum)=0
c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
virtual Theorem constPredicate(const Expr &e)=0
e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=}
virtual Theorem negatedInequality(const Expr &e)=0
Propagating negation over <,<=,>,>=.
virtual Theorem compactNonLinearTerm(const Expr &nonLinear)=0
virtual Theorem canonMultMtermMterm(const Expr &e)=0
virtual Theorem canonInvert(const Expr &e)=0
==> 1/e = e' where e' is canonical; takes e.
virtual Theorem canonMultConstTerm(const Expr &c1, const Expr &c2, const Expr &t)=0
c1*(c2*t) ==> c'*t, takes c1 and c2 and t
virtual Theorem canonMultTermConst(const Expr &c, const Expr &t)=0
t*c ==> c*t, takes constant c and term t
virtual Theorem multEqZero(const Expr &expr)=0
virtual Theorem intVarEqnConst(const Expr &eqn, const Theorem &isIntx)=0
virtual Theorem implyWeakerInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)=0
virtual Theorem equalLeaves3(const Theorem &thm)=0
virtual Theorem rightMinusLeft(const Expr &e)=0
e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}
virtual Theorem canonPowConst(const Expr &pow)=0
c^n = c' (compute the constant power expression)
virtual Theorem canonMultTerm1Term2(const Expr &t1, const Expr &t2)=0
t1*t2 ==> Error, takes t1 and t2 where both are non-constants
virtual Theorem trustedRewrite(const Expr &expr1, const Expr &expr2)=0
virtual Theorem elimPowerConst(const Expr &expr, const Rational &root)=0
virtual Theorem splitGrayShadow(const Theorem &g)=0
G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2)
virtual Theorem canonDividePlus(const Expr &e, const Expr &d)=0
(+ c ...)/d ==> push division to all the coefficients.
virtual Theorem powerOfOne(const Expr &e)=0
virtual Theorem clashingBounds(const Theorem &lowerBound, const Theorem &upperBound)=0
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)
virtual Theorem simpleIneqInt(const Expr &ineq, const Theorem &isIntRHS)=0
virtual Theorem canonDivide(const Expr &e)=0
Canonize t1/t2.
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')
virtual Theorem canonMultZero(const Expr &e)=0
0*t ==> 0, takes 0*t
virtual Theorem dummyTheorem(const Expr &e)=0
bool isIntx(const Expr &e, const Rational &x)
virtual Theorem implyNegatedInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)=0
virtual Theorem canonDivideMult(const Expr &cx, const Expr &d)=0
(c * x) / d ==> (c/d) * x, takes (c*x) and d
virtual Theorem cycleConflict(const std::vector< Theorem > &inequalitites)=0
virtual Theorem moveSumConstantRight(const Expr &e)=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.
virtual Theorem equalLeaves4(const Theorem &thm)=0
virtual Theorem expandGrayShadowRewrite(const Expr &theShadow)=0
virtual Theorem rafineStrictInteger(const Theorem &isIntConstrThm, const Expr &constr)=0
virtual Theorem expandDarkShadow(const Theorem &darkShadow)=0
DARK_SHADOW(t1, t2) ==> t1 <= t2.
virtual Theorem grayShadowConst(const Theorem &g)=0
|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a))
virtual Theorem canonUMinusToDivide(const Expr &e)=0
-(e) ==> e / (-1); takes 'e'
virtual Theorem intEqIrrational(const Expr &expr, const Theorem &isInt)=0
virtual Theorem multIneqn(const Expr &e, const Expr &z)=0
Multiplying inequation by a non-zero constant.
virtual Theorem expandGrayShadow0(const Theorem &g)=0
GRAY_SHADOW(v, e, c, c) ==> v=e+c.
virtual Theorem lessThanToLERewrite(const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)=0
virtual Theorem minusToPlus(const Expr &x, const Expr &y)=0
==> x - y = x + (-1) * y
virtual Theorem flipInequality(const Expr &e)=0
"op1 GE|GT op2" <==> op2 LE|LT op1
virtual Theorem isIntConst(const Expr &e)=0
return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant
virtual Theorem equalLeaves2(const Theorem &thm)=0
virtual Theorem intEqualityRationalConstant(const Theorem &isIntConstrThm, const Expr &constr)=0
virtual Theorem oneElimination(const Expr &x)=0
virtual Theorem addInequalities(const Theorem &thm1, const Theorem &thm2)=0
virtual Theorem leftMinusRight(const Expr &e)=0
e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=}
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.
virtual Theorem varToMult(const Expr &e)=0
==> e = 1 * e
virtual Theorem realShadow(const Theorem &alphaLTt, const Theorem &tLTbeta)=0
Real shadow: a <(=) t, t <(=) b ==> a <(=) b.
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 canonMultConstConst(const Expr &c1, const Expr &c2)=0
c1*c2 ==> c', takes constant c1*c2
virtual Theorem nonLinearIneqSignSplit(const Theorem &ineqThm)=0
virtual Theorem canonPlus(const Expr &e)=0
Canonize (PLUS t1 ... tn)
virtual Theorem rewriteLeavesConst(const Expr &e)
virtual Theorem implyWeakerInequality(const Expr &expr1, const Expr &expr2)=0
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.
virtual Theorem integerSplit(const Expr &intVar, const Rational &intPoint)=0
virtual Theorem realShadowEq(const Theorem &alphaLEt, const Theorem &tLEalpha)=0
Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha.
virtual Theorem canonFlattenSum(const Expr &e)=0
flattens the input. accepts a PLUS expr
virtual ~ArithProofRules()
Rational pow(Rational pow, const Rational &base)
Raise 'base' into the power of 'pow' (pow must be an integer)
virtual Theorem evenPowerEqNegConst(const Expr &expr)=0
virtual Theorem canonDivideVar(const Expr &e, const Expr &d)=0
x / d ==> (1/d) * x, takes x and d
virtual Theorem powEqZero(const Expr &expr)=0
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]
virtual Theorem canonMult(const Expr &e)=0
Canonize (MULT t1 ... tn)
virtual Theorem canonComboLikeTerms(const Expr &e)=0
combine like terms. accepts a flattened PLUS expr
virtual Theorem expandGrayShadow(const Theorem &g)=0
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2.
virtual Theorem diseqToIneq(const Theorem &diseq)=0
x /= y ==> (x < y) OR (x > y)
virtual Theorem divideEqnNonConst(const Expr &x, const Expr &y, const Expr &z)=0