CVC3
Public Member Functions

CVC3::ArithProofRules Class Reference

#include <arith_proof_rules.h>

Inherited by CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

List of all members.

Public Member Functions


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]
virtual Theorem CVC3::ArithProofRules::uMinusToMult ( const Expr e) [pure virtual]
virtual Theorem CVC3::ArithProofRules::minusToPlus ( const Expr x,
const Expr y 
) [pure virtual]
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, CVC3::ArithTheoremProducer3, 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:
ethe expression to transform
Returns:
rewrite theorem representing the transformation

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

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

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

Canon Rules for division by constant 'd'

Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, 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, CVC3::ArithTheoremProducer3, 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, CVC3::ArithTheoremProducer3, 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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonMultMtermMterm ( const Expr e) [pure virtual]
virtual Theorem CVC3::ArithProofRules::canonPlus ( const Expr e) [pure virtual]
virtual Theorem CVC3::ArithProofRules::canonMult ( const Expr e) [pure virtual]
virtual Theorem CVC3::ArithProofRules::canonInvert ( const Expr e) [pure virtual]

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

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

virtual Theorem CVC3::ArithProofRules::canonDivide ( const Expr e) [pure virtual]
virtual Theorem CVC3::ArithProofRules::canonMultTermConst ( const Expr c,
const Expr t 
) [pure virtual]
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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::canonMultZero ( const Expr e) [pure virtual]
virtual Theorem CVC3::ArithProofRules::canonMultOne ( const Expr e) [pure virtual]
virtual Theorem CVC3::ArithProofRules::canonMultConstConst ( const Expr c1,
const Expr c2 
) [pure virtual]
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, CVC3::ArithTheoremProducer3, 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, CVC3::ArithTheoremProducer3, 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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

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

flattens the input. accepts a PLUS expr

