#include <arith_theorem_producer.h>

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

Collaboration diagram for CVC3::ArithTheoremProducer:

[legend]

List of all members.

Public Member Functions

ArithTheoremProducer (TheoremManager *tm, TheoryArithNew *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)

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

TheoryArithNew * d_theoryArith

Detailed Description

Definition at line 32 of file arith_theorem_producer.h.

Constructor & Destructor Documentation

CVC3::ArithTheoremProducer::ArithTheoremProducer	(	TheoremManager *	tm,
		TheoryArithNew *	theoryArith
	)		`[inline]`

Constructor.

Definition at line 67 of file arith_theorem_producer.h.

Member Function Documentation

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

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

Definition at line 2252 of file arith_theorem_producer.cpp.

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

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

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

Definition at line 2192 of file arith_theorem_producer.cpp.

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

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

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

Definition at line 2211 of file arith_theorem_producer.cpp.

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

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

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

Definition at line 2231 of file arith_theorem_producer.cpp.

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

void ArithTheoremProducer::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 2268 of file arith_theorem_producer.cpp.

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

Expr ArithTheoremProducer::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 2288 of file arith_theorem_producer.cpp.

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

void ArithTheoremProducer::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 2316 of file arith_theorem_producer.cpp.

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

Expr ArithTheoremProducer::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 2336 of file arith_theorem_producer.cpp.

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

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

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

Definition at line 2261 of file arith_theorem_producer.cpp.

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

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

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

Definition at line 2353 of file arith_theorem_producer.cpp.

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

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

Create Expr from Rational (for convenience)

Definition at line 71 of file arith_theorem_producer.h.

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

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

Definition at line 72 of file arith_theorem_producer.h.

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

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

Definition at line 73 of file arith_theorem_producer.h.

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

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

Construct the dark shadow expression representing lhs <= rhs.

Definition at line 75 of file arith_theorem_producer.h.

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

Expr CVC3::ArithTheoremProducer::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 81 of file arith_theorem_producer.h.

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

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

==> e = 1 * e

Implements CVC3::ArithProofRules.

Definition at line 55 of file arith_theorem_producer.cpp.

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

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

Implements CVC3::ArithProofRules.

Definition at line 62 of file arith_theorem_producer.cpp.

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

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

Implements CVC3::ArithProofRules.

Definition at line 75 of file arith_theorem_producer.cpp.

Theorem ArithTheoremProducer::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 89 of file arith_theorem_producer.cpp.

Theorem ArithTheoremProducer::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 98 of file arith_theorem_producer.cpp.

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

Theorem ArithTheoremProducer::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 117 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isRational(), and CVC3::Expr::toString().

Theorem ArithTheoremProducer::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 145 of file arith_theorem_producer.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 ArithTheoremProducer::canonDivideVar	(	const Expr &	e,
		const Expr &	d
	)		`[virtual]`

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

Implements CVC3::ArithProofRules.

Definition at line 168 of file arith_theorem_producer.cpp.

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

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

Definition at line 2379 of file arith_theorem_producer.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 RATIONAL_EXPR.

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

Definition at line 203 of file arith_theorem_producer.cpp.

References DebugAssert, and CVC3::multExpr().

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

Definition at line 214 of file arith_theorem_producer.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, and CVC3::Expr::toString().

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

Definition at line 237 of file arith_theorem_producer.cpp.

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

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

Definition at line 256 of file arith_theorem_producer.cpp.

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

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

Definition at line 296 of file arith_theorem_producer.cpp.

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

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

Definition at line 335 of file arith_theorem_producer.cpp.

References CVC3::powExpr().

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

Definition at line 363 of file arith_theorem_producer.cpp.

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

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

Definition at line 434 of file arith_theorem_producer.cpp.

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

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

Definition at line 532 of file arith_theorem_producer.cpp.

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

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

Definition at line 551 of file arith_theorem_producer.cpp.

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

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

Implements CVC3::ArithProofRules.

Definition at line 574 of file arith_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, FatalAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::isMult(), CVC3::Expr::isRational(), CVC3::MULT, CVC3::PLUS, CVC3::POW, RATIONAL_EXPR, and CVC3::Expr::toString().

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

Canonize (PLUS t1 ... tn)

Implements CVC3::ArithProofRules.

Definition at line 746 of file arith_theorem_producer.cpp.

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

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

Definition at line 815 of file arith_theorem_producer.cpp.

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

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

Definition at line 831 of file arith_theorem_producer.cpp.

References CVC3::powExpr().

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

Definition at line 843 of file arith_theorem_producer.cpp.

References DebugAssert, CVC3::Expr::getKind(), CVC3::POW, CVC3::powExpr(), and CVC3::Expr::toString().

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

Definition at line 862 of file arith_theorem_producer.cpp.

References CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getKind(), CVC3::MULT, and CVC3::Expr::toString().

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

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

Implements CVC3::ArithProofRules.

Definition at line 885 of file arith_theorem_producer.cpp.

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

