CVC3
Public Member Functions | Static Public Member Functions | Private Attributes | List of all members
CVC3::ArithTheoremProducer3 Class Reference

#include <arith_theorem_producer3.h>

Inherits CVC3::ArithProofRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::ArithTheoremProducer3:
Collaboration graph

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:

\[\frac{\mathsf{int}(a\cdot x)\quad \mathsf{int}(C+\sum_{i=1}^{n}a_{i}\cdot x_{i})} {a\cdot x=C+\sum_{i=1}^{n}a_{i}\cdot x_{i} \quad\equiv\quad x=t_{2}\wedge 0=t_{3}} \]

See the detailed description for explanations.

 
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)
 
- Public Member Functions inherited from CVC3::ArithProofRules
virtual ~ArithProofRules ()
 
virtual Theorem rewriteLeavesConst (const Expr &e)
 
- Public Member Functions inherited from CVC3::TheoremProducer
 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

TheoryArith3d_theoryArith
 

Additional Inherited Members

- Protected Member Functions inherited from CVC3::TheoremProducer
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)
 
- Protected Attributes inherited from CVC3::TheoremProducer
TheoremManagerd_tm
 
ExprManagerd_em
 
const bool * d_checkProofs
 
Op d_pfOp
 
Expr d_hole
 

Detailed Description

Definition at line 32 of file arith_theorem_producer3.h.

Constructor & Destructor Documentation

CVC3::ArithTheoremProducer3::ArithTheoremProducer3 ( TheoremManager tm,
TheoryArith3 theoryArith 
)
inline

Constructor.

Definition at line 66 of file arith_theorem_producer3.h.

Member Function Documentation

Rational ArithTheoremProducer3::modEq ( const Rational i,
const Rational m 
)
private

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.

Expr ArithTheoremProducer3::create_t ( const Expr eqn)
private
Expr ArithTheoremProducer3::create_t2 ( const Expr lhs,
const Expr rhs,
const Expr t 
)
private
Expr ArithTheoremProducer3::create_t3 ( const Expr lhs,
const Expr rhs,
const Expr t 
)
private
void ArithTheoremProducer3::sumModM ( std::vector< Expr > &  summands,
const Expr sum,
const Rational m,
const Rational divisor 
)
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().

Expr ArithTheoremProducer3::monomialModM ( const Expr e,
const Rational m,
const Rational divisor 
)
private
void ArithTheoremProducer3::sumMulF ( std::vector< Expr > &  summands,
const Expr sum,
const Rational m,
const Rational divisor 
)
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().

Expr ArithTheoremProducer3::monomialMulF ( const Expr e,
const Rational m,
const Rational divisor 
)
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().

Rational ArithTheoremProducer3::f ( const Rational i,
const Rational m 
)
private

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().

Expr ArithTheoremProducer3::substitute ( const Expr term,
ExprMap< Expr > &  eMap 
)
private
Expr CVC3::ArithTheoremProducer3::rat ( Rational  r)
inline

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().

Type CVC3::ArithTheoremProducer3::realType ( )
inline

Definition at line 71 of file arith_theorem_producer3.h.

References d_theoryArith, and CVC3::TheoryArith::realType().

Type CVC3::ArithTheoremProducer3::intType ( )
inline

Definition at line 72 of file arith_theorem_producer3.h.

References d_theoryArith, and CVC3::TheoryArith::intType().

Expr CVC3::ArithTheoremProducer3::darkShadow ( const Expr lhs,
const Expr rhs 
)
inline

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().

Expr CVC3::ArithTheoremProducer3::grayShadow ( const Expr v,
const Expr e,
const Rational c1,
const Rational c2 
)
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().

Theorem ArithTheoremProducer3::varToMult ( const Expr e)
virtual

==> e = 1 * e

Implements CVC3::ArithProofRules.

Definition at line 56 of file arith_theorem_producer3.cpp.

Theorem ArithTheoremProducer3::uMinusToMult ( const Expr e)
virtual

