1 /*****************************************************************************/ 2 /*! 3 * \file arith_proof_rules.h 4 * \brief Arithmetic proof rules 5 * 6 * Author: Vijay Ganesh, Sergey Berezin 7 * 8 * Created: Dec 13 02:09:04 GMT 2002 9 * 10 * <hr> 11 * 12 * License to use, copy, modify, sell and/or distribute this software 13 * and its documentation for any purpose is hereby granted without 14 * royalty, subject to the terms and conditions defined in the \ref 15 * LICENSE file provided with this distribution. 16 * 17 * <hr> 18 * 19 */ 20 /*****************************************************************************/ 21 22 #ifndef _cvc3__arith_proof_rules_h_ 23 #define _cvc3__arith_proof_rules_h_ 24 25 #include <vector> 26 27 namespace CVC3 { 28 29 class Theorem; 30 class Expr; 31 class Rational; 32 33 class ArithProofRules { 34 public: 35 // Destructor ~ArithProofRules()36 virtual ~ArithProofRules() { } 37 38 //////////////////////////////////////////////////////////////////// 39 // Canonization rules 40 //////////////////////////////////////////////////////////////////// 41 42 //! ==> e = 1 * e 43 virtual Theorem varToMult(const Expr& e) = 0; 44 45 //! ==> -(e) = (-1) * e 46 virtual Theorem uMinusToMult(const Expr& e) = 0; 47 48 //! ==> x - y = x + (-1) * y 49 virtual Theorem minusToPlus(const Expr& x, const Expr& y) = 0; 50 51 //! -(e) ==> e / (-1); takes 'e' 52 /*! Canon Rule for unary minus: it just converts it to division by 53 * -1, the result is not yet canonical: 54 */ 55 virtual Theorem canonUMinusToDivide(const Expr& e) = 0; 56 57 /** 58 * Transform e = (SUM r t1 ... tn) @ 0 into (SUM t1 ... tn) @ -r. The first 59 * sum term (r) must be a rational and t1 ... tn terms must be canonised. 60 * 61 * @param e the expression to transform 62 * @return rewrite theorem representing the transformation 63 */ 64 virtual Theorem moveSumConstantRight(const Expr& e) = 0; 65 66 //! (c) / d ==> (c/d), takes c and d 67 /*! Canon Rules for division by constant 'd' */ 68 virtual Theorem canonDivideConst(const Expr& c, const Expr& d) = 0; 69 //! (c * x) / d ==> (c/d) * x, takes (c*x) and d 70 virtual Theorem canonDivideMult(const Expr& cx, const Expr& d) = 0; 71 //! (+ c ...)/d ==> push division to all the coefficients. 72 /*! The result is not canonical, but canonizing the summands will 73 * make it canonical. 74 * Takes (+ c ...) and d 75 */ 76 virtual Theorem canonDividePlus(const Expr& e, const Expr& d) = 0; 77 //! x / d ==> (1/d) * x, takes x and d 78 virtual Theorem canonDivideVar(const Expr& e, const Expr& d) = 0; 79 80 // Canon Rules for multiplication 81 82 // TODO Deepak: 83 // e == t1 * t2 where t1 and t2 are canonized expressions, i.e. it can be a 84 // 1) Rational constant 85 // 2) Arithmetic Leaf (var or term from another theory) 86 // 3) (POW rational leaf) 87 // 4) (MULT rational mterm'_1 ...) where each mterm' is of type (2) or (3) 88 // 5) (PLUS rational sterm_1 sterm_2 ...) where each sterm is of 89 // type (2) or (3) or (4) 90 virtual Theorem canonMultMtermMterm(const Expr& e) = 0; 91 //! Canonize (PLUS t1 ... tn) 92 virtual Theorem canonPlus(const Expr & e) = 0; 93 //! Canonize (MULT t1 ... tn) 94 virtual Theorem canonMult(const Expr & e) = 0; 95 //! ==> 1/e = e' where e' is canonical; takes e. 96 virtual Theorem canonInvert(const Expr & e) = 0; 97 //! Canonize t1/t2 98 virtual Theorem canonDivide(const Expr & e) = 0; 99 100 //! t*c ==> c*t, takes constant c and term t 101 virtual Theorem canonMultTermConst(const Expr& c, const Expr& t) = 0; 102 //! t1*t2 ==> Error, takes t1 and t2 where both are non-constants 103 virtual Theorem canonMultTerm1Term2(const Expr& t1, const Expr& t2) = 0; 104 //! 0*t ==> 0, takes 0*t 105 virtual Theorem canonMultZero(const Expr& e) = 0; 106 //! 1*t ==> t, takes 1*t 107 virtual Theorem canonMultOne(const Expr& e) = 0; 108 //! c1*c2 ==> c', takes constant c1*c2 109 virtual Theorem canonMultConstConst(const Expr& c1, const Expr& c2) = 0; 110 //! c1*(c2*t) ==> c'*t, takes c1 and c2 and t 111 virtual Theorem 112 canonMultConstTerm(const Expr& c1, const Expr& c2, const Expr&t) = 0; 113 //! c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum 114 virtual Theorem canonMultConstSum(const Expr& c1, const Expr& sum) = 0; 115 //! c^n = c' (compute the constant power expression) 116 virtual Theorem canonPowConst(const Expr& pow) = 0; 117 118 // Rules for addition 119 //! flattens the input. accepts a PLUS expr 120 virtual Theorem canonFlattenSum(const Expr& e) = 0; 121 122 //! combine like terms. accepts a flattened PLUS expr 123 virtual Theorem canonComboLikeTerms(const Expr& e) = 0; 124 125 // 0 = (* e1 e2 ...) <=> 0 = e1 OR 0 = e2 OR ... 126 virtual Theorem multEqZero(const Expr& expr) = 0; 127 128 // 0 = (^ c x) <=> false if c <=0 129 // <=> 0 = x if c > 0 130 virtual Theorem powEqZero(const Expr& expr) = 0; 131 132 // x^n = y^n <=> x = y (if n is odd) 133 // x^n = y^n <=> x = y OR x = -y (if n is even) 134 virtual Theorem elimPower(const Expr& expr) = 0; 135 136 // x^n = c <=> x = root (if n is odd and root^n = c) 137 // x^n = c <=> x = root OR x = -root (if n is even and root^n = c) 138 virtual Theorem elimPowerConst(const Expr& expr, const Rational& root) = 0; 139 140 // x^n = c <=> false (if n is even and c is negative) 141 virtual Theorem evenPowerEqNegConst(const Expr& expr) = 0; 142 143 // x^n = c <=> false (if x is an integer and c is not a perfect n power) 144 virtual Theorem intEqIrrational(const Expr& expr, const Theorem& isInt) = 0; 145 146 //! e0 \@ e1 <==> true | false, where \@ is {=,<,<=,>,>=} 147 /*! \param e takes e is (e0\@e1) where e0 and e1 are constants 148 */ 149 virtual Theorem constPredicate(const Expr& e) = 0; 150 151 //! e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=} 152 virtual Theorem rightMinusLeft(const Expr& e) = 0; 153 154 //! e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=} 155 virtual Theorem leftMinusRight(const Expr& e) = 0; 156 157 //! x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind') 158 virtual Theorem plusPredicate(const Expr& x, 159 const Expr& y, const Expr& z, int kind) = 0; 160 161 //! x = y <==> x * z = y * z, where z is a non-zero constant 162 virtual Theorem multEqn(const Expr& x, const Expr& y, const Expr& z) = 0; 163 164 // x = y <==> z=0 OR x * 1/z = y * 1/z 165 virtual Theorem divideEqnNonConst(const Expr& x, const Expr& y, const Expr& z) = 0; 166 167 //! Multiplying inequation by a non-zero constant 168 /*! 169 * z>0 ==> e[0] @ e[1] <==> e[0]*z @ e[1]*z 170 * 171 * z<0 ==> e[0] @ e[1] <==> e[1]*z @ e[0]*z 172 * 173 * for @ in {<,<=,>,>=}: 174 */ 175 virtual Theorem multIneqn(const Expr& e, const Expr& z) = 0; 176 177 //! x = y ==> x <= y and x >= y 178 virtual Theorem eqToIneq(const Expr& e) = 0; 179 180 //! "op1 GE|GT op2" <==> op2 LE|LT op1 181 virtual Theorem flipInequality(const Expr& e) = 0; 182 183 //! Propagating negation over <,<=,>,>= 184 /*! NOT (op1 < op2) <==> (op1 >= op2) 185 * 186 * NOT (op1 <= op2) <==> (op1 > op2) 187 * 188 * NOT (op1 > op2) <==> (op1 <= op2) 189 * 190 * NOT (op1 >= op2) <==> (op1 < op2) 191 */ 192 virtual Theorem negatedInequality(const Expr& e) = 0; 193 194 //! Real shadow: a <(=) t, t <(=) b ==> a <(=) b 195 virtual Theorem realShadow(const Theorem& alphaLTt, 196 const Theorem& tLTbeta) = 0; 197 198 //! Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha 199 virtual Theorem realShadowEq(const Theorem& alphaLEt, 200 const Theorem& tLEalpha) = 0; 201 202 //! Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c) 203 virtual Theorem finiteInterval(const Theorem& aLEt, 204 const Theorem& tLEac, 205 const Theorem& isInta, 206 const Theorem& isIntt) = 0; 207 208 //! Dark & Gray shadows when a <= b 209 /*! takes two integer ineqs (i.e. all vars are ints) 210 * "|- beta <= b.x" and "|- a.x <= alpha" and checks if "1 <= a <= b" 211 * and returns (D or G) and (!D or !G), where 212 * D = Dark_Shadow(ab-1, b.alpha - a.beta), 213 * G = Gray_Shadow(a.x, alpha, -(a-1), 0). 214 */ 215 virtual Theorem darkGrayShadow2ab(const Theorem& betaLEbx, 216 const Theorem& axLEalpha, 217 const Theorem& isIntAlpha, 218 const Theorem& isIntBeta, 219 const Theorem& isIntx)=0; 220 221 //! Dark & Gray shadows when b <= a 222 /*! takes two integer ineqs (i.e. all vars are ints) 223 * "|- beta <= b.x" and "|- a.x <= alpha" and checks if "1 <= b < a" 224 * and returns (D or G) and (!D or !G), where 225 * D = Dark_Shadow(ab-1, b.alpha - a.beta), 226 * G = Gray_Shadow(b.x, beta, 0, b-1). 227 */ 228 virtual Theorem darkGrayShadow2ba(const Theorem& betaLEbx, 229 const Theorem& axLEalpha, 230 const Theorem& isIntAlpha, 231 const Theorem& isIntBeta, 232 const Theorem& isIntx)=0; 233 234 //! DARK_SHADOW(t1, t2) ==> t1 <= t2 235 virtual Theorem expandDarkShadow(const Theorem& darkShadow)=0; 236 237 //! GRAY_SHADOW(v, e, c, c) ==> v=e+c. 238 virtual Theorem expandGrayShadow0(const Theorem& g)=0; 239 240 // [used to be] GRAY_SHADOW(t1, t2, i) ==> t1 = t2+i OR 241 // GRAY_SHADOW(t1, t2, i+/-1) 242 243 //! G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2) 244 /*! Here G1 = G(x,e,c1,c), 245 * G2 = G(x,e,c+1,c2), 246 * and c = floor((c1+c2)/2). 247 */ 248 virtual Theorem splitGrayShadow(const Theorem& g)=0; 249 250 251 virtual Theorem splitGrayShadowSmall(const Theorem& g)=0; 252 253 //! G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2 254 virtual Theorem expandGrayShadow(const Theorem& g)=0; 255 256 //! Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion] 257 /*! Implements three versions of the rule: 258 * 259 * \f[\frac{\mathrm{GRAY\_SHADOW}(ax,c,c1,c2)} 260 * {ax = c + i - \mathrm{sign}(i)\cdot j(c,i,a) 261 * \lor GRAY\_SHADOW(ax, c, i-\mathrm{sign}(i)\cdot (a+j(c,i,a)))}\f] 262 * 263 * where the conclusion may become FALSE or without the 264 * GRAY_SHADOW part, depending on the values of a, c and i. 265 */ 266 virtual Theorem expandGrayShadowConst(const Theorem& g)=0; 267 //! |- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a)) 268 /*! In the case the new c1 > c2, return |- FALSE */ 269 virtual Theorem grayShadowConst(const Theorem& g)=0; 270 271 //! a,b: INT; a < b ==> a <= b-1 [or a+1 <= b] 272 /*! Takes a Theorem(\\alpha < \\beta) and returns 273 * Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1) 274 * or Theorem(\\alpha < \\beta <==> \\alpha + 1 <= \\beta), 275 * depending on which side must be changed (changeRight flag) 276 */ 277 virtual Theorem lessThanToLE(const Theorem& less, 278 const Theorem& isIntLHS, 279 const Theorem& isIntRHS, 280 bool changeRight)=0; 281 282 virtual Theorem lessThanToLERewrite(const Expr& ineq, const Theorem& isIntLHS, 283 const Theorem& isIntRHS, bool changeRight) = 0; 284 285 286 /*! \param eqn is an equation 0 = a.x or 0 = c + a.x, where x is integer 287 * \param isIntx is a proof of IS_INTEGER(x) 288 * 289 * \return the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else 290 * return the theorem 0 = c + a.x <==> false. 291 * 292 * It also handles the special case of 0 = a.x <==> x = 0 293 */ 294 virtual Theorem intVarEqnConst(const Expr& eqn, 295 const Theorem& isIntx) = 0; 296 /*! IS_INTEGER(x) <=> EXISTS (y : INT) y = x 297 * where x is not already known to be an integer. 298 */ 299 virtual Theorem IsIntegerElim(const Theorem& isIntx) = 0; 300 301 /*! @brief Equality elimination rule for integers: 302 * \f[\frac{\mathsf{int}(a\cdot x)\quad 303 * \mathsf{int}(C+\sum_{i=1}^{n}a_{i}\cdot x_{i})} 304 * {a\cdot x=C+\sum_{i=1}^{n}a_{i}\cdot x_{i} 305 * \quad\equiv\quad x=t_{2}\wedge 0=t_{3}} 306 * \f] 307 * See the detailed description for explanations. 308 * 309 * This rule implements a step in the iterative algorithm for 310 * eliminating integer equality. The terms in the rule are 311 * defined as follows: 312 * 313 * \f[\begin{array}{rcl} 314 * t_{2} & = & 315 * -(C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) 316 * \cdot x_{i}-m\cdot\sigma(t))\\ & & \\ 317 * t_{3} & = & 318 * \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i} 319 * -a\cdot\sigma(t)\\ & & \\ 320 * t & = & 321 * (C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) 322 * \cdot x_{i}+x)/m\\ & & \\ 323 * m & = & a+1\\ & & \\ 324 * \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m} 325 * +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\ m\\ & & \\ 326 * i\ \mathbf{mod}\ m & = & i-m\left\lfloor\frac{i}{m} 327 * +\frac{1}{2}\right\rfloor 328 * \end{array} 329 * \f] 330 * 331 * All the variables and coefficients are integer, and a >= 2. 332 * 333 * \param eqn is the equation 334 * \f[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\f] 335 * 336 */ 337 338 /* 339 virtual Theorem eqElimIntRule(const Expr& eqn, 340 const Theorem& isIntLHS, 341 const Theorem& isIntRHS) = 0; 342 //! a <=> b ==> c AND a <=> c AND b. Takes "a <=> b" and "c". 343 virtual Theorem cANDaIffcANDb(const Theorem& thm, 344 const Expr& solvedEq) = 0; 345 virtual Theorem substSolvedFormRule(const Expr& e1, 346 ExprMap<Expr>& eMap) = 0; 347 virtual Theorem aANDcIffbANDc(const Theorem& thm, const Expr& newEq) = 0; 348 */ 349 350 /////////////////////////////////////////////////////////////////////// 351 // Alternative implementation of integer equality elimination 352 /////////////////////////////////////////////////////////////////////// 353 354 /*! @brief 355 * \f[\frac{\Gamma\models ax=t\quad 356 * \Gamma'\models\mathsf{int}(x)\quad 357 * \{\Gamma_i\models\mathsf{int}(x_i) | x_i\mbox{ is var in }t\}} 358 * {\Gamma,\Gamma',\bigcup_i\Gamma_i\models 359 * \exists (y:\mathrm{int}).\ x=t_2(y)\wedge 0=t_3(y)} 360 * \f] 361 * See detailed docs for more information. 362 * 363 * This rule implements a step in the iterative algorithm for 364 * eliminating integer equality. The terms in the rule are 365 * defined as follows: 366 * 367 * \f[\begin{array}{rcl} 368 * t & = & C+\sum_{i=1}^na_{i}\cdot x_{i}\\ 369 * t_{2}(y) & = & 370 * -(C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) 371 * \cdot x_{i}-m\cdot y)\\ & & \\ 372 * t_{3}(y) & = & 373 * \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i} 374 * -a\cdot y\\ & & \\ 375 * m & = & a+1\\ & & \\ 376 * \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m} 377 * +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\ m\\ & & \\ 378 * i\ \mathbf{mod}\ m & = & i-m\left\lfloor\frac{i}{m} 379 * +\frac{1}{2}\right\rfloor 380 * \end{array} 381 * \f] 382 * 383 * All the variables and coefficients are integer, and a >= 2. 384 * 385 * \param eqn is the equation ax=t: 386 * \f[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\f] 387 * 388 * \param isIntx is a Theorem deriving the integrality of the 389 * LHS variable: IS_INTEGER(x) 390 * 391 * \param isIntVars is a vector of Theorems deriving the 392 * integrality of all variables on the RHS 393 */ 394 virtual Theorem eqElimIntRule(const Theorem& eqn, 395 const Theorem& isIntx, 396 const std::vector<Theorem>& isIntVars) = 0; 397 398 /*! 399 * @brief return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c 400 * is a constant 401 * 402 * \param e is a predicate IS_INTEGER(c) where c is a rational constant 403 */ 404 virtual Theorem isIntConst(const Expr& e) = 0; 405 406 virtual Theorem equalLeaves1(const Theorem& thm) = 0; 407 virtual Theorem equalLeaves2(const Theorem& thm) = 0; 408 virtual Theorem equalLeaves3(const Theorem& thm) = 0; 409 virtual Theorem equalLeaves4(const Theorem& thm) = 0; 410 411 //! x /= y ==> (x < y) OR (x > y) 412 /*! Used in concrete model generation */ 413 virtual Theorem diseqToIneq(const Theorem& diseq) = 0; 414 415 virtual Theorem dummyTheorem(const Expr& e) = 0; 416 417 virtual Theorem oneElimination(const Expr& x) = 0; 418 419 virtual Theorem clashingBounds(const Theorem& lowerBound, const Theorem& upperBound) = 0; 420 421 virtual Theorem addInequalities(const Theorem& thm1, const Theorem& thm2) = 0; 422 virtual Theorem addInequalities(const std::vector<Theorem>& thms) = 0; 423 424 virtual Theorem implyWeakerInequality(const Expr& expr1, const Expr& expr2) = 0; 425 426 virtual Theorem implyNegatedInequality(const Expr& expr1, const Expr& expr2) = 0; 427 428 virtual Theorem integerSplit(const Expr& intVar, const Rational& intPoint) = 0; 429 430 virtual Theorem trustedRewrite(const Expr& expr1, const Expr& expr2) = 0; 431 432 virtual Theorem rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr) = 0; 433 434 virtual Theorem simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS) = 0; 435 436 virtual Theorem intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr) = 0; 437 438 virtual Theorem cycleConflict(const std::vector<Theorem>& inequalitites) = 0; 439 440 virtual Theorem implyEqualities(const std::vector<Theorem>& inequalities) = 0; 441 442 virtual Theorem implyWeakerInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) = 0; 443 444 virtual Theorem implyNegatedInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) = 0; 445 446 virtual Theorem expandGrayShadowRewrite(const Expr& theShadow) = 0; 447 448 virtual Theorem compactNonLinearTerm(const Expr& nonLinear) = 0; 449 450 virtual Theorem nonLinearIneqSignSplit(const Theorem& ineqThm) = 0; 451 452 virtual Theorem implyDiffLogicBothBounds(const Expr& x, std::vector<Theorem>& c1_le_x, Rational c1, 453 std::vector<Theorem>& x_le_c2, Rational c2) = 0; 454 455 virtual Theorem powerOfOne(const Expr& e) = 0; 456 457 virtual Theorem rewriteLeavesConst(const Expr& e); 458 459 }; // end of class ArithProofRules 460 } // end of namespace CVC3 461 462 #endif 463