CVC3::ArithProofRules Class Reference

#include <arith_proof_rules.h>

Inheritance diagram for CVC3::ArithProofRules:

[legend]List of all members.

Public Member Functions

virtual ~ArithProofRules ()
virtual Theorem varToMult (const Expr &e)=0
==> e = 1 * e
virtual Theorem uMinusToMult (const Expr &e)=0
==> -(e) = (-1) * e
virtual Theorem minusToPlus (const Expr &x, const Expr &y)=0
==> x - y = x + (-1) * y
virtual Theorem canonUMinusToDivide (const Expr &e)=0
-(e) ==> e / (-1); takes 'e'
virtual Theorem moveSumConstantRight (const Expr &e)=0
virtual Theorem canonDivideConst (const Expr &c, const Expr &d)=0
(c) / d ==> (c/d), takes c and d
virtual Theorem canonDivideMult (const Expr &cx, const Expr &d)=0
(c * x) / d ==> (c/d) * x, takes (c*x) and d
virtual Theorem canonDividePlus (const Expr &e, const Expr &d)=0
(+ c ...)/d ==> push division to all the coefficients.
virtual Theorem canonDivideVar (const Expr &e, const Expr &d)=0
x / d ==> (1/d) * x, takes x and d
virtual Theorem canonMultMtermMterm (const Expr &e)=0
virtual Theorem canonPlus (const Expr &e)=0
Canonize (PLUS t1 ... tn).
virtual Theorem canonMult (const Expr &e)=0
Canonize (MULT t1 ... tn).
virtual Theorem canonInvert (const Expr &e)=0
==> 1/e = e' where e' is canonical; takes e.
virtual Theorem canonDivide (const Expr &e)=0
Canonize t1/t2.
virtual Theorem canonMultTermConst (const Expr &c, const Expr &t)=0
t*c ==> c*t, takes constant c and term t
virtual Theorem canonMultTerm1Term2 (const Expr &t1, const Expr &t2)=0
t1*t2 ==> Error, takes t1 and t2 where both are non-constants
virtual Theorem canonMultZero (const Expr &e)=0
0*t ==> 0, takes 0*t
virtual Theorem canonMultOne (const Expr &e)=0
1*t ==> t, takes 1*t
virtual Theorem canonMultConstConst (const Expr &c1, const Expr &c2)=0
c1*c2 ==> c', takes constant c1*c2
virtual Theorem canonMultConstTerm (const Expr &c1, const Expr &c2, const Expr &t)=0
c1*(c2*t) ==> c'*t, takes c1 and c2 and t
virtual Theorem canonMultConstSum (const Expr &c1, const Expr &sum)=0
c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
virtual Theorem canonPowConst (const Expr &pow)=0
c^n = c' (compute the constant power expression)
virtual Theorem canonFlattenSum (const Expr &e)=0
flattens the input. accepts a PLUS expr
virtual Theorem canonComboLikeTerms (const Expr &e)=0
combine like terms. accepts a flattened PLUS expr
virtual Theorem constPredicate (const Expr &e)=0
e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=}
virtual Theorem rightMinusLeft (const Expr &e)=0
e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}
virtual Theorem leftMinusRight (const Expr &e)=0
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)=0
x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind')
virtual Theorem multEqn (const Expr &x, const Expr &y, const Expr &z)=0
x = y <==> x * z = y * z, where z is a non-zero constant
virtual Theorem multIneqn (const Expr &e, const Expr &z)=0
Multiplying inequation by a non-zero constant.
virtual Theorem eqToIneq (const Expr &e)=0
x = y ==> x <= y and x >= y
virtual Theorem flipInequality (const Expr &e)=0
"op1 GE|GT op2" <==> op2 LE|LT op1
virtual Theorem negatedInequality (const Expr &e)=0
Propagating negation over <,<=,>,>=.
virtual Theorem realShadow (const Theorem &alphaLTt, const Theorem &tLTbeta)=0
Real shadow: a <(=) t, t <(=) b ==> a <(=) b.
virtual Theorem realShadowEq (const Theorem &alphaLEt, const Theorem &tLEalpha)=0
Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha.
virtual Theorem finiteInterval (const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt)=0
Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c).
virtual Theorem darkGrayShadow2ab (const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0
Dark & Gray shadows when a <= b.
virtual Theorem darkGrayShadow2ba (const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0
Dark & Gray shadows when b <= a.
virtual Theorem expandDarkShadow (const Theorem &darkShadow)=0
DARK_SHADOW(t1, t2) ==> t1 <= t2.
virtual Theorem expandGrayShadow0 (const Theorem &g)=0
GRAY_SHADOW(v, e, c, c) ==> v=e+c.
virtual Theorem splitGrayShadow (const Theorem &g)=0
G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2).
virtual Theorem expandGrayShadow (const Theorem &g)=0
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2.
virtual Theorem expandGrayShadowConst (const Theorem &g)=0
Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion].
virtual Theorem grayShadowConst (const Theorem &g)=0
|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a))
virtual Theorem lessThanToLE (const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)=0
a,b: INT; a < b ==> a <= b-1 [or a+1 <= b]
virtual Theorem intVarEqnConst (const Expr &eqn, const Theorem &isIntx)=0
virtual Theorem eqElimIntRule (const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars)=0
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.
$\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.
virtual Theorem isIntConst (const Expr &e)=0
return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant
virtual Theorem equalLeaves1 (const Theorem &thm)=0
virtual Theorem equalLeaves2 (const Theorem &thm)=0
virtual Theorem equalLeaves3 (const Theorem &thm)=0
virtual Theorem equalLeaves4 (const Theorem &thm)=0
virtual Theorem diseqToIneq (const Theorem &diseq)=0
x /= y ==> (x < y) OR (x > y)
virtual Theorem dummyTheorem (const Expr &e)=0
virtual Theorem oneElimination (const Expr &x)=0
virtual Theorem clashingBounds (const Theorem &lowerBound, const Theorem &upperBound)=0
virtual Theorem addInequalities (const Theorem &thm1, const Theorem &thm2)=0
virtual Theorem implyWeakerInequality (const Expr &expr1, const Expr &expr2)=0
virtual Theorem implyNegatedInequality (const Expr &expr1, const Expr &expr2)=0
virtual Theorem integerSplit (const Expr &intVar, const Rational &intPoint)=0
virtual Theorem trustedRewrite (const Expr &expr1, const Expr &expr2)=0
virtual Theorem rafineStrictInteger (const Theorem &isIntConstrThm, const Expr &constr)=0