==> -(e) = (-1) * e

Implements CVC3::ArithProofRules.

Definition at line 64 of file arith_theorem_producer3.cpp.

Theorem ArithTheoremProducer3::minusToPlus ( const Expr x,
const Expr y 
)
virtual

==> x - y = x + (-1) * y

Implements CVC3::ArithProofRules.

Definition at line 72 of file arith_theorem_producer3.cpp.

Theorem ArithTheoremProducer3::canonUMinusToDivide ( const Expr e)
virtual

-(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.

Theorem ArithTheoremProducer3::canonDivideConst ( const Expr c,
const Expr d 
)
virtual

(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().

Theorem ArithTheoremProducer3::canonDivideMult ( const Expr cx,
const Expr d 
)
virtual

(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().

Theorem ArithTheoremProducer3::canonDividePlus ( const Expr e,
const Expr d 
)
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

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().

Theorem ArithTheoremProducer3::canonDivideVar ( const Expr e,
const Expr d 
)
virtual

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().

bool ArithTheoremProducer3::greaterthan ( const Expr l,
const Expr r 
)
static
Expr ArithTheoremProducer3::simplifiedMultExpr ( std::vector< Expr > &  mulKids)
virtual

Definition at line 196 of file arith_theorem_producer3.cpp.

References DebugAssert, and CVC3::multExpr().

Expr ArithTheoremProducer3::canonMultConstMult ( const Expr c,
const Expr e 
)
virtual
Expr ArithTheoremProducer3::canonMultConstPlus ( const Expr e1,
const Expr e2 
)
virtual
Expr ArithTheoremProducer3::canonMultPowPow ( const Expr e1,
const Expr e2 
)
virtual
Expr ArithTheoremProducer3::canonMultPowLeaf ( const Expr e1,
const Expr e2 
)
virtual
Expr ArithTheoremProducer3::canonMultLeafLeaf ( const Expr e1,
const Expr e2 
)
virtual

Definition at line 329 of file arith_theorem_producer3.cpp.

References CVC3::powExpr().

Expr ArithTheoremProducer3::canonMultLeafOrPowMult ( const Expr e1,
const Expr e2 
)
virtual
Expr ArithTheoremProducer3::canonCombineLikeTerms ( const std::vector< Expr > &  sumExprs)
virtual
Expr ArithTheoremProducer3::canonMultLeafOrPowOrMultPlus ( const Expr e1,
const Expr e2 
)
virtual
Expr ArithTheoremProducer3::canonMultPlusPlus ( const Expr e1,
const Expr e2 
)
virtual
Theorem ArithTheoremProducer3::canonMultMtermMterm ( const Expr e)
virtual
Theorem ArithTheoremProducer3::canonPlus ( const Expr e)
virtual

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.

Theorem ArithTheoremProducer3::canonInvertConst ( const Expr e)
virtual
Theorem ArithTheoremProducer3::canonInvertLeaf ( const Expr e)
virtual

Definition at line 785 of file arith_theorem_producer3.cpp.

References CVC3::powExpr().

Theorem ArithTheoremProducer3::canonInvertPow ( const Expr e)
virtual
Theorem ArithTheoremProducer3::canonInvertMult ( const Expr e)
virtual
Theorem ArithTheoremProducer3::canonInvert ( const Expr e)
virtual

==> 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().

Theorem ArithTheoremProducer3::moveSumConstantRight ( const Expr e)
virtual

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.

Parameters
ethe expression to transform
Returns
rewrite theorem representing the transformation

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().

Theorem ArithTheoremProducer3::canonDivide ( const Expr e)
virtual

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().

Theorem ArithTheoremProducer3::canonMult ( const Expr e)
virtual

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.

Theorem ArithTheoremProducer3::canonMultTermConst ( const Expr c,
const Expr t 
)
virtual

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().

Theorem ArithTheoremProducer3::canonMultTerm1Term2 ( const Expr t1,
const Expr t2 
)
virtual

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().

Theorem ArithTheoremProducer3::canonMultZero ( const Expr e)
virtual

0*t ==> 0, takes 0*t

Implements CVC3::ArithProofRules.

Definition at line 952 of file arith_theorem_producer3.cpp.

Theorem ArithTheoremProducer3::canonMultOne ( const Expr e)
virtual

1*t ==> t, takes 1*t

Implements CVC3::ArithProofRules.

Definition at line 960 of file arith_theorem_producer3.cpp.

Theorem ArithTheoremProducer3::canonMultConstConst ( const Expr c1,
const Expr c2 
)
virtual

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().

Theorem ArithTheoremProducer3::canonMultConstTerm ( const Expr c1,
const Expr c2,
const Expr t 
)
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().

Theorem ArithTheoremProducer3::canonMultConstSum ( const Expr c1,
const Expr sum 
)
virtual
Theorem ArithTheoremProducer3::canonPowConst ( const Expr pow)
virtual
Theorem ArithTheoremProducer3::canonFlattenSum ( const Expr e)
virtual
Theorem ArithTheoremProducer3::canonComboLikeTerms ( const Expr e)
virtual
Theorem ArithTheoremProducer3::multEqZero ( const Expr expr)
virtual
Theorem ArithTheoremProducer3::powEqZero ( const Expr expr)
virtual
Theorem ArithTheoremProducer3::elimPower ( const Expr expr)
virtual
Theorem ArithTheoremProducer3::elimPowerConst ( const Expr expr,
const Rational root 
)
virtual
Theorem ArithTheoremProducer3::evenPowerEqNegConst ( const Expr expr)
virtual
Theorem ArithTheoremProducer3::intEqIrrational ( const Expr expr,
const Theorem isInt 
)
virtual
Theorem ArithTheoremProducer3::constPredicate ( const Expr e)
virtual

e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=}

Parameters
etakes 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().

Theorem ArithTheoremProducer3::rightMinusLeft ( const Expr e)
virtual

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.

Theorem ArithTheoremProducer3::leftMinusRight ( const Expr e)
virtual

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.

Theorem ArithTheoremProducer3::plusPredicate ( const Expr x,
const Expr y,
const Expr z,
int  kind 
)
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().

Theorem ArithTheoremProducer3::multEqn ( const Expr x,
const Expr y,
const Expr z 
)
virtual

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().

Theorem ArithTheoremProducer3::divideEqnNonConst ( const Expr x,
const Expr y,
const Expr z 
)
virtual

Implements CVC3::ArithProofRules.

Definition at line 1394 of file arith_theorem_producer3.cpp.

References CVC3::Expr::eqExpr(), and CVC3::orExpr().

Theorem ArithTheoremProducer3::multIneqn ( const Expr e,
const Expr z 
)
virtual

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().

Theorem ArithTheoremProducer3::eqToIneq ( const Expr e)
virtual
Theorem ArithTheoremProducer3::flipInequality ( const Expr e)
virtual

"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().

Theorem ArithTheoremProducer3::negatedInequality ( const Expr e)
virtual

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().

Theorem ArithTheoremProducer3::realShadow ( const Theorem alphaLTt,
const Theorem tLTbeta 
)
virtual
Theorem ArithTheoremProducer3::realShadowEq ( const Theorem alphaLEt,
const Theorem tLEalpha 
)
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().

Theorem ArithTheoremProducer3::finiteInterval ( const Theorem aLEt,
const Theorem tLEac,
const Theorem isInta,
const Theorem isIntt 
)
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().

Theorem ArithTheoremProducer3::darkGrayShadow2ab ( const Theorem betaLEbx,
const Theorem axLEalpha,
const Theorem isIntAlpha,
const Theorem isIntBeta,
const Theorem isIntx 
)
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().

Theorem ArithTheoremProducer3::darkGrayShadow2ba ( const Theorem betaLEbx,
const Theorem axLEalpha,
const Theorem isIntAlpha,
const Theorem isIntBeta,
const Theorem isIntx 
)
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().

Theorem ArithTheoremProducer3::expandDarkShadow ( const Theorem darkShadow)
virtual
Theorem ArithTheoremProducer3::expandGrayShadow0 ( const Theorem g)
virtual
Theorem ArithTheoremProducer3::splitGrayShadow ( const Theorem g)
virtual

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().

Theorem ArithTheoremProducer3::splitGrayShadowSmall ( const Theorem grayShadow)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3024 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::expandGrayShadow ( const Theorem g)
virtual
Theorem ArithTheoremProducer3::expandGrayShadowConst ( const Theorem g)
virtual

Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion].

Implements three versions of the rule:

\[\frac{\mathrm{GRAY\_SHADOW}(ax,c,c1,c2)} {ax = c + i - \mathrm{sign}(i)\cdot j(c,i,a) \lor GRAY\_SHADOW(ax, c, i-\mathrm{sign}(i)\cdot (a+j(c,i,a)))}\]

 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().

Theorem ArithTheoremProducer3::grayShadowConst ( const Theorem g)
virtual

|- 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().

Theorem ArithTheoremProducer3::lessThanToLE ( const Theorem less,
const Theorem isIntLHS,
const Theorem isIntRHS,
bool  changeRight 
)
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().

Theorem ArithTheoremProducer3::lessThanToLERewrite ( const Expr ineq,
const Theorem isIntLHS,
const Theorem isIntRHS,
bool  changeRight 
)
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().

Theorem ArithTheoremProducer3::intVarEqnConst ( const Expr eqn,
const Theorem isIntx 
)
virtual
Parameters
eqnis an equation 0 = a.x or 0 = c + a.x
isIntxis a proof of IS_INTEGER(x)
Returns
the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else return the theorem 0 = c + a.x <==> false.

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().

Theorem ArithTheoremProducer3::IsIntegerElim ( const Theorem isIntx)
virtual

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.

Theorem ArithTheoremProducer3::eqElimIntRule ( const Theorem eqn,
const Theorem isIntx,
const std::vector< Theorem > &  isIntVars 
)
virtual

Equality elimination rule for integers:

\[\frac{\mathsf{int}(a\cdot x)\quad \mathsf{int}(C+\sum_{i=1}^{n}a_{i}\cdot x_{i})} {a\cdot x=C+\sum_{i=1}^{n}a_{i}\cdot x_{i} \quad\equiv\quad x=t_{2}\wedge 0=t_{3}} \]

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:

\[\begin{array}{rcl} t_{2} & = & -(C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) \cdot x_{i}-m\cdot\sigma(t))\\ & & \\ t_{3} & = & \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i} -a\cdot\sigma(t)\\ & & \\ t & = & (C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) \cdot x_{i}+x)/m\\ & & \\ m & = & a+1\\ & & \\ \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m} +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\ m\\ & & \\ i\ \mathbf{mod}\ m & = & i-m\left\lfloor\frac{i}{m} +\frac{1}{2}\right\rfloor \end{array} \]

 All the variables and coefficients are integer, and a >= 2.

 \param eqn is the equation

