/*****************************************************************************/
/*!
* \file arith_proof_rules.h
* \brief Arithmetic proof rules
*
* Author: Vijay Ganesh, Sergey Berezin
*
* Created: Dec 13 02:09:04 GMT 2002
*
* <hr>
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
* <hr>
*
*/
/*****************************************************************************/
#ifndef _cvc3__arith_proof_rules_h_
#define _cvc3__arith_proof_rules_h_
#include <vector>
namespace CVC3 {
class Theorem;
class Expr;
class Rational;
class ArithProofRules {
public:
// Destructor
virtual ~ArithProofRules() { }
////////////////////////////////////////////////////////////////////
// Canonization rules
////////////////////////////////////////////////////////////////////
//! ==> e = 1 * e
virtual Theorem varToMult(const Expr& e) = 0;
//! ==> -(e) = (-1) * e
virtual Theorem uMinusToMult(const Expr& e) = 0;
//! ==> x - y = x + (-1) * y
virtual Theorem minusToPlus(const Expr& x, const Expr& y) = 0;
//! -(e) ==> e / (-1); takes 'e'
/*! Canon Rule for unary minus: it just converts it to division by
* -1, the result is not yet canonical:
*/
virtual Theorem canonUMinusToDivide(const Expr& e) = 0;
/**
* 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.
*
* @param e the expression to transform
* @return rewrite theorem representing the transformation
*/
virtual Theorem moveSumConstantRight(const Expr& e) = 0;
//! (c) / d ==> (c/d), takes c and d
/*! Canon Rules for division by constant 'd' */
virtual Theorem canonDivideConst(const Expr& c, const Expr& d) = 0;
//! (c * x) / d ==> (c/d) * x, takes (c*x) and d
virtual Theorem canonDivideMult(const Expr& cx, const Expr& d) = 0;
//! (+ 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
*/
virtual Theorem canonDividePlus(const Expr& e, const Expr& d) = 0;
//! x / d ==> (1/d) * x, takes x and d
virtual Theorem canonDivideVar(const Expr& e, const Expr& d) = 0;
// Canon Rules for multiplication
// TODO Deepak:
// e == t1 * t2 where t1 and t2 are canonized expressions, i.e. it can be a
// 1) Rational constant
// 2) Arithmetic Leaf (var or term from another theory)
// 3) (POW rational leaf)
// 4) (MULT rational mterm'_1 ...) where each mterm' is of type (2) or (3)
// 5) (PLUS rational sterm_1 sterm_2 ...) where each sterm is of
// type (2) or (3) or (4)
virtual Theorem canonMultMtermMterm(const Expr& e) = 0;
//! Canonize (PLUS t1 ... tn)
virtual Theorem canonPlus(const Expr & e) = 0;
//! Canonize (MULT t1 ... tn)
virtual Theorem canonMult(const Expr & e) = 0;
//! ==> 1/e = e' where e' is canonical; takes e.
virtual Theorem canonInvert(const Expr & e) = 0;
//! Canonize t1/t2
virtual Theorem canonDivide(const Expr & e) = 0;
//! t*c ==> c*t, takes constant c and term t
virtual Theorem canonMultTermConst(const Expr& c, const Expr& t) = 0;
//! t1*t2 ==> Error, takes t1 and t2 where both are non-constants
virtual Theorem canonMultTerm1Term2(const Expr& t1, const Expr& t2) = 0;
//! 0*t ==> 0, takes 0*t
virtual Theorem canonMultZero(const Expr& e) = 0;
//! 1*t ==> t, takes 1*t
virtual Theorem canonMultOne(const Expr& e) = 0;
//! c1*c2 ==> c', takes constant c1*c2
virtual Theorem canonMultConstConst(const Expr& c1, const Expr& c2) = 0;
//! c1*(c2*t) ==> c'*t, takes c1 and c2 and t
virtual Theorem
canonMultConstTerm(const Expr& c1, const Expr& c2, const Expr&t) = 0;
//! c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
virtual Theorem canonMultConstSum(const Expr& c1, const Expr& sum) = 0;
//! c^n = c' (compute the constant power expression)
virtual Theorem canonPowConst(const Expr& pow) = 0;
// Rules for addition
//! flattens the input. accepts a PLUS expr
virtual Theorem canonFlattenSum(const Expr& e) = 0;
//! combine like terms. accepts a flattened PLUS expr
virtual Theorem canonComboLikeTerms(const Expr& e) = 0;
//! e0 \@ e1 <==> true | false, where \@ is {=,<,<=,>,>=}
/*! \param e takes e is (e0\@e1) where e0 and e1 are constants
*/
virtual Theorem constPredicate(const Expr& e) = 0;
//! e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}
virtual Theorem rightMinusLeft(const Expr& e) = 0;
//! e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=}
virtual Theorem leftMinusRight(const Expr& e) = 0;
//! x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind')
virtual Theorem plusPredicate(const Expr& x,
const Expr& y, const Expr& z, int kind) = 0;
//! x = y <==> x * z = y * z, where z is a non-zero constant
virtual Theorem multEqn(const Expr& x, const Expr& y, const Expr& z) = 0;
//! 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 {<,<=,>,>=}:
*/
virtual Theorem multIneqn(const Expr& e, const Expr& z) = 0;
//! x = y ==> x <= y and x >= y
virtual Theorem eqToIneq(const Expr& e) = 0;
//! "op1 GE|GT op2" <==> op2 LE|LT op1
virtual Theorem flipInequality(const Expr& e) = 0;
//! Propagating negation over <,<=,>,>=
/*! NOT (op1 < op2) <==> (op1 >= op2)
*
* NOT (op1 <= op2) <==> (op1 > op2)
*
* NOT (op1 > op2) <==> (op1 <= op2)
*
* NOT (op1 >= op2) <==> (op1 < op2)
*/
virtual Theorem negatedInequality(const Expr& e) = 0;
//! Real shadow: a <(=) t, t <(=) b ==> a <(=) b
virtual Theorem realShadow(const Theorem& alphaLTt,
const Theorem& tLTbeta) = 0;
//! Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha
virtual Theorem realShadowEq(const Theorem& alphaLEt,
const Theorem& tLEalpha) = 0;
//! Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c)
virtual Theorem finiteInterval(const Theorem& aLEt,
const Theorem& tLEac,
const Theorem& isInta,
const Theorem& isIntt) = 0;
//! 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).
*/
virtual Theorem darkGrayShadow2ab(const Theorem& betaLEbx,
const Theorem& axLEalpha,
const Theorem& isIntAlpha,
const Theorem& isIntBeta,
const Theorem& isIntx)=0;
//! 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).
*/
virtual Theorem darkGrayShadow2ba(const Theorem& betaLEbx,
const Theorem& axLEalpha,
const Theorem& isIntAlpha,
const Theorem& isIntBeta,
const Theorem& isIntx)=0;
//! DARK_SHADOW(t1, t2) ==> t1 <= t2
virtual Theorem expandDarkShadow(const Theorem& darkShadow)=0;
//! GRAY_SHADOW(v, e, c, c) ==> v=e+c.
virtual Theorem expandGrayShadow0(const Theorem& g)=0;
// [used to be] GRAY_SHADOW(t1, t2, i) ==> t1 = t2+i OR
// GRAY_SHADOW(t1, t2, i+/-1)
//! 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).
*/
virtual Theorem splitGrayShadow(const Theorem& g)=0;
//! G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2
virtual Theorem expandGrayShadow(const Theorem& g)=0;
//! Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion]
/*! Implements three versions of the rule:
*
* \f[\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)))}\f]
*
* where the conclusion may become FALSE or without the
* GRAY_SHADOW part, depending on the values of a, c and i.
*/
virtual Theorem expandGrayShadowConst(const Theorem& g)=0;
//! |- 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 */
virtual Theorem grayShadowConst(const Theorem& g)=0;
//! 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)
*/
virtual Theorem lessThanToLE(const Theorem& less,
const Theorem& isIntLHS,
const Theorem& isIntRHS,
bool changeRight)=0;
/*! \param eqn is an equation 0 = a.x or 0 = c + a.x, where x is integer
* \param isIntx is a proof of IS_INTEGER(x)
*
* \return 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
*/
virtual Theorem intVarEqnConst(const Expr& eqn,
const Theorem& isIntx) = 0;
/*! @brief Equality elimination rule for integers:
* \f[\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}}
* \f]
* 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:
*
* \f[\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}
* \f]
*
* All the variables and coefficients are integer, and a >= 2.
*
* \param eqn is the equation
* \f[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\f]
*
*/
/*
virtual Theorem eqElimIntRule(const Expr& eqn,
const Theorem& isIntLHS,
const Theorem& isIntRHS) = 0;
//! a <=> b ==> c AND a <=> c AND b. Takes "a <=> b" and "c".
virtual Theorem cANDaIffcANDb(const Theorem& thm,
const Expr& solvedEq) = 0;
virtual Theorem substSolvedFormRule(const Expr& e1,
ExprMap<Expr>& eMap) = 0;
virtual Theorem aANDcIffbANDc(const Theorem& thm, const Expr& newEq) = 0;
*/
///////////////////////////////////////////////////////////////////////
// Alternative implementation of integer equality elimination
///////////////////////////////////////////////////////////////////////
/*! @brief
* \f[\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)}
* \f]
* 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:
*
* \f[\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}
* \f]
*
* All the variables and coefficients are integer, and a >= 2.
*
* \param eqn is the equation ax=t:
* \f[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\f]
*
* \param isIntx is a Theorem deriving the integrality of the
* LHS variable: IS_INTEGER(x)
*
* \param isIntVars is a vector of Theorems deriving the
* integrality of all variables on the RHS
*/
virtual Theorem eqElimIntRule(const Theorem& eqn,
const Theorem& isIntx,
const std::vector<Theorem>& isIntVars) = 0;
/*!
* @brief return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c
* is a constant
*
* \param e is a predicate IS_INTEGER(c) where c is a rational constant
*/
virtual Theorem isIntConst(const Expr& e) = 0;
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;
//! x /= y ==> (x < y) OR (x > y)
/*! Used in concrete model generation */
virtual Theorem diseqToIneq(const Theorem& diseq) = 0;
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;
}; // end of class ArithProofRules
} // end of namespace CVC3
#endif
syntax highlighted by Code2HTML, v. 0.9.1