Detailed Description

Definition at line 33 of file arith_proof_rules.h.

Constructor & Destructor Documentation

virtual CVC3::ArithProofRules::~ArithProofRules ( ) [inline, virtual]

Definition at line 36 of file arith_proof_rules.h.

Member Function Documentation

virtual Theorem CVC3::ArithProofRules::varToMult ( const Expr & e ) [pure virtual]

==> e = 1 * e

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::uMinusToMult ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::canon(), and CVC3::TheoryArithNew::canon().

virtual Theorem CVC3::ArithProofRules::minusToPlus	(	const Expr &	x,
		const Expr &	y
	)			`[pure virtual]`

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::canon(), and CVC3::TheoryArithNew::canon().

virtual Theorem CVC3::ArithProofRules::canonUMinusToDivide ( const Expr & e ) [pure 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:

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::moveSumConstantRight ( const Expr & e ) [pure 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:

the expression to transform

Returns:: rewrite theorem representing the transformation

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonDivideConst	(	const Expr &	c,
		const Expr &	d
	)			`[pure virtual]`

Canon Rules for division by constant 'd'

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonDivideMult	(	const Expr &	cx,
		const Expr &	d
	)			`[pure virtual]`

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonDividePlus	(	const Expr &	e,
		const Expr &	d
	)			`[pure 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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonDivideVar	(	const Expr &	e,
		const Expr &	d
	)			`[pure virtual]`

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonMultMtermMterm ( const Expr & e ) [pure virtual]

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonPlus ( const Expr & e ) [pure virtual]

Canonize (PLUS t1 ... tn).

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::TheoryArithNew::getUpperBoundExplanation(), and CVC3::TheoryArithNew::rewrite().

virtual Theorem CVC3::ArithProofRules::canonMult ( const Expr & e ) [pure virtual]

Canonize (MULT t1 ... tn).

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::canon(), and CVC3::TheoryArithNew::canon().

virtual Theorem CVC3::ArithProofRules::canonInvert ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonDivide ( const Expr & e ) [pure virtual]

Canonize t1/t2.

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::canon(), and CVC3::TheoryArithNew::canon().

virtual Theorem CVC3::ArithProofRules::canonMultTermConst	(	const Expr &	c,
		const Expr &	t
	)			`[pure virtual]`

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::getLowerBoundExplanation(), and CVC3::TheoryArithNew::getUpperBoundExplanation().

virtual Theorem CVC3::ArithProofRules::canonMultTerm1Term2	(	const Expr &	t1,
		const Expr &	t2
	)			`[pure virtual]`

t1*t2 ==> Error, takes t1 and t2 where both are non-constants

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonMultZero ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonMultOne ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonMultConstConst	(	const Expr &	c1,
		const Expr &	c2
	)			`[pure virtual]`

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::getLowerBoundExplanation(), and CVC3::TheoryArithNew::getUpperBoundExplanation().

virtual Theorem CVC3::ArithProofRules::canonMultConstTerm	(	const Expr &	c1,
		const Expr &	c2,
		const Expr &	t
	)			`[pure virtual]`

c1*(c2*t) ==> c'*t, takes c1 and c2 and t

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonMultConstSum	(	const Expr &	c1,
		const Expr &	sum
	)			`[pure virtual]`

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonPowConst ( const Expr & pow ) [pure virtual]

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::canon(), and CVC3::TheoryArithNew::canon().

virtual Theorem CVC3::ArithProofRules::canonFlattenSum ( const Expr & e ) [pure virtual]

flattens the input. accepts a PLUS expr

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonComboLikeTerms ( const Expr & e ) [pure virtual]

combine like terms. accepts a flattened PLUS expr

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::constPredicate ( const Expr & e ) [pure virtual]

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

Parameters:

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::rewrite(), and CVC3::TheoryArithNew::rewrite().

virtual Theorem CVC3::ArithProofRules::rightMinusLeft ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::rewrite(), and CVC3::TheoryArithNew::rewrite().

virtual Theorem CVC3::ArithProofRules::leftMinusRight ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::plusPredicate	(	const Expr &	x,
		const Expr &	y,
		const Expr &	z,
		int	kind
	)			`[pure virtual]`

x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind')

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), and CVC3::TheoryArithNew::rewrite().

virtual Theorem CVC3::ArithProofRules::multEqn	(	const Expr &	x,
		const Expr &	y,
		const Expr &	z
	)			`[pure virtual]`

x = y <==> x * z = y * z, where z is a non-zero constant

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), and CVC3::TheoryArithNew::processSimpleIntEq().

virtual Theorem CVC3::ArithProofRules::multIneqn	(	const Expr &	e,
		const Expr &	z
	)			`[pure 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 {<,<=,>,>=}:

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::processFiniteInterval(), and CVC3::TheoryArithNew::processFiniteInterval().

virtual Theorem CVC3::ArithProofRules::eqToIneq ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::rewrite().

virtual Theorem CVC3::ArithProofRules::flipInequality ( const Expr & e ) [pure virtual]

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::rewrite().

virtual Theorem CVC3::ArithProofRules::negatedInequality ( const Expr & e ) [pure virtual]

Propagating negation over <,<=,>,>=.

NOT (op1 < op2) <==> (op1 >= op2)

NOT (op1 <= op2) <==> (op1 > op2)

NOT (op1 > op2) <==> (op1 <= op2)

NOT (op1 >= op2) <==> (op1 < op2)

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithOld::rewrite(), and CVC3::TheoryArithNew::rewrite().

virtual Theorem CVC3::ArithProofRules::realShadow	(	const Theorem &	alphaLTt,
		const Theorem &	tLTbeta
	)			`[pure virtual]`

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::normalizeProjectIneqs().

virtual Theorem CVC3::ArithProofRules::realShadowEq	(	const Theorem &	alphaLEt,
		const Theorem &	tLEalpha
	)			`[pure virtual]`

Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha.

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::normalizeProjectIneqs().

virtual Theorem CVC3::ArithProofRules::finiteInterval	(	const Theorem &	aLEt,
		const Theorem &	tLEac,
		const Theorem &	isInta,
		const Theorem &	isIntt
	)			`[pure virtual]`

Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c).

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::processFiniteInterval(), and CVC3::TheoryArithNew::processFiniteInterval().

virtual Theorem CVC3::ArithProofRules::darkGrayShadow2ab	(	const Theorem &	betaLEbx,
		const Theorem &	axLEalpha,
		const Theorem &	isIntAlpha,
		const Theorem &	isIntBeta,
		const Theorem &	isIntx
	)			`[pure 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).

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::normalizeProjectIneqs().

virtual Theorem CVC3::ArithProofRules::darkGrayShadow2ba	(	const Theorem &	betaLEbx,
		const Theorem &	axLEalpha,
		const Theorem &	isIntAlpha,
		const Theorem &	isIntBeta,
		const Theorem &	isIntx
	)			`[pure 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).

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::normalizeProjectIneqs().

virtual Theorem CVC3::ArithProofRules::expandDarkShadow ( const Theorem & darkShadow ) [pure virtual]

DARK_SHADOW(t1, t2) ==> t1 <= t2.

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::assertFact().

virtual Theorem CVC3::ArithProofRules::expandGrayShadow0 ( const Theorem & g ) [pure virtual]

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::assertFact().

virtual Theorem CVC3::ArithProofRules::splitGrayShadow ( const Theorem & g ) [pure 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).

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::assertFact().

virtual Theorem CVC3::ArithProofRules::expandGrayShadow ( const Theorem & g ) [pure virtual]

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::assertFact().

virtual Theorem CVC3::ArithProofRules::expandGrayShadowConst ( const Theorem & g ) [pure 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.

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::grayShadowConst ( const Theorem & g ) [pure 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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::assertFact().

virtual Theorem CVC3::ArithProofRules::lessThanToLE	(	const Theorem &	less,
		const Theorem &	isIntLHS,
		const Theorem &	isIntRHS,
		bool	changeRight
	)			`[pure virtual]`

a,b: INT; a < b ==> a <= b-1 [or a+1 <= b]

Takes a Theorem(\alpha < \beta) and returns Theorem(\alpha < \beta <==> \alpha <= \beta -1) or Theorem(\alpha < \beta <==> \alpha + 1 <= \beta), depending on which side must be changed (changeRight flag)

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::projectInequalities().

virtual Theorem CVC3::ArithProofRules::intVarEqnConst	(	const Expr &	eqn,
		const Theorem &	isIntx
	)			`[pure virtual]`

Parameters:

	eqn	is an equation 0 = a.x or 0 = c + a.x, where x is integer
	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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::processSimpleIntEq(), and CVC3::TheoryArithNew::processSimpleIntEq().

virtual Theorem CVC3::ArithProofRules::eqElimIntRule	(	const Theorem &	eqn,
		const Theorem &	isIntx,
		const std::vector< Theorem > &	isIntVars
	)			`[pure 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.

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::processSimpleIntEq(), and CVC3::TheoryArithNew::processSimpleIntEq().

virtual Theorem CVC3::ArithProofRules::isIntConst ( const Expr & e ) [pure virtual]

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

Parameters:

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::equalLeaves1 ( const Theorem & thm ) [pure virtual]

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::equalLeaves2 ( const Theorem & thm ) [pure virtual]

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::equalLeaves3 ( const Theorem & thm ) [pure virtual]

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::equalLeaves4 ( const Theorem & thm ) [pure virtual]

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::diseqToIneq ( const Theorem & diseq ) [pure virtual]

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

Used in concrete model generation

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::checkSat().

virtual Theorem CVC3::ArithProofRules::dummyTheorem ( const Expr & e ) [pure virtual]

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::rewrite().

virtual Theorem CVC3::ArithProofRules::oneElimination ( const Expr & x ) [pure virtual]

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::assertFact(), and CVC3::TheoryArithNew::pivotRule().

virtual Theorem CVC3::ArithProofRules::clashingBounds	(	const Theorem &	lowerBound,
		const Theorem &	upperBound
	)			`[pure virtual]`

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::assertLower(), CVC3::TheoryArithNew::assertUpper(), CVC3::TheoryArithNew::getLowerBoundExplanation(), and CVC3::TheoryArithNew::getUpperBoundExplanation().

virtual Theorem CVC3::ArithProofRules::addInequalities	(	const Theorem &	thm1,
		const Theorem &	thm2
	)			`[pure virtual]`

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::getLowerBoundExplanation(), and CVC3::TheoryArithNew::getUpperBoundExplanation().

virtual Theorem CVC3::ArithProofRules::implyWeakerInequality	(	const Expr &	expr1,
		const Expr &	expr2
	)			`[pure virtual]`

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::propagateTheory().

virtual Theorem CVC3::ArithProofRules::implyNegatedInequality	(	const Expr &	expr1,
		const Expr &	expr2
	)			`[pure virtual]`

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::propagateTheory().

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

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::checkSatInteger().

virtual Theorem CVC3::ArithProofRules::trustedRewrite	(	const Expr &	expr1,
		const Expr &	expr2
	)			`[pure virtual]`

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::rafineStrictInteger	(	const Theorem &	isIntConstrThm,
		const Expr &	constr
	)			`[pure virtual]`

Implemented in CVC3::ArithTheoremProducer, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithNew::rafineIntegerConstraints().

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

arith_proof_rules.h

Generated on Tue Jul 3 14:41:22 2007 for CVC3 by

1.5.1