\[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\]

\[\frac{\Gamma\models ax=t\quad \Gamma'\models\mathsf{int}(x)\quad \{\Gamma_i\models\mathsf{int}(x_i) | x_i\mbox{ is var in }t\}} {\Gamma,\Gamma',\bigcup_i\Gamma_i\models \exists (y:\mathrm{int}).\ x=t_2(y)\wedge 0=t_3(y)} \]

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:

\[\begin{array}{rcl} t & = & C+\sum_{i=1}^na_{i}\cdot x_{i}\\ t_{2}(y) & = & -(C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) \cdot x_{i}-m\cdot y)\\ & & \\ t_{3}(y) & = & \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i} -a\cdot y\\ & & \\ m & = & a+1\\ & & \\ \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m} +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\ m\\ & & \\ i\ \mathbf{mod}\ m & = & i-m\left\lfloor\frac{i}{m} +\frac{1}{2}\right\rfloor \end{array} \]

 All the variables and coefficients are integer, and a >= 2.

 \param eqn is the equation ax=t:

\[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\]

 \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.

Theorem ArithTheoremProducer3::isIntConst ( const Expr e)
virtual

return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant

Parameters
eis 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().

Theorem ArithTheoremProducer3::equalLeaves1 ( const Theorem e)
virtual
Theorem ArithTheoremProducer3::equalLeaves2 ( const Theorem e)
virtual
Theorem ArithTheoremProducer3::equalLeaves3 ( const Theorem e)
virtual
Theorem ArithTheoremProducer3::equalLeaves4 ( const Theorem e)
virtual
Theorem ArithTheoremProducer3::diseqToIneq ( const Theorem diseq)
virtual
Theorem ArithTheoremProducer3::dummyTheorem ( const Expr e)
virtual