Implemented in CVC3::ArithTheoremProducer, CVC3::ArithTheoremProducer3, 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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::multEqZero ( const Expr expr) [pure virtual]
virtual Theorem CVC3::ArithProofRules::powEqZero ( const Expr expr) [pure virtual]
virtual Theorem CVC3::ArithProofRules::elimPower ( const Expr expr) [pure virtual]
virtual Theorem CVC3::ArithProofRules::elimPowerConst ( const Expr expr,
const Rational root 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::evenPowerEqNegConst ( const Expr expr) [pure virtual]
virtual Theorem CVC3::ArithProofRules::intEqIrrational ( const Expr expr,
const Theorem isInt 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::constPredicate ( const Expr e) [pure virtual]

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

Parameters:
etakes e is (e0@e1) where e0 and e1 are constants

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

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

virtual Theorem CVC3::ArithProofRules::rightMinusLeft ( const Expr e) [pure virtual]
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, CVC3::ArithTheoremProducer3, 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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

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

virtual Theorem CVC3::ArithProofRules::multEqn ( const Expr x,
const Expr y,
const Expr z 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::divideEqnNonConst ( const Expr x,
const Expr y,
const Expr z 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::multIneqn ( const Expr e,
const Expr z 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::eqToIneq ( const Expr e) [pure virtual]
virtual Theorem CVC3::ArithProofRules::flipInequality ( const Expr e) [pure virtual]
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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), and CVC3::TheoryArith3::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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::finiteInterval ( const Theorem aLEt,
const Theorem tLEac,
const Theorem isInta,
const Theorem isIntt 
) [pure virtual]
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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::expandDarkShadow ( const Theorem darkShadow) [pure virtual]
virtual Theorem CVC3::ArithProofRules::expandGrayShadow0 ( const Theorem g) [pure virtual]
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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::assertFact(), and CVC3::TheoryArith3::assertFact().

virtual Theorem CVC3::ArithProofRules::splitGrayShadowSmall ( const Theorem g) [pure virtual]
virtual Theorem CVC3::ArithProofRules::expandGrayShadow ( const Theorem g) [pure virtual]
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, CVC3::ArithTheoremProducer3, 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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::assertFact(), and CVC3::TheoryArith3::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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

virtual Theorem CVC3::ArithProofRules::lessThanToLERewrite ( const Expr ineq,
const Theorem isIntLHS,
const Theorem isIntRHS,
bool  changeRight 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::intVarEqnConst ( const Expr eqn,
const Theorem isIntx 
) [pure virtual]
Parameters:
eqnis an equation 0 = a.x or 0 = c + a.x, where x is integer
isIntxis a proof of IS_INTEGER(x)
Returns:
the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else return the theorem 0 = c + a.x <==> false.

It also handles the special case of 0 = a.x <==> x = 0

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

virtual Theorem CVC3::ArithProofRules::IsIntegerElim ( const Theorem isIntx) [pure virtual]

IS_INTEGER(x) <=> EXISTS (y : INT) y = x where x is not already known to be an integer.

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

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

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.

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:
eqnis 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:
eqnis the equation ax=t:

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

isIntxis a Theorem deriving the integrality of the LHS variable: IS_INTEGER(x)
isIntVarsis a vector of Theorems deriving the integrality of all variables on the RHS

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

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:
eis a predicate IS_INTEGER(c) where c is a rational constant

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

virtual Theorem CVC3::ArithProofRules::equalLeaves1 ( const Theorem thm) [pure virtual]
virtual Theorem CVC3::ArithProofRules::equalLeaves2 ( const Theorem thm) [pure virtual]
virtual Theorem CVC3::ArithProofRules::equalLeaves3 ( const Theorem thm) [pure virtual]
virtual Theorem CVC3::ArithProofRules::equalLeaves4 ( const Theorem thm) [pure virtual]
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, CVC3::ArithTheoremProducer3, and CVC3::ArithTheoremProducerOld.

Referenced by CVC3::TheoryArithOld::checkSat(), and CVC3::TheoryArith3::checkSat().

virtual Theorem CVC3::ArithProofRules::dummyTheorem ( const Expr e) [pure virtual]
virtual Theorem CVC3::ArithProofRules::oneElimination ( const Expr x) [pure virtual]
virtual Theorem CVC3::ArithProofRules::clashingBounds ( const Theorem lowerBound,
const Theorem upperBound 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::addInequalities ( const Theorem thm1,
const Theorem thm2 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::addInequalities ( const std::vector< Theorem > &  thms) [pure virtual]
virtual Theorem CVC3::ArithProofRules::implyWeakerInequality ( const Expr expr1,
const Expr expr2 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::implyNegatedInequality ( const Expr expr1,
const Expr expr2 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::integerSplit ( const Expr intVar,
const Rational intPoint 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::trustedRewrite ( const Expr expr1,
const Expr expr2 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::rafineStrictInteger ( const Theorem isIntConstrThm,
const Expr constr 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::simpleIneqInt ( const Expr ineq,
const Theorem isIntRHS 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::intEqualityRationalConstant ( const Theorem isIntConstrThm,
const Expr constr 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::cycleConflict ( const std::vector< Theorem > &  inequalitites) [pure virtual]
virtual Theorem CVC3::ArithProofRules::implyEqualities ( const std::vector< Theorem > &  inequalities) [pure virtual]
virtual Theorem CVC3::ArithProofRules::implyWeakerInequalityDiffLogic ( const std::vector< Theorem > &  antecedentThms,
const Expr implied 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::implyNegatedInequalityDiffLogic ( const std::vector< Theorem > &  antecedentThms,
const Expr implied 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::expandGrayShadowRewrite ( const Expr theShadow) [pure virtual]
virtual Theorem CVC3::ArithProofRules::compactNonLinearTerm ( const Expr nonLinear) [pure virtual]
virtual Theorem CVC3::ArithProofRules::nonLinearIneqSignSplit ( const Theorem ineqThm) [pure virtual]
virtual Theorem CVC3::ArithProofRules::implyDiffLogicBothBounds ( const Expr x,
std::vector< Theorem > &  c1_le_x,
Rational  c1,
std::vector< Theorem > &  x_le_c2,
Rational  c2 
) [pure virtual]
virtual Theorem CVC3::ArithProofRules::powerOfOne ( const Expr e) [pure virtual]
Theorem ArithProofRules::rewriteLeavesConst ( const Expr e) [virtual]

Reimplemented in CVC3::ArithTheoremProducerOld.

Definition at line 3243 of file arith_theorem_producer.cpp.

References DebugAssert.

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


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