CVC3::ArithTheoremProducerOld Class Reference

#include <arith_theorem_producer_old.h>

Inheritance diagram for CVC3::ArithTheoremProducerOld:

[legend]

Collaboration diagram for CVC3::ArithTheoremProducerOld:

[legend]

List of all members.

Public Member Functions

ArithTheoremProducerOld (TheoremManager *tm, TheoryArithOld *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)
Theorem rewriteLeavesConst (const Expr &e)

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).
void getLeaves (const Expr &e, std::set< Rational > &s, ExprHashMap< bool > &cache)
Compute the special modulus: i - m*floor(i/m+1/2).

Private Attributes

TheoryArithOld * d_theoryArith

Detailed Description

Definition at line 31 of file arith_theorem_producer_old.h.

Constructor & Destructor Documentation

CVC3::ArithTheoremProducerOld::ArithTheoremProducerOld	(	TheoremManager *	tm,
		TheoryArithOld *	theoryArith
	)			`[inline]`

Constructor.

Definition at line 66 of file arith_theorem_producer_old.h.

Member Function Documentation

Rational ArithTheoremProducerOld::modEq	(	const Rational &	i,
		const Rational &	m
	)			`[private]`

Compute the special modulus: i - m*floor(i/m+1/2).

Definition at line 2429 of file arith_theorem_producer_old.cpp.

References DebugAssert, CVC3::Rational::toString(), and CVC3::TRACE.

Referenced by f(), monomialModM(), and sumModM().

Expr ArithTheoremProducerOld::create_t ( const Expr & eqn ) [private]

Create the term 't'. See eqElimIntRule().

Definition at line 2369 of file arith_theorem_producer_old.cpp.

References CLASS_NAME, DebugAssert, CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isPlus(), monomialModM(), CVC3::multExpr(), CVC3::plusExpr(), rat(), sumModM(), CVC3::Rational::toString(), and CVC3::Expr::toString().

Expr ArithTheoremProducerOld::create_t2	(	const Expr &	lhs,
		const Expr &	rhs,
		const Expr &	t
	)			`[private]`

Create the term 't2'. See eqElimIntRule().

Definition at line 2388 of file arith_theorem_producer_old.cpp.

References DebugAssert, CVC3::Expr::getRational(), CVC3::isPlus(), CVC3::Expr::isRational(), monomialModM(), CVC3::plusExpr(), rat(), sumModM(), and CVC3::Rational::toString().

Referenced by eqElimIntRule().

Expr ArithTheoremProducerOld::create_t3	(	const Expr &	lhs,
		const Expr &	rhs,
		const Expr &	t
	)			`[private]`

Create the term 't3'. See eqElimIntRule().

Definition at line 2408 of file arith_theorem_producer_old.cpp.

References DebugAssert, CVC3::Expr::getRational(), CVC3::isPlus(), CVC3::Expr::isRational(), monomialMulF(), CVC3::plusExpr(), rat(), sumMulF(), and CVC3::Rational::toString().

Referenced by eqElimIntRule().

void ArithTheoremProducerOld::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 2445 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), CLASS_NAME, DebugAssert, CVC3::Expr::end(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), modEq(), monomialModM(), rat(), and CVC3::Rational::toString().

Referenced by create_t(), and create_t2().

Expr ArithTheoremProducerOld::monomialModM	(	const Expr &	e,
		const Rational &	m,
		const Rational &	divisor
	)			`[private]`

Compute the special modulus: i - m*floor(i/m+1/2).

Definition at line 2465 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getKids(), CVC3::Expr::getRational(), CVC3::isMult(), modEq(), CVC3::multExpr(), rat(), CVC3::Expr::toString(), CVC3::Rational::toString(), and CVC3::TRACE.

Referenced by create_t(), create_t2(), and sumModM().

void ArithTheoremProducerOld::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 2493 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), CLASS_NAME, DebugAssert, CVC3::Expr::end(), f(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), monomialMulF(), rat(), and CVC3::Rational::toString().