Implements CVC3::ArithProofRules.

Definition at line 2748 of file arith_theorem_producer3.cpp.

Theorem ArithTheoremProducer3::oneElimination ( const Expr x)
virtual
Theorem ArithTheoremProducer3::clashingBounds ( const Theorem lowerBound,
const Theorem upperBound 
)
virtual
Theorem ArithTheoremProducer3::addInequalities ( const Theorem thm1,
const Theorem thm2 
)
virtual
Theorem ArithTheoremProducer3::addInequalities ( const std::vector< Theorem > &  thms)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3061 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::implyWeakerInequality ( const Expr expr1,
const Expr expr2 
)
virtual
Theorem ArithTheoremProducer3::implyNegatedInequality ( const Expr expr1,
const Expr expr2 
)
virtual
Theorem ArithTheoremProducer3::integerSplit ( const Expr intVar,
const Rational intPoint 
)
virtual
Theorem ArithTheoremProducer3::trustedRewrite ( const Expr expr1,
const Expr expr2 
)
virtual

Implements CVC3::ArithProofRules.

Definition at line 2938 of file arith_theorem_producer3.cpp.

Theorem ArithTheoremProducer3::rafineStrictInteger ( const Theorem isIntConstrThm,
const Expr constr 
)
virtual
Theorem ArithTheoremProducer3::simpleIneqInt ( const Expr ineq,
const Theorem isIntRHS 
)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3073 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::intEqualityRationalConstant ( const Theorem isIntConstrThm,
const Expr constr 
)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3083 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::cycleConflict ( const std::vector< Theorem > &  inequalitites)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3088 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::implyEqualities ( const std::vector< Theorem > &  inequalities)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3093 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::implyWeakerInequalityDiffLogic ( const std::vector< Theorem > &  antecedentThms,
const Expr implied 
)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3029 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::implyNegatedInequalityDiffLogic ( const std::vector< Theorem > &  antecedentThms,
const Expr implied 
)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3034 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::expandGrayShadowRewrite ( const Expr theShadow)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3039 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::compactNonLinearTerm ( const Expr nonLinear)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3044 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::nonLinearIneqSignSplit ( const Theorem ineqThm)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3049 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::implyDiffLogicBothBounds ( const Expr x,
std::vector< Theorem > &  c1_le_x,
Rational  c1,
std::vector< Theorem > &  x_le_c2,
Rational  c2 
)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3054 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::powerOfOne ( const Expr e)
virtual

Implements CVC3::ArithProofRules.

Definition at line 3066 of file arith_theorem_producer3.cpp.

References DebugAssert.

Member Data Documentation

TheoryArith3* CVC3::ArithTheoremProducer3::d_theoryArith
private

Definition at line 33 of file arith_theorem_producer3.h.

Referenced by darkShadow(), grayShadow(), intType(), and realType().


The documentation for this class was generated from the following files: