22 #ifndef _cvc3__arith_theorem_producer_h_
23 #define _cvc3__arith_theorem_producer_h_
52 void sumModM(std::vector<Expr>& summands,
const Expr& sum,
56 void sumMulF(std::vector<Expr>& summands,
const Expr& sum,
221 const Expr& z,
int kind);
279 const Theorem& isIntRHS,
bool changeRight);
282 const Theorem& isIntRHS,
bool changeRight);
288 const std::vector<Theorem>& isIntVars);
337 std::vector<Theorem>& x_le_c2,
Rational c2);
Theorem eqElimIntRule(const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars)
Equality elimination rule for integers: See the detailed description for explanations.
virtual Theorem canonPowConst(const Expr &pow)
c^n = c' (compute the constant power expression)
Theorem trustedRewrite(const Expr &expr1, const Expr &expr2)
Theorem equalLeaves4(const Theorem &e)
Data structure of expressions in CVC3.
virtual Expr simplifiedMultExpr(std::vector< Expr > &mulKids)
Expr monomialMulF(const Expr &e, const Rational &m, const Rational &divisor)
Compute the special modulus: i - m*floor(i/m+1/2)
virtual Theorem canonUMinusToDivide(const Expr &e)
-(e) ==> e / (-1); takes 'e'
Theorem equalLeaves3(const Theorem &e)
virtual Theorem canonDividePlus(const Expr &e, const Expr &d)
(+ c ...)/d ==> push division to all the coefficients.
virtual Expr canonMultConstPlus(const Expr &e1, const Expr &e2)
Rational modEq(const Rational &i, const Rational &m)
Compute the special modulus: i - m*floor(i/m+1/2)
ArithTheoremProducer(TheoremManager *tm, TheoryArithNew *theoryArith)
Constructor.
Expr grayShadow(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)
Construct the gray shadow expression representing c1 <= v - e <= c2.
Theorem integerSplit(const Expr &intVar, const Rational &intPoint)
Theorem simpleIneqInt(const Expr &ineq, const Theorem &isIntRHS)
virtual Theorem intEqIrrational(const Expr &expr, const Theorem &isInt)
virtual Theorem leftMinusRight(const Expr &e)
e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=}
virtual Theorem canonPlus(const Expr &e)
Canonize (PLUS t1 ... tn)
virtual Theorem canonMultOne(const Expr &e)
1*t ==> t, takes 1*t
Expr substitute(const Expr &term, ExprMap< Expr > &eMap)
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)
Theorem equalLeaves2(const Theorem &e)
MS C++ specific settings.
Rational f(const Rational &i, const Rational &m)
Compute floor(i/m+1/2) + mod(i,m)
Theorem lessThanToLE(const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)
virtual Theorem elimPower(const Expr &expr)
Theorem dummyTheorem(const Expr &e)
virtual Theorem canonInvert(const Expr &e)
==> 1/e = e' where e' is canonical; takes e.
Theorem implyNegatedInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)
virtual Theorem canonDivide(const Expr &e)
Theorem expandGrayShadow0(const Theorem &grayShadow)
GRAY_SHADOW(v, e, c, c) ==> v=e+c.
virtual Theorem elimPowerConst(const Expr &expr, const Rational &root)
virtual Theorem multEqZero(const Expr &expr)
virtual Theorem minusToPlus(const Expr &x, const Expr &y)
==> x - y = x + (-1) * y
virtual Expr canonMultPowPow(const Expr &e1, const Expr &e2)
virtual Theorem powEqZero(const Expr &expr)
Theorem realShadowEq(const Theorem &alphaLEt, const Theorem &tLEalpha)
alpha <= t <= alpha ==> t = alpha
virtual Expr canonMultLeafLeaf(const Expr &e1, const Expr &e2)
Theorem intVarEqnConst(const Expr &eqn, const Theorem &isIntx)
Theorem expandDarkShadow(const Theorem &darkShadow)
virtual Theorem canonDivideVar(const Expr &e1, const Expr &e2)
x / d ==> (1/d) * x, takes x and d
bool isIntx(const Expr &e, const Rational &x)
static bool greaterthan(const Expr &, const Expr &)
virtual Theorem canonFlattenSum(const Expr &e)
flattens the input. accepts a PLUS expr
Theorem isIntConst(const Expr &e)
return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant
virtual Expr canonMultLeafOrPowMult(const Expr &e1, const Expr &e2)
Theorem implyWeakerInequality(const Expr &expr1, const Expr &expr2)
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
Theorem intEqualityRationalConstant(const Theorem &isIntConstrThm, const Expr &constr)
virtual Theorem canonMultZero(const Expr &e)
0*t ==> 0, takes 0*t
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 canonInvertConst(const Expr &e)
Theorem grayShadowConst(const Theorem &g)
|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a))
virtual Theorem varToMult(const Expr &e)
==> e = 1 * e
Expr create_t3(const Expr &lhs, const Expr &rhs, const Expr &t)
Create the term 't3'. See eqElimIntRule().
virtual Theorem canonDivideConst(const Expr &c, const Expr &d)
(c) / d ==> (c/d), takes c and d
Theorem clashingBounds(const Theorem &lowerBound, const Theorem &upperBound)
Theorem implyWeakerInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)
Theorem diseqToIneq(const Theorem &diseq)
x /= y ==> (x < y) OR (x > y)
virtual Theorem canonComboLikeTerms(const Expr &e)
combine like terms. accepts a flattened PLUS expr
virtual Theorem canonMultMtermMterm(const Expr &e)
Theorem negatedInequality(const Expr &e)
Propagating negation over <,<=,>,>=.
Theorem IsIntegerElim(const Theorem &isIntx)
Theorem implyDiffLogicBothBounds(const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2)
Expr monomialModM(const Expr &e, const Rational &m, const Rational &divisor)
Compute the special modulus: i - m*floor(i/m+1/2)
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 canonMultTermConst(const Expr &c, const Expr &t)
t*c ==> c*t, takes constant c and term t
virtual Theorem flipInequality(const Expr &e)
"op1 GE|GT op2" <==> op2 LE|LT op1
virtual Theorem moveSumConstantRight(const Expr &e)
Theorem equalLeaves1(const Theorem &e)
Theorem expandGrayShadow(const Theorem &grayShadow)
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2.
virtual Expr canonMultConstMult(const Expr &c, const Expr &e)
Expr newRatExpr(const Rational &r)
Theorem expandGrayShadowConst(const Theorem &grayShadow)
Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion].
Theorem powerOfOne(const Expr &e)
Theorem addInequalities(const Theorem &thm1, const Theorem &thm2)
Theorem realShadow(const Theorem &alphaLTt, const Theorem &tLTbeta)
Real shadow: a <(=) t, t <(=) b ==> a <(=) b.
Theorem oneElimination(const Expr &x)
virtual Theorem canonMultConstSum(const Expr &c1, const Expr &sum)
c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
Theorem implyEqualities(const std::vector< Theorem > &inequalities)
virtual Theorem canonMultTerm1Term2(const Expr &t1, const Expr &t2)
t1*t2 ==> Error, takes t1 and t2 where both are non-constants
virtual Expr canonMultPlusPlus(const Expr &e1, const Expr &e2)
Expr darkShadow(const Expr &lhs, const Expr &rhs)
Construct the dark shadow expression representing lhs <= rhs.
Expr rat(Rational r)
Create Expr from Rational (for convenience)
virtual Theorem canonMult(const Expr &e)
virtual Theorem canonDivideMult(const Expr &cx, const Expr &d)
(c * x) / d ==> (c/d) * x, takes (c*x) and d
Theorem rafineStrictInteger(const Theorem &isIntConstrThm, const Expr &constr)
Theorem splitGrayShadowSmall(const Theorem &grayShadow)
virtual Theorem constPredicate(const Expr &e)
e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=}
virtual Theorem canonInvertLeaf(const Expr &e)
virtual Theorem canonMultConstConst(const Expr &c1, const Expr &c2)
c1*c2 ==> c', takes constant c1*c2
Expr darkShadow(const Expr &lhs, const Expr &rhs)
Construct the dark shadow expression representing lhs <= rhs.
Theorem implyNegatedInequality(const Expr &expr1, const Expr &expr2)
virtual Theorem canonMultConstTerm(const Expr &c1, const Expr &c2, const Expr &t)
c1*(c2*t) ==> c'*t, takes c1 and c2 and t
Theorem nonLinearIneqSignSplit(const Theorem &ineqThm)
virtual Expr canonCombineLikeTerms(const std::vector< Expr > &sumExprs)
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') wit...
Theorem splitGrayShadow(const Theorem &grayShadow)
G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2)
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 expandGrayShadowRewrite(const Expr &theShadow)
Theorem lessThanToLERewrite(const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)
Theorem cycleConflict(const std::vector< Theorem > &inequalitites)
TheoryArithNew * d_theoryArith
virtual Theorem evenPowerEqNegConst(const Expr &expr)
Theorem darkGrayShadow2ba(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)
Dark & Gray shadows when b <= a.
virtual Theorem eqToIneq(const Expr &e)
x = y ==> x <= y and x >= y
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.
Rational pow(Rational pow, const Rational &base)
Raise 'base' into the power of 'pow' (pow must be an integer)
virtual Theorem canonInvertPow(const Expr &e)
Theorem darkGrayShadow2ab(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)
Dark & Gray shadows when a <= b.
virtual Expr canonMultLeafOrPowOrMultPlus(const Expr &e1, const Expr &e2)
Expr create_t(const Expr &eqn)
Create the term 't'. See eqElimIntRule().
virtual Theorem canonInvertMult(const Expr &e)
virtual Theorem uMinusToMult(const Expr &e)
==> -(e) = (-1) * e
Rational constRHSGrayShadow(const Rational &c, const Rational &b, const Rational &a)
Implements j(c,b,a)
Theorem compactNonLinearTerm(const Expr &nonLinear)
virtual Expr canonMultPowLeaf(const Expr &e1, const Expr &e2)
Expr create_t2(const Expr &lhs, const Expr &rhs, const Expr &t)
Create the term 't2'. See eqElimIntRule().
virtual Theorem rightMinusLeft(const Expr &e)
e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}