Referenced by create_t3().

Expr ArithTheoremProducerOld::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 2513 of file arith_theorem_producer_old.cpp.

References DebugAssert, f(), CVC3::isMult(), CVC3::multExpr(), rat(), and CVC3::Rational::toString().

Referenced by create_t3(), and sumMulF().

Rational ArithTheoremProducerOld::f	(	const Rational &	i,
		const Rational &	m
	)			`[private]`

Compute floor(i/m+1/2) + mod(i,m).

Definition at line 2438 of file arith_theorem_producer_old.cpp.

References DebugAssert, modEq(), and CVC3::Rational::toString().

Referenced by monomialMulF(), and sumMulF().

Expr ArithTheoremProducerOld::substitute	(	const Expr &	term,
		ExprMap< Expr > &	eMap
	)			`[private]`

Compute the special modulus: i - m*floor(i/m+1/2).

Definition at line 2530 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::isMult(), CVC3::isPlus(), and CVC3::plusExpr().

void ArithTheoremProducerOld::getLeaves	(	const Expr &	e,
		std::set< Rational > &	s,
		ExprHashMap< bool > &	cache
	)			`[private]`

Compute the special modulus: i - m*floor(i/m+1/2).

Definition at line 3838 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), d_theoryArith, DebugAssert, CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), CVC3::Expr::getRational(), CVC3::Expr::isAtomic(), CVC3::Expr::isITE(), CVC3::Theory::isLeaf(), and CVC3::Expr::isRational().

Referenced by rewriteLeavesConst().

Expr CVC3::ArithTheoremProducerOld::rat ( Rational r ) [inline]

Create Expr from Rational (for convenience).

Definition at line 70 of file arith_theorem_producer_old.h.

References CVC3::TheoremProducer::d_em, and CVC3::ExprManager::newRatExpr().

Referenced by canonCombineLikeTerms(), canonComboLikeTerms(), canonDivideConst(), canonDivideMult(), canonDividePlus(), canonDivideVar(), canonInvertConst(), canonInvertLeaf(), canonInvertMult(), canonInvertPow(), canonMult(), canonMultConstConst(), canonMultConstMult(), canonMultConstTerm(), canonMultLeafLeaf(), canonMultLeafOrPowMult(), canonMultOne(), canonMultPowLeaf(), canonMultPowPow(), canonMultZero(), canonPowConst(), canonUMinusToDivide(), compactNonLinearTerm(), create_t(), create_t2(), create_t3(), darkGrayShadow2ab(), darkGrayShadow2ba(), divideEqnNonConst(), elimPowerConst(), eqElimIntRule(), expandGrayShadow(), expandGrayShadowConst(), expandGrayShadowRewrite(), grayShadowConst(), implyDiffLogicBothBounds(), integerSplit(), intVarEqnConst(), leftMinusRight(), lessThanToLE(), lessThanToLERewrite(), minusToPlus(), monomialModM(), monomialMulF(), moveSumConstantRight(), multEqZero(), nonLinearIneqSignSplit(), powEqZero(), rafineStrictInteger(), rightMinusLeft(), simpleIneqInt(), simplifiedMultExpr(), splitGrayShadowSmall(), sumModM(), sumMulF(), uMinusToMult(), and varToMult().

Type CVC3::ArithTheoremProducerOld::realType ( ) [inline]

Definition at line 71 of file arith_theorem_producer_old.h.

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

Type CVC3::ArithTheoremProducerOld::intType ( ) [inline]

Definition at line 72 of file arith_theorem_producer_old.h.

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

Referenced by eqElimIntRule().

Expr CVC3::ArithTheoremProducerOld::darkShadow	(	const Expr &	lhs,
		const Expr &	rhs
	)			`[inline]`

Construct the dark shadow expression representing lhs <= rhs.