Theorem ArithTheoremProducer::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 2773 of file arith_theorem_producer.cpp.

References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::isEq(), CVC3::isIneq(), CVC3::isPlus(), CVC3::Expr::isRational(), CVC3::isRational(), CVC3::plusExpr(), MiniSat::right(), and CVC3::Expr::toString().

Theorem ArithTheoremProducer::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_producer.cpp.

References DebugAssert, CVC3::DIVIDE, CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), and CVC3::Expr::toString().

Theorem ArithTheoremProducer::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 781 of file arith_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::MULT.

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

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

Implements CVC3::ArithProofRules.

Definition at line 931 of file arith_theorem_producer.cpp.

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

Theorem ArithTheoremProducer::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 945 of file arith_theorem_producer.cpp.

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

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

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

Implements CVC3::ArithProofRules.

Definition at line 958 of file arith_theorem_producer.cpp.

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

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

Implements CVC3::ArithProofRules.

Definition at line 967 of file arith_theorem_producer.cpp.

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

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

Implements CVC3::ArithProofRules.

Definition at line 983 of file arith_theorem_producer.cpp.

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

Theorem ArithTheoremProducer::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 1001 of file arith_theorem_producer.cpp.

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

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

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

Implements CVC3::ArithProofRules.

Definition at line 1021 of file arith_theorem_producer.cpp.

References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::isRational(), CVC3::PLUS, CVC3::plusExpr(), and CVC3::Expr::toString().

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

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

Implements CVC3::ArithProofRules.

Definition at line 1043 of file arith_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Rational::isInteger(), CVC3::Expr::isRational(), CVC3::pow(), CVC3::POW, and CVC3::Expr::toString().

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

flattens the input. accepts a PLUS expr

Implements CVC3::ArithProofRules.

Definition at line 1070 of file arith_theorem_producer.cpp.

References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::PLUS, CVC3::plusExpr(), and CVC3::Expr::toString().

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

combine like terms. accepts a flattened PLUS expr

Implements CVC3::ArithProofRules.

