CVC3  2.4.1
arith_theorem_producer3.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file arith_theorem_producer.cpp
4  *
5  * Author: Vijay Ganesh, Sergey Berezin
6  *
7  * Created: Dec 13 02:09:04 GMT 2002
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 // CLASS: ArithProofRules
21 //
22 // AUTHOR: Sergey Berezin, 12/11/2002
23 // AUTHOR: Vijay Ganesh, 05/30/2003
24 //
25 // Description: TRUSTED implementation of arithmetic proof rules.
26 //
27 ///////////////////////////////////////////////////////////////////////////////
28 
29 // This code is trusted
30 #define _CVC3_TRUSTED_
31 
33 #include "theory_core.h"
34 #include "theory_arith3.h"
35 
36 using namespace std;
37 using namespace CVC3;
38 
39 ////////////////////////////////////////////////////////////////////
40 // TheoryArith: trusted method for creating ArithTheoremProducer3
41 ////////////////////////////////////////////////////////////////////
42 
43 ArithProofRules* TheoryArith3::createProofRules3() {
44  return new ArithTheoremProducer3(theoryCore()->getTM(), this);
45 }
46 
47 ////////////////////////////////////////////////////////////////////
48 // Canonization rules
49 ////////////////////////////////////////////////////////////////////
50 
51 
52 #define CLASS_NAME "ArithTheoremProducer3"
53 
54 
55 // Rule for variables: e == 1 * e
56 Theorem ArithTheoremProducer3::varToMult(const Expr& e) {
57  Proof pf;
58  if(withProof()) pf = newPf("var_to_mult", e);
59  return newRWTheorem(e, (rat(1) * e), Assumptions::emptyAssump(), pf);
60 }
61 
62 
63 // Rule for unary minus: -e == (-1) * e
64 Theorem ArithTheoremProducer3::uMinusToMult(const Expr& e) {
65  Proof pf;
66  if(withProof()) pf = newPf("uminus_to_mult", e);
67  return newRWTheorem((-e), (rat(-1) * e), Assumptions::emptyAssump(), pf);
68 }
69 
70 
71 // ==> x - y = x + (-1) * y
72 Theorem ArithTheoremProducer3::minusToPlus(const Expr& x, const Expr& y)
73 {
74  Proof pf;
75  if(withProof()) pf = newPf("minus_to_plus", x, y);
76  return newRWTheorem((x-y), (x + (rat(-1) * y)), Assumptions::emptyAssump(), pf);
77 }
78 
79 
80 // Rule for unary minus: -e == e/(-1)
81 // This is to reduce the number of almost identical rules for uminus and div
82 Theorem ArithTheoremProducer3::canonUMinusToDivide(const Expr& e) {
83  Proof pf;
84  if(withProof()) pf = newPf("canon_uminus", e);
85  return newRWTheorem((-e), (e / rat(-1)), Assumptions::emptyAssump(), pf);
86 }
87 
88 // Rules for division by constant
89 
90 // (c)/(d) ==> (c/d). When d==0, c/0 = 0 (our total extension).
91 Theorem ArithTheoremProducer3::canonDivideConst(const Expr& c,
92  const Expr& d) {
93  // Make sure c and d are a const
94  if(CHECK_PROOFS) {
96  CLASS_NAME "::canonDivideConst:\n c not a constant: "
97  + c.toString());
99  CLASS_NAME "::canonDivideConst:\n d not a constant: "
100  + d.toString());
101  }
102  Proof pf;
103  if(withProof())
104  pf = newPf("canon_divide_const", c, d, d_hole);
105  const Rational& dr = d.getRational();
106  return newRWTheorem((c/d), (rat(dr==0? 0 : (c.getRational()/dr))), Assumptions::emptyAssump(), pf);
107 }
108 
109 // (c * x)/d ==> (c/d) * x, takes (c*x) and d
110 Theorem ArithTheoremProducer3::canonDivideMult(const Expr& cx,
111  const Expr& d) {
112  // Check the format of c*x
113  if(CHECK_PROOFS) {
114  CHECK_SOUND(isMult(cx) && isRational(cx[0]),
115  CLASS_NAME "::canonDivideMult:\n "
116  "Not a (c * x) expression: "
117  + cx.toString());
119  CLASS_NAME "::canonDivideMult:\n "
120  "d is not a constant: " + d.toString());
121  }
122  const Rational& dr = d.getRational();
123  Rational cdr(dr==0? 0 : (cx[0].getRational()/dr));
124  Expr cd(rat(cdr));
125  Proof pf;
126  if(withProof())
127  pf = newPf("canon_divide_mult", cx[0], cx[1], d);
128  // (c/d) may be == 1, so we also need to canonize 1*x to x
129  if(cdr == 1)
130  return newRWTheorem((cx/d), (cx[1]), Assumptions::emptyAssump(), pf);
131  else if(cdr == 0) // c/0 == 0 case
132  return newRWTheorem((cx/d), cd, Assumptions::emptyAssump(), pf);
133  else
134  return newRWTheorem((cx/d), (cd*cx[1]), Assumptions::emptyAssump(), pf);
135 }
136 
137 // (+ t1 ... tn)/d ==> (+ (t1/d) ... (tn/d))
138 Theorem ArithTheoremProducer3::canonDividePlus(const Expr& sum, const Expr& d) {
139  if(CHECK_PROOFS) {
140  CHECK_SOUND(isPlus(sum) && sum.arity() >= 2 && isRational(sum[0]),
141  CLASS_NAME "::canonUMinusPlus:\n "
142  "Expr is not a canonical sum: "
143  + sum.toString());
145  CLASS_NAME "::canonUMinusPlus:\n "
146  "d is not a const: " + d.toString());
147  }
148  // First, propagate '/d' down to the args
149  Proof pf;
150  if(withProof())
151  pf = newPf("canon_divide_plus", rat(sum.arity()),
152  sum.begin(), sum.end());
153  vector<Expr> newKids;
154  for(Expr::iterator i=sum.begin(), iend=sum.end(); i!=iend; ++i)
155  newKids.push_back((*i)/d);
156  // (+ t1 ... tn)/d == (+ (t1/d) ... (tn/d))
157  return newRWTheorem((sum/d), (plusExpr(newKids)), Assumptions::emptyAssump(), pf);
158 }
159 
160 // x/(d) ==> (1/d) * x, unless d == 1
161 Theorem ArithTheoremProducer3::canonDivideVar(const Expr& e, const Expr& d) {
162  if(CHECK_PROOFS) {
164  CLASS_NAME "::canonDivideVar:\n "
165  "d is not a const: " + d.toString());
166  }
167  Proof pf;
168 
169  if(withProof())
170  pf = newPf("canon_divide_var", e);
171 
172  const Rational& dr = d.getRational();
173  if(dr == 1)
174  return newRWTheorem(e/d, e, Assumptions::emptyAssump(), pf);
175  if(dr == 0) // e/0 == 0 (total extension of division)
176  return newRWTheorem(e/d, d, Assumptions::emptyAssump(), pf);
177  else
178  return newRWTheorem(e/d, rat(1/dr) * e, Assumptions::emptyAssump(), pf);
179 }
180 
181 
182 // Multiplication
183 // (MULT expr1 expr2 expr3 ...)
184 // Each expr is in canonical form, i.e. it can be a
185 // 1) Rational constant
186 // 2) Arithmetic Leaf (var or term from another theory)
187 // 3) (POW rational leaf)
188 // where rational cannot be 0 or 1
189 // 4) (MULT rational mterm'_1 ...) where each mterm' is of type (2) or (3)
190 // If rational == 1 then there should be at least two mterms
191 // 5) (PLUS rational sterm_1 ...) where each sterm is of
192 // type (2) or (3) or (4)
193 // if rational == 0 then there should be at least two sterms
194 
195 
196 Expr ArithTheoremProducer3::simplifiedMultExpr(std::vector<Expr> & mulKids)
197 {
198  DebugAssert(mulKids.size() >= 1 && mulKids[0].isRational(), "");
199  if (mulKids.size() == 1) {
200  return mulKids[0];
201  }
202  if ((mulKids[0] == rat(1)) && mulKids.size() == 2) {
203  return mulKids[1];
204  }
205  else
206  return multExpr(mulKids);
207 }
208 
209 Expr ArithTheoremProducer3::canonMultConstMult(const Expr & c,
210  const Expr & e)
211 {
212  // c is a rational
213  // e is (MULT rat mterm'_1 ....)
214  // assume that e2 is already in canonic form
215  DebugAssert(c.isRational() && e.getKind() == MULT, "");
216  std::vector<Expr> mulKids;
217  DebugAssert ((e.arity() > 1) && (e[0].isRational()),
218  "ArithTheoremProducer3::canonMultConstMult: "
219  "a canonized MULT expression must have arity "
220  "greater than 1: and first child must be "
221  "rational " + e.toString());
222  Expr::iterator i = e.begin();
223  mulKids.push_back(rat(c.getRational() * (*i).getRational()));
224  ++i;
225  for(; i != e.end(); ++i) {
226  mulKids.push_back(*i);
227  }
228  return simplifiedMultExpr(mulKids);
229 }
230 
231 Expr ArithTheoremProducer3::canonMultConstPlus(const Expr & e1,
232  const Expr & e2)
233 {
234  DebugAssert(e1.isRational() && e2.getKind() == PLUS &&
235  e2.arity() > 0, "");
236  // e1 is a rational
237  // e2 is of the form (PLUS rational sterm1 sterm2 ...)
238  // assume that e2 is already in canonic form
239  std::vector<Theorem> thmPlusVector;
240  Expr::iterator i = e2.begin();
241  for(; i!= e2.end(); ++i) {
242  thmPlusVector.push_back(canonMultMtermMterm(e1*(*i)));
243  }
244 
245  Theorem thmPlus1 =
246  d_theoryArith->substitutivityRule(e2.getOp(), thmPlusVector);
247  return thmPlus1.getRHS();
248 }
249 
250 Expr ArithTheoremProducer3::canonMultPowPow(const Expr & e1,
251  const Expr & e2)
252 {
253  DebugAssert(e1.getKind() == POW && e2.getKind() == POW, "");
254  // (POW r1 leaf1) * (POW r2 leaf2)
255  Expr leaf1 = e1[1];
256  Expr leaf2 = e2[1];
257  Expr can_expr;
258  if (leaf1 == leaf2) {
259  Rational rsum = e1[0].getRational() + e2[0].getRational();
260  if (rsum == 0) {
261  return rat(1);
262  }
263  else if (rsum == 1) {
264  return leaf1;
265  }
266  else
267  {
268  return powExpr(rat(rsum), leaf1);
269  }
270  }
271  else
272  {
273  std::vector<Expr> mulKids;
274  mulKids.push_back(rat(1));
275  // the leafs should be put in decreasing order
276  if (leaf1 < leaf2) {
277  mulKids.push_back(e2);
278  mulKids.push_back(e1);
279  }
280  else
281  {
282  mulKids.push_back(e1);
283  mulKids.push_back(e2);
284  }
285  // FIXME: don't really need to simplify, just wrap up a MULT?
286  return simplifiedMultExpr(mulKids);
287  }
288 }
289 
290 Expr ArithTheoremProducer3::canonMultPowLeaf(const Expr & e1,
291  const Expr & e2)
292 {
293  DebugAssert(e1.getKind() == POW, "");
294  // (POW r1 leaf1) * leaf2
295  Expr leaf1 = e1[1];
296  Expr leaf2 = e2;
297  Expr can_expr;
298  if (leaf1 == leaf2) {
299  Rational rsum = e1[0].getRational() + 1;
300  if (rsum == 0) {
301  return rat(1);
302  }
303  else if (rsum == 1) {
304  return leaf1;
305  }
306  else
307  {
308  return powExpr(rat(rsum), leaf1);
309  }
310  }
311  else
312  {
313  std::vector<Expr> mulKids;
314  mulKids.push_back(rat(1));
315  // the leafs should be put in decreasing order
316  if (leaf1 < leaf2) {
317  mulKids.push_back(e2);
318  mulKids.push_back(e1);
319  }
320  else
321  {
322  mulKids.push_back(e1);
323  mulKids.push_back(e2);
324  }
325  return simplifiedMultExpr(mulKids);
326  }
327 }
328 
329 Expr ArithTheoremProducer3::canonMultLeafLeaf(const Expr & e1,
330  const Expr & e2)
331 {
332  // leaf1 * leaf2
333  Expr leaf1 = e1;
334  Expr leaf2 = e2;
335  Expr can_expr;
336  if (leaf1 == leaf2) {
337  return powExpr(rat(2), leaf1);
338  }
339  else
340  {
341  std::vector<Expr> mulKids;
342  mulKids.push_back(rat(1));
343  // the leafs should be put in decreasing order
344  if (leaf1 < leaf2) {
345  mulKids.push_back(e2);
346  mulKids.push_back(e1);
347  }
348  else
349  {
350  mulKids.push_back(e1);
351  mulKids.push_back(e2);
352  }
353  return simplifiedMultExpr(mulKids);
354  }
355 }
356 
357 Expr ArithTheoremProducer3::canonMultLeafOrPowMult(const Expr & e1,
358  const Expr & e2)
359 {
360  DebugAssert(e2.getKind() == MULT, "");
361  // Leaf * (MULT rat1 mterm1 ...)
362  // (POW r1 leaf1) * (MULT rat1 mterm1 ...) where
363  // each mterm is a leaf or (POW r leaf). Furthermore the leafs
364  // in the mterms are in descending order
365  Expr leaf1 = e1.getKind() == POW ? e1[1] : e1;
366  std::vector<Expr> mulKids;
367  DebugAssert(e2.arity() > 1, "MULT expr must have arity 2 or more");
368  Expr::iterator i = e2.begin();
369  // push the rational
370  mulKids.push_back(*i);
371  ++i;
372  // Now i points to the first mterm
373  for(; i != e2.end(); ++i) {
374  Expr leaf2 = ((*i).getKind() == POW) ? (*i)[1] : (*i);
375  if (leaf1 == leaf2) {
376  Rational r1 = e1.getKind() == POW ? e1[0].getRational() : 1;
377  Rational r2 =
378  ((*i).getKind() == POW ? (*i)[0].getRational() : 1);
379  // if r1 + r2 == 0 then it is the case of x^n * x^{-n}
380  // So, nothing needs to be added
381  if (r1 + r2 != 0) {
382  if (r1 + r2 == 1) {
383  mulKids.push_back(leaf1);
384  }
385  else
386  {
387  mulKids.push_back(powExpr(rat(r1 + r2), leaf1));
388  }
389  }
390  break;
391  }
392  // This ensures that the leaves in the mterms are also arranged
393  // in decreasing order
394  // Note that this will need to be changed if we want the order to
395  // be increasing order.
396  else if (leaf2 < leaf1) {
397  mulKids.push_back(e1);
398  mulKids.push_back(*i);
399  break;
400  }
401  else // leaf1 < leaf2
402  mulKids.push_back(*i);
403  }
404  if (i == e2.end()) {
405  mulKids.push_back(e1);
406  }
407  else
408  {
409  // e1 and *i have already been added
410  for (++i; i != e2.end(); ++i) {
411  mulKids.push_back(*i);
412  }
413  }
414  return simplifiedMultExpr(mulKids);
415 }
416 
417 // Local class for ordering monomials; note, that it flips the
418 // ordering given by greaterthan(), to sort in ascending order.
419 class MonomialLess {
420 public:
421  bool operator()(const Expr& e1, const Expr& e2) const {
422  return ArithTheoremProducer3::greaterthan(e1,e2);
423  }
424 };
425 
426 typedef map<Expr,Rational,MonomialLess> MonomMap;
427 
428 Expr
429 ArithTheoremProducer3::canonCombineLikeTerms(const std::vector<Expr> & sumExprs)
430 {
431  Rational constant = 0;
432  MonomMap sumHashMap;
433  vector<Expr> sumKids;
434 
435  // Add each distinct mterm (not including the rational) into
436  // an appropriate hash map entry
437  std::vector<Expr>::const_iterator i = sumExprs.begin();
438  for (; i != sumExprs.end(); ++i) {
439  Expr mul = *i;
440  if (mul.isRational()) {
441  constant = constant + mul.getRational();
442  }
443  else {
444  switch (mul.getKind()) {
445  case MULT: {
446  std::vector<Expr> mulKids;
447  DebugAssert(mul.arity() > 1 && mul[0].isRational(),"");
448  mulKids.push_back(rat(1));
449  Expr::iterator j = mul.begin();
450  ++j;
451  for (; j!= mul.end(); ++j) {
452  mulKids.push_back(*j);
453  }
454 
455  // make sure that tempExpr is also in canonic form
456  Expr tempExpr = mulKids.size() > 2 ? multExpr(mulKids): mulKids[1];
457  MonomMap::iterator i=sumHashMap.find(tempExpr);
458  if (i == sumHashMap.end()) {
459  sumHashMap[tempExpr] = mul[0].getRational();
460  }
461  else {
462  (*i).second += mul[0].getRational();
463  }
464  }
465  break;
466  default: {
467  MonomMap::iterator i=sumHashMap.find(mul);
468  // covers the case of POW, leaf
469  if (i == sumHashMap.end()) {
470  sumHashMap[mul] = 1;
471  }
472  else {
473  (*i).second += 1;
474  }
475  break;
476  }
477  }
478  }
479  }
480  // Now transfer to sumKids
481  sumKids.push_back(rat(constant));
482  MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end();
483  for(; j != jend; ++j) {
484  if ((*j).second != 0)
485  sumKids.push_back
486  (canonMultMtermMterm(rat((*j).second) * (*j).first).getRHS());
487  }
488 
489  /*
490  for (unsigned k = 0; k < sumKids.size(); ++k)
491  {
492  cout << "sumKids[" << k << "] = " << sumKids[k].toString() << endl;
493  }
494  */
495 
496  // The ordering in map guarantees the correct order; no need to sort
497 
498  // std::sort(sumKids.begin(), sumKids.end(), greaterthan);
499 
500  if ((constant == 0) && (sumKids.size() == 2)) {
501  return sumKids[1];
502  }
503  else if (sumKids.size() == 1) {
504  return sumKids[0];
505  }
506  else
507  return plusExpr(sumKids);
508 }
509 
510 Expr ArithTheoremProducer3::canonMultLeafOrPowOrMultPlus(const Expr & e1,
511  const Expr & e2)
512 {
513  DebugAssert(e2.getKind() == PLUS, "");
514  // Leaf * (PLUS rational sterm1 ...)
515  // or
516  // (POW n1 x1) * (PLUS rational sterm1 ...)
517  // or
518  // (MULT r1 m1 m2 ...) * (PLUS rational sterm1 ...)
519  // assume that e1 and e2 are themselves canonized
520  std::vector<Expr> sumExprs;
521  // Multiply each term in turn.
522  Expr::iterator i = e2.begin();
523  for (; i != e2.end(); ++i) {
524  sumExprs.push_back(canonMultMtermMterm(e1 * (*i)).getRHS());
525  }
526  return canonCombineLikeTerms(sumExprs);
527 }
528 
529 Expr ArithTheoremProducer3::canonMultPlusPlus(const Expr & e1,
530  const Expr & e2)
531 {
532  DebugAssert(e1.getKind() == PLUS && e2.getKind() == PLUS, "");
533  // (PLUS r1 .... ) * (PLUS r1' ...)
534  // assume that e1 and e2 are themselves canonized
535 
536  std::vector<Expr> sumExprs;
537  // Multiply each term in turn.
538  Expr::iterator i = e1.begin();
539  for (; i != e1.end(); ++i) {
540  Expr::iterator j = e2.begin();
541  for (; j != e2.end(); ++j) {
542  sumExprs.push_back(canonMultMtermMterm((*i) * (*j)).getRHS());
543  }
544  }
545  return canonCombineLikeTerms(sumExprs);
546 }
547 
548 
549 
550 // The following produces a Theorem which is the result of multiplication
551 // of two canonized mterms. e = e1*e2
552 Theorem
553 ArithTheoremProducer3::canonMultMtermMterm(const Expr& e)
554 {
555  if(CHECK_PROOFS) {
556  CHECK_SOUND(isMult(e) && e.arity() == 2,
557  "canonMultMtermMterm: e = "+e.toString());
558  }
559  Proof pf;
560  Expr rhs;
561  const Expr& e1 = e[0];
562  const Expr& e2 = e[1];
563  string cmmm = "canon_mult_mterm_mterm";
564 
565  if (e1.isRational()) {
566  // e1 is a Rational
567  const Rational& c = e1.getRational();
568  if (c == 0)
569  return canonMultZero(e2);
570  else if (c == 1)
571  return canonMultOne(e2);
572  else {
573  switch (e2.getKind()) {
574  case RATIONAL_EXPR :
575  // rat * rat
576  return canonMultConstConst(e1,e2);
577  break;
578  // TODO case of leaf
579  case POW:
580  // rat * (POW rat leaf)
581  // nothing to simplify
582  return d_theoryArith->reflexivityRule (e);
583 
584  break;
585  case MULT:
586  rhs = canonMultConstMult(e1,e2);
587  if(withProof()) pf = newPf(cmmm,e,rhs);
588  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
589  break;
590  case PLUS:
591  rhs = canonMultConstPlus(e1,e2);
592  if(withProof()) pf = newPf(cmmm,e,rhs);
593  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
594  break;
595  default:
596  // TODO: I am going to assume that this is just a leaf
597  // i.e., a variable or term from another theory
598  return d_theoryArith->reflexivityRule(e);
599  break;
600  }
601  }
602  }
603  else if (e1.getKind() == POW) {
604  switch (e2.getKind()) {
605  case RATIONAL_EXPR:
606  // switch the order of the two arguments
607  return canonMultMtermMterm(e2 * e1);
608  break;
609  case POW:
610  rhs = canonMultPowPow(e1,e2);
611  if(withProof()) pf = newPf(cmmm,e,rhs);
612  return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
613  break;
614  case MULT:
615  rhs = canonMultLeafOrPowMult(e1,e2);
616  if(withProof()) pf = newPf(cmmm,e,rhs);
617  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
618  break;
619  case PLUS:
620  rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
621  if(withProof()) pf = newPf(cmmm,e,rhs);
622  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
623  break;
624  default:
625  rhs = canonMultPowLeaf(e1,e2);
626  if(withProof()) pf = newPf(cmmm,e,rhs);
627  return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
628  break;
629  }
630  }
631  else if (e1.getKind() == MULT) {
632  switch (e2.getKind()) {
633  case RATIONAL_EXPR:
634  case POW:
635  // switch the order of the two arguments
636  return canonMultMtermMterm(e2 * e1);
637  break;
638  case MULT:
639  {
640  // (Mult r m1 m2 ...) (Mult r' m1' m2' ...)
641  Expr result = e2;
642  Expr::iterator i = e1.begin();
643  for (; i != e1.end(); ++i) {
644  result = canonMultMtermMterm((*i) * result).getRHS();
645  }
646  if(withProof()) pf = newPf(cmmm,e,result);
647  return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
648  }
649  break;
650  case PLUS:
651  rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
652  if(withProof()) pf = newPf(cmmm,e,rhs);
653  return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
654  break;
655  default:
656  // leaf
657  // switch the order of the two arguments
658  return canonMultMtermMterm(e2 * e1);
659  break;
660  }
661  }
662  else if (e1.getKind() == PLUS) {
663  switch (e2.getKind()) {
664  case RATIONAL_EXPR:
665  case POW:
666  case MULT:
667  // switch the order of the two arguments
668  return canonMultMtermMterm(e2 * e1);
669  break;
670  case PLUS:
671  rhs = canonMultPlusPlus(e1,e2);
672  if(withProof()) pf = newPf(cmmm,e,rhs);
673  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
674  break;
675  default:
676  // leaf
677  // switch the order of the two arguments
678  return canonMultMtermMterm(e2 * e1);
679  break;
680  }
681  }
682  else {
683  // leaf
684  switch (e2.getKind()) {
685  case RATIONAL_EXPR:
686  // switch the order of the two arguments
687  return canonMultMtermMterm(e2 * e1);
688  break;
689  case POW:
690  rhs = canonMultPowLeaf(e2,e1);
691  if(withProof()) pf = newPf(cmmm,e,rhs);
692  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
693  break;
694  case MULT:
695  rhs = canonMultLeafOrPowMult(e1,e2);;
696  if(withProof()) pf = newPf(cmmm,e,rhs);
697  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
698  break;
699  case PLUS:
700  rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
701  if(withProof()) pf = newPf(cmmm,e,rhs);
702  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
703  break;
704  default:
705  // leaf * leaf
706  rhs = canonMultLeafLeaf(e1,e2);
707  if(withProof()) pf = newPf(cmmm,e,rhs);
708  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
709  break;
710  }
711  }
712  FatalAssert(false, "Unreachable");
713  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
714 }
715 
716 // (PLUS expr1 expr2 ...) where each expr is itself in canonic form
717 Theorem
718 ArithTheoremProducer3::canonPlus(const Expr& e)
719 {
720  Proof pf;
721 
722  if (withProof()) {
723  pf = newPf("canon_plus", e);
724  }
725  DebugAssert(e.getKind() == PLUS, "");
726 
727  // First flatten the PLUS
728 
729  std::vector<Expr> sumKids;
730  Expr::iterator i = e.begin();
731  for(; i != e.end(); ++i) {
732  if ((*i).getKind() != PLUS) {
733  sumKids.push_back(*i);
734  }
735  else
736  {
737  Expr::iterator j = (*i).begin();
738  for(; j != (*i).end(); ++j)
739  sumKids.push_back(*j);
740  }
741  }
742  Expr val = canonCombineLikeTerms(sumKids);
743  if (withProof()) {
744  pf = newPf("canon_plus", e, val);
745  }
746  return newRWTheorem(e, val, Assumptions::emptyAssump(), pf);
747 }
748 
749 // (MULT expr1 expr2 ...) where each expr is itself in canonic form
750 Theorem
751 ArithTheoremProducer3::canonMult(const Expr& e)
752 {
753  Proof pf;
754  DebugAssert(e.getKind() == MULT && e.arity() > 1, "");
755  Expr::iterator i = e.begin();
756  Expr result = *i;
757  ++i;
758  for (; i != e.end(); ++i) {
759  result = canonMultMtermMterm(result * (*i)).getRHS();
760  }
761  if (withProof()) {
762  pf = newPf("canon_mult", e,result);
763  }
764  return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
765 }
766 
767 
768 Theorem
769 ArithTheoremProducer3::canonInvertConst(const Expr& e)
770 {
771  if(CHECK_PROOFS)
772  CHECK_SOUND(isRational(e), "expecting a rational: e = "+e.toString());
773 
774  Proof pf;
775 
776  if (withProof()) {
777  pf = newPf("canon_invert_const", e);
778  }
779  const Rational& er = e.getRational();
780  return newRWTheorem((rat(1)/e), rat(er==0? 0 : (1/er)), Assumptions::emptyAssump(), pf);
781 }
782 
783 
784 Theorem
785 ArithTheoremProducer3::canonInvertLeaf(const Expr& e)
786 {
787  Proof pf;
788 
789  if (withProof()) {
790  pf = newPf("canon_invert_leaf", e);
791  }
792  return newRWTheorem((rat(1)/e), powExpr(rat(-1), e), Assumptions::emptyAssump(), pf);
793 }
794 
795 
796 Theorem
797 ArithTheoremProducer3::canonInvertPow(const Expr& e)
798 {
799  DebugAssert(e.getKind() == POW, "expecting a rational"+e[0].toString());
800 
801  Proof pf;
802 
803  if (withProof()) {
804  pf = newPf("canon_invert_pow", e);
805  }
806  if (e[0].getRational() == -1)
807  return newRWTheorem((rat(1)/e), e[1], Assumptions::emptyAssump(), pf);
808  else
809  return newRWTheorem((rat(1)/e),
810  powExpr(rat(-e[0].getRational()), e),
811  Assumptions::emptyAssump(),
812  pf);
813 }
814 
815 Theorem
816 ArithTheoremProducer3::canonInvertMult(const Expr& e)
817 {
818  DebugAssert(e.getKind() == MULT, "expecting a rational"+e[0].toString());
819 
820  Proof pf;
821 
822  if (withProof()) {
823  pf = newPf("canon_invert_mult", e);
824  }
825 
826  DebugAssert(e.arity() > 1, "MULT should have arity > 1"+e.toString());
827  Expr result = canonInvert(e[0]).getRHS();
828  for (int i = 1; i < e.arity(); ++i) {
829  result =
830  canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS();
831  }
832  return newRWTheorem((rat(1)/e), result, Assumptions::emptyAssump(), pf);
833 }
834 
835 
836 // Given an expression e in Canonic form generate 1/e in canonic form
837 // This function assumes that e is not a PLUS expression
838 Theorem
839 ArithTheoremProducer3::canonInvert(const Expr& e)
840 {
841  DebugAssert(e.getKind() != PLUS,
842  "Cannot do inverse on a PLUS"+e.toString());
843  switch (e.getKind()) {
844  case RATIONAL_EXPR:
845  return canonInvertConst(e);
846  break;
847  case POW:
848  return canonInvertPow(e);
849  break;
850  case MULT:
851  return canonInvertMult(e);
852  break;
853  default:
854  // leaf
855  return canonInvertLeaf(e);
856  break;
857  }
858 }
859 
860 
861 Theorem ArithTheoremProducer3::moveSumConstantRight(const Expr& e) {
862 
863  // Check soundness of the rule if necessary
864  if (CHECK_PROOFS) {
865  CHECK_SOUND(isIneq(e) || e.isEq(), "moveSumConstantRight: input must be Eq or Ineq: " + e.toString());
866  CHECK_SOUND(isRational(e[0]) || isPlus(e[0]), "moveSumConstantRight: left side must be a canonised sum: " + e.toString());
867  CHECK_SOUND(isRational(e[1]) && e[1].getRational() == 0, "moveSumConstantRight: right side must be 0: " + e.toString());
868  }
869 
870  // The rational constant of the sum
871  Rational r = 0;
872 
873  // The right hand side of the expression
874  Expr right = e[0];
875 
876  // The vector of sum terms
877  vector<Expr> sumTerms;
878 
879  // Get all the non rational children and
880  if (!right.isRational())
881  for(Expr::iterator it = right.begin(); it != right.end(); it ++) {
882  // If the term is rational then add the rational number to r
883  if ((*it).isRational()) r = r + (*it).getRational();
884  // Otherwise just add the sumTerm to the sumTerms
885  else sumTerms.push_back((*it));
886  }
887 
888  // Setup the new expression
889  Expr transformed;
890  if (sumTerms.size() > 1)
891  // If the number of summands is > 1 return the sum of them
892  transformed = Expr(e.getKind(), plusExpr(sumTerms), rat(-r));
893  else
894  // Otherwise return the one summand as itself
895  transformed = Expr(e.getKind(), sumTerms[0], rat(-r));
896 
897 
898  // If proof is needed set it up
899  Proof pf;
900  if (withProof()) pf = newPf("arithm_sum_constant_right", e);
901 
902  // Retrun the theorem explaining the transformation
903  return newRWTheorem(e, transformed, Assumptions::emptyAssump(), pf);
904 }
905 
906 Theorem
907 ArithTheoremProducer3::canonDivide(const Expr& e)
908 {
909  DebugAssert(e.getKind() == DIVIDE, "Expecting Divide"+e.toString());
910  Proof pf;
911 
912  if (withProof()) {
913  pf = newPf("canon_invert_divide", e);
914  }
915 
916  Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf);
917 
918  return d_theoryArith->transitivityRule(thm, canonMult(thm.getRHS()));
919 }
920 
921 
922 // Rules for multiplication
923 // t*c ==> c*t, takes constant c and term t
924 Theorem
925 ArithTheoremProducer3::canonMultTermConst(const Expr& c, const Expr& t) {
926  Proof pf;
927  if(CHECK_PROOFS) {
929  CLASS_NAME "::canonMultTermConst:\n "
930  "c is not a constant: " + c.toString());
931  }
932  if(withProof()) pf = newPf("canon_mult_term_const", c, t);
933  return newRWTheorem((t*c), (c*t), Assumptions::emptyAssump(), pf);
934 }
935 
936 // Rules for multiplication
937 // t1*t2 ==> Error, takes t1 and t2 where both are non-constants
938 Theorem
939 ArithTheoremProducer3::canonMultTerm1Term2(const Expr& t1, const Expr& t2) {
940  // Proof pf;
941  // if(withProof()) pf = newPf("canon_mult_term1_term2", t1, t2);
942  if(CHECK_PROOFS) {
943  CHECK_SOUND(false, "Fatal Error: We don't support multiplication"
944  "of two non constant terms at this time "
945  + t1.toString() + " and " + t2.toString());
946  }
947  return Theorem();
948 }
949 
950 // Rules for multiplication
951 // 0*x = 0, takes x
952 Theorem ArithTheoremProducer3::canonMultZero(const Expr& e) {
953  Proof pf;
954  if(withProof()) pf = newPf("canon_mult_zero", e);
955  return newRWTheorem((rat(0)*e), rat(0), Assumptions::emptyAssump(), pf);
956 }
957 
958 // Rules for multiplication
959 // 1*x ==> x, takes x
960 Theorem ArithTheoremProducer3::canonMultOne(const Expr& e) {
961  Proof pf;
962  if(withProof()) pf = newPf("canon_mult_one", e);
963  return newRWTheorem((rat(1)*e), e, Assumptions::emptyAssump(), pf);
964 }
965 
966 // Rules for multiplication
967 // c1*c2 ==> c', takes constant c1*c2
968 Theorem
969 ArithTheoremProducer3::canonMultConstConst(const Expr& c1, const Expr& c2) {
970  Proof pf;
971  if(CHECK_PROOFS) {
973  CLASS_NAME "::canonMultConstConst:\n "
974  "c1 is not a constant: " + c1.toString());
976  CLASS_NAME "::canonMultConstConst:\n "
977  "c2 is not a constant: " + c2.toString());
978  }
979  if(withProof()) pf = newPf("canon_mult_const_const", c1, c2);
980  return
981  newRWTheorem((c1*c2), rat(c1.getRational()*c2.getRational()), Assumptions::emptyAssump(), pf);
982 }
983 
984 // Rules for multiplication
985 // c1*(c2*t) ==> c'*t, takes c1 and c2 and t
986 Theorem
987 ArithTheoremProducer3::canonMultConstTerm(const Expr& c1,
988  const Expr& c2,const Expr& t) {
989  Proof pf;
990  if(CHECK_PROOFS) {
992  CLASS_NAME "::canonMultConstTerm:\n "
993  "c1 is not a constant: " + c1.toString());
995  CLASS_NAME "::canonMultConstTerm:\n "
996  "c2 is not a constant: " + c2.toString());
997  }
998 
999  if(withProof()) pf = newPf("canon_mult_const_term", c1, c2, t);
1000  return
1001  newRWTheorem(c1*(c2*t), rat(c1.getRational()*c2.getRational())*t, Assumptions::emptyAssump(), pf);
1002 }
1003 
1004 // Rules for multiplication
1005 // c1*(+ c2 v1 ...) ==> (+ c1c2 c1v1 ...), takes c1 and the sum
1006 Theorem
1007 ArithTheoremProducer3::canonMultConstSum(const Expr& c1, const Expr& sum) {
1008  Proof pf;
1009  std::vector<Expr> sumKids;
1010 
1011  if(CHECK_PROOFS) {
1012  CHECK_SOUND(isRational(c1),
1013  CLASS_NAME "::canonMultConstTerm:\n "
1014  "c1 is not a constant: " + c1.toString());
1015  CHECK_SOUND(PLUS == sum.getKind(),
1016  CLASS_NAME "::canonMultConstTerm:\n "
1017  "the kind must be a PLUS: " + sum.toString());
1018  }
1019  Expr::iterator i = sum.begin();
1020  for(; i != sum.end(); ++i)
1021  sumKids.push_back(c1*(*i));
1022  Expr ret = plusExpr(sumKids);
1023  if(withProof()) pf = newPf("canon_mult_const_sum", c1, sum, ret);
1024  return newRWTheorem((c1*sum),ret , Assumptions::emptyAssump(), pf);
1025 }
1026 
1027 
1028 // c^n = c' (compute the constant power expression)
1029 Theorem
1030 ArithTheoremProducer3::canonPowConst(const Expr& e) {
1031  if(CHECK_PROOFS) {
1032  CHECK_SOUND(e.getKind() == POW && e.arity() == 2
1033  && e[0].isRational() && e[1].isRational(),
1034  "ArithTheoremProducer3::canonPowConst("+e.toString()+")");
1035  }
1036  const Rational& p = e[0].getRational();
1037  const Rational& base = e[1].getRational();
1038  if(CHECK_PROOFS) {
1039  CHECK_SOUND(p.isInteger(),
1040  "ArithTheoremProducer3::canonPowConst("+e.toString()+")");
1041  }
1042  Expr res;
1043  if (base == 0 && p < 0) {
1044  res = rat(0);
1045  }
1046  else res = rat(pow(p, base));
1047  Proof pf;
1048  if(withProof())
1049  pf = newPf("canon_pow_const", e);
1050  return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
1051 }
1052 
1053 
1054 // Rules for addition
1055 // flattens the input. accepts a PLUS expr
1056 Theorem
1057 ArithTheoremProducer3::canonFlattenSum(const Expr& e) {
1058  Proof pf;
1059  std::vector<Expr> sumKids;
1060  if(CHECK_PROOFS) {
1061  CHECK_SOUND(PLUS == e.getKind(),
1062  CLASS_NAME "::canonFlattenSum:\n"
1063  "input must be a PLUS:" + e.toString());
1064  }
1065 
1066  Expr::iterator i = e.begin();
1067  for(; i != e.end(); ++i){
1068  if (PLUS != (*i).getKind())
1069  sumKids.push_back(*i);
1070  else {
1071  Expr::iterator j = (*i).begin();
1072  for(; j != (*i).end(); ++j)
1073  sumKids.push_back(*j);
1074  }
1075  }
1076  Expr ret = plusExpr(sumKids);
1077  if(withProof()) pf = newPf("canon_flatten_sum", e,ret);
1078  return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
1079 }
1080 
1081 // Rules for addition
1082 // combine like terms. accepts a flattened PLUS expr
1083 Theorem
1084 ArithTheoremProducer3::canonComboLikeTerms(const Expr& e) {
1085  Proof pf;
1086  std::vector<Expr> sumKids;
1087  ExprMap<Rational> sumHashMap;
1088  Rational constant = 0;
1089 
1090  if(CHECK_PROOFS) {
1091  Expr::iterator k = e.begin();
1092  for(; k != e.end(); ++k)
1093  CHECK_SOUND(!isPlus(*k),
1094  CLASS_NAME "::canonComboLikeTerms:\n"
1095  "input must be a flattened PLUS:" + k->toString());
1096  }
1097  Expr::iterator i = e.begin();
1098  for(; i != e.end(); ++i){
1099  if(i->isRational())
1100  constant = constant + i->getRational();
1101  else {
1102  if (!isMult(*i)) {
1103  if(0 == sumHashMap.count((*i)))
1104  sumHashMap[*i] = 1;
1105  else
1106  sumHashMap[*i] += 1;
1107  }
1108  else {
1109  if(0 == sumHashMap.count((*i)[1]))
1110  sumHashMap[(*i)[1]] = (*i)[0].getRational();
1111  else
1112  sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational();
1113  }
1114  }
1115  }
1116 
1117  sumKids.push_back(rat(constant));
1118  ExprMap<Rational>::iterator j = sumHashMap.begin();
1119  for(; j != sumHashMap.end(); ++j) {
1120  if(0 == (*j).second)
1121  ;//do nothing
1122  else if (1 == (*j).second)
1123  sumKids.push_back((*j).first);
1124  else
1125  sumKids.push_back(rat((*j).second) * (*j).first);
1126  }
1127 
1128  //constant is same as sumKids[0].
1129  //corner cases: "0 + monomial" and "constant"(no monomials)
1130 
1131  Expr ret;
1132  if(2 == sumKids.size() && 0 == constant) ret = sumKids[1];
1133  else if (1 == sumKids.size()) ret = sumKids[0];
1134  else ret = plusExpr(sumKids);
1135 
1136  if(withProof()) pf = newPf("canon_combo_like_terms",e,ret);
1137  return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1138 }
1139 
1140 
1141 // 0 = (* e1 e2 ...) <=> 0 = e1 OR 0 = e2 OR ...
1142 Theorem ArithTheoremProducer3::multEqZero(const Expr& expr)
1143 {
1144  if (CHECK_PROOFS) {
1145  CHECK_SOUND(expr.isEq() && expr[0].isRational() &&
1146  expr[0].getRational() == 0 &&
1147  isMult(expr[1]) && expr[1].arity() > 1,
1148  "multEqZero invariant violated"+expr.toString());
1149  }
1150  Proof pf;
1151  vector<Expr> kids;
1152  Expr::iterator i = expr[1].begin(), iend = expr[1].end();
1153  for (; i != iend; ++i) {
1154  kids.push_back(rat(0).eqExpr(*i));
1155  }
1156  if (withProof()) {
1157  pf = newPf("multEqZero", expr);
1158  }
1159  return newRWTheorem(expr, Expr(OR, kids), Assumptions::emptyAssump(), pf);
1160 }
1161 
1162 
1163 // 0 = (^ c x) <=> false if c <=0
1164 // <=> 0 = x if c > 0
1165 Theorem ArithTheoremProducer3::powEqZero(const Expr& expr)
1166 {
1167  if (CHECK_PROOFS) {
1168  CHECK_SOUND(expr.isEq() && expr[0].isRational() &&
1169  expr[0].getRational() == 0 &&
1170  isPow(expr[1]) && expr[1].arity() == 2 &&
1171  expr[1][0].isRational(),
1172  "powEqZero invariant violated"+expr.toString());
1173  }
1174  Proof pf;
1175  if (withProof()) {
1176  pf = newPf("powEqZero", expr);
1177  }
1178  Rational r = expr[1][0].getRational();
1179  Expr res;
1180  if (r <= 0) {
1181  res = d_em->falseExpr();
1182  }
1183  else {
1184  res = rat(0).eqExpr(expr[1][1]);
1185  }
1186  return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1187 }
1188 
1189 
1190 // x^n = y^n <=> x = y (if n is odd)
1191 // x^n = y^n <=> x = y OR x = -y (if n is even)
1192 Theorem ArithTheoremProducer3::elimPower(const Expr& expr)
1193 {
1194  if (CHECK_PROOFS) {
1195  CHECK_SOUND(expr.isEq() && isPow(expr[0]) &&
1196  isPow(expr[1]) &&
1197  isIntegerConst(expr[0][0]) &&
1198  expr[0][0].getRational() > 0 &&
1199  expr[0][0] == expr[1][0],
1200  "elimPower invariant violated"+expr.toString());
1201  }
1202  Proof pf;
1203  if (withProof()) {
1204  pf = newPf("elimPower", expr);
1205  }
1206  Rational r = expr[0][0].getRational();
1207  Expr res = expr[0][1].eqExpr(expr[1][1]);
1208  if (r % 2 == 0) {
1209  res = res.orExpr(expr[0][1].eqExpr(-expr[1][1]));
1210  }
1211  return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1212 }
1213 
1214 
1215 // x^n = c <=> x = root (if n is odd and root^n = c)
1216 // x^n = c <=> x = root OR x = -root (if n is even and root^n = c)
1217 Theorem ArithTheoremProducer3::elimPowerConst(const Expr& expr, const Rational& root)
1218 {
1219  if (CHECK_PROOFS) {
1220  CHECK_SOUND(expr.isEq() && isPow(expr[0]) &&
1221  isIntegerConst(expr[0][0]) &&
1222  expr[0][0].getRational() > 0 &&
1223  expr[1].isRational() &&
1224  pow(expr[0][0].getRational(), root) == expr[1].getRational(),
1225  "elimPowerConst invariant violated"+expr.toString());
1226  }
1227  Proof pf;
1228  if (withProof()) {
1229  pf = newPf("elimPowerConst", expr, rat(root));
1230  }
1231  Rational r = expr[0][0].getRational();
1232  Expr res = expr[0][1].eqExpr(rat(root));
1233  if (r % 2 == 0) {
1234  res = res.orExpr(expr[0][1].eqExpr(rat(-root)));
1235  }
1236  return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1237 }
1238 
1239 
1240 // x^n = c <=> false (if n is even and c is negative)
1241 Theorem ArithTheoremProducer3::evenPowerEqNegConst(const Expr& expr)
1242 {
1243  if (CHECK_PROOFS) {
1244  CHECK_SOUND(expr.isEq() && isPow(expr[0]) &&
1245  expr[1].isRational() &&
1246  isIntegerConst(expr[0][0]) &&
1247  expr[0][0].getRational() % 2 == 0 &&
1248  expr[1].getRational() < 0,
1249  "evenPowerEqNegConst invariant violated"+expr.toString());
1250  }
1251  Proof pf;
1252  if (withProof()) {
1253  pf = newPf("evenPowerEqNegConst", expr);
1254  }
1255  return newRWTheorem(expr, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
1256 }
1257 
1258 
1259 // x^n = c <=> false (if x is an integer and c is not a perfect n power)
1260 Theorem ArithTheoremProducer3::intEqIrrational(const Expr& expr, const Theorem& isIntx)
1261 {
1262  if (CHECK_PROOFS) {
1263  CHECK_SOUND(expr.isEq() && isPow(expr[0]) &&
1264  expr[1].isRational() &&
1265  expr[1].getRational() != 0 &&
1266  isIntegerConst(expr[0][0]) &&
1267  expr[0][0].getRational() > 0 &&
1268  ratRoot(expr[1].getRational(), expr[0][0].getRational().getUnsigned()) == 0,
1269  "intEqIrrational invariant violated"+expr.toString());
1270  CHECK_SOUND(isIntPred(isIntx.getExpr()) && isIntx.getExpr()[0] == expr[0][1],
1271  "ArithTheoremProducer3::intEqIrrational:\n "
1272  "wrong integrality constraint:\n expr = "
1273  +expr.toString()+"\n isIntx = "
1274  +isIntx.getExpr().toString());
1275  }
1276  const Assumptions& assump(isIntx.getAssumptionsRef());
1277  Proof pf;
1278  if (withProof()) {
1279  pf = newPf("int_eq_irr", expr, isIntx.getProof());
1280  }
1281  return newRWTheorem(expr, d_em->falseExpr(), assump, pf);
1282 }
1283 
1284 
1285 // e[0] kind e[1] <==> true when e[0] kind e[1],
1286 // false when e[0] !kind e[1], for constants only
1287 Theorem ArithTheoremProducer3::constPredicate(const Expr& e) {
1288  if(CHECK_PROOFS) {
1289  CHECK_SOUND(e.arity() == 2 && isRational(e[0]) && isRational(e[1]),
1290  CLASS_NAME "::constPredicate:\n "
1291  "non-const parameters: " + e.toString());
1292  }
1293  Proof pf;
1294  bool result(false);
1295  int kind = e.getKind();
1296  Rational r1 = e[0].getRational(), r2 = e[1].getRational();
1297  switch(kind) {
1298  case EQ:
1299  result = (r1 == r2)?true : false;
1300  break;
1301  case LT:
1302  result = (r1 < r2)?true : false;
1303  break;
1304  case LE:
1305  result = (r1 <= r2)?true : false;
1306  break;
1307  case GT:
1308  result = (r1 > r2)?true : false;
1309  break;
1310  case GE:
1311  result = (r1 >= r2)?true : false;
1312  break;
1313  default:
1314  if(CHECK_PROOFS) {
1315  CHECK_SOUND(false,
1316  "ArithTheoremProducer3::constPredicate: wrong kind");
1317  }
1318  break;
1319  }
1320  Expr ret = (result) ? d_em->trueExpr() : d_em->falseExpr();
1321  if(withProof()) pf = newPf("const_predicate", e,ret);
1322  return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1323 }
1324 
1325 // e[0] kind e[1] <==> 0 kind e[1] - e[0]
1326 Theorem ArithTheoremProducer3::rightMinusLeft(const Expr& e)
1327 {
1328  Proof pf;
1329  int kind = e.getKind();
1330  if(CHECK_PROOFS) {
1331  CHECK_SOUND((EQ==kind) ||
1332  (LT==kind) ||
1333  (LE==kind) ||
1334  (GE==kind) ||
1335  (GT==kind),
1336  "ArithTheoremProducer3::rightMinusLeft: wrong kind");
1337  }
1338  if(withProof()) pf = newPf("right_minus_left",e);
1339  return newRWTheorem(e, Expr(e.getOp(), rat(0), e[1] - e[0]), Assumptions::emptyAssump(), pf);
1340 }
1341 
1342 
1343 // e[0] kind e[1] <==> 0 kind e[1] - e[0]
1344 Theorem ArithTheoremProducer3::leftMinusRight(const Expr& e)
1345 {
1346  Proof pf;
1347  int kind = e.getKind();
1348  if(CHECK_PROOFS) {
1349  CHECK_SOUND((EQ==kind) ||
1350  (LT==kind) ||
1351  (LE==kind) ||
1352  (GE==kind) ||
1353  (GT==kind),
1354  "ArithTheoremProducer3::rightMinusLeft: wrong kind");
1355  }
1356  if(withProof()) pf = newPf("left_minus_right",e);
1357  return newRWTheorem(e, Expr(e.getOp(), e[0] - e[1], rat(0)), Assumptions::emptyAssump(), pf);
1358 }
1359 
1360 
1361 // x kind y <==> x + z kind y + z
1362 Theorem ArithTheoremProducer3::plusPredicate(const Expr& x,
1363  const Expr& y,
1364  const Expr& z, int kind) {
1365  if(CHECK_PROOFS) {
1366  CHECK_SOUND((EQ==kind) ||
1367  (LT==kind) ||
1368  (LE==kind) ||
1369  (GE==kind) ||
1370  (GT==kind),
1371  "ArithTheoremProducer3::plusPredicate: wrong kind");
1372  }
1373  Proof pf;
1374  Expr left = Expr(kind, x, y);
1375  Expr right = Expr(kind, x + z, y + z);
1376  if(withProof()) pf = newPf("plus_predicate",left,right);
1377  return newRWTheorem(left, right, Assumptions::emptyAssump(), pf);
1378 }
1379 
1380 // x = y <==> x * z = y * z
1381 Theorem ArithTheoremProducer3::multEqn(const Expr& x,
1382  const Expr& y,
1383  const Expr& z) {
1384  Proof pf;
1385  if(CHECK_PROOFS)
1386  CHECK_SOUND(z.isRational() && z.getRational() != 0,
1387  "ArithTheoremProducer3::multEqn(): multiplying equation by 0");
1388  if(withProof()) pf = newPf("mult_eqn", x, y, z);
1389  return newRWTheorem(x.eqExpr(y), (x * z).eqExpr(y * z), Assumptions::emptyAssump(), pf);
1390 }
1391 
1392 
1393 // x = y <==> z=0 OR x * 1/z = y * 1/z
1394 Theorem ArithTheoremProducer3::divideEqnNonConst(const Expr& x,
1395  const Expr& y,
1396  const Expr& z) {
1397  Proof pf;
1398  if(withProof()) pf = newPf("mult_eqn_nonconst", x, y, z);
1399  return newRWTheorem(x.eqExpr(y), (z.eqExpr(rat(0))).orExpr((x / z).eqExpr(y / z)),
1400  Assumptions::emptyAssump(), pf);
1401 }
1402 
1403 
1404 // if z is +ve, return e[0] LT|LE|GT|GE e[1] <==> e[0]*z LT|LE|GT|GE e[1]*z
1405 // if z is -ve, return e[0] LT|LE|GT|GE e[1] <==> e[1]*z LT|LE|GT|GE e[0]*z
1406 Theorem ArithTheoremProducer3::multIneqn(const Expr& e, const Expr& z)
1407 {
1408  int kind = e.getKind();
1409 
1410  if(CHECK_PROOFS) {
1411  CHECK_SOUND((LT==kind) ||
1412  (LE==kind) ||
1413  (GE==kind) ||
1414  (GT==kind),
1415  "ArithTheoremProducer3::multIneqn: wrong kind");
1416  CHECK_SOUND(z.isRational() && z.getRational() != 0,
1417  "ArithTheoremProducer3::multIneqn: "
1418  "z must be non-zero rational: " + z.toString());
1419  }
1420  Op op(e.getOp());
1421  Proof pf;
1422 
1423  Expr ret;
1424  if(0 < z.getRational())
1425  ret = Expr(op, e[0]*z, e[1]*z);
1426  else
1427  ret = Expr(op, e[1]*z, e[0]*z);
1428  if(withProof()) pf = newPf("mult_ineqn", e, ret);
1429  return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1430 }
1431 
1432 
1433 Theorem ArithTheoremProducer3::eqToIneq(const Expr& e) {
1434 
1435  // Check soundness of the rule if necessary
1436  if (CHECK_PROOFS)
1437  CHECK_SOUND(e.isEq(), "eqToIneq: input must be an equality: " + e.toString());
1438 
1439  // The proof object we will use
1440  Proof pf;
1441 
1442  // The parts of the equality x = y
1443  const Expr& x = e[0];
1444  const Expr& y = e[1];
1445 
1446  // Setup the proof if needed
1447  if (withProof())
1448  pf = newPf("eqToIneq", e);
1449 
1450  // Retrun the theorem explaining the transformation
1451  return newRWTheorem(e, leExpr(x,y).andExpr(geExpr(x,y)), Assumptions::emptyAssump(), pf);
1452 }
1453 
1454 // "op1 GE|GT op2" <==> op2 LE|LT op1
1455 Theorem ArithTheoremProducer3::flipInequality(const Expr& e)
1456 {
1457  Proof pf;
1458  if(CHECK_PROOFS) {
1459  CHECK_SOUND(isGT(e) || isGE(e),
1460  "ArithTheoremProducer3::flipInequality: wrong kind: " +
1461  e.toString());
1462  }
1463 
1464  int kind = isGE(e) ? LE : LT;
1465  Expr ret = Expr(kind, e[1], e[0]);
1466  if(withProof()) pf = newPf("flip_inequality", e,ret);
1467  return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
1468 }
1469 
1470 
1471 // NOT (op1 LT op2) <==> (op1 GE op2)
1472 // NOT (op1 LE op2) <==> (op1 GT op2)
1473 // NOT (op1 GT op2) <==> (op1 LE op2)
1474 // NOT (op1 GE op2) <==> (op1 LT op2)
1475 Theorem ArithTheoremProducer3::negatedInequality(const Expr& e)
1476 {
1477  const Expr& ineq = e[0];
1478  if(CHECK_PROOFS) {
1479  CHECK_SOUND(e.isNot(),
1480  "ArithTheoremProducer3::negatedInequality: wrong kind: " +
1481  e.toString());
1482  CHECK_SOUND(isIneq(ineq),
1483  "ArithTheoremProducer3::negatedInequality: wrong kind: " +
1484  (ineq).toString());
1485  }
1486  Proof pf;
1487  if(withProof()) pf = newPf("negated_inequality", e);
1488 
1489  int kind;
1490  // NOT (op1 LT op2) <==> (op1 GE op2)
1491  // NOT (op1 LE op2) <==> (op1 GT op2)
1492  // NOT (op1 GT op2) <==> (op1 LE op2)
1493  // NOT (op1 GE op2) <==> (op1 LT op2)
1494  kind =
1495  isLT(ineq) ? GE :
1496  isLE(ineq) ? GT :
1497  isGT(ineq) ? LE :
1498  LT;
1499  return newRWTheorem(e, Expr(kind, ineq[0], ineq[1]), Assumptions::emptyAssump(), pf);
1500 }
1501 
1502 //takes two ineqs "|- alpha LT|LE t" and "|- t LT|LE beta"
1503 //and returns "|- alpha LT|LE beta"
1504 Theorem ArithTheoremProducer3::realShadow(const Theorem& alphaLTt,
1505  const Theorem& tLTbeta)
1506 {
1507  const Expr& expr1 = alphaLTt.getExpr();
1508  const Expr& expr2 = tLTbeta.getExpr();
1509  if(CHECK_PROOFS) {
1510  CHECK_SOUND((isLE(expr1) || isLT(expr1)) &&
1511  (isLE(expr2) || isLT(expr2)),
1512  "ArithTheoremProducer3::realShadow: Wrong Kind: " +
1513  alphaLTt.toString() + tLTbeta.toString());
1514 
1515  CHECK_SOUND(expr1[1] == expr2[0],
1516  "ArithTheoremProducer3::realShadow:"
1517  " t must be same for both inputs: " +
1518  expr1[1].toString() + " , " + expr2[0].toString());
1519  }
1520  Assumptions a(alphaLTt, tLTbeta);
1521  int firstKind = expr1.getKind();
1522  int secondKind = expr2.getKind();
1523  int kind = (firstKind == secondKind) ? firstKind : LT;
1524  Proof pf;
1525  if(withProof()) {
1526  vector<Proof> pfs;
1527  pfs.push_back(alphaLTt.getProof());
1528  pfs.push_back(tLTbeta.getProof());
1529  pf = newPf("real_shadow",expr1, expr2, pfs);
1530  }
1531  return newTheorem(Expr(kind, expr1[0], expr2[1]), a, pf);
1532 }
1533 
1534 //! alpha <= t <= alpha ==> t = alpha
1535 
1536 /*! takes two ineqs "|- alpha LE t" and "|- t LE alpha"
1537  and returns "|- t = alpha"
1538 */
1539 Theorem ArithTheoremProducer3::realShadowEq(const Theorem& alphaLEt,
1540  const Theorem& tLEalpha)
1541 {
1542  const Expr& expr1 = alphaLEt.getExpr();
1543  const Expr& expr2 = tLEalpha.getExpr();
1544  if(CHECK_PROOFS) {
1545  CHECK_SOUND(isLE(expr1) && isLE(expr2),
1546  "ArithTheoremProducer3::realShadowLTLE: Wrong Kind: " +
1547  alphaLEt.toString() + tLEalpha.toString());
1548 
1549  CHECK_SOUND(expr1[1] == expr2[0],
1550  "ArithTheoremProducer3::realShadowLTLE:"
1551  " t must be same for both inputs: " +
1552  alphaLEt.toString() + " , " + tLEalpha.toString());
1553 
1554  CHECK_SOUND(expr1[0] == expr2[1],
1555  "ArithTheoremProducer3::realShadowLTLE:"
1556  " alpha must be same for both inputs: " +
1557  alphaLEt.toString() + " , " + tLEalpha.toString());
1558  }
1559  Assumptions a(alphaLEt, tLEalpha);
1560  Proof pf;
1561  if(withProof()) {
1562  vector<Proof> pfs;
1563  pfs.push_back(alphaLEt.getProof());
1564  pfs.push_back(tLEalpha.getProof());
1565  pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs);
1566  }
1567  return newRWTheorem(expr1[0], expr1[1], a, pf);
1568 }
1569 
1570 Theorem
1571 ArithTheoremProducer3::finiteInterval(const Theorem& aLEt,
1572  const Theorem& tLEac,
1573  const Theorem& isInta,
1574  const Theorem& isIntt) {
1575  const Expr& e1 = aLEt.getExpr();
1576  const Expr& e2 = tLEac.getExpr();
1577  if(CHECK_PROOFS) {
1578  CHECK_SOUND(isLE(e1) && isLE(e2),
1579  "ArithTheoremProducer3::finiteInterval:\n e1 = "
1580  +e1.toString()+"\n e2 = "+e2.toString());
1581  // term 't' is the same in both inequalities
1582  CHECK_SOUND(e1[1] == e2[0],
1583  "ArithTheoremProducer3::finiteInterval:\n e1 = "
1584  +e1.toString()+"\n e2 = "+e2.toString());
1585  // RHS in e2 is (a+c)
1586  CHECK_SOUND(isPlus(e2[1]) && e2[1].arity() == 2,
1587  "ArithTheoremProducer3::finiteInterval:\n e1 = "
1588  +e1.toString()+"\n e2 = "+e2.toString());
1589  // term 'a' in LHS of e1 and RHS of e2 is the same
1590  CHECK_SOUND(e1[0] == e2[1][0],
1591  "ArithTheoremProducer3::finiteInterval:\n e1 = "
1592  +e1.toString()+"\n e2 = "+e2.toString());
1593  // 'c' in the RHS of e2 is a positive integer constant
1594  CHECK_SOUND(e2[1][1].isRational() && e2[1][1].getRational().isInteger()
1595  && e2[1][1].getRational() >= 1,
1596  "ArithTheoremProducer3::finiteInterval:\n e1 = "
1597  +e1.toString()+"\n e2 = "+e2.toString());
1598  // Integrality constraints
1599  const Expr& isIntaExpr = isInta.getExpr();
1600  const Expr& isInttExpr = isIntt.getExpr();
1601  CHECK_SOUND(isIntPred(isIntaExpr) && isIntaExpr[0] == e1[0],
1602  "Wrong integrality constraint:\n e1 = "
1603  +e1.toString()+"\n isInta = "+isIntaExpr.toString());
1604  CHECK_SOUND(isIntPred(isInttExpr) && isInttExpr[0] == e1[1],
1605  "Wrong integrality constraint:\n e1 = "
1606  +e1.toString()+"\n isIntt = "+isInttExpr.toString());
1607  }
1608  vector<Theorem> thms;
1609  thms.push_back(aLEt);
1610  thms.push_back(tLEac);
1611  thms.push_back(isInta);
1612  thms.push_back(isIntt);
1613  Assumptions a(thms);
1614  Proof pf;
1615  if(withProof()) {
1616  vector<Expr> es;
1617  vector<Proof> pfs;
1618  es.push_back(e1);
1619  es.push_back(e2);
1620  es.push_back(isInta.getExpr());
1621  es.push_back(isIntt.getExpr());
1622  pfs.push_back(aLEt.getProof());
1623  pfs.push_back(tLEac.getProof());
1624  pfs.push_back(isInta.getProof());
1625  pfs.push_back(isIntt.getProof());
1626  pf = newPf("finite_interval", es, pfs);
1627  }
1628  // Construct GRAY_SHADOW(t, a, 0, c)
1629  Expr g(grayShadow(e1[1], e1[0], 0, e2[1][1].getRational()));
1630  return newTheorem(g, a, pf);
1631 }
1632 
1633 
1634 // Dark & Gray shadows when a <= b
1635 Theorem ArithTheoremProducer3::darkGrayShadow2ab(const Theorem& betaLEbx,
1636  const Theorem& axLEalpha,
1637  const Theorem& isIntAlpha,
1638  const Theorem& isIntBeta,
1639  const Theorem& isIntx) {
1640  const Expr& expr1 = betaLEbx.getExpr();
1641  const Expr& expr2 = axLEalpha.getExpr();
1642  const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
1643  const Expr& isIntBetaExpr = isIntBeta.getExpr();
1644  const Expr& isIntxExpr = isIntx.getExpr();
1645 
1646  if(CHECK_PROOFS) {
1647  CHECK_SOUND(isLE(expr1) && isLE(expr2),
1648  "ArithTheoremProducer3::darkGrayShadow2ab: Wrong Kind: " +
1649  betaLEbx.toString() + axLEalpha.toString());
1650  }
1651 
1652  const Expr& beta = expr1[0];
1653  const Expr& bx = expr1[1];
1654  const Expr& ax = expr2[0];
1655  const Expr& alpha = expr2[1];
1656  Rational a = isMult(ax)? ax[0].getRational() : 1;
1657  Rational b = isMult(bx)? bx[0].getRational() : 1;
1658  const Expr& x = isMult(ax)? ax[1] : ax;
1659 
1660  if(CHECK_PROOFS) {
1661  // Integrality constraints
1662  CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
1663  "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1664  "wrong integrality constraint:\n alpha = "
1665  +alpha.toString()+"\n isIntAlpha = "
1666  +isIntAlphaExpr.toString());
1667  CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
1668  "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1669  "wrong integrality constraint:\n beta = "
1670  +beta.toString()+"\n isIntBeta = "
1671  +isIntBetaExpr.toString());
1672  CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
1673  "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1674  "wrong integrality constraint:\n x = "
1675  +x.toString()+"\n isIntx = "
1676  +isIntxExpr.toString());
1677  // Expressions ax and bx should match on x
1678  CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
1679  "ArithTheoremProducer3::darkGrayShadow2ab:\n ax<=alpha: " +
1680  axLEalpha.toString());
1681  CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
1682  "ArithTheoremProducer3::darkGrayShadow2ab:\n beta<=bx: "
1683  +betaLEbx.toString()
1684  +"\n ax<=alpha: "+ axLEalpha.toString());
1685  CHECK_SOUND(1 <= a && a <= b && 2 <= b,
1686  "ArithTheoremProducer3::darkGrayShadow2ab:\n beta<=bx: "
1687  +betaLEbx.toString()
1688  +"\n ax<=alpha: "+ axLEalpha.toString());
1689  }
1690  vector<Theorem> thms;
1691  thms.push_back(betaLEbx);
1692  thms.push_back(axLEalpha);
1693  thms.push_back(isIntAlpha);
1694  thms.push_back(isIntBeta);
1695  thms.push_back(isIntx);
1696  Assumptions A(thms);
1697 
1698  Expr bAlpha = multExpr(rat(b), alpha);
1699  Expr aBeta = multExpr(rat(a), beta);
1700  Expr t = minusExpr(bAlpha, aBeta);
1701  Expr d = darkShadow(rat(a*b-1), t);
1702  Expr g = grayShadow(ax, alpha, -a+1, 0);
1703 
1704  Proof pf;
1705  if(withProof()) {
1706  vector<Expr> exprs;
1707  exprs.push_back(expr1);
1708  exprs.push_back(expr2);
1709  exprs.push_back(d);
1710  exprs.push_back(g);
1711 
1712  vector<Proof> pfs;
1713  pfs.push_back(betaLEbx.getProof());
1714  pfs.push_back(axLEalpha.getProof());
1715  pfs.push_back(isIntAlpha.getProof());
1716  pfs.push_back(isIntBeta.getProof());
1717  pfs.push_back(isIntx.getProof());
1718 
1719  pf = newPf("dark_grayshadow_2ab", exprs, pfs);
1720  }
1721 
1722  return newTheorem((d || g), A, pf);
1723 }
1724 
1725 // Dark & Gray shadows when b <= a
1726 Theorem ArithTheoremProducer3::darkGrayShadow2ba(const Theorem& betaLEbx,
1727  const Theorem& axLEalpha,
1728  const Theorem& isIntAlpha,
1729  const Theorem& isIntBeta,
1730  const Theorem& isIntx) {
1731  const Expr& expr1 = betaLEbx.getExpr();
1732  const Expr& expr2 = axLEalpha.getExpr();
1733  const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
1734  const Expr& isIntBetaExpr = isIntBeta.getExpr();
1735  const Expr& isIntxExpr = isIntx.getExpr();
1736 
1737  if(CHECK_PROOFS) {
1738  CHECK_SOUND(isLE(expr1) && isLE(expr2),
1739  "ArithTheoremProducer3::darkGrayShadow2ba: Wrong Kind: " +
1740  betaLEbx.toString() + axLEalpha.toString());
1741  }
1742 
1743  const Expr& beta = expr1[0];
1744  const Expr& bx = expr1[1];
1745  const Expr& ax = expr2[0];
1746  const Expr& alpha = expr2[1];
1747  Rational a = isMult(ax)? ax[0].getRational() : 1;
1748  Rational b = isMult(bx)? bx[0].getRational() : 1;
1749  const Expr& x = isMult(ax)? ax[1] : ax;
1750 
1751  if(CHECK_PROOFS) {
1752  // Integrality constraints
1753  CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
1754  "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1755  "wrong integrality constraint:\n alpha = "
1756  +alpha.toString()+"\n isIntAlpha = "
1757  +isIntAlphaExpr.toString());
1758  CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
1759  "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1760  "wrong integrality constraint:\n beta = "
1761  +beta.toString()+"\n isIntBeta = "
1762  +isIntBetaExpr.toString());
1763  CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
1764  "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1765  "wrong integrality constraint:\n x = "
1766  +x.toString()+"\n isIntx = "
1767  +isIntxExpr.toString());
1768  // Expressions ax and bx should match on x
1769  CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
1770  "ArithTheoremProducer3::darkGrayShadow2ba:\n ax<=alpha: " +
1771  axLEalpha.toString());
1772  CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
1773  "ArithTheoremProducer3::darkGrayShadow2ba:\n beta<=bx: "
1774  +betaLEbx.toString()
1775  +"\n ax<=alpha: "+ axLEalpha.toString());
1776  CHECK_SOUND(1 <= b && b <= a && 2 <= a,
1777  "ArithTheoremProducer3::darkGrayShadow2ba:\n beta<=bx: "
1778  +betaLEbx.toString()
1779  +"\n ax<=alpha: "+ axLEalpha.toString());
1780  }
1781  vector<Theorem> thms;
1782  thms.push_back(betaLEbx);
1783  thms.push_back(axLEalpha);
1784  thms.push_back(isIntAlpha);
1785  thms.push_back(isIntBeta);
1786  thms.push_back(isIntx);
1787  Assumptions A(thms);
1788  Proof pf;
1789  if(withProof()) {
1790  vector<Proof> pfs;
1791  pfs.push_back(betaLEbx.getProof());
1792  pfs.push_back(axLEalpha.getProof());
1793  pfs.push_back(isIntAlpha.getProof());
1794  pfs.push_back(isIntBeta.getProof());
1795  pfs.push_back(isIntx.getProof());
1796 
1797  pf = newPf("dark_grayshadow_2ba", betaLEbx.getExpr(),
1798  axLEalpha.getExpr(), pfs);
1799  }
1800 
1801  Expr bAlpha = multExpr(rat(b), alpha);
1802  Expr aBeta = multExpr(rat(a), beta);
1803  Expr t = minusExpr(bAlpha, aBeta);
1804  Expr d = darkShadow(rat(a*b-1), t);
1805  Expr g = grayShadow(bx, beta, 0, b-1);
1806  return newTheorem((d || g), A, pf);
1807 }
1808 
1809 /*! takes a dark shadow and expands it into an inequality.
1810 */
1811 Theorem ArithTheoremProducer3::expandDarkShadow(const Theorem& darkShadow) {
1812  const Expr& theShadow = darkShadow.getExpr();
1813  if(CHECK_PROOFS){
1814  CHECK_SOUND(isDarkShadow(theShadow),
1815  "ArithTheoremProducer3::expandDarkShadow: not DARK_SHADOW: " +
1816  theShadow.toString());
1817  }
1818  Proof pf;
1819  if(withProof())
1820  pf = newPf("expand_dark_shadow", theShadow, darkShadow.getProof());
1821  return newTheorem(leExpr(theShadow[0], theShadow[1]), darkShadow.getAssumptionsRef(), pf);
1822 }
1823 
1824 
1825 // takes a grayShadow (c1==c2) and expands it into an equality
1826 Theorem ArithTheoremProducer3::expandGrayShadow0(const Theorem& grayShadow) {
1827  const Expr& theShadow = grayShadow.getExpr();
1828  if(CHECK_PROOFS) {
1829  CHECK_SOUND(isGrayShadow(theShadow),
1830  "ArithTheoremProducer3::expandGrayShadowConst0:"
1831  " not GRAY_SHADOW: " +
1832  theShadow.toString());
1833  CHECK_SOUND(theShadow[2] == theShadow[3],
1834  "ArithTheoremProducer3::expandGrayShadow0: c1!=c2: " +
1835  theShadow.toString());
1836  }
1837  Proof pf;
1838  if(withProof()) pf = newPf("expand_gray_shadowconst0", theShadow,
1839  grayShadow.getProof());
1840  const Expr& v = theShadow[0];
1841  const Expr& e = theShadow[1];
1842  return newRWTheorem(v, e + theShadow[2], grayShadow.getAssumptionsRef(), pf);
1843 }
1844 
1845 
1846 // G ==> (G1 or G2) and (!G1 or !G2),
1847 // where G = G(x, e, c1, c2),
1848 // G1 = G(x,e,c1,c)
1849 // G2 = G(x,e,c+1,c2),
1850 // and c = floor((c1+c2)/2)
1851 // DEJAN: TRY THE MIDDLE IMMEDIATELY, WE MIGHT GET LUCKY
1852 Theorem ArithTheoremProducer3::splitGrayShadow(const Theorem& gThm) {
1853  const Expr& theShadow = gThm.getExpr();
1854  if(CHECK_PROOFS) {
1855  CHECK_SOUND(isGrayShadow(theShadow),
1856  "ArithTheoremProducer3::expandGrayShadowConst: not a shadow" +
1857  theShadow.toString());
1858  }
1859 
1860  const Rational& c1 = theShadow[2].getRational();
1861  const Rational& c2 = theShadow[3].getRational();
1862 
1863  if(CHECK_PROOFS) {
1864  CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
1865  "ArithTheoremProducer3::expandGrayShadow: " +
1866  theShadow.toString());
1867  }
1868 
1869  const Expr& v = theShadow[0];
1870  const Expr& e = theShadow[1];
1871 
1872  Proof pf;
1873  Rational c(floor((c1+c2) / 2));
1874  Expr g1(grayShadow(v, e, c1, c));
1875  Expr g2(grayShadow(v, e, c+1, c2));
1876 
1877  if(withProof()){
1878  vector<Expr> exprs;
1879  exprs.push_back(theShadow);
1880  exprs.push_back(g1);
1881  exprs.push_back(g2);
1882  pf = newPf("split_gray_shadow", exprs, gThm.getProof());
1883  }
1884 
1885  return newTheorem((g1 || g2) && (!g1 || !g2), gThm.getAssumptionsRef(), pf);
1886 }
1887 
1888 
1889 Theorem ArithTheoremProducer3::expandGrayShadow(const Theorem& gThm) {
1890  const Expr& theShadow = gThm.getExpr();
1891  if(CHECK_PROOFS) {
1892  CHECK_SOUND(isGrayShadow(theShadow),
1893  "ArithTheoremProducer3::expandGrayShadowConst: not a shadow" +
1894  theShadow.toString());
1895  }
1896 
1897  const Rational& c1 = theShadow[2].getRational();
1898  const Rational& c2 = theShadow[3].getRational();
1899 
1900  if(CHECK_PROOFS) {
1901  CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
1902  "ArithTheoremProducer3::expandGrayShadow: " +
1903  theShadow.toString());
1904  }
1905 
1906  const Expr& v = theShadow[0];
1907  const Expr& e = theShadow[1];
1908 
1909  Proof pf;
1910  if(withProof())
1911  pf = newPf("expand_gray_shadow", theShadow, gThm.getProof());
1912  Expr ineq1(leExpr(e+rat(c1), v));
1913  Expr ineq2(leExpr(v, e+rat(c2)));
1914  return newTheorem(ineq1 && ineq2, gThm.getAssumptionsRef(), pf);
1915 }
1916 
1917 
1918 // Expanding GRAY_SHADOW(a*x, c, b), where c is a constant
1919 Theorem
1920 ArithTheoremProducer3::expandGrayShadowConst(const Theorem& gThm) {
1921  const Expr& theShadow = gThm.getExpr();
1922  const Expr& ax = theShadow[0];
1923  const Expr& cExpr = theShadow[1];
1924  const Expr& bExpr = theShadow[2];
1925 
1926  if(CHECK_PROOFS) {
1927  CHECK_SOUND(!isMult(ax) || ax[0].isRational(),
1928  "ArithTheoremProducer3::expandGrayShadowConst: "
1929  "'a' in a*x is not a const: " +theShadow.toString());
1930  }
1931 
1932  Rational a = isMult(ax)? ax[0].getRational() : 1;
1933 
1934  if(CHECK_PROOFS) {
1935  CHECK_SOUND(isGrayShadow(theShadow),
1936  "ArithTheoremProducer3::expandGrayShadowConst: "
1937  "not a GRAY_SHADOW: " +theShadow.toString());
1938  CHECK_SOUND(a.isInteger() && a >= 1,
1939  "ArithTheoremProducer3::expandGrayShadowConst: "
1940  "'a' is not integer: " +theShadow.toString());
1941  CHECK_SOUND(cExpr.isRational(),
1942  "ArithTheoremProducer3::expandGrayShadowConst: "
1943  "'c' is not rational" +theShadow.toString());
1944  CHECK_SOUND(bExpr.isRational() && bExpr.getRational().isInteger(),
1945  "ArithTheoremProducer3::expandGrayShadowConst: b not integer: "
1946  +theShadow.toString());
1947  }
1948 
1949  const Rational& b = bExpr.getRational();
1950  const Rational& c = cExpr.getRational();
1951  Rational j = constRHSGrayShadow(c,b,a);
1952  // Compute sign(b)*j(c,b,a)
1953  Rational signB = (b>0)? 1 : -1;
1954  // |b| (absolute value of b)
1955  Rational bAbs = abs(b);
1956 
1957  const Assumptions& assump(gThm.getAssumptionsRef());
1958  Proof pf;
1959  Theorem conc; // Conclusion of the rule
1960 
1961  if(bAbs < j) {
1962  if(withProof())
1963  pf = newPf("expand_gray_shadow_const_0", theShadow,
1964  gThm.getProof());
1965  conc = newTheorem(d_em->falseExpr(), assump, pf);
1966  } else if(bAbs < a+j) {
1967  if(withProof())
1968  pf = newPf("expand_gray_shadow_const_1", theShadow,
1969  gThm.getProof());
1970  conc = newRWTheorem(ax, rat(c+b-signB*j), assump, pf);
1971  } else {
1972  if(withProof())
1973  pf = newPf("expand_gray_shadow_const", theShadow,
1974  gThm.getProof());
1975  Expr newGrayShadow(Expr(GRAY_SHADOW, ax, cExpr, rat(b-signB*(a+j))));
1976  conc = newTheorem(ax.eqExpr(rat(c+b-signB*j)).orExpr(newGrayShadow),
1977  assump, pf);
1978  }
1979 
1980  return conc;
1981 }
1982 
1983 
1984 Theorem
1985 ArithTheoremProducer3::grayShadowConst(const Theorem& gThm) {
1986  const Expr& g = gThm.getExpr();
1987  bool checkProofs(CHECK_PROOFS);
1988  if(checkProofs) {
1989  CHECK_SOUND(isGrayShadow(g), "ArithTheoremProducer3::grayShadowConst("
1990  +g.toString()+")");
1991  }
1992 
1993  const Expr& ax = g[0];
1994  const Expr& e = g[1];
1995  const Rational& c1 = g[2].getRational();
1996  const Rational& c2 = g[3].getRational();
1997  Expr aExpr, x;
1998  d_theoryArith->separateMonomial(ax, aExpr, x);
1999 
2000  if(checkProofs) {
2002  "ArithTheoremProducer3::grayShadowConst("+g.toString()+")");
2003  CHECK_SOUND(aExpr.isRational(),
2004  "ArithTheoremProducer3::grayShadowConst("+g.toString()+")");
2005  }
2006 
2007  const Rational& a = aExpr.getRational();
2008  const Rational& c = e.getRational();
2009 
2010  if(checkProofs) {
2011  CHECK_SOUND(a.isInteger() && a >= 2,
2012  "ArithTheoremProducer3::grayShadowConst("+g.toString()+")");
2013  }
2014 
2015  Rational newC1 = ceil((c1+c)/a), newC2 = floor((c2+c)/a);
2016  Expr newG((newC1 > newC2)? d_em->falseExpr()
2017  : grayShadow(x, rat(0), newC1, newC2));
2018  Proof pf;
2019  if(withProof())
2020  pf = newPf("gray_shadow_const", g, newG, gThm.getProof());
2021  return newTheorem(newG, gThm.getAssumptionsRef(), pf);
2022 }
2023 
2024 
2025 Rational ArithTheoremProducer3::constRHSGrayShadow(const Rational& c,
2026  const Rational& b,
2027  const Rational& a) {
2028  DebugAssert(c.isInteger() &&
2029  b.isInteger() &&
2030  a.isInteger() &&
2031  b != 0,
2032  "ArithTheoremProducer3::constRHSGrayShadow: a, b, c must be ints");
2033  if (b > 0)
2034  return mod(c+b, a);
2035  else
2036  return mod(a-(c+b), a);
2037 }
2038 
2039 /*! Takes a Theorem(\\alpha < \\beta) and returns
2040  * Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1)
2041  * where \\alpha and \\beta are integer expressions
2042  */
2043 Theorem ArithTheoremProducer3::lessThanToLE(const Theorem& less,
2044  const Theorem& isIntLHS,
2045  const Theorem& isIntRHS,
2046  bool changeRight) {
2047  const Expr& ineq = less.getExpr();
2048  const Expr& isIntLHSexpr = isIntLHS.getExpr();
2049  const Expr& isIntRHSexpr = isIntRHS.getExpr();
2050 
2051  if(CHECK_PROOFS) {
2052  CHECK_SOUND(isLT(ineq),
2053  "ArithTheoremProducer3::LTtoLE: ineq must be <");
2054  // Integrality check
2055  CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0],
2056  "ArithTheoremProducer3::lessThanToLE: bad integrality check:\n"
2057  " ineq = "+ineq.toString()+"\n isIntLHS = "
2058  +isIntLHSexpr.toString());
2059  CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1],
2060  "ArithTheoremProducer3::lessThanToLE: bad integrality check:\n"
2061  " ineq = "+ineq.toString()+"\n isIntRHS = "
2062  +isIntRHSexpr.toString());
2063  }
2064  vector<Theorem> thms;
2065  thms.push_back(less);
2066  thms.push_back(isIntLHS);
2067  thms.push_back(isIntRHS);
2068  Assumptions a(thms);
2069  Proof pf;
2070  Expr le = changeRight?
2071  leExpr(ineq[0], ineq[1] + rat(-1))
2072  : leExpr(ineq[0] + rat(1), ineq[1]);
2073  if(withProof()) {
2074  vector<Proof> pfs;
2075  pfs.push_back(less.getProof());
2076  pfs.push_back(isIntLHS.getProof());
2077  pfs.push_back(isIntRHS.getProof());
2078  pf = newPf(changeRight? "lessThan_To_LE_rhs" : "lessThan_To_LE_lhs",
2079  ineq,le, pfs);
2080  }
2081 
2082  return newRWTheorem(ineq, le, a, pf);
2083 }
2084 
2085 
2086 /*! \param eqn is an equation 0 = a.x or 0 = c + a.x
2087  * \param isIntx is a proof of IS_INTEGER(x)
2088  *
2089  * \return the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else
2090  * return the theorem 0 = c + a.x <==> false.
2091  *
2092  * It also handles the special case of 0 = a.x <==> x = 0
2093  */
2094 Theorem
2095 ArithTheoremProducer3::intVarEqnConst(const Expr& eqn,
2096  const Theorem& isIntx) {
2097  const Expr& left(eqn[0]);
2098  const Expr& right(eqn[1]);
2099  const Expr& isIntxexpr(isIntx.getExpr());
2100 
2101  if(CHECK_PROOFS) {
2102  CHECK_SOUND((isMult(right) && right[0].isRational())
2103  || (right.arity() == 2 && isPlus(right)
2104  && right[0].isRational()
2105  && ((!isMult(right[1]) || right[1][0].isRational()))),
2106  "ArithTheoremProducer3::intVarEqnConst: "
2107  "rhs has a wrong format: " + right.toString());
2108  CHECK_SOUND(left.isRational() && 0 == left.getRational(),
2109  "ArithTheoremProducer3:intVarEqnConst:left is not a zero: " +
2110  left.toString());
2111  }
2112  // Integrality constraint
2113  Expr x(right);
2114  Rational a(1), c(0);
2115  if(isMult(right)) {
2116  Expr aExpr;
2117  d_theoryArith->separateMonomial(right, aExpr, x);
2118  a = aExpr.getRational();
2119  } else { // right is a PLUS
2120  c = right[0].getRational();
2121  Expr aExpr;
2122  d_theoryArith->separateMonomial(right[1], aExpr, x);
2123  a = aExpr.getRational();
2124  }
2125  if(CHECK_PROOFS) {
2126  CHECK_SOUND(isIntPred(isIntxexpr) && isIntxexpr[0] == x,
2127  "ArithTheoremProducer3:intVarEqnConst: "
2128  "bad integrality constraint:\n right = " +
2129  right.toString()+"\n isIntx = "+isIntxexpr.toString());
2130  CHECK_SOUND(a!=0, "ArithTheoremProducer3:intVarEqnConst: eqn = "
2131  +eqn.toString());
2132  }
2133  const Assumptions& assump(isIntx.getAssumptionsRef());
2134 
2135  /*
2136  Proof pf;
2137  if(withProof())
2138  pf = newPf("int_const_eq", eqn, isIntx.getProof());
2139 
2140  // Solve for x: x = r = -c/a
2141  Rational r(-c/a);
2142 
2143  if(r.isInteger()){
2144  return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf);
2145  else
2146  return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
2147  */
2148 
2149  Proof pf;
2150  // Solve for x: x = r = -c/a
2151  Rational r(-c/a);
2152 
2153  if(r.isInteger()){
2154  if(withProof())
2155  pf = newPf("int_const_eq", eqn, x.eqExpr(rat(r)),isIntx.getProof());
2156  return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf);
2157  }
2158  else{
2159  if(withProof())
2160  pf = newPf("int_const_eq", eqn, d_em->falseExpr(),isIntx.getProof());
2161  return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
2162  }
2163 }
2164 
2165 
2166 Expr
2167 ArithTheoremProducer3::create_t(const Expr& eqn) {
2168  const Expr& lhs = eqn[0];
2169  DebugAssert(isMult(lhs),
2170  CLASS_NAME "create_t : lhs must be a MULT"
2171  + lhs.toString());
2172  const Expr& x = lhs[1];
2173  Rational m = lhs[0].getRational()+1;
2174  DebugAssert(m > 0, "ArithTheoremProducer3::create_t: m = "+m.toString());
2175  vector<Expr> kids;
2176  if(isPlus(eqn[1]))
2177  sumModM(kids, eqn[1], m, m);
2178  else
2179  kids.push_back(monomialModM(eqn[1], m, m));
2180 
2181  kids.push_back(multExpr(rat(1/m), x));
2182  return plusExpr(kids);
2183 }
2184 
2185 Expr
2186 ArithTheoremProducer3::create_t2(const Expr& lhs, const Expr& rhs,
2187  const Expr& sigma) {
2188  Rational m = lhs[0].getRational()+1;
2189  DebugAssert(m > 0, "ArithTheoremProducer3::create_t2: m = "+m.toString());
2190  vector<Expr> kids;
2191  if(isPlus(rhs))
2192  sumModM(kids, rhs, m, -1);
2193  else {
2194  kids.push_back(rat(0)); // For canonical form
2195  Expr monom = monomialModM(rhs, m, -1);
2196  if(!monom.isRational())
2197  kids.push_back(monom);
2198  else
2199  DebugAssert(monom.getRational() == 0, "");
2200  }
2201  kids.push_back(rat(m)*sigma);
2202  return plusExpr(kids);
2203 }
2204 
2205 Expr
2206 ArithTheoremProducer3::create_t3(const Expr& lhs, const Expr& rhs,
2207  const Expr& sigma) {
2208  const Rational& a = lhs[0].getRational();
2209  Rational m = a+1;
2210  DebugAssert(m > 0, "ArithTheoremProducer3::create_t3: m = "+m.toString());
2211  vector<Expr> kids;
2212  if(isPlus(rhs))
2213  sumMulF(kids, rhs, m, 1);
2214  else {
2215  kids.push_back(rat(0)); // For canonical form
2216  Expr monom = monomialMulF(rhs, m, 1);
2217  if(!monom.isRational())
2218  kids.push_back(monom);
2219  else
2220  DebugAssert(monom.getRational() == 0, "");
2221  }
2222  kids.push_back(rat(-a)*sigma);
2223  return plusExpr(kids);
2224 }
2225 
2226 Rational
2227 ArithTheoremProducer3::modEq(const Rational& i, const Rational& m) {
2228  DebugAssert(m > 0, "ArithTheoremProducer3::modEq: m = "+m.toString());
2229  Rational half(1,2);
2230  Rational res((i - m*(floor((i/m) + half))));
2231  TRACE("arith eq", "modEq("+i.toString()+", "+m.toString()+") = ", res, "");
2232  return res;
2233 }
2234 
2235 Rational
2236 ArithTheoremProducer3::f(const Rational& i, const Rational& m) {
2237  DebugAssert(m > 0, "ArithTheoremProducer3::f: m = "+m.toString());
2238  Rational half(1,2);
2239  return (floor(i/m + half)+modEq(i,m));
2240 }
2241 
2242 void
2243 ArithTheoremProducer3::sumModM(vector<Expr>& summands, const Expr& sum,
2244  const Rational& m, const Rational& divisor) {
2245  DebugAssert(divisor != 0, "ArithTheoremProducer3::sumModM: divisor = "
2246  +divisor.toString());
2247  Expr::iterator i = sum.begin();
2248  DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
2249  Rational C = i->getRational();
2250  C = modEq(C,m)/divisor;
2251  summands.push_back(rat(C));
2252  i++;
2253  for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
2254  Expr monom = monomialModM(*i, m, divisor);
2255  if(!monom.isRational())
2256  summands.push_back(monom);
2257  else
2258  DebugAssert(monom.getRational() == 0, "");
2259  }
2260 }
2261 
2262 Expr
2263 ArithTheoremProducer3::monomialModM(const Expr& i,
2264  const Rational& m, const Rational& divisor)
2265 {
2266  DebugAssert(divisor != 0, "ArithTheoremProducer3::monomialModM: divisor = "
2267  +divisor.toString());
2268  Expr res;
2269  if(isMult(i)) {
2270  Rational ai = i[0].getRational();
2271  ai = modEq(ai,m)/divisor;
2272  if(0 == ai) res = rat(0);
2273  else if(1 == ai && i.arity() == 2) res = i[1];
2274  else {
2275  vector<Expr> kids = i.getKids();
2276  kids[0] = rat(ai);
2277  res = multExpr(kids);
2278  }
2279  } else { // It's a single variable
2280  Rational ai = modEq(1,m)/divisor;
2281  if(1 == ai) res = i;
2282  else res = rat(ai)*i;
2283  }
2284  DebugAssert(!res.isNull(), "ArithTheoremProducer3::monomialModM()");
2285  TRACE("arith eq", "monomialModM(i="+i.toString()+", m="+m.toString()
2286  +", div="+divisor.toString()+") = ", res, "");
2287  return res;
2288 }
2289 
2290 void
2291 ArithTheoremProducer3::sumMulF(vector<Expr>& summands, const Expr& sum,
2292  const Rational& m, const Rational& divisor) {
2293  DebugAssert(divisor != 0, "ArithTheoremProducer3::sumMulF: divisor = "
2294  +divisor.toString());
2295  Expr::iterator i = sum.begin();
2296  DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
2297  Rational C = i->getRational();
2298  C = f(C,m)/divisor;
2299  summands.push_back(rat(C));
2300  i++;
2301  for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
2302  Expr monom = monomialMulF(*i, m, divisor);
2303  if(!monom.isRational())
2304  summands.push_back(monom);
2305  else
2306  DebugAssert(monom.getRational() == 0, "");
2307  }
2308 }
2309 
2310 Expr
2311 ArithTheoremProducer3::monomialMulF(const Expr& i,
2312  const Rational& m, const Rational& divisor)
2313 {
2314  DebugAssert(divisor != 0, "ArithTheoremProducer3::monomialMulF: divisor = "
2315  +divisor.toString());
2316  Rational ai = isMult(i) ? (i)[0].getRational() : 1;
2317  Expr xi = isMult(i) ? (i)[1] : (i);
2318  ai = f(ai,m)/divisor;
2319  if(0 == ai) return rat(0);
2320  if(1 == ai) return xi;
2321  return multExpr(rat(ai), xi);
2322 }
2323 
2324 // This recursive function accepts a term, t, and a 'map' of
2325 // substitutions [x1/t1, x2/t2,...,xn/tn]. it returns a t' which is
2326 // basically t[x1/t1,x2/t2...xn/tn]
2327 Expr
2328 ArithTheoremProducer3::substitute(const Expr& term, ExprMap<Expr>& eMap)
2329 {
2330  ExprMap<Expr>::iterator i, iend = eMap.end();
2331 
2332  i = eMap.find(term);
2333  if(iend != i)
2334  return (*i).second;
2335 
2336  if (isMult(term)) {
2337  //in this case term is of the form c.x
2338  i = eMap.find(term[1]);
2339  if(iend != i)
2340  return term[0]*(*i).second;
2341  else
2342  return term;
2343  }
2344 
2345  if(isPlus(term)) {
2346  vector<Expr> output;
2347  for(Expr::iterator j = term.begin(), jend = term.end(); j != jend; ++j)
2348  output.push_back(substitute(*j, eMap));
2349  return plusExpr(output);
2350  }
2351  return term;
2352 }
2353 
2354 bool ArithTheoremProducer3::greaterthan(const Expr & l, const Expr & r)
2355 {
2356  // DebugAssert(l != r, "");
2357  if (l==r) return false;
2358 
2359  switch(l.getKind()) {
2360  case RATIONAL_EXPR:
2361  DebugAssert(!r.isRational(), "");
2362  return true;
2363  break;
2364  case POW:
2365  switch (r.getKind()) {
2366  case RATIONAL_EXPR:
2367  // TODO:
2368  // alternately I could return (not greaterthan(r,l))
2369  return false;
2370  break;
2371  case POW:
2372  // x^n > y^n if x > y
2373  // x^n1 > x^n2 if n1 > n2
2374  return
2375  ((r[1] < l[1]) ||
2376  ((r[1]==l[1]) && (r[0].getRational() < l[0].getRational())));
2377  break;
2378 
2379  case MULT:
2380  DebugAssert(r.arity() > 1, "");
2381  DebugAssert((r.arity() > 2) || (r[1] != l), "");
2382  if (r[1] == l) return false;
2383  return greaterthan(l, r[1]);
2384  break;
2385  case PLUS:
2386  DebugAssert(false, "");
2387  return true;
2388  break;
2389  default:
2390  // leaf
2391  return ((r < l[1]) || ((r == l[1]) && l[0].getRational() > 1));
2392  break;
2393  }
2394  break;
2395  case MULT:
2396  DebugAssert(l.arity() > 1, "");
2397  switch (r.getKind()) {
2398  case RATIONAL_EXPR:
2399  return false;
2400  break;
2401  case POW:
2402  DebugAssert(l.arity() > 1, "");
2403  DebugAssert((l.arity() > 2) || (l[1] != r), "");
2404  // TODO:
2405  // alternately return (not greaterthan(r,l)
2406  return ((l[1] == r) || greaterthan(l[1], r));
2407  break;
2408  case MULT:
2409  {
2410 
2411  DebugAssert(r.arity() > 1, "");
2412  Expr::iterator i = l.begin();
2413  Expr::iterator j = r.begin();
2414  ++i;
2415  ++j;
2416  for (; i != l.end() && j != r.end(); ++i, ++j) {
2417  if (*i == *j)
2418  continue;
2419  return greaterthan(*i,*j);
2420  }
2421  DebugAssert(i != l.end() || j != r.end(), "");
2422  if (i == l.end()) {
2423  // r is bigger
2424  return false;
2425  }
2426  else
2427  {
2428  // l is bigger
2429  return true;
2430  }
2431  }
2432  break;
2433  case PLUS:
2434  DebugAssert(false, "");
2435  return true;
2436  break;
2437  default:
2438  // leaf
2439  DebugAssert((l.arity() > 2) || (l[1] != r), "");
2440  return ((l[1] == r) || greaterthan(l[1], r));
2441  break;
2442  }
2443  break;
2444  case PLUS:
2445  DebugAssert(false, "");
2446  return true;
2447  break;
2448  default:
2449  // leaf
2450  switch (r.getKind()) {
2451  case RATIONAL_EXPR:
2452  return false;
2453  break;
2454  case POW:
2455  return ((r[1] < l) || ((r[1] == l) && (r[0].getRational() < 1)));
2456  break;
2457  case MULT:
2458  DebugAssert(r.arity() > 1, "");
2459  DebugAssert((r.arity() > 2) || (r[1] != l), "");
2460  if (l == r[1]) return false;
2461  return greaterthan(l,r[1]);
2462  break;
2463  case PLUS:
2464  DebugAssert(false, "");
2465  return true;
2466  break;
2467  default:
2468  // leaf
2469  return (r < l);
2470  break;
2471  }
2472  break;
2473  }
2474 }
2475 
2476 
2477 /*! IS_INTEGER(x) |= EXISTS (y : INT) y = x
2478  * where x is not already known to be an integer.
2479  */
2480 Theorem ArithTheoremProducer3::IsIntegerElim(const Theorem& isIntx)
2481 {
2482  Expr expr = isIntx.getExpr();
2483  if (CHECK_PROOFS) {
2484  CHECK_SOUND(expr.getKind() == IS_INTEGER,
2485  "Expected IS_INTEGER predicate");
2486  }
2487  expr = expr[0];
2488  DebugAssert(!d_theoryArith->isInteger(expr), "Expected non-integer");
2489 
2490  Assumptions a(isIntx);
2491  Proof pf;
2492 
2493  if (withProof())
2494  {
2495  pf = newPf("isIntElim", isIntx.getProof());
2496  }
2497 
2498  Expr newVar = d_em->newBoundVarExpr(d_theoryArith->intType());
2499  Expr res = d_em->newClosureExpr(EXISTS, newVar, newVar.eqExpr(expr));
2500 
2501  return newTheorem(res, a, pf);
2502 }
2503 
2504 
2505 Theorem
2506 ArithTheoremProducer3::eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
2507  const vector<Theorem>& isIntVars) {
2508  TRACE("arith eq", "eqElimIntRule(", eqn.getExpr(), ") {");
2509  Proof pf;
2510 
2511  if(CHECK_PROOFS)
2512  CHECK_SOUND(eqn.isRewrite(),
2513  "ArithTheoremProducer3::eqElimInt: input must be an equation" +
2514  eqn.toString());
2515 
2516  const Expr& lhs = eqn.getLHS();
2517  const Expr& rhs = eqn.getRHS();
2518  Expr a, x;
2519  d_theoryArith->separateMonomial(lhs, a, x);
2520 
2521  if(CHECK_PROOFS) {
2522  // Checking LHS
2523  const Expr& isIntxe = isIntx.getExpr();
2524  CHECK_SOUND(isIntPred(isIntxe) && isIntxe[0] == x,
2525  "ArithTheoremProducer3::eqElimInt\n eqn = "
2526  +eqn.getExpr().toString()
2527  +"\n isIntx = "+isIntxe.toString());
2529  && a.getRational() >= 2,
2530  "ArithTheoremProducer3::eqElimInt:\n lhs = "+lhs.toString());
2531  // Checking RHS
2532  // It cannot be a division (we don't handle it)
2533  CHECK_SOUND(!isDivide(rhs),
2534  "ArithTheoremProducer3::eqElimInt:\n rhs = "+rhs.toString());
2535  // If it's a single monomial, then it's the only "variable"
2536  if(!isPlus(rhs)) {
2537  Expr c, v;
2538  d_theoryArith->separateMonomial(rhs, c, v);
2539  CHECK_SOUND(isIntVars.size() == 1
2540  && isIntPred(isIntVars[0].getExpr())
2541  && isIntVars[0].getExpr()[0] == v
2542  && isRational(c) && c.getRational().isInteger(),
2543  "ArithTheoremProducer3::eqElimInt:\n rhs = "+rhs.toString()
2544  +"isIntVars.size = "+int2string(isIntVars.size()));
2545  } else { // RHS is a plus
2546  CHECK_SOUND(isIntVars.size() + 1 == (size_t)rhs.arity(),
2547  "ArithTheoremProducer3::eqElimInt: rhs = "+rhs.toString());
2548  // Check the free constant
2549  CHECK_SOUND(isRational(rhs[0]) && rhs[0].getRational().isInteger(),
2550  "ArithTheoremProducer3::eqElimInt: rhs = "+rhs.toString());
2551  // Check the vars
2552  for(size_t i=0, iend=isIntVars.size(); i<iend; ++i) {
2553  Expr c, v;
2554  d_theoryArith->separateMonomial(rhs[i+1], c, v);
2555  const Expr& isInt(isIntVars[i].getExpr());
2556  CHECK_SOUND(isIntPred(isInt) && isInt[0] == v
2557  && isRational(c) && c.getRational().isInteger(),
2558  "ArithTheoremProducer3::eqElimInt:\n rhs["+int2string(i+1)
2559  +"] = "+rhs[i+1].toString()
2560  +"\n isInt = "+isInt.toString());
2561  }
2562  }
2563  }
2564 
2565  // Creating a fresh bound variable
2566  static int varCount(0);
2567  Expr newVar = d_em->newBoundVarExpr("_int_var", int2string(varCount++));
2568  newVar.setType(intType());
2569  Expr t2 = create_t2(lhs, rhs, newVar);
2570  Expr t3 = create_t3(lhs, rhs, newVar);
2571  vector<Expr> vars;
2572  vars.push_back(newVar);
2573  Expr res = d_em->newClosureExpr(EXISTS, vars,
2574  x.eqExpr(t2) && rat(0).eqExpr(t3));
2575 
2576  vector<Theorem> thms(isIntVars);
2577  thms.push_back(isIntx);
2578  thms.push_back(eqn);
2579  Assumptions assump(thms);
2580 
2581  if(withProof()) {
2582  vector<Proof> pfs;
2583  pfs.push_back(eqn.getProof());
2584  pfs.push_back(isIntx.getProof());
2585  vector<Theorem>::const_iterator i=isIntVars.begin(), iend=isIntVars.end();
2586  for(; i!=iend; ++i)
2587  pfs.push_back(i->getProof());
2588  pf = newPf("eq_elim_int", eqn.getExpr(), res, pfs);
2589  }
2590 
2591  Theorem thm(newTheorem(res, assump, pf));
2592  TRACE("arith eq", "eqElimIntRule => ", thm.getExpr(), " }");
2593  return thm;
2594 }
2595 
2596 
2597 Theorem
2598 ArithTheoremProducer3::isIntConst(const Expr& e) {
2599  Proof pf;
2600 
2601  if(CHECK_PROOFS) {
2602  CHECK_SOUND(isIntPred(e) && e[0].isRational(),
2603  "ArithTheoremProducer3::isIntConst(e = "
2604  +e.toString()+")");
2605  }
2606  if(withProof())
2607  pf = newPf("is_int_const", e);
2608  bool isInt = e[0].getRational().isInteger();
2609  return newRWTheorem(e, isInt? d_em->trueExpr() : d_em->falseExpr(), Assumptions::emptyAssump(), pf);
2610 }
2611 
2612 
2613 Theorem
2614 ArithTheoremProducer3::equalLeaves1(const Theorem& thm)
2615 {
2616  Proof pf;
2617  const Expr& e = thm.getRHS();
2618 
2619  if (CHECK_PROOFS) {
2620  CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
2621  e[1].getRational() == Rational(0) &&
2622  e[0].getKind() == PLUS &&
2623  e[0].arity() == 3 &&
2624  e[0][0].getKind() == RATIONAL_EXPR &&
2625  e[0][0].getRational() == Rational(0) &&
2626  e[0][1].getKind() == MULT &&
2627  e[0][1].arity() == 2 &&
2628  e[0][1][0].getKind() == RATIONAL_EXPR &&
2629  e[0][1][0].getRational() == Rational(-1),
2630  "equalLeaves1");
2631  }
2632  if (withProof())
2633  {
2634  vector<Proof> pfs;
2635  pfs.push_back(thm.getProof());
2636  pf = newPf("equalLeaves1", e, pfs);
2637  }
2638  return newRWTheorem(e, e[0][1][1].eqExpr(e[0][2]), thm.getAssumptionsRef(), pf);
2639 }
2640 
2641 
2642 Theorem
2643 ArithTheoremProducer3::equalLeaves2(const Theorem& thm)
2644 {
2645  Proof pf;
2646  const Expr& e = thm.getRHS();
2647 
2648  if (CHECK_PROOFS) {
2649  CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
2650  e[0].getRational() == Rational(0) &&
2651  e[1].getKind() == PLUS &&
2652  e[1].arity() == 3 &&
2653  e[1][0].getKind() == RATIONAL_EXPR &&
2654  e[1][0].getRational() == Rational(0) &&
2655  e[1][1].getKind() == MULT &&
2656  e[1][1].arity() == 2 &&
2657  e[1][1][0].getKind() == RATIONAL_EXPR &&
2658  e[1][1][0].getRational() == Rational(-1),
2659  "equalLeaves2");
2660  }
2661  if (withProof())
2662  {
2663  vector<Proof> pfs;
2664  pfs.push_back(thm.getProof());
2665  pf = newPf("equalLeaves2", e, pfs);
2666  }
2667  return newRWTheorem(e, e[1][1][1].eqExpr(e[1][2]), thm.getAssumptionsRef(), pf);
2668 }
2669 
2670 
2671 Theorem
2672 ArithTheoremProducer3::equalLeaves3(const Theorem& thm)
2673 {
2674  Proof pf;
2675  const Expr& e = thm.getRHS();
2676 
2677  if (CHECK_PROOFS) {
2678  CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
2679  e[1].getRational() == Rational(0) &&
2680  e[0].getKind() == PLUS &&
2681  e[0].arity() == 3 &&
2682  e[0][0].getKind() == RATIONAL_EXPR &&
2683  e[0][0].getRational() == Rational(0) &&
2684  e[0][2].getKind() == MULT &&
2685  e[0][2].arity() == 2 &&
2686  e[0][2][0].getKind() == RATIONAL_EXPR &&
2687  e[0][2][0].getRational() == Rational(-1),
2688  "equalLeaves3");
2689  }
2690  if (withProof())
2691  {
2692  vector<Proof> pfs;
2693  pfs.push_back(thm.getProof());
2694  pf = newPf("equalLeaves3", e, pfs);
2695  }
2696  return newRWTheorem(e, e[0][2][1].eqExpr(e[0][1]), thm.getAssumptionsRef(), pf);
2697 }
2698 
2699 
2700 Theorem
2701 ArithTheoremProducer3::equalLeaves4(const Theorem& thm)
2702 {
2703  Proof pf;
2704  const Expr& e = thm.getRHS();
2705 
2706  if (CHECK_PROOFS) {
2707  CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
2708  e[0].getRational() == Rational(0) &&
2709  e[1].getKind() == PLUS &&
2710  e[1].arity() == 3 &&
2711  e[1][0].getKind() == RATIONAL_EXPR &&
2712  e[1][0].getRational() == Rational(0) &&
2713  e[1][2].getKind() == MULT &&
2714  e[1][2].arity() == 2 &&
2715  e[1][2][0].getKind() == RATIONAL_EXPR &&
2716  e[1][2][0].getRational() == Rational(-1),
2717  "equalLeaves4");
2718  }
2719  if (withProof())
2720  {
2721  vector<Proof> pfs;
2722  pfs.push_back(thm.getProof());
2723  pf = newPf("equalLeaves4", e, pfs);
2724  }
2725  return newRWTheorem(e, e[1][2][1].eqExpr(e[1][1]), thm.getAssumptionsRef(), pf);
2726 }
2727 
2728 Theorem
2729 ArithTheoremProducer3::diseqToIneq(const Theorem& diseq) {
2730  Proof pf;
2731 
2732  const Expr& e = diseq.getExpr();
2733 
2734  if(CHECK_PROOFS) {
2735  CHECK_SOUND(e.isNot() && e[0].isEq(),
2736  "ArithTheoremProducer3::diseqToIneq: expected disequality:\n"
2737  " e = "+e.toString());
2738  }
2739 
2740  const Expr& x = e[0][0];
2741  const Expr& y = e[0][1];
2742 
2743  if(withProof())
2744  pf = newPf(e, diseq.getProof());
2745  return newTheorem(ltExpr(x,y).orExpr(gtExpr(x,y)), diseq.getAssumptionsRef(), pf);
2746 }
2747 
2748 Theorem ArithTheoremProducer3::dummyTheorem(const Expr& e) {
2749  Proof pf;
2750  return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
2751 }
2752 
2753 Theorem ArithTheoremProducer3::oneElimination(const Expr& e) {
2754 
2755  // Check soundness
2756  if (CHECK_PROOFS)
2757  CHECK_SOUND(isMult(e) &&
2758  e.arity() == 2 &&
2759  e[0].isRational() &&
2760  e[0].getRational() == 1,
2761  "oneElimination: input must be a multiplication by one" + e.toString());
2762 
2763  // The proof object that we will us
2764  Proof pf;
2765 
2766  // Setup the proof if needed
2767  if (withProof())
2768  pf = newPf("oneElimination", e);
2769 
2770  // Return the rewrite theorem that explains the phenomenon
2771  return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
2772 }
2773 
2774 Theorem ArithTheoremProducer3::clashingBounds(const Theorem& lowerBound, const Theorem& upperBound) {
2775 
2776  // Get the expressions
2777  const Expr& lowerBoundExpr = lowerBound.getExpr();
2778  const Expr& upperBoundExpr = upperBound.getExpr();
2779 
2780  // Check soundness
2781  if (CHECK_PROOFS) {
2782  CHECK_SOUND(isLE(lowerBoundExpr) || isLT(lowerBoundExpr), "clashingBounds: lowerBound should be >= or > " + lowerBoundExpr.toString());
2783  CHECK_SOUND(isGE(upperBoundExpr) || isGT(upperBoundExpr), "clashingBounds: upperBound should be <= or < " + upperBoundExpr.toString());
2784  CHECK_SOUND(lowerBoundExpr[0].isRational(), "clashingBounds: lowerBound left side should be a rational " + lowerBoundExpr.toString());
2785  CHECK_SOUND(upperBoundExpr[0].isRational(), "clashingBounds: upperBound left side should be a rational " + upperBoundExpr.toString());
2786  CHECK_SOUND(lowerBoundExpr[1] == upperBoundExpr[1], "clashingBounds: bounds not on the same term " + lowerBoundExpr.toString() + ", " + upperBoundExpr.toString());
2787 
2788  // Get the bounds
2789  Rational lowerBoundR = lowerBoundExpr[0].getRational();
2790  Rational upperBoundR = upperBoundExpr[0].getRational();
2791 
2792  if (isLE(lowerBoundExpr) && isGE(upperBoundExpr)) {
2793  CHECK_SOUND(upperBoundR < lowerBoundR, "clashingBounds: bounds are satisfiable");
2794  } else {
2795  CHECK_SOUND(upperBoundR <= lowerBoundR, "clashingBounds: bounds are satisfiable");
2796  }
2797  }
2798 
2799  // The proof object that we will use
2800  Proof pf;
2801  // Setup the proof if needed
2802  if (withProof())
2803  pf = newPf("clashingBounds", lowerBoundExpr, upperBoundExpr);
2804 
2805  // Put the bounds expressions in the assumptions
2806  Assumptions assumptions;
2807  assumptions.add(lowerBound);
2808  assumptions.add(upperBound);
2809 
2810  // Return the theorem
2811  return newTheorem(d_em->falseExpr(), assumptions, pf);
2812 }
2813 
2814 Theorem ArithTheoremProducer3::addInequalities(const Theorem& thm1, const Theorem& thm2) {
2815 
2816  // Get the expressions of the theorem
2817  const Expr& expr1 = thm1.getExpr();
2818  const Expr& expr2 = thm2.getExpr();
2819 
2820  // Check soundness
2821  if (CHECK_PROOFS) {
2822 
2823  CHECK_SOUND(isIneq(expr1), "addInequalities: expecting an inequality for thm1, got " + expr1.toString());
2824  CHECK_SOUND(isIneq(expr2), "addInequalities: expecting an inequality for thm2, got " + expr2.toString());
2825 
2826  if (isLE(expr1) || isLT(expr1))
2827  CHECK_SOUND(isLE(expr2) || isLT(expr2), "addInequalities: expr2 should be <(=) also " + expr2.toString());
2828  if (isGE(expr1) || isGT(expr1))
2829  CHECK_SOUND(isGE(expr2) || isGT(expr2), "addInequalities: expr2 should be >(=) also" + expr2.toString());
2830  }
2831 
2832  // Create the assumptions
2833  Assumptions a(thm1, thm2);
2834 
2835  // Get the kinds of the inequalitites
2836  int kind1 = expr1.getKind();
2837  int kind2 = expr2.getKind();
2838 
2839  // Set-up the resulting inequality
2840  int kind = (kind1 == kind2) ? kind1 : ((kind1 == LT) || (kind2 == LT))? LT : GT;
2841 
2842  // Create the proof object
2843  Proof pf;
2844  if(withProof()) {
2845  vector<Proof> pfs;
2846  pfs.push_back(thm1.getProof());
2847  pfs.push_back(thm2.getProof());
2848  pf = newPf("addInequalities", expr1, expr2, pfs);
2849  }
2850 
2851  // Create the new expressions
2852  Expr leftSide = plusExpr(expr1[0], expr2[0]);
2853  Expr rightSide = plusExpr(expr1[1], expr2[1]);
2854 
2855  // Return the theorem
2856  return newTheorem(Expr(kind, leftSide, rightSide), a, pf);
2857 }
2858 
2859 Theorem ArithTheoremProducer3::implyWeakerInequality(const Expr& expr1, const Expr& expr2) {
2860 
2861  // Check soundness
2862  if (CHECK_PROOFS) {
2863 
2864  // Both must be inequalitites
2865  CHECK_SOUND(isIneq(expr1), "implyWeakerInequality: expr1 should be an inequality" + expr1.toString());
2866  CHECK_SOUND(isIneq(expr2), "implyWeakerInequality: expr1 should be an inequality" + expr2.toString());
2867 
2868  // Should be of the same type
2869  if (isLE(expr1) || isLT(expr1))
2870  CHECK_SOUND(isLE(expr2) || isLT(expr2), "implyWeakerInequality: expr2 should be <(=) also " + expr2.toString());
2871  if (isGE(expr1) || isGT(expr1))
2872  CHECK_SOUND(isGE(expr2) || isGT(expr2), "implyWeakerInequality: expr2 should be >(=) also" + expr2.toString());
2873 
2874  // Left sides must be rational numbers
2875  CHECK_SOUND(expr1[0].isRational(), "implyWeakerInequality: expr1 should have a rational on the left side" + expr1.toString());
2876  CHECK_SOUND(expr2[0].isRational(), "implyWeakerInequality: expr2 should have a rational on the left side" + expr2.toString());
2877 
2878  // Right sides must be identical
2879  CHECK_SOUND(expr1[1] == expr2[1], "implyWeakerInequality: the expression must be the same" + expr1.toString() + " and " + expr2.toString());
2880 
2881  Rational expr1rat = expr1[0].getRational();
2882  Rational expr2rat = expr2[0].getRational();
2883 
2884 
2885  // Check the bounds
2886  if (isLE(expr1) || isLT(expr2)) {
2887  CHECK_SOUND(expr2rat < expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
2888  } else {
2889  CHECK_SOUND(expr2rat <= expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
2890  }
2891  if (isGE(expr1) || isGT(expr2)) {
2892  CHECK_SOUND(expr2rat > expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
2893  } else {
2894  CHECK_SOUND(expr2rat >= expr1rat, "implyWeakerInequality: the implication doesn't apply" + expr1.toString() + " and " + expr2.toString());
2895  }
2896  }
2897 
2898  // Create the proof object
2899  Proof pf;
2900  if(withProof()) pf = newPf("implyWeakerInequality", expr1, expr2);
2901 
2902  // Return the theorem
2903  return newTheorem(expr1.impExpr(expr2), Assumptions::emptyAssump(), pf);
2904 }
2905 
2906 Theorem ArithTheoremProducer3::implyNegatedInequality(const Expr& expr1, const Expr& expr2) {
2907 
2908  // Check soundness
2909  if (CHECK_PROOFS) {
2910  CHECK_SOUND(isIneq(expr1), "implyNegatedInequality: lowerBound should be an inequality " + expr1.toString());
2911  CHECK_SOUND(isIneq(expr2), "implyNegatedInequality: upperBound should be be an inequality " + expr2.toString());
2912  CHECK_SOUND(expr1[0].isRational(), "implyNegatedInequality: lowerBound left side should be a rational " + expr1.toString());
2913  CHECK_SOUND(expr2[0].isRational(), "implyNegatedInequality: upperBound left side should be a rational " + expr2.toString());
2914  CHECK_SOUND(expr1[1] == expr2[1], "implyNegatedInequality: bounds not on the same term " + expr1.toString() + ", " + expr2.toString());
2915 
2916  // Get the bounds
2917  Rational lowerBoundR = expr1[0].getRational();
2918  Rational upperBoundR = expr2[0].getRational();
2919 
2920  if (isLE(expr1) && isGE(expr2))
2921  CHECK_SOUND(upperBoundR < lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
2922  if (isLT(expr1) || isGT(expr2))
2923  CHECK_SOUND(upperBoundR <= lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
2924  if (isGE(expr1) && isLE(expr2))
2925  CHECK_SOUND(upperBoundR > lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
2926  if (isGT(expr1) || isLT(expr2))
2927  CHECK_SOUND(upperBoundR >= lowerBoundR, "implyNegatedInequality: cant imply negation" + expr1.toString() + ", " + expr2.toString());
2928  }
2929 
2930  // The proof object that we will use
2931  Proof pf;
2932  if (withProof()) pf = newPf("implyNegatedInequality", expr1, expr2);
2933 
2934  // Return the theorem
2935  return newTheorem(expr1.impExpr(expr2.negate()), Assumptions::emptyAssump(), pf);
2936 }
2937 
2938 Theorem ArithTheoremProducer3::trustedRewrite(const Expr& expr1, const Expr& expr2) {
2939 
2940  // The proof object that we will us
2941  Proof pf;
2942 
2943  // Setup the proof if needed
2944  if (withProof()) pf = newPf("trustedRewrite", expr1, expr2);
2945 
2946  // Return the rewrite theorem that explains the phenomenon
2947  return newRWTheorem(expr1, expr2, Assumptions::emptyAssump(), pf);
2948 
2949 }
2950 
2951 Theorem ArithTheoremProducer3::integerSplit(const Expr& intVar, const Rational& intPoint) {
2952 
2953  // Check soundness
2954  if (CHECK_PROOFS) {
2955  CHECK_SOUND(intPoint.isInteger(), "integerSplit: we can only split on integer points, given" + intPoint.toString());
2956  }
2957 
2958  // Create the expression
2959  const Expr& split = Expr(IS_INTEGER, intVar).impExpr(leExpr(intVar, rat(intPoint)).orExpr(geExpr(intVar, rat(intPoint + 1))));
2960 
2961  // The proof object that we will use
2962  Proof pf;
2963  if (withProof()) pf = newPf("integerSplit", intVar, rat(intPoint));
2964 
2965  // Return the theorem
2966  return newTheorem(split, Assumptions::emptyAssump(), pf);
2967 }
2968 
2969 
2970 Theorem ArithTheoremProducer3::rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr) {
2971 
2972 
2973  // Check soundness
2974  if (CHECK_PROOFS) {
2975  // Right side of the constraint should correspond to the proved integer expression
2976  CHECK_SOUND(isIneq(constr), "rafineStrictInteger: expected a constraint got : " + constr.toString());
2977  CHECK_SOUND(isIntConstrThm.getExpr()[0] == constr[1], "rafineStrictInteger: proof of intger doesn't correspond to the constarint right side");
2978  CHECK_SOUND(constr[0].isRational(), "rafineStrictInteger: right side of the constraint muts be a rational");
2979  }
2980 
2981  // Get the contraint bound
2982  Rational bound = constr[0].getRational();
2983 
2984  // Get the kind of the constraint
2985  int kind = constr.getKind();
2986 
2987  // If the bound is strict, make it non-strict
2988  switch (kind) {
2989  case LT:
2990  kind = LE;
2991  if (bound.isInteger()) bound ++; // 3 < x --> 4 <= x
2992  else bound = ceil(bound); // 3.4 < x --> 4 <= x
2993  break;
2994  case LE:
2995  kind = LE;
2996  if (!bound.isInteger()) bound = ceil(bound); // 3.5 <= x --> 4 <= x
2997  break;
2998  case GT:
2999  kind = GE;
3000  if (bound.isInteger()) bound --; // 3 > x --> 2 >= x
3001  else bound = floor(bound); // 3.4 > x --> 3 >= x
3002  break;
3003  case GE:
3004  kind = GE;
3005  if (!bound.isInteger()) bound = floor(bound); // 3.4 >= x --> 3 >= x
3006  break;
3007  }
3008 
3009  // The new constraint
3010  Expr newConstr(kind, rat(bound), constr[1]);
3011 
3012  // Pick up the assumptions from the integer proof
3013  const Assumptions& assump(isIntConstrThm.getAssumptionsRef());
3014 
3015  // Construct the proof object if necessary
3016  Proof pf;
3017  if (withProof()) pf = newPf("rafineStrictInteger", constr, isIntConstrThm.getProof());
3018 
3019  // Return the rewrite theorem that explains the phenomenon
3020  return newRWTheorem(constr, newConstr, assump, pf);
3021 }
3022 
3023 
3024 Theorem ArithTheoremProducer3::splitGrayShadowSmall(const Theorem& gThm) {
3025  DebugAssert(false, "Not implemented!!!");
3026  return Theorem();
3027 }
3028 
3029 Theorem ArithTheoremProducer3::implyWeakerInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) {
3030  DebugAssert(false, "Not implemented!!!");
3031  return Theorem();
3032 }
3033 
3034 Theorem ArithTheoremProducer3::implyNegatedInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) {
3035  DebugAssert(false, "Not implemented!!!");
3036  return Theorem();
3037 }
3038 
3039 Theorem ArithTheoremProducer3::expandGrayShadowRewrite(const Expr& theShadow) {
3040  DebugAssert(false, "Not implemented!!!");
3041  return Theorem();
3042 }
3043 
3044 Theorem ArithTheoremProducer3::compactNonLinearTerm(const Expr& nonLinear) {
3045  DebugAssert(false, "Not implemented!!!");
3046  return Theorem();
3047 }
3048 
3049 Theorem ArithTheoremProducer3::nonLinearIneqSignSplit(const Theorem& ineqThm) {
3050  DebugAssert(false, "Not implemented!!!");
3051  return Theorem();
3052 }
3053 
3054 Theorem ArithTheoremProducer3::implyDiffLogicBothBounds(const Expr& x,
3055  std::vector<Theorem>& c1_le_x, Rational c1,
3056  std::vector<Theorem>& x_le_c2, Rational c2) {
3057  DebugAssert(false, "Not implemented!!!");
3058  return Theorem();
3059 }
3060 
3061 Theorem ArithTheoremProducer3::addInequalities(const vector<Theorem>& thms) {
3062  DebugAssert(false, "Not implemented!!!");
3063  return Theorem();
3064 }
3065 
3066 Theorem ArithTheoremProducer3::powerOfOne(const Expr& e) {
3067  DebugAssert(false, "Not implemented!!!");
3068  return Theorem();
3069 }
3070 
3071 //
3072 // This one is here just to compile... the code is in old arithmetic
3073 Theorem ArithTheoremProducer3::simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS)
3074 {
3075  DebugAssert(false, "Not implemented!!!");
3076  return Theorem();
3077 }
3078 
3079 // Given:
3080 // 0 = c + t
3081 // where t is integer and c is not
3082 // deduce bot
3083 Theorem ArithTheoremProducer3::intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr) {
3084  DebugAssert(false, "Not implemented!!!");
3085  return Theorem();
3086 }
3087 
3088 Theorem ArithTheoremProducer3::cycleConflict(const vector<Theorem>& inequalitites) {
3089  DebugAssert(false, "Not implemented!!!");
3090  return Theorem();
3091 }
3092 
3093 Theorem ArithTheoremProducer3::implyEqualities(const vector<Theorem>& inequalitites) {
3094  DebugAssert(false, "Not implemented!!!");
3095  return Theorem();
3096 }
3097 
3098 
3099 /*! Takes a Theorem(\\alpha < \\beta) and returns
3100  * Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1)
3101  * where \\alpha and \\beta are integer expressions
3102  */
3103 Theorem ArithTheoremProducer3::lessThanToLERewrite(const Expr& ineq,
3104  const Theorem& isIntLHS,
3105  const Theorem& isIntRHS,
3106  bool changeRight) {
3107 
3108  const Expr& isIntLHSexpr = isIntLHS.getExpr();
3109  const Expr& isIntRHSexpr = isIntRHS.getExpr();
3110 
3111  if(CHECK_PROOFS) {
3112  CHECK_SOUND(isLT(ineq), "ArithTheoremProducerOld::LTtoLE: ineq must be <");
3113  // Integrality check
3114  CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0],
3115  "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
3116  " ineq = "+ineq.toString()+"\n isIntLHS = "
3117  +isIntLHSexpr.toString());
3118  CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1],
3119  "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
3120  " ineq = "+ineq.toString()+"\n isIntRHS = "
3121  +isIntRHSexpr.toString());
3122  }
3123 
3124  vector<Theorem> thms;
3125  thms.push_back(isIntLHS);
3126  thms.push_back(isIntRHS);
3127  Assumptions a(thms);
3128  Proof pf;
3129  Expr le = changeRight? leExpr(ineq[0], ineq[1] + rat(-1)) : leExpr(ineq[0] + rat(1), ineq[1]);
3130  if(withProof()) {
3131  vector<Proof> pfs;
3132  pfs.push_back(isIntLHS.getProof());
3133  pfs.push_back(isIntRHS.getProof());
3134  pf = newPf(changeRight? "lessThan_To_LE_rhs" : "lessThan_To_LE_lhs", le, pfs);
3135  }
3136 
3137  return newRWTheorem(ineq, le, a, pf);
3138 }