Definition at line 74 of file arith_theorem_producer_old.h.

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

Expr CVC3::ArithTheoremProducerOld::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_producer_old.h.

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

Referenced by darkGrayShadow2ab(), darkGrayShadow2ba(), finiteInterval(), grayShadowConst(), implyDiffLogicBothBounds(), and splitGrayShadow().

Theorem ArithTheoremProducerOld::varToMult ( const Expr & e ) [virtual]

==> e = 1 * e

Implements CVC3::ArithProofRules.

Definition at line 57 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::uMinusToMult ( const Expr & e ) [virtual]

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

Implements CVC3::ArithProofRules.

Definition at line 65 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::minusToPlus	(	const Expr &	x,
		const Expr &	y
	)			`[virtual]`

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

Implements CVC3::ArithProofRules.

Definition at line 73 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 83 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 92 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::TheoremProducer::d_hole, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 111 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 139 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::isPlus(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::plusExpr(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::canonDivideVar	(	const Expr &	e,
		const Expr &	d
	)			`[virtual]`

x / d ==> (1/d) * x, takes x and d

Implements CVC3::ArithProofRules.

Definition at line 162 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

bool ArithTheoremProducerOld::greaterthan	(	const Expr &	l,
		const Expr &	r
	)			`[static]`

Definition at line 2556 of file arith_theorem_producer_old.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 CVC3::RATIONAL_EXPR.

Referenced by MonomialLess::operator()().

Expr ArithTheoremProducerOld::simplifiedMultExpr ( std::vector< Expr > & mulKids ) [virtual]

Definition at line 197 of file arith_theorem_producer_old.cpp.

References DebugAssert, CVC3::multExpr(), and rat().

Referenced by canonMultConstMult(), canonMultLeafLeaf(), canonMultLeafOrPowMult(), canonMultPowLeaf(), and canonMultPowPow().

Expr ArithTheoremProducerOld::canonMultConstMult	(	const Expr &	c,
		const Expr &	e
	)			`[virtual]`

Definition at line 210 of file arith_theorem_producer_old.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, rat(), simplifiedMultExpr(), and CVC3::Expr::toString().

Referenced by canonMultMtermMterm().

Expr ArithTheoremProducerOld::canonMultConstPlus	(	const Expr &	e1,
		const Expr &	e2
	)			`[virtual]`

Definition at line 232 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), canonMultMtermMterm(), d_theoryArith, DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Theorem::getRHS(), CVC3::Expr::isRational(), CVC3::PLUS, and CVC3::Theory::substitutivityRule().

Referenced by canonMultMtermMterm().

Expr ArithTheoremProducerOld::canonMultPowPow	(	const Expr &	e1,
		const Expr &	e2
	)			`[virtual]`

Definition at line 251 of file arith_theorem_producer_old.cpp.

References DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::POW, CVC3::powExpr(), rat(), and simplifiedMultExpr().

Referenced by canonMultMtermMterm().

Expr ArithTheoremProducerOld::canonMultPowLeaf	(	const Expr &	e1,
		const Expr &	e2
	)			`[virtual]`

Definition at line 291 of file arith_theorem_producer_old.cpp.

References DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::POW, CVC3::powExpr(), rat(), and simplifiedMultExpr().

Referenced by canonMultMtermMterm().

Expr ArithTheoremProducerOld::canonMultLeafLeaf	(	const Expr &	e1,
		const Expr &	e2
	)			`[virtual]`

Definition at line 330 of file arith_theorem_producer_old.cpp.

References CVC3::powExpr(), rat(), and simplifiedMultExpr().

Referenced by canonMultMtermMterm().

Expr ArithTheoremProducerOld::canonMultLeafOrPowMult	(	const Expr &	e1,
		const Expr &	e2
	)			`[virtual]`

Definition at line 358 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::MULT, CVC3::POW, CVC3::powExpr(), rat(), and simplifiedMultExpr().

Referenced by canonMultMtermMterm().

Expr ArithTheoremProducerOld::canonCombineLikeTerms ( const std::vector< Expr > & sumExprs ) [virtual]

Definition at line 430 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), canonMultMtermMterm(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::Expr::isRational(), CVC3::MULT, CVC3::multExpr(), CVC3::plusExpr(), and rat().

Referenced by canonMultLeafOrPowOrMultPlus(), canonMultPlusPlus(), and canonPlus().

Expr ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus	(	const Expr &	e1,
		const Expr &	e2
	)			`[virtual]`

Definition at line 511 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), canonCombineLikeTerms(), canonMultMtermMterm(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::PLUS.

Referenced by canonMultMtermMterm().

Expr ArithTheoremProducerOld::canonMultPlusPlus	(	const Expr &	e1,
		const Expr &	e2
	)			`[virtual]`

Definition at line 530 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), canonCombineLikeTerms(), canonMultMtermMterm(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::PLUS.

Referenced by canonMultMtermMterm().

Theorem ArithTheoremProducerOld::canonMultMtermMterm ( const Expr & e ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 554 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), canonMultConstConst(), canonMultConstMult(), canonMultConstPlus(), canonMultLeafLeaf(), canonMultLeafOrPowMult(), canonMultLeafOrPowOrMultPlus(), canonMultOne(), canonMultPlusPlus(), canonMultPowLeaf(), canonMultPowPow(), canonMultZero(), CHECK_PROOFS, CHECK_SOUND, d_theoryArith, CVC3::Assumptions::emptyAssump(), FatalAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::isMult(), CVC3::Expr::isRational(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::POW, CVC3::RATIONAL_EXPR, CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Referenced by canonCombineLikeTerms(), canonInvertMult(), canonMult(), canonMultConstPlus(), canonMultLeafOrPowOrMultPlus(), and canonMultPlusPlus().

Theorem ArithTheoremProducerOld::canonPlus ( const Expr & e ) [virtual]

Canonize (PLUS t1 ... tn).

Implements CVC3::ArithProofRules.

Definition at line 719 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), canonCombineLikeTerms(), DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::canonInvertConst ( const Expr & e ) [virtual]

Definition at line 819 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Referenced by canonInvert().

Theorem ArithTheoremProducerOld::canonInvertLeaf ( const Expr & e ) [virtual]

Definition at line 835 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::powExpr(), rat(), and CVC3::TheoremProducer::withProof().

Referenced by canonInvert().

Theorem ArithTheoremProducerOld::canonInvertPow ( const Expr & e ) [virtual]

Definition at line 847 of file arith_theorem_producer_old.cpp.

References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::POW, CVC3::powExpr(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Referenced by canonInvert().

Theorem ArithTheoremProducerOld::canonInvertMult ( const Expr & e ) [virtual]

Definition at line 866 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), canonInvert(), canonMultMtermMterm(), DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Referenced by canonInvert().

Theorem ArithTheoremProducerOld::canonInvert ( const Expr & e ) [virtual]

==> 1/e = e' where e' is canonical; takes e.

Implements CVC3::ArithProofRules.

Definition at line 889 of file arith_theorem_producer_old.cpp.

References canonInvertConst(), canonInvertLeaf(), canonInvertMult(), canonInvertPow(), DebugAssert, CVC3::Expr::getKind(), CVC3::MULT, CVC3::PLUS, CVC3::POW, CVC3::RATIONAL_EXPR, and CVC3::Expr::toString().

Referenced by canonDivide(), and canonInvertMult().

Theorem ArithTheoremProducerOld::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:

e

the expression to transform

Returns:: rewrite theorem representing the transformation

Implements CVC3::ArithProofRules.

Definition at line 911 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::isEq(), CVC3::isIneq(), CVC3::isPlus(), CVC3::Expr::isRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::plusExpr(), rat(), MiniSat::right(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::canonDivide ( const Expr & e ) [virtual]

e[0]/e[1] ==> e[0]*(e[1])^-1

Implements CVC3::ArithProofRules.

Definition at line 957 of file arith_theorem_producer_old.cpp.

References canonInvert(), canonMult(), d_theoryArith, DebugAssert, CVC3::DIVIDE, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::transitivityRule(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 752 of file arith_theorem_producer_old.cpp.

References CVC3::TheoryArithOld::addMultiplicativeSignSplit(), CVC3::Expr::andExpr(), CVC3::Expr::arity(), CVC3::Expr::begin(), canonMultMtermMterm(), CVC3::TheoremProducer::d_em, d_theoryArith, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::eqExpr(), CVC3::ExprManager::falseExpr(), CVC3::geExpr(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::Expr::iffExpr(), CVC3::Expr::impExpr(), CVC3::isPlus(), CVC3::isPow(), CVC3::Expr::isRational(), CVC3::leExpr(), CVC3::ltExpr(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoryArithOld::nonlinearSignSplit(), CVC3::orExpr(), rat(), CVC3::Expr::toString(), CVC3::TRACE, CVC3::ExprManager::trueExpr(), CVC3::TheoremProducer::withProof(), and CVC3::XOR.

Referenced by canonDivide().

Theorem ArithTheoremProducerOld::canonMultTermConst	(	const Expr &	c,
		const Expr &	t
	)			`[virtual]`

t*c ==> c*t, takes constant c and term t

Implements CVC3::ArithProofRules.

Definition at line 975 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 989 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, and CVC3::Expr::toString().

Theorem ArithTheoremProducerOld::canonMultZero ( const Expr & e ) [virtual]

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

Implements CVC3::ArithProofRules.

Definition at line 1002 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().

Referenced by canonMultMtermMterm().

Theorem ArithTheoremProducerOld::canonMultOne ( const Expr & e ) [virtual]

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

Implements CVC3::ArithProofRules.

Definition at line 1010 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().

Referenced by canonMultMtermMterm().

Theorem ArithTheoremProducerOld::canonMultConstConst	(	const Expr &	c1,
		const Expr &	c2
	)			`[virtual]`

c1*c2 ==> c', takes constant c1*c2

Implements CVC3::ArithProofRules.

Definition at line 1019 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Referenced by canonMultMtermMterm().

Theorem ArithTheoremProducerOld::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 1037 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::canonMultConstSum	(	const Expr &	c1,
		const Expr &	sum
	)			`[virtual]`

c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum

Implements CVC3::ArithProofRules.

Definition at line 1057 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::plusExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::canonPowConst ( const Expr & pow ) [virtual]

c^n = c' (compute the constant power expression)

Implements CVC3::ArithProofRules.

Definition at line 1080 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Rational::isInteger(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::POW, rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::canonFlattenSum ( const Expr & e ) [virtual]

flattens the input. accepts a PLUS expr

Implements CVC3::ArithProofRules.

Definition at line 1107 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::plusExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::canonComboLikeTerms ( const Expr & e ) [virtual]

combine like terms. accepts a flattened PLUS expr

Implements CVC3::ArithProofRules.

Definition at line 1134 of file arith_theorem_producer_old.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::ExprMap< Data >::count(), CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::isMult(), CVC3::isPlus(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::plusExpr(), rat(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::multEqZero ( const Expr & expr ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 1192 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::isPow(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::OR, rat(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::powEqZero ( const Expr & expr ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 1239 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::ExprManager::falseExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isPow(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::elimPower ( const Expr & expr ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 1266 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, d_theoryArith, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::elimPowerConst	(	const Expr &	expr,
		const Rational &	root
	)			`[virtual]`

Implements CVC3::ArithProofRules.

Definition at line 1285 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, d_theoryArith, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::orExpr(), CVC3::pow(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::evenPowerEqNegConst ( const Expr & expr ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 1310 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, d_theoryArith, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::isEq(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::intEqIrrational	(	const Expr &	expr,
		const Theorem &	isInt
	)			`[virtual]`

Implements CVC3::ArithProofRules.

Definition at line 1330 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, d_theoryArith, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isEq(), CVC3::isIntPred(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::ratRoot(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::constPredicate ( const Expr & e ) [virtual]

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

Parameters:

e

takes e is (e0@e1) where e0 and e1 are constants

Implements CVC3::ArithProofRules.

Definition at line 1355 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::EQ, CVC3::ExprManager::falseExpr(), CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::GT, CVC3::isRational(), CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::rightMinusLeft ( const Expr & e ) [virtual]

e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}

Implements CVC3::ArithProofRules.

Definition at line 1394 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::EQ, CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::GT, CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::leftMinusRight ( const Expr & e ) [virtual]

e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=}

Implements CVC3::ArithProofRules.

Definition at line 1412 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::EQ, CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::GT, CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 1430 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::EQ, CVC3::GE, CVC3::GT, CVC3::LE, MiniSat::left(), CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), MiniSat::right(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 1449 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::divideEqnNonConst	(	const Expr &	x,
		const Expr &	y,
		const Expr &	z
	)			`[virtual]`

Implements CVC3::ArithProofRules.

Definition at line 1462 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), rat(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 1474 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Expr::getRational(), CVC3::GT, CVC3::Expr::isRational(), CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::eqToIneq ( const Expr & e ) [virtual]

x = y ==> x <= y and x >= y

Implements CVC3::ArithProofRules.

Definition at line 1631 of file arith_theorem_producer_old.cpp.

References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::geExpr(), CVC3::Expr::isEq(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::flipInequality ( const Expr & e ) [virtual]

"op1 GE|GT op2" <==> op2 LE|LT op1

Implements CVC3::ArithProofRules.

Definition at line 1653 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::isGE(), CVC3::isGT(), CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 1673 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::GE, CVC3::GT, CVC3::isGT(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::Expr::isNot(), CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::realShadow	(	const Theorem &	alphaLTt,
		const Theorem &	tLTbeta
	)			`[virtual]`

Real shadow: a <(=) t, t <(=) b ==> a <(=) b.

Implements CVC3::ArithProofRules.

Definition at line 1702 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::isLE(), CVC3::isLT(), CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 1737 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isLE(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 1769 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), grayShadow(), CVC3::isIntPred(), CVC3::isLE(), CVC3::isPlus(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 1833 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, d_theoryArith, CVC3::geExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), grayShadow(), CVC3::isIntPred(), CVC3::isLE(), CVC3::minusExpr(), CVC3::multExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), rat(), CVC3::TheoryArithOld::separateMonomial(), CVC3::Expr::toString(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 1926 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, d_theoryArith, CVC3::geExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), grayShadow(), CVC3::isIntPred(), CVC3::isLE(), CVC3::minusExpr(), CVC3::multExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), rat(), CVC3::TheoryArithOld::separateMonomial(), CVC3::Expr::toString(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::expandDarkShadow ( const Theorem & darkShadow ) [virtual]

takes a dark shadow and expands it into an inequality.

Implements CVC3::ArithProofRules.

Definition at line 2014 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isDarkShadow(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::expandGrayShadow0 ( const Theorem & g ) [virtual]

GRAY_SHADOW(v, e, c, c) ==> v=e+c.

Implements CVC3::ArithProofRules.

Definition at line 2029 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isGrayShadow(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 2054 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), grayShadow(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::splitGrayShadowSmall ( const Theorem & grayShadow ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 3456 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Rational::getInt(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::orExpr(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::expandGrayShadow ( const Theorem & g ) [virtual]

G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2.

Implements CVC3::ArithProofRules.

Definition at line 2091 of file arith_theorem_producer_old.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(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 2122 of file arith_theorem_producer_old.cpp.

References CVC3::abs(), CHECK_PROOFS, CHECK_SOUND, constRHSGrayShadow(), CVC3::TheoremProducer::d_em, CVC3::Expr::eqExpr(), CVC3::ExprManager::falseExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::GRAY_SHADOW, CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::isMult(), CVC3::Expr::isRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::orExpr(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 2187 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, d_theoryArith, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), grayShadow(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), rat(), CVC3::TheoryArithOld::separateMonomial(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Rational ArithTheoremProducerOld::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 2227 of file arith_theorem_producer_old.cpp.

References DebugAssert, and CVC3::Rational::isInteger().

Referenced by expandGrayShadowConst().

Theorem ArithTheoremProducerOld::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 2245 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isIntPred(), CVC3::isLT(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 3416 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isIntPred(), CVC3::isLT(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::intVarEqnConst	(	const Expr &	eqn,
		const Theorem &	isIntx
	)			`[virtual]`

Parameters:

	eqn	is an equation 0 = a.x or 0 = c + a.x
	isIntx	is 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 2297 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, d_theoryArith, CVC3::Expr::eqExpr(), CVC3::ExprManager::falseExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::Rational::isInteger(), CVC3::isIntPred(), CVC3::isMult(), CVC3::isPlus(), CVC3::Expr::isRational(), CVC3::isRational(), MiniSat::left(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), MiniSat::right(), CVC3::TheoryArithOld::separateMonomial(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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 2682 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, d_theoryArith, DebugAssert, CVC3::Expr::eqExpr(), CVC3::EXISTS, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::TheoryArith::intType(), CVC3::IS_INTEGER, CVC3::TheoryArithOld::isInteger(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::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.

Parameters:

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.

Parameters:

eqn

is the equation ax=t:

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

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

Implements CVC3::ArithProofRules.

Definition at line 2708 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, create_t2(), create_t3(), CVC3::TheoremProducer::d_em, d_theoryArith, CVC3::Expr::eqExpr(), CVC3::EXISTS, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::int2string(), intType(), CVC3::isDivide(), CVC3::isInt(), CVC3::Rational::isInteger(), CVC3::isIntPred(), CVC3::isPlus(), CVC3::isRational(), CVC3::Theorem::isRewrite(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), rat(), CVC3::TheoryArithOld::separateMonomial(), CVC3::Expr::setType(), CVC3::Rational::toString(), CVC3::Expr::toString(), CVC3::Theorem::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::isIntConst ( const Expr & e ) [virtual]

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

Parameters:

e

is a predicate IS_INTEGER(c) where c is a rational constant

Implements CVC3::ArithProofRules.

Definition at line 2800 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::getRational(), CVC3::isInt(), CVC3::Rational::isInteger(), CVC3::isIntPred(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::equalLeaves1 ( const Theorem & e ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 2816 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::RATIONAL_EXPR, and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::equalLeaves2 ( const Theorem & e ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 2845 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::RATIONAL_EXPR, and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::equalLeaves3 ( const Theorem & e ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 2874 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::RATIONAL_EXPR, and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::equalLeaves4 ( const Theorem & e ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 2903 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::RATIONAL_EXPR, and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::diseqToIneq ( const Theorem & diseq ) [virtual]

x /= y ==> (x < y) OR (x > y)

Used in concrete model generation

Implements CVC3::ArithProofRules.

Definition at line 2931 of file arith_theorem_producer_old.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::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::dummyTheorem ( const Expr & e ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 2950 of file arith_theorem_producer_old.cpp.

References CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::ExprManager::trueExpr().

Theorem ArithTheoremProducerOld::oneElimination ( const Expr & x ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 2955 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isMult(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::clashingBounds	(	const Theorem &	lowerBound,
		const Theorem &	upperBound
	)			`[virtual]`

Implements CVC3::ArithProofRules.

Definition at line 2976 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getRational(), CVC3::isGE(), CVC3::isGT(), CVC3::isLE(), CVC3::isLT(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::addInequalities	(	const Theorem &	thm1,
		const Theorem &	thm2
	)			`[virtual]`

Implements CVC3::ArithProofRules.

Definition at line 3016 of file arith_theorem_producer_old.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::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::plusExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::addInequalities ( const std::vector< Theorem > & thms ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 3775 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::plusExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::implyWeakerInequality	(	const Expr &	expr1,
		const Expr &	expr2
	)			`[virtual]`

Theorem ArithTheoremProducerOld::implyNegatedInequality	(	const Expr &	expr1,
		const Expr &	expr2
	)			`[virtual]`

Theorem ArithTheoremProducerOld::integerSplit	(	const Expr &	intVar,
		const Rational &	intPoint
	)			`[virtual]`

Implements CVC3::ArithProofRules.

Definition at line 3230 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::geExpr(), CVC3::IS_INTEGER, CVC3::Rational::isInteger(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::orExpr(), rat(), CVC3::Rational::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::trustedRewrite	(	const Expr &	expr1,
		const Expr &	expr2
	)			`[virtual]`

Implements CVC3::ArithProofRules.

Definition at line 3217 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::rafineStrictInteger	(	const Theorem &	isIntConstrThm,
		const Expr &	constr
	)			`[virtual]`

Theorem ArithTheoremProducerOld::simpleIneqInt	(	const Expr &	ineq,
		const Theorem &	isIntRHS
	)			`[virtual]`

Theorem ArithTheoremProducerOld::intEqualityRationalConstant	(	const Theorem &	isIntConstrThm,
		const Expr &	constr
	)			`[virtual]`

Theorem ArithTheoremProducerOld::cycleConflict ( const std::vector< Theorem > & inequalitites ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 3369 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::add(), CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::implyEqualities ( const std::vector< Theorem > & inequalities ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 3388 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::add(), CVC3::andExpr(), CVC3::Expr::eqExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::RAW_LIST, and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::implyWeakerInequalityDiffLogic	(	const std::vector< Theorem > &	antecedentThms,
		const Expr &	implied
	)			`[virtual]`

Implements CVC3::ArithProofRules.

Definition at line 3494 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::add(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::RAW_LIST, and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::implyNegatedInequalityDiffLogic	(	const std::vector< Theorem > &	antecedentThms,
		const Expr &	implied
	)			`[virtual]`

Implements CVC3::ArithProofRules.

Definition at line 3516 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::add(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::notExpr(), CVC3::RAW_LIST, and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::expandGrayShadowRewrite ( const Expr & theShadow ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 3539 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::compactNonLinearTerm ( const Expr & nonLinear ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 3567 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::Assumptions::emptyAssump(), CVC3::Rational::getInt(), CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isPow(), CVC3::isRational(), CVC3::multExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::plusExpr(), rat(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::nonLinearIneqSignSplit ( const Theorem & ineqThm ) [virtual]

Theorem ArithTheoremProducerOld::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 3742 of file arith_theorem_producer_old.cpp.

References CVC3::Assumptions::add(), grayShadow(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), rat(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::powerOfOne ( const Expr & e ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 3823 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::isPow(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::rewriteLeavesConst ( const Expr & e ) [virtual]

Member Data Documentation

TheoryArithOld* CVC3::ArithTheoremProducerOld::d_theoryArith [private]

Definition at line 32 of file arith_theorem_producer_old.h.

Referenced by canonDivide(), canonMult(), canonMultConstPlus(), canonMultMtermMterm(), darkGrayShadow2ab(), darkGrayShadow2ba(), darkShadow(), elimPower(), elimPowerConst(), eqElimIntRule(), evenPowerEqNegConst(), getLeaves(), grayShadow(), grayShadowConst(), intEqIrrational(), intType(), intVarEqnConst(), IsIntegerElim(), rafineStrictInteger(), realType(), and rewriteLeavesConst().

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