Definition at line 1097 of file arith_theorem_producer.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::ExprMap< Data >::count(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::isMult(), CVC3::isPlus(), and CVC3::plusExpr().

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

Implements CVC3::ArithProofRules.

Definition at line 1155 of file arith_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::end(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isMult(), CVC3::Expr::isRational(), OR, and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 1178 of file arith_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isPow(), CVC3::Expr::isRational(), and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 1205 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isPow(), CVC3::Expr::orExpr(), and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 1230 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isPow(), CVC3::Expr::isRational(), CVC3::Expr::orExpr(), CVC3::pow(), and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 1254 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isPow(), CVC3::Expr::isRational(), and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 1273 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isIntPred(), CVC3::isPow(), CVC3::Expr::isRational(), CVC3::ratRoot(), and CVC3::Expr::toString().

Theorem ArithTheoremProducer::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 1300 of file arith_theorem_producer.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 ArithTheoremProducer::rightMinusLeft ( const Expr & e ) [virtual]

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

Implements CVC3::ArithProofRules.

Definition at line 1340 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, EQ, CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::GT, CVC3::LE, and CVC3::LT.

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

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

Implements CVC3::ArithProofRules.

Definition at line 1357 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, EQ, CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::GT, CVC3::LE, and CVC3::LT.

Theorem ArithTheoremProducer::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 1376 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, EQ, CVC3::GE, CVC3::GT, CVC3::LE, MiniSat::left(), CVC3::LT, and MiniSat::right().

Theorem ArithTheoremProducer::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 1395 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), and CVC3::Expr::isRational().

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

Implements CVC3::ArithProofRules.

Definition at line 1408 of file arith_theorem_producer.cpp.

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

Theorem ArithTheoremProducer::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 1420 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::GE, CVC3::geExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Expr::getRational(), CVC3::GT, CVC3::gtExpr(), CVC3::isIneq(), CVC3::Expr::isRational(), CVC3::LE, CVC3::leExpr(), CVC3::LT, CVC3::ltExpr(), and CVC3::Expr::toString().

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

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

Implements CVC3::ArithProofRules.

Definition at line 2818 of file arith_theorem_producer.cpp.

References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::geExpr(), CVC3::Expr::isEq(), CVC3::leExpr(), and CVC3::Expr::toString().

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

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

Implements CVC3::ArithProofRules.

Definition at line 1498 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::isGE(), CVC3::isGT(), CVC3::LE, CVC3::LT, and CVC3::Expr::toString().

Theorem ArithTheoremProducer::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 1518 of file arith_theorem_producer.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 ArithTheoremProducer::realShadow	(	const Theorem &	alphaLTt,
		const Theorem &	tLTbeta
	)		`[virtual]`

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

Implements CVC3::ArithProofRules.

Definition at line 1547 of file arith_theorem_producer.cpp.

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

Theorem ArithTheoremProducer::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 1582 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isLE(), and CVC3::Theorem::toString().

Theorem ArithTheoremProducer::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 1614 of file arith_theorem_producer.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 ArithTheoremProducer::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 1678 of file arith_theorem_producer.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::Expr::toString(), and CVC3::Theorem::toString().

Theorem ArithTheoremProducer::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 1769 of file arith_theorem_producer.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::Expr::toString(), and CVC3::Theorem::toString().

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

takes a dark shadow and expands it into an inequality.

Implements CVC3::ArithProofRules.

Definition at line 1854 of file arith_theorem_producer.cpp.

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

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

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

Implements CVC3::ArithProofRules.

Definition at line 1869 of file arith_theorem_producer.cpp.

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

Theorem ArithTheoremProducer::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 1894 of file arith_theorem_producer.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 ArithTheoremProducer::splitGrayShadowSmall ( const Theorem & grayShadow ) [virtual]

Implements CVC3::ArithProofRules.

Definition at line 3190 of file arith_theorem_producer.cpp.

References DebugAssert.

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

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

Implements CVC3::ArithProofRules.

Definition at line 1931 of file arith_theorem_producer.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(), and CVC3::Expr::toString().

Theorem ArithTheoremProducer::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 1962 of file arith_theorem_producer.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::Expr::isRational(), CVC3::isRational(), CVC3::Expr::orExpr(), and CVC3::Expr::toString().

Theorem ArithTheoremProducer::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 2027 of file arith_theorem_producer.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 ArithTheoremProducer::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 2067 of file arith_theorem_producer.cpp.

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

Theorem ArithTheoremProducer::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 2085 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isIntPred(), CVC3::isLT(), CVC3::leExpr(), and CVC3::Expr::toString().

Theorem ArithTheoremProducer::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 3152 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isIntPred(), CVC3::isLT(), CVC3::leExpr(), and CVC3::Expr::toString().

Theorem ArithTheoremProducer::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 2138 of file arith_theorem_producer.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::Expr::isRational(), CVC3::isRational(), MiniSat::left(), MiniSat::right(), and CVC3::Expr::toString().

Theorem ArithTheoremProducer::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 2505 of file arith_theorem_producer.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 ArithTheoremProducer::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 2531 of file arith_theorem_producer.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::Expr::toString(), CVC3::Theorem::toString(), and TRACE.

Theorem ArithTheoremProducer::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 2623 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::isInt(), CVC3::Rational::isInteger(), CVC3::isIntPred(), CVC3::isRational(), and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 2639 of file arith_theorem_producer.cpp.

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

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

Implements CVC3::ArithProofRules.

Definition at line 2668 of file arith_theorem_producer.cpp.

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

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

Implements CVC3::ArithProofRules.

Definition at line 2697 of file arith_theorem_producer.cpp.

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

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

Implements CVC3::ArithProofRules.

Definition at line 2726 of file arith_theorem_producer.cpp.

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

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

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

Used in concrete model generation

Implements CVC3::ArithProofRules.

Definition at line 2754 of file arith_theorem_producer.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::orExpr(), and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 2839 of file arith_theorem_producer.cpp.

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

Implements CVC3::ArithProofRules.

Definition at line 2844 of file arith_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::isMult(), CVC3::Expr::isRational(), and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 2865 of file arith_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Expr::getRational(), CVC3::isGE(), CVC3::isGT(), CVC3::isLE(), CVC3::isLT(), CVC3::isRational(), and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 2905 of file arith_theorem_producer.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::plusExpr(), and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 3227 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Implements CVC3::ArithProofRules.

Definition at line 2950 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::Expr::impExpr(), CVC3::isGE(), CVC3::isGT(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::isRational(), and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 3004 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getRational(), CVC3::Expr::impExpr(), CVC3::isGE(), CVC3::isGT(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::isRational(), CVC3::Expr::negate(), and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 3049 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::geExpr(), CVC3::Expr::impExpr(), CVC3::IS_INTEGER, CVC3::Rational::isInteger(), CVC3::leExpr(), CVC3::orExpr(), and CVC3::Rational::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 3036 of file arith_theorem_producer.cpp.

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

Implements CVC3::ArithProofRules.

Definition at line 3068 of file arith_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::GE, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::GT, CVC3::isIneq(), CVC3::Rational::isInteger(), CVC3::isRational(), CVC3::LE, CVC3::LT, and CVC3::Expr::toString().

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

Implements CVC3::ArithProofRules.

Definition at line 3123 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Implements CVC3::ArithProofRules.

Definition at line 3133 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Implements CVC3::ArithProofRules.

Definition at line 3138 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Implements CVC3::ArithProofRules.

Definition at line 3143 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Implements CVC3::ArithProofRules.

Definition at line 3195 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Implements CVC3::ArithProofRules.

Definition at line 3200 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Implements CVC3::ArithProofRules.

Definition at line 3205 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Implements CVC3::ArithProofRules.

Definition at line 3210 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Implements CVC3::ArithProofRules.

Definition at line 3215 of file arith_theorem_producer.cpp.

References DebugAssert.

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