CVC3  2.4.1
arith_theorem_producer_old.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_arith_old.h"
35 #include <algorithm>
36 
37 using namespace std;
38 using namespace CVC3;
39 
40 ////////////////////////////////////////////////////////////////////
41 // TheoryArith: trusted method for creating ArithTheoremProducerOld
42 ////////////////////////////////////////////////////////////////////
43 
44 ArithProofRules* TheoryArithOld::createProofRulesOld() {
45  return new ArithTheoremProducerOld(theoryCore()->getTM(), this);
46 }
47 
48 ////////////////////////////////////////////////////////////////////
49 // Canonization rules
50 ////////////////////////////////////////////////////////////////////
51 
52 
53 #define CLASS_NAME "ArithTheoremProducerOld"
54 
55 
56 // Rule for variables: e == 1 * e
57 Theorem ArithTheoremProducerOld::varToMult(const Expr& e) {
58  Proof pf;
59  if(withProof()) pf = newPf("var_to_mult", e);
60  return newRWTheorem(e, (rat(1) * e), Assumptions::emptyAssump(), pf);
61 }
62 
63 
64 // Rule for unary minus: -e == (-1) * e
65 Theorem ArithTheoremProducerOld::uMinusToMult(const Expr& e) {
66  Proof pf;
67  if(withProof()) pf = newPf("uminus_to_mult", e);
68  return newRWTheorem((-e), (rat(-1) * e), Assumptions::emptyAssump(), pf);
69 }
70 
71 
72 // ==> x - y = x + (-1) * y
73 Theorem ArithTheoremProducerOld::minusToPlus(const Expr& x, const Expr& y)
74 {
75  Proof pf;
76  if(withProof()) pf = newPf("minus_to_plus", x, y);
77  return newRWTheorem((x-y), (x + (rat(-1) * y)), Assumptions::emptyAssump(), pf);
78 }
79 
80 
81 // Rule for unary minus: -e == e/(-1)
82 // This is to reduce the number of almost identical rules for uminus and div
83 Theorem ArithTheoremProducerOld::canonUMinusToDivide(const Expr& e) {
84  Proof pf;
85  if(withProof()) pf = newPf("canon_uminus", e);
86  return newRWTheorem((-e), (e / rat(-1)), Assumptions::emptyAssump(), pf);
87 }
88 
89 // Rules for division by constant
90 
91 // (c)/(d) ==> (c/d). When d==0, c/0 = 0 (our total extension).
92 Theorem ArithTheoremProducerOld::canonDivideConst(const Expr& c,
93  const Expr& d) {
94  // Make sure c and d are a const
95  if(CHECK_PROOFS) {
97  CLASS_NAME "::canonDivideConst:\n c not a constant: "
98  + c.toString());
100  CLASS_NAME "::canonDivideConst:\n d not a constant: "
101  + d.toString());
102  }
103  Proof pf;
104  if(withProof())
105  pf = newPf("canon_divide_const", c, d, d_hole);
106  const Rational& dr = d.getRational();
107  return newRWTheorem((c/d), (rat(dr==0? 0 : (c.getRational()/dr))), Assumptions::emptyAssump(), pf);
108 }
109 
110 // (c * x)/d ==> (c/d) * x, takes (c*x) and d
111 Theorem ArithTheoremProducerOld::canonDivideMult(const Expr& cx,
112  const Expr& d) {
113  // Check the format of c*x
114  if(CHECK_PROOFS) {
115  CHECK_SOUND(isMult(cx) && isRational(cx[0]),
116  CLASS_NAME "::canonDivideMult:\n "
117  "Not a (c * x) expression: "
118  + cx.toString());
120  CLASS_NAME "::canonDivideMult:\n "
121  "d is not a constant: " + d.toString());
122  }
123  const Rational& dr = d.getRational();
124  Rational cdr(dr==0? 0 : (cx[0].getRational()/dr));
125  Expr cd(rat(cdr));
126  Proof pf;
127  if(withProof())
128  pf = newPf("canon_divide_mult", cx[0], cx[1], d);
129  // (c/d) may be == 1, so we also need to canonize 1*x to x
130  if(cdr == 1)
131  return newRWTheorem((cx/d), (cx[1]), Assumptions::emptyAssump(), pf);
132  else if(cdr == 0) // c/0 == 0 case
133  return newRWTheorem((cx/d), cd, Assumptions::emptyAssump(), pf);
134  else
135  return newRWTheorem((cx/d), (cd*cx[1]), Assumptions::emptyAssump(), pf);
136 }
137 
138 // (+ t1 ... tn)/d ==> (+ (t1/d) ... (tn/d))
139 Theorem ArithTheoremProducerOld::canonDividePlus(const Expr& sum, const Expr& d) {
140  if(CHECK_PROOFS) {
141  CHECK_SOUND(isPlus(sum) && sum.arity() >= 2 && isRational(sum[0]),
142  CLASS_NAME "::canonUMinusPlus:\n "
143  "Expr is not a canonical sum: "
144  + sum.toString());
146  CLASS_NAME "::canonUMinusPlus:\n "
147  "d is not a const: " + d.toString());
148  }
149  // First, propagate '/d' down to the args
150  Proof pf;
151  if(withProof())
152  pf = newPf("canon_divide_plus", rat(sum.arity()),
153  sum.begin(), sum.end());
154  vector<Expr> newKids;
155  for(Expr::iterator i=sum.begin(), iend=sum.end(); i!=iend; ++i)
156  newKids.push_back((*i)/d);
157  // (+ t1 ... tn)/d == (+ (t1/d) ... (tn/d))
158  return newRWTheorem((sum/d), (plusExpr(newKids)), Assumptions::emptyAssump(), pf);
159 }
160 
161 // x/(d) ==> (1/d) * x, unless d == 1
162 Theorem ArithTheoremProducerOld::canonDivideVar(const Expr& e, const Expr& d) {
163  if(CHECK_PROOFS) {
165  CLASS_NAME "::canonDivideVar:\n "
166  "d is not a const: " + d.toString());
167  }
168  Proof pf;
169 
170  if(withProof())
171  pf = newPf("canon_divide_var", e);
172 
173  const Rational& dr = d.getRational();
174  if(dr == 1)
175  return newRWTheorem(e/d, e, Assumptions::emptyAssump(), pf);
176  if(dr == 0) // e/0 == 0 (total extension of division)
177  return newRWTheorem(e/d, d, Assumptions::emptyAssump(), pf);
178  else
179  return newRWTheorem(e/d, rat(1/dr) * e, Assumptions::emptyAssump(), pf);
180 }
181 
182 
183 // Multiplication
184 // (MULT expr1 expr2 expr3 ...)
185 // Each expr is in canonical form, i.e. it can be a
186 // 1) Rational constant
187 // 2) Arithmetic Leaf (var or term from another theory)
188 // 3) (POW rational leaf)
189 // where rational cannot be 0 or 1
190 // 4) (MULT rational mterm'_1 ...) where each mterm' is of type (2) or (3)
191 // If rational == 1 then there should be at least two mterms
192 // 5) (PLUS rational sterm_1 ...) where each sterm is of
193 // type (2) or (3) or (4)
194 // if rational == 0 then there should be at least two sterms
195 
196 
197 Expr ArithTheoremProducerOld::simplifiedMultExpr(std::vector<Expr> & mulKids)
198 {
199  DebugAssert(mulKids.size() >= 1 && mulKids[0].isRational(), "");
200  if (mulKids.size() == 1) {
201  return mulKids[0];
202  }
203  if ((mulKids[0] == rat(1)) && mulKids.size() == 2) {
204  return mulKids[1];
205  }
206  else
207  return multExpr(mulKids);
208 }
209 
210 Expr ArithTheoremProducerOld::canonMultConstMult(const Expr & c,
211  const Expr & e)
212 {
213  // c is a rational
214  // e is (MULT rat mterm'_1 ....)
215  // assume that e2 is already in canonic form
216  DebugAssert(c.isRational() && e.getKind() == MULT, "");
217  std::vector<Expr> mulKids;
218  DebugAssert ((e.arity() > 1) && (e[0].isRational()),
219  "ArithTheoremProducerOld::canonMultConstMult: "
220  "a canonized MULT expression must have arity "
221  "greater than 1: and first child must be "
222  "rational " + e.toString());
223  Expr::iterator i = e.begin();
224  mulKids.push_back(rat(c.getRational() * (*i).getRational()));
225  ++i;
226  for(; i != e.end(); ++i) {
227  mulKids.push_back(*i);
228  }
229  return simplifiedMultExpr(mulKids);
230 }
231 
232 Expr ArithTheoremProducerOld::canonMultConstPlus(const Expr & e1,
233  const Expr & e2)
234 {
235  DebugAssert(e1.isRational() && e2.getKind() == PLUS &&
236  e2.arity() > 0, "");
237  // e1 is a rational
238  // e2 is of the form (PLUS rational sterm1 sterm2 ...)
239  // assume that e2 is already in canonic form
240  std::vector<Theorem> thmPlusVector;
241  Expr::iterator i = e2.begin();
242  for(; i!= e2.end(); ++i) {
243  thmPlusVector.push_back(canonMultMtermMterm(e1*(*i)));
244  }
245 
246  Theorem thmPlus1 =
247  d_theoryArith->substitutivityRule(e2.getOp(), thmPlusVector);
248  return thmPlus1.getRHS();
249 }
250 
251 Expr ArithTheoremProducerOld::canonMultPowPow(const Expr & e1,
252  const Expr & e2)
253 {
254  DebugAssert(e1.getKind() == POW && e2.getKind() == POW, "");
255  // (POW r1 leaf1) * (POW r2 leaf2)
256  Expr leaf1 = e1[1];
257  Expr leaf2 = e2[1];
258  Expr can_expr;
259  if (leaf1 == leaf2) {
260  Rational rsum = e1[0].getRational() + e2[0].getRational();
261  if (rsum == 0) {
262  return rat(1);
263  }
264  else if (rsum == 1) {
265  return leaf1;
266  }
267  else
268  {
269  return powExpr(rat(rsum), leaf1);
270  }
271  }
272  else
273  {
274  std::vector<Expr> mulKids;
275  mulKids.push_back(rat(1));
276  // the leafs should be put in decreasing order
277  if (leaf1 < leaf2) {
278  mulKids.push_back(e2);
279  mulKids.push_back(e1);
280  }
281  else
282  {
283  mulKids.push_back(e1);
284  mulKids.push_back(e2);
285  }
286  // FIXME: don't really need to simplify, just wrap up a MULT?
287  return simplifiedMultExpr(mulKids);
288  }
289 }
290 
291 Expr ArithTheoremProducerOld::canonMultPowLeaf(const Expr & e1,
292  const Expr & e2)
293 {
294  DebugAssert(e1.getKind() == POW, "");
295  // (POW r1 leaf1) * leaf2
296  Expr leaf1 = e1[1];
297  Expr leaf2 = e2;
298  Expr can_expr;
299  if (leaf1 == leaf2) {
300  Rational rsum = e1[0].getRational() + 1;
301  if (rsum == 0) {
302  return rat(1);
303  }
304  else if (rsum == 1) {
305  return leaf1;
306  }
307  else
308  {
309  return powExpr(rat(rsum), leaf1);
310  }
311  }
312  else
313  {
314  std::vector<Expr> mulKids;
315  mulKids.push_back(rat(1));
316  // the leafs should be put in decreasing order
317  if (leaf1 < leaf2) {
318  mulKids.push_back(e2);
319  mulKids.push_back(e1);
320  }
321  else
322  {
323  mulKids.push_back(e1);
324  mulKids.push_back(e2);
325  }
326  return simplifiedMultExpr(mulKids);
327  }
328 }
329 
330 Expr ArithTheoremProducerOld::canonMultLeafLeaf(const Expr & e1,
331  const Expr & e2)
332 {
333  // leaf1 * leaf2
334  Expr leaf1 = e1;
335  Expr leaf2 = e2;
336  Expr can_expr;
337  if (leaf1 == leaf2) {
338  return powExpr(rat(2), leaf1);
339  }
340  else
341  {
342  std::vector<Expr> mulKids;
343  mulKids.push_back(rat(1));
344  // the leafs should be put in decreasing order
345  if (leaf1 < leaf2) {
346  mulKids.push_back(e2);
347  mulKids.push_back(e1);
348  }
349  else
350  {
351  mulKids.push_back(e1);
352  mulKids.push_back(e2);
353  }
354  return simplifiedMultExpr(mulKids);
355  }
356 }
357 
358 Expr ArithTheoremProducerOld::canonMultLeafOrPowMult(const Expr & e1,
359  const Expr & e2)
360 {
361  DebugAssert(e2.getKind() == MULT, "");
362  // Leaf * (MULT rat1 mterm1 ...)
363  // (POW r1 leaf1) * (MULT rat1 mterm1 ...) where
364  // each mterm is a leaf or (POW r leaf). Furthermore the leafs
365  // in the mterms are in descending order
366  Expr leaf1 = e1.getKind() == POW ? e1[1] : e1;
367  std::vector<Expr> mulKids;
368  DebugAssert(e2.arity() > 1, "MULT expr must have arity 2 or more");
369  Expr::iterator i = e2.begin();
370  // push the rational
371  mulKids.push_back(*i);
372  ++i;
373  // Now i points to the first mterm
374  for(; i != e2.end(); ++i) {
375  Expr leaf2 = ((*i).getKind() == POW) ? (*i)[1] : (*i);
376  if (leaf1 == leaf2) {
377  Rational r1 = e1.getKind() == POW ? e1[0].getRational() : 1;
378  Rational r2 =
379  ((*i).getKind() == POW ? (*i)[0].getRational() : 1);
380  // if r1 + r2 == 0 then it is the case of x^n * x^{-n}
381  // So, nothing needs to be added
382  if (r1 + r2 != 0) {
383  if (r1 + r2 == 1) {
384  mulKids.push_back(leaf1);
385  }
386  else
387  {
388  mulKids.push_back(powExpr(rat(r1 + r2), leaf1));
389  }
390  }
391  break;
392  }
393  // This ensures that the leaves in the mterms are also arranged
394  // in decreasing order
395  // Note that this will need to be changed if we want the order to
396  // be increasing order.
397  else if (leaf2 < leaf1) {
398  mulKids.push_back(e1);
399  mulKids.push_back(*i);
400  break;
401  }
402  else // leaf1 < leaf2
403  mulKids.push_back(*i);
404  }
405  if (i == e2.end()) {
406  mulKids.push_back(e1);
407  }
408  else
409  {
410  // e1 and *i have already been added
411  for (++i; i != e2.end(); ++i) {
412  mulKids.push_back(*i);
413  }
414  }
415  return simplifiedMultExpr(mulKids);
416 }
417 
418 // Local class for ordering monomials; note, that it flips the
419 // ordering given by greaterthan(), to sort in ascending order.
420 class MonomialLess {
421 public:
422  bool operator()(const Expr& e1, const Expr& e2) const {
423  return ArithTheoremProducerOld::greaterthan(e1,e2);
424  }
425 };
426 
427 typedef map<Expr,Rational,MonomialLess> MonomMap;
428 
429 Expr
430 ArithTheoremProducerOld::canonCombineLikeTerms(const std::vector<Expr> & sumExprs)
431 {
432  Rational constant = 0;
433  MonomMap sumHashMap;
434  vector<Expr> sumKids;
435 
436  // Add each distinct mterm (not including the rational) into
437  // an appropriate hash map entry
438  std::vector<Expr>::const_iterator i = sumExprs.begin();
439  for (; i != sumExprs.end(); ++i) {
440  Expr mul = *i;
441  if (mul.isRational()) {
442  constant = constant + mul.getRational();
443  }
444  else {
445  switch (mul.getKind()) {
446  case MULT: {
447  std::vector<Expr> mulKids;
448  DebugAssert(mul.arity() > 1 && mul[0].isRational(),"");
449  mulKids.push_back(rat(1));
450  Expr::iterator j = mul.begin();
451  ++j;
452  for (; j!= mul.end(); ++j) {
453  mulKids.push_back(*j);
454  }
455 
456  // make sure that tempExpr is also in canonic form
457  Expr tempExpr = mulKids.size() > 2 ? multExpr(mulKids): mulKids[1];
458  MonomMap::iterator i=sumHashMap.find(tempExpr);
459  if (i == sumHashMap.end()) {
460  sumHashMap[tempExpr] = mul[0].getRational();
461  }
462  else {
463  (*i).second += mul[0].getRational();
464  }
465  }
466  break;
467  default: {
468  MonomMap::iterator i=sumHashMap.find(mul);
469  // covers the case of POW, leaf
470  if (i == sumHashMap.end()) {
471  sumHashMap[mul] = 1;
472  }
473  else {
474  (*i).second += 1;
475  }
476  break;
477  }
478  }
479  }
480  }
481  // Now transfer to sumKids
482  sumKids.push_back(rat(constant));
483  MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end();
484  for(; j != jend; ++j) {
485  if ((*j).second != 0)
486  sumKids.push_back
487  (canonMultMtermMterm(rat((*j).second) * (*j).first).getRHS());
488  }
489 
490  /*
491  for (unsigned k = 0; k < sumKids.size(); ++k)
492  {
493  cout << "sumKids[" << k << "] = " << sumKids[k].toString() << endl;
494  }
495  */
496 
497  // The ordering in map guarantees the correct order; no need to sort
498 
499  // std::sort(sumKids.begin(), sumKids.end(), greaterthan);
500 
501  if ((constant == 0) && (sumKids.size() == 2)) {
502  return sumKids[1];
503  }
504  else if (sumKids.size() == 1) {
505  return sumKids[0];
506  }
507  else
508  return plusExpr(sumKids);
509 }
510 
511 Expr ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(const Expr & e1,
512  const Expr & e2)
513 {
514  DebugAssert(e2.getKind() == PLUS, "");
515  // Leaf * (PLUS rational sterm1 ...)
516  // or
517  // (POW n1 x1) * (PLUS rational sterm1 ...)
518  // or
519  // (MULT r1 m1 m2 ...) * (PLUS rational sterm1 ...)
520  // assume that e1 and e2 are themselves canonized
521  std::vector<Expr> sumExprs;
522  // Multiply each term in turn.
523  Expr::iterator i = e2.begin();
524  for (; i != e2.end(); ++i) {
525  sumExprs.push_back(canonMultMtermMterm(e1 * (*i)).getRHS());
526  }
527  return canonCombineLikeTerms(sumExprs);
528 }
529 
530 Expr ArithTheoremProducerOld::canonMultPlusPlus(const Expr & e1,
531  const Expr & e2)
532 {
533  DebugAssert(e1.getKind() == PLUS && e2.getKind() == PLUS, "");
534  // (PLUS r1 .... ) * (PLUS r1' ...)
535  // assume that e1 and e2 are themselves canonized
536 
537  std::vector<Expr> sumExprs;
538  // Multiply each term in turn.
539  Expr::iterator i = e1.begin();
540  for (; i != e1.end(); ++i) {
541  Expr::iterator j = e2.begin();
542  for (; j != e2.end(); ++j) {
543  sumExprs.push_back(canonMultMtermMterm((*i) * (*j)).getRHS());
544  }
545  }
546  return canonCombineLikeTerms(sumExprs);
547 }
548 
549 
550 
551 // The following produces a Theorem which is the result of multiplication
552 // of two canonized mterms. e = e1*e2
553 Theorem
554 ArithTheoremProducerOld::canonMultMtermMterm(const Expr& e)
555 {
556  if(CHECK_PROOFS) {
557  CHECK_SOUND(isMult(e) && e.arity() == 2,
558  "canonMultMtermMterm: e = "+e.toString());
559  }
560  Proof pf;
561  Expr rhs;
562  const Expr& e1 = e[0];
563  const Expr& e2 = e[1];
564  string cmmm = "canon_mult_mterm_mterm";
565 
566  if (e1.isRational()) {
567  // e1 is a Rational
568  const Rational& c = e1.getRational();
569  if (c == 0)
570  return canonMultZero(e2);
571  else if (c == 1)
572  return canonMultOne(e2);
573  else {
574  switch (e2.getKind()) {
575  case RATIONAL_EXPR :
576  // rat * rat
577  return canonMultConstConst(e1,e2);
578  break;
579  // TODO case of leaf
580  case POW:
581  // rat * (POW rat leaf)
582  // nothing to simplify
583  return d_theoryArith->reflexivityRule (e);
584 
585  break;
586  case MULT:
587  rhs = canonMultConstMult(e1,e2);
588  if(withProof()) pf = newPf(cmmm,e,rhs);
589  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
590  break;
591  case PLUS:
592  rhs = canonMultConstPlus(e1,e2);
593  if(withProof()) pf = newPf(cmmm,e,rhs);
594  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
595  break;
596  default:
597  // TODO: I am going to assume that this is just a leaf
598  // i.e., a variable or term from another theory
599  return d_theoryArith->reflexivityRule(e);
600  break;
601  }
602  }
603  }
604  else if (e1.getKind() == POW) {
605  switch (e2.getKind()) {
606  case RATIONAL_EXPR:
607  // switch the order of the two arguments
608  return canonMultMtermMterm(e2 * e1);
609  break;
610  case POW:
611  rhs = canonMultPowPow(e1,e2);
612  if(withProof()) pf = newPf(cmmm,e,rhs);
613  return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
614  break;
615  case MULT:
616  rhs = canonMultLeafOrPowMult(e1,e2);
617  if(withProof()) pf = newPf(cmmm,e,rhs);
618  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
619  break;
620  case PLUS:
621  rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
622  if(withProof()) pf = newPf(cmmm,e,rhs);
623  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
624  break;
625  default:
626  rhs = canonMultPowLeaf(e1,e2);
627  if(withProof()) pf = newPf(cmmm,e,rhs);
628  return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
629  break;
630  }
631  }
632  else if (e1.getKind() == MULT) {
633  switch (e2.getKind()) {
634  case RATIONAL_EXPR:
635  case POW:
636  // switch the order of the two arguments
637  return canonMultMtermMterm(e2 * e1);
638  break;
639  case MULT:
640  {
641  // (Mult r m1 m2 ...) (Mult r' m1' m2' ...)
642  Expr result = e2;
643  Expr::iterator i = e1.begin();
644  for (; i != e1.end(); ++i) {
645  result = canonMultMtermMterm((*i) * result).getRHS();
646  }
647  if(withProof()) pf = newPf(cmmm,e,result);
648  return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
649  }
650  break;
651  case PLUS:
652  rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
653  if(withProof()) pf = newPf(cmmm,e,rhs);
654  return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
655  break;
656  default:
657  // leaf
658  // switch the order of the two arguments
659  return canonMultMtermMterm(e2 * e1);
660  break;
661  }
662  }
663  else if (e1.getKind() == PLUS) {
664  switch (e2.getKind()) {
665  case RATIONAL_EXPR:
666  case POW:
667  case MULT:
668  // switch the order of the two arguments
669  return canonMultMtermMterm(e2 * e1);
670  break;
671  case PLUS:
672  rhs = canonMultPlusPlus(e1,e2);
673  if(withProof()) pf = newPf(cmmm,e,rhs);
674  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
675  break;
676  default:
677  // leaf
678  // switch the order of the two arguments
679  return canonMultMtermMterm(e2 * e1);
680  break;
681  }
682  }
683  else {
684  // leaf
685  switch (e2.getKind()) {
686  case RATIONAL_EXPR:
687  // switch the order of the two arguments
688  return canonMultMtermMterm(e2 * e1);
689  break;
690  case POW:
691  rhs = canonMultPowLeaf(e2,e1);
692  if(withProof()) pf = newPf(cmmm,e,rhs);
693  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
694  break;
695  case MULT:
696  rhs = canonMultLeafOrPowMult(e1,e2);;
697  if(withProof()) pf = newPf(cmmm,e,rhs);
698  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
699  break;
700  case PLUS:
701  rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
702  if(withProof()) pf = newPf(cmmm,e,rhs);
703  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
704  break;
705  default:
706  // leaf * leaf
707  rhs = canonMultLeafLeaf(e1,e2);
708  if(withProof()) pf = newPf(cmmm,e,rhs);
709  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
710  break;
711  }
712  }
713  FatalAssert(false, "Unreachable");
714  return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
715 }
716 
717 // (PLUS expr1 expr2 ...) where each expr is itself in canonic form
718 Theorem
719 ArithTheoremProducerOld::canonPlus(const Expr& e)
720 {
721  Proof pf;
722 
723  if (withProof()) {
724  pf = newPf("canon_plus", e);
725  }
726  DebugAssert(e.getKind() == PLUS, "");
727 
728  // First flatten the PLUS
729 
730  std::vector<Expr> sumKids;
731  Expr::iterator i = e.begin();
732  for(; i != e.end(); ++i) {
733  if ((*i).getKind() != PLUS) {
734  sumKids.push_back(*i);
735  }
736  else
737  {
738  Expr::iterator j = (*i).begin();
739  for(; j != (*i).end(); ++j)
740  sumKids.push_back(*j);
741  }
742  }
743  Expr val = canonCombineLikeTerms(sumKids);
744  if (withProof()) {
745  pf = newPf("canon_plus", e, val);
746  }
747  return newRWTheorem(e, val, Assumptions::emptyAssump(), pf);
748 }
749 
750 // (MULT expr1 expr2 ...) where each expr is itself in canonic form
751 Theorem
752 ArithTheoremProducerOld::canonMult(const Expr& e)
753 {
754  Proof pf;
755  TRACE("arith canon", "canonMult(", e.toString(), ")");
756  DebugAssert(e.getKind() == MULT && e.arity() > 1, "");
757  Expr::iterator i = e.begin();
758  Expr result = *i;
759  ++i;
760  for (; i != e.end(); ++i) {
761  result = canonMultMtermMterm(result * (*i)).getRHS();
762  }
763  if (withProof()) {
764  pf = newPf("canon_mult", e,result);
765  }
766 
767  // If multiplicative sign split is on do it
768  if (d_theoryArith->nonlinearSignSplit()) {
769 
770  // Add the sign splits
771  Expr positive = d_em->trueExpr();
772  Expr negative = d_em->falseExpr();
773  vector<Expr> zero;
774 
775  // we do the case split if it's not trivial
776  int count_non_trivial = 0;
777  int count_constants = 0;
778 
779  // a1*a2*...*an is positive if there is an even number of negative ones
780  // a1*a2*...*an is negative if there is an odd number of negative ones
781  for (i = e.begin(); i != e.end(); ++i) {
782  Expr current = (*i);
783 
784  if (isPlus(current)) count_non_trivial ++;
785  if (current.isRational()) count_constants ++;
786  if (isPow(current) && current[0].getRational() < 0) {
787  // Bail on negative powers, it's normalization
788  count_non_trivial = 0;
789  break;
790  }
791 
792  zero.push_back(current.eqExpr(rat(0)));
793  positive = Expr(XOR, positive, ltExpr(current, rat(0)));
794  negative = Expr(XOR, negative, ltExpr(current, rat(0)));
795  }
796 
797  if (count_non_trivial > 0 && !count_constants == (e.arity() - 1)) {
798  // Any of the factors is zero
799  Expr zero_lemma = orExpr(zero).iffExpr(result.eqExpr(rat(0)));
800  Expr positive_lemma = positive.impExpr(geExpr(result, rat(0)));
801  Expr negative_lemma = negative.impExpr(leExpr(result, rat(0)));
802  Expr lemma = positive_lemma.andExpr(negative_lemma.andExpr(zero_lemma));
803 
804  Proof split_pf;
805  if (withProof()) split_pf = newPf("multiplicative_sign_split", e, lemma);
806  Theorem case_split_thm = newTheorem(lemma, Assumptions::emptyAssump(), split_pf);
807 
808  TRACE("arith nonlinear", "adding sign split: ", lemma, "");
809 
810  d_theoryArith->addMultiplicativeSignSplit(case_split_thm);
811  }
812  }
813 
814  return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
815 }
816 
817 
818 Theorem
819 ArithTheoremProducerOld::canonInvertConst(const Expr& e)
820 {
821  if(CHECK_PROOFS)
822  CHECK_SOUND(isRational(e), "expecting a rational: e = "+e.toString());
823 
824  Proof pf;
825 
826  if (withProof()) {
827  pf = newPf("canon_invert_const", e);
828  }
829  const Rational& er = e.getRational();
830  return newRWTheorem((rat(1)/e), rat(er==0? 0 : (1/er)), Assumptions::emptyAssump(), pf);
831 }
832 
833 
834 Theorem
835 ArithTheoremProducerOld::canonInvertLeaf(const Expr& e)
836 {
837  Proof pf;
838 
839  if (withProof()) {
840  pf = newPf("canon_invert_leaf", e);
841  }
842  return newRWTheorem((rat(1)/e), powExpr(rat(-1), e), Assumptions::emptyAssump(), pf);
843 }
844 
845 
846 Theorem
847 ArithTheoremProducerOld::canonInvertPow(const Expr& e)
848 {
849  DebugAssert(e.getKind() == POW, "expecting a rational"+e[0].toString());
850 
851  Proof pf;
852 
853  if (withProof()) {
854  pf = newPf("canon_invert_pow", e);
855  }
856  if (e[0].getRational() == -1)
857  return newRWTheorem((rat(1)/e), e[1], Assumptions::emptyAssump(), pf);
858  else
859  return newRWTheorem((rat(1)/e),
860  powExpr(rat(-e[0].getRational()), e[1]),
861  Assumptions::emptyAssump(),
862  pf);
863 }
864 
865 Theorem
866 ArithTheoremProducerOld::canonInvertMult(const Expr& e)
867 {
868  DebugAssert(e.getKind() == MULT, "expecting a rational"+e[0].toString());
869 
870  Proof pf;
871 
872  if (withProof()) {
873  pf = newPf("canon_invert_mult", e);
874  }
875 
876  DebugAssert(e.arity() > 1, "MULT should have arity > 1"+e.toString());
877  Expr result = canonInvert(e[0]).getRHS();
878  for (int i = 1; i < e.arity(); ++i) {
879  result =
880  canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS();
881  }
882  return newRWTheorem((rat(1)/e), result, Assumptions::emptyAssump(), pf);
883 }
884 
885 
886 // Given an expression e in Canonic form generate 1/e in canonic form
887 // This function assumes that e is not a PLUS expression
888 Theorem
889 ArithTheoremProducerOld::canonInvert(const Expr& e)
890 {
891  DebugAssert(e.getKind() != PLUS,
892  "Cannot do inverse on a PLUS"+e.toString());
893  switch (e.getKind()) {
894  case RATIONAL_EXPR:
895  return canonInvertConst(e);
896  break;
897  case POW:
898  return canonInvertPow(e);
899  break;
900  case MULT:
901  return canonInvertMult(e);
902  break;
903  default:
904  // leaf
905  return canonInvertLeaf(e);
906  break;
907  }
908 }
909 
910 
911 Theorem ArithTheoremProducerOld::moveSumConstantRight(const Expr& e) {
912 
913  // Check soundness of the rule if necessary
914  if (CHECK_PROOFS) {
915  CHECK_SOUND(isIneq(e) || e.isEq(), "moveSumConstantRight: input must be Eq or Ineq: " + e.toString());
916  CHECK_SOUND(isRational(e[0]) || isPlus(e[0]), "moveSumConstantRight: left side must be a canonised sum: " + e.toString());
917  CHECK_SOUND(isRational(e[1]) && e[1].getRational() == 0, "moveSumConstantRight: right side must be 0: " + e.toString());
918  }
919 
920  // The rational constant of the sum
921  Rational r = 0;
922 
923  // The right hand side of the expression
924  Expr right = e[0];
925 
926  // The vector of sum terms
927  vector<Expr> sumTerms;
928 
929  // Get all the non rational children and
930  if (!right.isRational())
931  for(Expr::iterator it = right.begin(); it != right.end(); it ++) {
932  // If the term is rational then add the rational number to r
933  if ((*it).isRational()) r = r + (*it).getRational();
934  // Otherwise just add the sumTerm to the sumTerms
935  else sumTerms.push_back((*it));
936  }
937 
938  // Setup the new expression
939  Expr transformed;
940  if (sumTerms.size() > 1)
941  // If the number of summands is > 1 return the sum of them
942  transformed = Expr(e.getKind(), plusExpr(sumTerms), rat(-r));
943  else
944  // Otherwise return the one summand as itself
945  transformed = Expr(e.getKind(), sumTerms[0], rat(-r));
946 
947 
948  // If proof is needed set it up
949  Proof pf;
950  if (withProof()) pf = newPf("arithm_sum_constant_right", e);
951 
952  // Retrun the theorem explaining the transformation
953  return newRWTheorem(e, transformed, Assumptions::emptyAssump(), pf);
954 }
955 
956 Theorem
957 ArithTheoremProducerOld::canonDivide(const Expr& e)
958 {
959  DebugAssert(e.getKind() == DIVIDE, "Expecting Divide"+e.toString());
960  Proof pf;
961 
962  if (withProof()) {
963  pf = newPf("canon_invert_divide", e);
964  }
965 
966  Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf);
967 
968  return d_theoryArith->transitivityRule(thm, canonMult(thm.getRHS()));
969 }
970 
971 
972 // Rules for multiplication
973 // t*c ==> c*t, takes constant c and term t
974 Theorem
975 ArithTheoremProducerOld::canonMultTermConst(const Expr& c, const Expr& t) {
976  Proof pf;
977  if(CHECK_PROOFS) {
979  CLASS_NAME "::canonMultTermConst:\n "
980  "c is not a constant: " + c.toString());
981  }
982  if(withProof()) pf = newPf("canon_mult_term_const", c, t);
983  return newRWTheorem((t*c), (c*t), Assumptions::emptyAssump(), pf);
984 }
985 
986 // Rules for multiplication
987 // t1*t2 ==> Error, takes t1 and t2 where both are non-constants
988 Theorem
989 ArithTheoremProducerOld::canonMultTerm1Term2(const Expr& t1, const Expr& t2) {
990  // Proof pf;
991  // if(withProof()) pf = newPf("canon_mult_term1_term2", t1, t2);
992  if(CHECK_PROOFS) {
993  CHECK_SOUND(false, "Fatal Error: We don't support multiplication"
994  "of two non constant terms at this time "
995  + t1.toString() + " and " + t2.toString());
996  }
997  return Theorem();
998 }
999 
1000 // Rules for multiplication
1001 // 0*x = 0, takes x
1002 Theorem ArithTheoremProducerOld::canonMultZero(const Expr& e) {
1003  Proof pf;
1004  if(withProof()) pf = newPf("canon_mult_zero", e);
1005  return newRWTheorem((rat(0)*e), rat(0), Assumptions::emptyAssump(), pf);
1006 }
1007 
1008 // Rules for multiplication
1009 // 1*x ==> x, takes x
1010 Theorem ArithTheoremProducerOld::canonMultOne(const Expr& e) {
1011  Proof pf;
1012  if(withProof()) pf = newPf("canon_mult_one", e);
1013  return newRWTheorem((rat(1)*e), e, Assumptions::emptyAssump(), pf);
1014 }
1015 
1016 // Rules for multiplication
1017 // c1*c2 ==> c', takes constant c1*c2
1018 Theorem
1019 ArithTheoremProducerOld::canonMultConstConst(const Expr& c1, const Expr& c2) {
1020  Proof pf;
1021  if(CHECK_PROOFS) {
1022  CHECK_SOUND(isRational(c1),
1023  CLASS_NAME "::canonMultConstConst:\n "
1024  "c1 is not a constant: " + c1.toString());
1025  CHECK_SOUND(isRational(c2),
1026  CLASS_NAME "::canonMultConstConst:\n "
1027  "c2 is not a constant: " + c2.toString());
1028  }
1029  if(withProof()) pf = newPf("canon_mult_const_const", c1, c2);
1030  return
1031  newRWTheorem((c1*c2), rat(c1.getRational()*c2.getRational()), Assumptions::emptyAssump(), pf);
1032 }
1033 
1034 // Rules for multiplication
1035 // c1*(c2*t) ==> c'*t, takes c1 and c2 and t
1036 Theorem
1037 ArithTheoremProducerOld::canonMultConstTerm(const Expr& c1,
1038  const Expr& c2,const Expr& t) {
1039  Proof pf;
1040  if(CHECK_PROOFS) {
1041  CHECK_SOUND(isRational(c1),
1042  CLASS_NAME "::canonMultConstTerm:\n "
1043  "c1 is not a constant: " + c1.toString());
1044  CHECK_SOUND(isRational(c2),
1045  CLASS_NAME "::canonMultConstTerm:\n "
1046  "c2 is not a constant: " + c2.toString());
1047  }
1048 
1049  if(withProof()) pf = newPf("canon_mult_const_term", c1, c2, t);
1050  return
1051  newRWTheorem(c1*(c2*t), rat(c1.getRational()*c2.getRational())*t, Assumptions::emptyAssump(), pf);
1052 }
1053 
1054 // Rules for multiplication
1055 // c1*(+ c2 v1 ...) ==> (+ c1c2 c1v1 ...), takes c1 and the sum
1056 Theorem
1057 ArithTheoremProducerOld::canonMultConstSum(const Expr& c1, const Expr& sum) {
1058  Proof pf;
1059  std::vector<Expr> sumKids;
1060 
1061  if(CHECK_PROOFS) {
1062  CHECK_SOUND(isRational(c1),
1063  CLASS_NAME "::canonMultConstTerm:\n "
1064  "c1 is not a constant: " + c1.toString());
1065  CHECK_SOUND(PLUS == sum.getKind(),
1066  CLASS_NAME "::canonMultConstTerm:\n "
1067  "the kind must be a PLUS: " + sum.toString());
1068  }
1069  Expr::iterator i = sum.begin();
1070  for(; i != sum.end(); ++i)
1071  sumKids.push_back(c1*(*i));
1072  Expr ret = plusExpr(sumKids);
1073  if(withProof()) pf = newPf("canon_mult_const_sum", c1, sum, ret);
1074  return newRWTheorem((c1*sum),ret , Assumptions::emptyAssump(), pf);
1075 }
1076 
1077 
1078 // c^n = c' (compute the constant power expression)
1079 Theorem
1080 ArithTheoremProducerOld::canonPowConst(const Expr& e) {
1081  if(CHECK_PROOFS) {
1082  CHECK_SOUND(e.getKind() == POW && e.arity() == 2
1083  && e[0].isRational() && e[1].isRational(),
1084  "ArithTheoremProducerOld::canonPowConst("+e.toString()+")");
1085  }
1086  const Rational& p = e[0].getRational();
1087  const Rational& base = e[1].getRational();
1088  if(CHECK_PROOFS) {
1089  CHECK_SOUND(p.isInteger(),
1090  "ArithTheoremProducerOld::canonPowConst("+e.toString()+")");
1091  }
1092  Expr res;
1093  if (base == 0 && p < 0) {
1094  res = rat(0);
1095  }
1096  else res = rat(pow(p, base));
1097  Proof pf;
1098  if(withProof())
1099  pf = newPf("canon_pow_const", e, res);
1100  return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
1101 }
1102 
1103 
1104 // Rules for addition
1105 // flattens the input. accepts a PLUS expr
1106 Theorem
1107 ArithTheoremProducerOld::canonFlattenSum(const Expr& e) {
1108  Proof pf;
1109  std::vector<Expr> sumKids;
1110  if(CHECK_PROOFS) {
1111  CHECK_SOUND(PLUS == e.getKind(),
1112  CLASS_NAME "::canonFlattenSum:\n"
1113  "input must be a PLUS:" + e.toString());
1114  }
1115 
1116  Expr::iterator i = e.begin();
1117  for(; i != e.end(); ++i){
1118  if (PLUS != (*i).getKind())
1119  sumKids.push_back(*i);
1120  else {
1121  Expr::iterator j = (*i).begin();
1122  for(; j != (*i).end(); ++j)
1123  sumKids.push_back(*j);
1124  }
1125  }
1126  Expr ret = plusExpr(sumKids);
1127  if(withProof()) pf = newPf("canon_flatten_sum", e,ret);
1128  return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
1129 }
1130 
1131 // Rules for addition
1132 // combine like terms. accepts a flattened PLUS expr
1133 Theorem
1134 ArithTheoremProducerOld::canonComboLikeTerms(const Expr& e) {
1135  Proof pf;
1136  std::vector<Expr> sumKids;
1137  ExprMap<Rational> sumHashMap;
1138  Rational constant = 0;
1139 
1140  if(CHECK_PROOFS) {
1141  Expr::iterator k = e.begin();
1142  for(; k != e.end(); ++k)
1143  CHECK_SOUND(!isPlus(*k),
1144  CLASS_NAME "::canonComboLikeTerms:\n"
1145  "input must be a flattened PLUS:" + k->toString());
1146  }
1147  Expr::iterator i = e.begin();
1148  for(; i != e.end(); ++i){
1149  if(i->isRational())
1150  constant = constant + i->getRational();
1151  else {
1152  if (!isMult(*i)) {
1153  if(0 == sumHashMap.count((*i)))
1154  sumHashMap[*i] = 1;
1155  else
1156  sumHashMap[*i] += 1;
1157  }
1158  else {
1159  if(0 == sumHashMap.count((*i)[1]))
1160  sumHashMap[(*i)[1]] = (*i)[0].getRational();
1161  else
1162  sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational();
1163  }
1164  }
1165  }
1166 
1167  sumKids.push_back(rat(constant));
1168  ExprMap<Rational>::iterator j = sumHashMap.begin();
1169  for(; j != sumHashMap.end(); ++j) {
1170  if(0 == (*j).second)
1171  ;//do nothing
1172  else if (1 == (*j).second)
1173  sumKids.push_back((*j).first);
1174  else
1175  sumKids.push_back(rat((*j).second) * (*j).first);
1176  }
1177 
1178  //constant is same as sumKids[0].
1179  //corner cases: "0 + monomial" and "constant"(no monomials)
1180 
1181  Expr ret;
1182  if(2 == sumKids.size() && 0 == constant) ret = sumKids[1];
1183  else if (1 == sumKids.size()) ret = sumKids[0];
1184  else ret = plusExpr(sumKids);
1185 
1186  if(withProof()) pf = newPf("canon_combo_like_terms",e,ret);
1187  return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1188 }
1189 
1190 
1191 // 0 = (* e1 e2 ...) <=> 0 = e1 OR 0 = e2 OR ...
1192 Theorem ArithTheoremProducerOld::multEqZero(const Expr& expr)
1193 {
1194  Proof pf;
1195  vector<Expr> kids;
1196 
1197  int side = expr[0].isRational() ? 1 : 0;
1198 
1199  vector<Expr> non_zero;
1200 
1201  Expr::iterator i = expr[side].begin(), iend = expr[side].end();
1202  for (; i != iend; ++i) {
1203  Expr x = *i;
1204  // If a rational it can't be 0, so it is false, i.e. just skip it
1205  if (x.isRational()) {
1206  CHECK_SOUND(x.getRational() != 0, "multEqZero: once of the constants is 0");
1207  } else {
1208  Expr leaf = x;
1209  if (isPow(x)) {
1210  // We assume that 1 / 0 = 0 for simplicity and totality.
1211  // Divisions by zero that affect the result can be identified by enabling TCCs.
1212  // if (x[0].getRational() < 0) {
1213  // non_zero.push_back(x[1].eqExpr(rat(0)).notExpr());
1214  // continue;
1215  // }
1216  // else
1217  leaf = x[1];
1218  }
1219  if (leaf >= rat(0))
1220  kids.push_back(leaf.eqExpr(rat(0)));
1221  else
1222  kids.push_back(rat(0).eqExpr(leaf));
1223  }
1224  }
1225  Expr newExpr;
1226  if (kids.size() == 1) newExpr = kids[0];
1227  else newExpr = Expr(OR, kids);
1228  if (withProof()) {
1229  pf = newPf("multEqZero", expr);
1230  }
1231  // if (non_zero.size() == 0)
1232  return newRWTheorem(expr, newExpr, Assumptions::emptyAssump(), pf);
1233  // else return newRWTheorem(expr, Expr(OR, kids).andExpr(Expr(AND, non_zero)), Assumptions::emptyAssump(), pf);
1234 }
1235 
1236 
1237 // 0 = (^ c x) <=> false if c <=0
1238 // <=> 0 = x if c > 0
1239 Theorem ArithTheoremProducerOld::powEqZero(const Expr& expr)
1240 {
1241  if (CHECK_PROOFS) {
1242  CHECK_SOUND(expr.isEq() && expr[0].isRational() &&
1243  expr[0].getRational() == 0 &&
1244  isPow(expr[1]) && expr[1].arity() == 2 &&
1245  expr[1][0].isRational(),
1246  "powEqZero invariant violated"+expr.toString());
1247  }
1248  Proof pf;
1249  if (withProof()) {
1250  pf = newPf("powEqZero", expr);
1251  }
1252  Rational r = expr[1][0].getRational();
1253  Expr res;
1254  if (r <= 0) {
1255  res = d_em->falseExpr();
1256  }
1257  else {
1258  res = rat(0).eqExpr(expr[1][1]);
1259  }
1260  return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1261 }
1262 
1263 
1264 // x^n - y^n = 0 <=> x = y (if n is odd)
1265 // x^n - y^n = 0 <=> x = y OR x = -y (if n is even)
1266 Theorem ArithTheoremProducerOld::elimPower(const Expr& expr)
1267 {
1268  Expr power1, power2;
1269  bool ok = d_theoryArith->isPowersEquality(expr, power1, power2);
1270  if (CHECK_PROOFS)
1271  CHECK_SOUND(ok, "elimPower invariant violated"+expr.toString());
1272  Proof pf;
1273  if (withProof())
1274  pf = newPf("elimPower", expr);
1275  Rational r = power1[0].getRational();
1276  Expr res = power1[1].eqExpr(power2[1]);
1277  if (r % 2 == 0)
1278  res = res.orExpr(power1[1].eqExpr(-power2[1]));
1279  return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1280 }
1281 
1282 
1283 // x^n = c <=> x = root (if n is odd and root^n = c)
1284 // x^n = c <=> x = root OR x = -root (if n is even and root^n = c)
1285 Theorem ArithTheoremProducerOld::elimPowerConst(const Expr& expr, const Rational& root)
1286 {
1287  if (CHECK_PROOFS)
1288  CHECK_SOUND(expr.isEq(), "elimPowerConst invariant violated" + expr.toString());
1289  Rational constant;
1290  Expr power;
1291  bool ok = d_theoryArith->isPowerEquality(expr, constant, power);
1292  if (CHECK_PROOFS) {
1293  CHECK_SOUND(ok, "elimPowerConst invariant violated" + expr.toString());
1294  CHECK_SOUND(pow(power[0].getRational(), root) == constant, "elimPowerConst invariant violated" + expr.toString());
1295  }
1296 
1297  Proof pf;
1298  if (withProof())
1299  pf = newPf("elimPowerConst", expr, rat(root));
1300  Rational r = power[0].getRational();
1301  Expr res = power[1].eqExpr(rat(root));
1302  if (r % 2 == 0)
1303  res = res.orExpr(power[1].eqExpr(rat(-root)));
1304 
1305  return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1306 }
1307 
1308 
1309 // x^n = c <=> false (if n is even and c is negative)
1310 Theorem ArithTheoremProducerOld::evenPowerEqNegConst(const Expr& expr)
1311 {
1312  if (CHECK_PROOFS)
1313  CHECK_SOUND(expr.isEq(), "evenPowerEqNegConst, expecting equality, got " + expr.toString());
1314  Rational constant;
1315  Expr power;
1316  bool ok = d_theoryArith->isPowerEquality(expr, constant, power);
1317  if (CHECK_PROOFS) {
1318  CHECK_SOUND(ok, "evenPowerEqNegConst invariant violated" + expr.toString());
1319  CHECK_SOUND(constant < 0, "evenPowerEqNegConst invariant violated" + expr.toString());
1320  CHECK_SOUND(power[0].getRational().isInteger() && power[0].getRational() % 2 == 0, "evenPowerEqNegConst invariant violated" + expr.toString());
1321  }
1322  Proof pf;
1323  if (withProof())
1324  pf = newPf("evenPowerEqNegConst", expr);
1325  return newRWTheorem(expr, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
1326 }
1327 
1328 
1329 // x^n = c <=> ` (if x is an integer and c is not a perfect n power)
1330 Theorem ArithTheoremProducerOld::intEqIrrational(const Expr& expr, const Theorem& isIntx)
1331 {
1332  if (CHECK_PROOFS)
1333  CHECK_SOUND(expr.isEq(), "intEqIrrational invariant violated" + expr.toString());
1334  Rational constant;
1335  Expr power;
1336  bool ok = d_theoryArith->isPowerEquality(expr, constant, power);
1337  if (CHECK_PROOFS) {
1338  CHECK_SOUND(ok, "intEqIrrational invariant violated" + expr.toString());
1339  CHECK_SOUND(constant != 0, "intEqIrrational invariant violated" + expr.toString());
1340  CHECK_SOUND(power[0].getRational() > 0, "intEqIrrational invariant violated" + expr.toString());
1341  CHECK_SOUND(ratRoot(constant, power[0].getRational().getUnsigned()) == 0, "intEqIrrational invariant violated" + expr.toString());
1342  CHECK_SOUND(isIntPred(isIntx.getExpr()) && isIntx.getExpr()[0] == expr[0], "intEqIrrational invariant violated" + isIntx.getExpr()[0].toString());
1343  }
1344 
1345  const Assumptions& assump(isIntx.getAssumptionsRef());
1346  Proof pf;
1347  if (withProof())
1348  pf = newPf("int_eq_irr", expr, isIntx.getProof());
1349  return newRWTheorem(expr, d_em->falseExpr(), assump, pf);
1350 }
1351 
1352 
1353 // e[0] kind e[1] <==> true when e[0] kind e[1],
1354 // false when e[0] !kind e[1], for constants only
1355 Theorem ArithTheoremProducerOld::constPredicate(const Expr& e) {
1356  if(CHECK_PROOFS) {
1357  CHECK_SOUND(e.arity() == 2 && isRational(e[0]) && isRational(e[1]),
1358  CLASS_NAME "::constPredicate:\n "
1359  "non-const parameters: " + e.toString());
1360  }
1361  Proof pf;
1362  bool result(false);
1363  int kind = e.getKind();
1364  Rational r1 = e[0].getRational(), r2 = e[1].getRational();
1365  switch(kind) {
1366  case EQ:
1367  result = (r1 == r2)?true : false;
1368  break;
1369  case LT:
1370  result = (r1 < r2)?true : false;
1371  break;
1372  case LE:
1373  result = (r1 <= r2)?true : false;
1374  break;
1375  case GT:
1376  result = (r1 > r2)?true : false;
1377  break;
1378  case GE:
1379  result = (r1 >= r2)?true : false;
1380  break;
1381  default:
1382  if(CHECK_PROOFS) {
1383  CHECK_SOUND(false,
1384  "ArithTheoremProducerOld::constPredicate: wrong kind");
1385  }
1386  break;
1387  }
1388  Expr ret = (result) ? d_em->trueExpr() : d_em->falseExpr();
1389  if(withProof()) pf = newPf("const_predicate", e,ret);
1390  return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1391 }
1392 
1393 // e[0] kind e[1] <==> 0 kind e[1] - e[0]
1394 Theorem ArithTheoremProducerOld::rightMinusLeft(const Expr& e)
1395 {
1396  Proof pf;
1397  int kind = e.getKind();
1398  if(CHECK_PROOFS) {
1399  CHECK_SOUND((EQ==kind) ||
1400  (LT==kind) ||
1401  (LE==kind) ||
1402  (GE==kind) ||
1403  (GT==kind),
1404  "ArithTheoremProducerOld::rightMinusLeft: wrong kind");
1405  }
1406  if(withProof()) pf = newPf("right_minus_left",e);
1407  return newRWTheorem(e, Expr(e.getOp(), rat(0), e[1] - e[0]), Assumptions::emptyAssump(), pf);
1408 }
1409 
1410 
1411 // e[0] kind e[1] <==> 0 kind e[1] - e[0]
1412 Theorem ArithTheoremProducerOld::leftMinusRight(const Expr& e)
1413 {
1414  Proof pf;
1415  int kind = e.getKind();
1416  if(CHECK_PROOFS) {
1417  CHECK_SOUND((EQ==kind) ||
1418  (LT==kind) ||
1419  (LE==kind) ||
1420  (GE==kind) ||
1421  (GT==kind),
1422  "ArithTheoremProducerOld::rightMinusLeft: wrong kind");
1423  }
1424  if(withProof()) pf = newPf("left_minus_right",e);
1425  return newRWTheorem(e, Expr(e.getOp(), e[0] - e[1], rat(0)), Assumptions::emptyAssump(), pf);
1426 }
1427 
1428 
1429 // x kind y <==> x + z kind y + z
1430 Theorem ArithTheoremProducerOld::plusPredicate(const Expr& x,
1431  const Expr& y,
1432  const Expr& z, int kind) {
1433  if(CHECK_PROOFS) {
1434  CHECK_SOUND((EQ==kind) ||
1435  (LT==kind) ||
1436  (LE==kind) ||
1437  (GE==kind) ||
1438  (GT==kind),
1439  "ArithTheoremProducerOld::plusPredicate: wrong kind");
1440  }
1441  Proof pf;
1442  Expr left = Expr(kind, x, y);
1443  Expr right = Expr(kind, x + z, y + z);
1444  if(withProof()) pf = newPf("plus_predicate",left,right);
1445  return newRWTheorem(left, right, Assumptions::emptyAssump(), pf);
1446 }
1447 
1448 // x = y <==> x * z = y * z
1449 Theorem ArithTheoremProducerOld::multEqn(const Expr& x,
1450  const Expr& y,
1451  const Expr& z) {
1452  Proof pf;
1453  if(CHECK_PROOFS)
1454  CHECK_SOUND(z.isRational() && z.getRational() != 0,
1455  "ArithTheoremProducerOld::multEqn(): multiplying equation by 0");
1456  if(withProof()) pf = newPf("mult_eqn", x, y, z);
1457  return newRWTheorem(x.eqExpr(y), (x * z).eqExpr(y * z), Assumptions::emptyAssump(), pf);
1458 }
1459 
1460 
1461 // x = y <==> z=0 OR x * 1/z = y * 1/z
1462 Theorem ArithTheoremProducerOld::divideEqnNonConst(const Expr& x,
1463  const Expr& y,
1464  const Expr& z) {
1465  Proof pf;
1466  if(withProof()) pf = newPf("mult_eqn_nonconst", x, y, z);
1467  return newRWTheorem(x.eqExpr(y), (z.eqExpr(rat(0))).orExpr((x / z).eqExpr(y / z)),
1468  Assumptions::emptyAssump(), pf);
1469 }
1470 
1471 
1472 // if z is +ve, return e[0] LT|LE|GT|GE e[1] <==> e[0]*z LT|LE|GT|GE e[1]*z
1473 // if z is -ve, return e[0] LT|LE|GT|GE e[1] <==> e[1]*z LT|LE|GT|GE e[0]*z
1474 Theorem ArithTheoremProducerOld::multIneqn(const Expr& e, const Expr& z)
1475 {
1476  int kind = e.getKind();
1477 
1478  if(CHECK_PROOFS) {
1479  CHECK_SOUND((LT==kind) ||
1480  (LE==kind) ||
1481  (GE==kind) ||
1482  (GT==kind),
1483  "ArithTheoremProducerOld::multIneqn: wrong kind");
1484  CHECK_SOUND(z.isRational() && z.getRational() != 0,
1485  "ArithTheoremProducerOld::multIneqn: "
1486  "z must be non-zero rational: " + z.toString());
1487  }
1488  Op op(e.getOp());
1489  Proof pf;
1490 
1491  Expr ret;
1492  if(0 < z.getRational())
1493  ret = Expr(op, e[0]*z, e[1]*z);
1494  else
1495  ret = Expr(op, e[1]*z, e[0]*z);
1496  if(withProof()) pf = newPf("mult_ineqn", e, ret);
1497  return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1498 }
1499 
1500 
1501 //
1502 // If expr:
1503 // If b > 0 then (0 <= a + bx) <==> (0 <= floor(a/b) + x)
1504 // b < 0 then (0 <= a + bx) <==> (0 >= ceil(a/b) + x)
1505 // b > 0 then (0 >= a + bx) <==> (0 >= ceil(a/b) + x)
1506 // b < 0 then (0 >= a + bx) <==> (0 <= floor(a/b) + x)
1507 //
1508 Theorem ArithTheoremProducerOld::simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS)
1509 {
1510  // Get the inequality parts
1511  Expr lhs = ineq[0];
1512  Expr rhs = ineq[1];
1513 
1514  // Get the kind of the inequality
1515  int kind = ineq.getKind();
1516 
1517 
1518  if(CHECK_PROOFS) {
1519  // isIntRHS should be an int proof of rhs
1520  const Expr& isIntRHSExpr = isIntRHS.getExpr();
1521  CHECK_SOUND(isIntPred(isIntRHSExpr) && isIntRHSExpr[0] == rhs, "ArithTheoremProducerOld::multSimpleIneqnInt: not an integer proof of rhs");
1522 
1523  // It's an inequality
1524  CHECK_SOUND((LT == kind) || (LE==kind) || (GE==kind) || (GT==kind), "ArithTheoremProducerOld::multSimpleIneqnInt: wrong kind");
1525 
1526  // Left-hand side is 0
1527  CHECK_SOUND(lhs.isRational() && lhs.getRational() == 0, "ArithTheoremProducerOld::multSimpleIneqnInt: left-hand side must be 0");
1528 
1529  // Tight hand side is a sum (a + b*x) where a and b are integers, x is a var
1530  CHECK_SOUND(isPlus(rhs), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side must be a plus");
1531  CHECK_SOUND(rhs.arity() == 2, "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus");
1532 
1533  Expr a = rhs[0]; // Should be an integer
1534  Expr bx = rhs[1]; // Should be an integer multiplied by a variable
1535 
1536  // a is an integer
1537  CHECK_SOUND(a.isRational() && a.getRational().isInteger(), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of a constant");
1538 
1539  // bx should be a multiplication of an intgere and a variable
1540  CHECK_SOUND(isMult(bx) && bx.arity() == 2, "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication");
1541  Expr b = bx[0];
1542  Expr x = bx[1];
1543 
1544  // b should be an integer
1545  CHECK_SOUND(b.isRational() && b.getRational().isInteger(), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication of a constant");
1546  // x should be a variable
1547  CHECK_SOUND(x.isVar(), "ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication of a constant and a leaf");
1548 
1549  // GCD(a, b) should be 1
1550  //CHECK_SOUND(gcd(a.getRational(), b.getRational()) == 1, "ArithTheoremProducerOld::multSimpleIneqnInt: inequation not normalized!!!");
1551  }
1552 
1553  Proof pf;
1554  if(withProof()) {
1555  vector<Proof> pfs;
1556  pfs.push_back(isIntRHS.getProof());
1557  pf = newPf("simpleineqint", ineq, pf);
1558  }
1559 
1560  Rational a = rhs[0].getRational();
1561  Rational b = rhs[1][0].getRational();
1562  Expr x = rhs[1][1];
1563 
1564  Rational new_const;
1565  Expr ret;
1566  switch (kind) {
1567  case LT:
1568  if (b > 0) {
1569  new_const = floor(a/b);
1570  if (new_const != 0)
1571  ret = Expr(kind, rat(0), rat(new_const) + x);
1572  else
1573  ret = Expr(kind, rat(0), x);
1574  }
1575  else {
1576  new_const = ceil(a/b);
1577  //ret = geExpr(rat(0), rat(new_const) + x);
1578  if (new_const != 0)
1579  ret = Expr(kind, rat(0), rat(-new_const) + rat(-1)*x);
1580  else
1581  ret = Expr(kind, rat(0), rat(-1)*x);
1582  }
1583  break;
1584  break;
1585  case LE:
1586  if (b > 0) {
1587  new_const = floor(a/b);
1588  if (new_const != 0)
1589  ret = Expr(kind, rat(0), rat(new_const) + x);
1590  else
1591  ret = Expr(kind, rat(0), x);
1592  }
1593  else {
1594  new_const = ceil(a/b);
1595  //ret = geExpr(rat(0), rat(new_const) + x);
1596  if (new_const != 0)
1597  ret = Expr(kind, rat(0), rat(-new_const) + rat(-1)*x);
1598  else
1599  ret = Expr(kind, rat(0), rat(-1)*x);
1600  }
1601  break;
1602  case GE:
1603  case GT:
1604  // Setup the result kind
1605  if (kind == GT) kind = LT;
1606  else kind = LE;
1607 
1608  if (b > 0) {
1609  new_const = ceil(a/b);
1610  //ret = geExpr(rat(0), rat(new_const) + x);
1611  if (new_const != 0)
1612  ret = Expr(kind, rat(0), rat(-new_const) + rat(-1)*x);
1613  else
1614  ret = Expr(kind, rat(0), rat(-1)*x);
1615  }
1616  else {
1617  new_const = floor(a/b);
1618  if (new_const != 0)
1619  ret = Expr(kind, rat(0), rat(new_const) + x);
1620  else
1621  ret = Expr(kind, rat(0), x);
1622  }
1623  break;
1624  }
1625 
1626  // Return the new theorem
1627  return newRWTheorem(ineq, ret, Assumptions::emptyAssump(), pf);
1628 }
1629 
1630 
1631 Theorem ArithTheoremProducerOld::eqToIneq(const Expr& e) {
1632 
1633  // Check soundness of the rule if necessary
1634  if (CHECK_PROOFS)
1635  CHECK_SOUND(e.isEq(), "eqToIneq: input must be an equality: " + e.toString());
1636 
1637  // The proof object we will use
1638  Proof pf;
1639 
1640  // The parts of the equality x = y
1641  const Expr& x = e[0];
1642  const Expr& y = e[1];
1643 
1644  // Setup the proof if needed
1645  if (withProof())
1646  pf = newPf("eqToIneq", e);
1647 
1648  // Retrun the theorem explaining the transformation
1649  return newRWTheorem(e, leExpr(x,y).andExpr(geExpr(x,y)), Assumptions::emptyAssump(), pf);
1650 }
1651 
1652 // "op1 GE|GT op2" <==> op2 LE|LT op1
1653 Theorem ArithTheoremProducerOld::flipInequality(const Expr& e)
1654 {
1655  Proof pf;
1656  if(CHECK_PROOFS) {
1657  CHECK_SOUND(isGT(e) || isGE(e),
1658  "ArithTheoremProducerOld::flipInequality: wrong kind: " +
1659  e.toString());
1660  }
1661 
1662  int kind = isGE(e) ? LE : LT;
1663  Expr ret = Expr(kind, e[1], e[0]);
1664  if(withProof()) pf = newPf("flip_inequality", e,ret);
1665  return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
1666 }
1667 
1668 
1669 // NOT (op1 LT op2) <==> (op1 GE op2)
1670 // NOT (op1 LE op2) <==> (op1 GT op2)
1671 // NOT (op1 GT op2) <==> (op1 LE op2)
1672 // NOT (op1 GE op2) <==> (op1 LT op2)
1673 Theorem ArithTheoremProducerOld::negatedInequality(const Expr& e)
1674 {
1675  const Expr& ineq = e[0];
1676  if(CHECK_PROOFS) {
1677  CHECK_SOUND(e.isNot(),
1678  "ArithTheoremProducerOld::negatedInequality: wrong kind: " +
1679  e.toString());
1680  CHECK_SOUND(isIneq(ineq),
1681  "ArithTheoremProducerOld::negatedInequality: wrong kind: " +
1682  (ineq).toString());
1683  }
1684  Proof pf;
1685  if(withProof()) pf = newPf("negated_inequality", e);
1686 
1687  int kind;
1688  // NOT (op1 LT op2) <==> (op1 GE op2)
1689  // NOT (op1 LE op2) <==> (op1 GT op2)
1690  // NOT (op1 GT op2) <==> (op1 LE op2)
1691  // NOT (op1 GE op2) <==> (op1 LT op2)
1692  kind =
1693  isLT(ineq) ? GE :
1694  isLE(ineq) ? GT :
1695  isGT(ineq) ? LE :
1696  LT;
1697  return newRWTheorem(e, Expr(kind, ineq[0], ineq[1]), Assumptions::emptyAssump(), pf);
1698 }
1699 
1700 //takes two ineqs "|- alpha LT|LE t" and "|- t LT|LE beta"
1701 //and returns "|- alpha LT|LE beta"
1702 Theorem ArithTheoremProducerOld::realShadow(const Theorem& alphaLTt,
1703  const Theorem& tLTbeta)
1704 {
1705  const Expr& expr1 = alphaLTt.getExpr();
1706  const Expr& expr2 = tLTbeta.getExpr();
1707  if(CHECK_PROOFS) {
1708  CHECK_SOUND((isLE(expr1) || isLT(expr1)) &&
1709  (isLE(expr2) || isLT(expr2)),
1710  "ArithTheoremProducerOld::realShadow: Wrong Kind: " +
1711  alphaLTt.toString() + tLTbeta.toString());
1712 
1713  CHECK_SOUND(expr1[1] == expr2[0],
1714  "ArithTheoremProducerOld::realShadow:"
1715  " t must be same for both inputs: " +
1716  expr1[1].toString() + " , " + expr2[0].toString());
1717  }
1718  Assumptions a(alphaLTt, tLTbeta);
1719  int firstKind = expr1.getKind();
1720  int secondKind = expr2.getKind();
1721  int kind = (firstKind == secondKind) ? firstKind : LT;
1722  Proof pf;
1723  if(withProof()) {
1724  vector<Proof> pfs;
1725  pfs.push_back(alphaLTt.getProof());
1726  pfs.push_back(tLTbeta.getProof());
1727  pf = newPf("real_shadow",expr1, expr2, pfs);
1728  }
1729  return newTheorem(Expr(kind, expr1[0], expr2[1]), a, pf);
1730 }
1731 
1732 //! alpha <= t <= alpha ==> t = alpha
1733 
1734 /*! takes two ineqs "|- alpha LE t" and "|- t LE alpha"
1735  and returns "|- t = alpha"
1736 */
1737 Theorem ArithTheoremProducerOld::realShadowEq(const Theorem& alphaLEt,
1738  const Theorem& tLEalpha)
1739 {
1740  const Expr& expr1 = alphaLEt.getExpr();
1741  const Expr& expr2 = tLEalpha.getExpr();
1742  if(CHECK_PROOFS) {
1743  CHECK_SOUND(isLE(expr1) && isLE(expr2),
1744  "ArithTheoremProducerOld::realShadowLTLE: Wrong Kind: " +
1745  alphaLEt.toString() + tLEalpha.toString());
1746 
1747  CHECK_SOUND(expr1[1] == expr2[0],
1748  "ArithTheoremProducerOld::realShadowLTLE:"
1749  " t must be same for both inputs: " +
1750  alphaLEt.toString() + " , " + tLEalpha.toString());
1751 
1752  CHECK_SOUND(expr1[0] == expr2[1],
1753  "ArithTheoremProducerOld::realShadowLTLE:"
1754  " alpha must be same for both inputs: " +
1755  alphaLEt.toString() + " , " + tLEalpha.toString());
1756  }
1757  Assumptions a(alphaLEt, tLEalpha);
1758  Proof pf;
1759  if(withProof()) {
1760  vector<Proof> pfs;
1761  pfs.push_back(alphaLEt.getProof());
1762  pfs.push_back(tLEalpha.getProof());
1763  pf = newPf("real_shadow_eq", alphaLEt.getExpr(), tLEalpha.getExpr(), pfs);
1764  }
1765  return newRWTheorem(expr1[0], expr1[1], a, pf);
1766 }
1767 
1768 Theorem
1769 ArithTheoremProducerOld::finiteInterval(const Theorem& aLEt,
1770  const Theorem& tLEac,
1771  const Theorem& isInta,
1772  const Theorem& isIntt) {
1773  const Expr& e1 = aLEt.getExpr();
1774  const Expr& e2 = tLEac.getExpr();
1775  if(CHECK_PROOFS) {
1776  CHECK_SOUND(isLE(e1) && isLE(e2),
1777  "ArithTheoremProducerOld::finiteInterval:\n e1 = "
1778  +e1.toString()+"\n e2 = "+e2.toString());
1779  // term 't' is the same in both inequalities
1780  CHECK_SOUND(e1[1] == e2[0],
1781  "ArithTheoremProducerOld::finiteInterval:\n e1 = "
1782  +e1.toString()+"\n e2 = "+e2.toString());
1783  // RHS in e2 is (a+c)
1784  CHECK_SOUND(isPlus(e2[1]) && e2[1].arity() == 2,
1785  "ArithTheoremProducerOld::finiteInterval:\n e1 = "
1786  +e1.toString()+"\n e2 = "+e2.toString());
1787  // term 'a' in LHS of e1 and RHS of e2 is the same
1788  CHECK_SOUND(e1[0] == e2[1][0],
1789  "ArithTheoremProducerOld::finiteInterval:\n e1 = "
1790  +e1.toString()+"\n e2 = "+e2.toString());
1791  // 'c' in the RHS of e2 is a positive integer constant
1792  CHECK_SOUND(e2[1][1].isRational() && e2[1][1].getRational().isInteger()
1793  && e2[1][1].getRational() >= 1,
1794  "ArithTheoremProducerOld::finiteInterval:\n e1 = "
1795  +e1.toString()+"\n e2 = "+e2.toString());
1796  // Integrality constraints
1797  const Expr& isIntaExpr = isInta.getExpr();
1798  const Expr& isInttExpr = isIntt.getExpr();
1799  CHECK_SOUND(isIntPred(isIntaExpr) && isIntaExpr[0] == e1[0],
1800  "Wrong integrality constraint:\n e1 = "
1801  +e1.toString()+"\n isInta = "+isIntaExpr.toString());
1802  CHECK_SOUND(isIntPred(isInttExpr) && isInttExpr[0] == e1[1],
1803  "Wrong integrality constraint:\n e1 = "
1804  +e1.toString()+"\n isIntt = "+isInttExpr.toString());
1805  }
1806  vector<Theorem> thms;
1807  thms.push_back(aLEt);
1808  thms.push_back(tLEac);
1809  thms.push_back(isInta);
1810  thms.push_back(isIntt);
1811  Assumptions a(thms);
1812  Proof pf;
1813  if(withProof()) {
1814  vector<Expr> es;
1815  vector<Proof> pfs;
1816  es.push_back(e1);
1817  es.push_back(e2);
1818  es.push_back(isInta.getExpr());
1819  es.push_back(isIntt.getExpr());
1820  pfs.push_back(aLEt.getProof());
1821  pfs.push_back(tLEac.getProof());
1822  pfs.push_back(isInta.getProof());
1823  pfs.push_back(isIntt.getProof());
1824  pf = newPf("finite_interval", es, pfs);
1825  }
1826  // Construct GRAY_SHADOW(t, a, 0, c)
1827  Expr g(grayShadow(e1[1], e1[0], 0, e2[1][1].getRational()));
1828  return newTheorem(g, a, pf);
1829 }
1830 
1831 
1832 // Dark & Gray shadows when a <= b
1833 Theorem ArithTheoremProducerOld::darkGrayShadow2ab(const Theorem& betaLEbx,
1834  const Theorem& axLEalpha,
1835  const Theorem& isIntAlpha,
1836  const Theorem& isIntBeta,
1837  const Theorem& isIntx) {
1838  const Expr& expr1 = betaLEbx.getExpr();
1839  const Expr& expr2 = axLEalpha.getExpr();
1840  const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
1841  const Expr& isIntBetaExpr = isIntBeta.getExpr();
1842  const Expr& isIntxExpr = isIntx.getExpr();
1843 
1844  if(CHECK_PROOFS) {
1845  CHECK_SOUND(isLE(expr1) && isLE(expr2),
1846  "ArithTheoremProducerOld::darkGrayShadow2ab: Wrong Kind: " +
1847  betaLEbx.toString() + axLEalpha.toString());
1848  }
1849 
1850  const Expr& beta = expr1[0];
1851  const Expr& bx = expr1[1];
1852  const Expr& ax = expr2[0];
1853  const Expr& alpha = expr2[1];
1854  Expr a_expr, b_expr, x;
1855  d_theoryArith->separateMonomial(ax, a_expr, x);
1856  d_theoryArith->separateMonomial(bx, b_expr, x);
1857  Rational a = a_expr.getRational();
1858  Rational b = b_expr.getRational();
1859 
1860  if(CHECK_PROOFS) {
1861  // Integrality constraints
1862  CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
1863  "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1864  "wrong integrality constraint:\n alpha = "
1865  +alpha.toString()+"\n isIntAlpha = "
1866  +isIntAlphaExpr.toString());
1867  CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
1868  "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1869  "wrong integrality constraint:\n beta = "
1870  +beta.toString()+"\n isIntBeta = "
1871  +isIntBetaExpr.toString());
1872  CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
1873  "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1874  "wrong integrality constraint:\n x = "
1875  +x.toString()+"\n isIntx = "
1876  +isIntxExpr.toString());
1877  // NOT FOR NONLINEAR: Expressions ax and bx should match on x
1878 // CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
1879 // "ArithTheoremProducerOld::darkGrayShadow2ab:\n ax<=alpha: " +
1880 // axLEalpha.toString());
1881 // CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
1882 // "ArithTheoremProducerOld::darkGrayShadow2ab:\n beta<=bx: "
1883 // +betaLEbx.toString()
1884 // +"\n ax<=alpha: "+ axLEalpha.toString());
1885  CHECK_SOUND(1 <= a && a <= b && 2 <= b,
1886  "ArithTheoremProducerOld::darkGrayShadow2ab:\n beta<=bx: "
1887  +betaLEbx.toString()
1888  +"\n ax<=alpha: "+ axLEalpha.toString());
1889  }
1890  vector<Theorem> thms;
1891  thms.push_back(betaLEbx);
1892  thms.push_back(axLEalpha);
1893  thms.push_back(isIntAlpha);
1894  thms.push_back(isIntBeta);
1895  thms.push_back(isIntx);
1896  Assumptions A(thms);
1897 
1898  Expr bAlpha = multExpr(rat(b), alpha);
1899  Expr aBeta = multExpr(rat(a), beta);
1900  Expr t = minusExpr(bAlpha, aBeta);
1901  Expr d = geExpr(t, rat(a*b-1));
1902  Expr g = grayShadow(ax, alpha, -a+1, 0);
1903 
1904  Proof pf;
1905  if(withProof()) {
1906  vector<Expr> exprs;
1907  exprs.push_back(expr1);
1908  exprs.push_back(expr2);
1909  exprs.push_back(d);
1910  exprs.push_back(g);
1911 
1912  vector<Proof> pfs;
1913  pfs.push_back(betaLEbx.getProof());
1914  pfs.push_back(axLEalpha.getProof());
1915  pfs.push_back(isIntAlpha.getProof());
1916  pfs.push_back(isIntBeta.getProof());
1917  pfs.push_back(isIntx.getProof());
1918 
1919  pf = newPf("dark_grayshadow_2ab", exprs, pfs);
1920  }
1921 
1922  return newTheorem((d || g), A, pf);
1923 }
1924 
1925 // Dark & Gray shadows when b <= a
1926 Theorem ArithTheoremProducerOld::darkGrayShadow2ba(const Theorem& betaLEbx,
1927  const Theorem& axLEalpha,
1928  const Theorem& isIntAlpha,
1929  const Theorem& isIntBeta,
1930  const Theorem& isIntx) {
1931  const Expr& expr1 = betaLEbx.getExpr();
1932  const Expr& expr2 = axLEalpha.getExpr();
1933  const Expr& isIntAlphaExpr = isIntAlpha.getExpr();
1934  const Expr& isIntBetaExpr = isIntBeta.getExpr();
1935  const Expr& isIntxExpr = isIntx.getExpr();
1936 
1937  if(CHECK_PROOFS) {
1938  CHECK_SOUND(isLE(expr1) && isLE(expr2),
1939  "ArithTheoremProducerOld::darkGrayShadow2ba: Wrong Kind: " +
1940  betaLEbx.toString() + axLEalpha.toString());
1941  }
1942 
1943  const Expr& beta = expr1[0];
1944  const Expr& bx = expr1[1];
1945  const Expr& ax = expr2[0];
1946  const Expr& alpha = expr2[1];
1947 
1948  Expr a_expr, b_expr, x;
1949  d_theoryArith->separateMonomial(ax, a_expr, x);
1950  d_theoryArith->separateMonomial(bx, b_expr, x);
1951  Rational a = a_expr.getRational();
1952  Rational b = b_expr.getRational();
1953 
1954  if(CHECK_PROOFS) {
1955  // Integrality constraints
1956  CHECK_SOUND(isIntPred(isIntAlphaExpr) && isIntAlphaExpr[0] == alpha,
1957  "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1958  "wrong integrality constraint:\n alpha = "
1959  +alpha.toString()+"\n isIntAlpha = "
1960  +isIntAlphaExpr.toString());
1961  CHECK_SOUND(isIntPred(isIntBetaExpr) && isIntBetaExpr[0] == beta,
1962  "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1963  "wrong integrality constraint:\n beta = "
1964  +beta.toString()+"\n isIntBeta = "
1965  +isIntBetaExpr.toString());
1966  CHECK_SOUND(isIntPred(isIntxExpr) && isIntxExpr[0] == x,
1967  "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1968  "wrong integrality constraint:\n x = "
1969  +x.toString()+"\n isIntx = "
1970  +isIntxExpr.toString());
1971  // NOT FOR NONLINEAR: Expressions ax and bx should match on x
1972 // CHECK_SOUND(!isMult(ax) || ax.arity() == 2,
1973 // "ArithTheoremProducerOld::darkGrayShadow2ba:\n ax<=alpha: " +
1974 // axLEalpha.toString());
1975 // CHECK_SOUND(!isMult(bx) || (bx.arity() == 2 && bx[1] == x),
1976 // "ArithTheoremProducerOld::darkGrayShadow2ba:\n beta<=bx: "
1977 // +betaLEbx.toString()
1978 // +"\n ax<=alpha: "+ axLEalpha.toString());
1979  CHECK_SOUND(1 <= b && b <= a && 2 <= a,
1980  "ArithTheoremProducerOld::darkGrayShadow2ba:\n beta<=bx: "
1981  +betaLEbx.toString()
1982  +"\n ax<=alpha: "+ axLEalpha.toString());
1983  }
1984  vector<Theorem> thms;
1985  thms.push_back(betaLEbx);
1986  thms.push_back(axLEalpha);
1987  thms.push_back(isIntAlpha);
1988  thms.push_back(isIntBeta);
1989  thms.push_back(isIntx);
1990  Assumptions A(thms);
1991  Proof pf;
1992  if(withProof()) {
1993  vector<Proof> pfs;
1994  pfs.push_back(betaLEbx.getProof());
1995  pfs.push_back(axLEalpha.getProof());
1996  pfs.push_back(isIntAlpha.getProof());
1997  pfs.push_back(isIntBeta.getProof());
1998  pfs.push_back(isIntx.getProof());
1999 
2000  pf = newPf("dark_grayshadow_2ba", betaLEbx.getExpr(),
2001  axLEalpha.getExpr(), pfs);
2002  }
2003 
2004  Expr bAlpha = multExpr(rat(b), alpha);
2005  Expr aBeta = multExpr(rat(a), beta);
2006  Expr t = minusExpr(bAlpha, aBeta);
2007  Expr d = geExpr(t, rat(a*b-1));
2008  Expr g = grayShadow(bx, beta, 0, b-1);
2009  return newTheorem((d || g), A, pf);
2010 }
2011 
2012 /*! takes a dark shadow and expands it into an inequality.
2013 */
2014 Theorem ArithTheoremProducerOld::expandDarkShadow(const Theorem& darkShadow) {
2015  const Expr& theShadow = darkShadow.getExpr();
2016  if(CHECK_PROOFS){
2017  CHECK_SOUND(isDarkShadow(theShadow),
2018  "ArithTheoremProducerOld::expandDarkShadow: not DARK_SHADOW: " +
2019  theShadow.toString());
2020  }
2021  Proof pf;
2022  if(withProof())
2023  pf = newPf("expand_dark_shadow", theShadow, darkShadow.getProof());
2024  return newTheorem(leExpr(theShadow[0], theShadow[1]), darkShadow.getAssumptionsRef(), pf);
2025 }
2026 
2027 
2028 // takes a grayShadow (c1==c2) and expands it into an equality
2029 Theorem ArithTheoremProducerOld::expandGrayShadow0(const Theorem& grayShadow) {
2030  const Expr& theShadow = grayShadow.getExpr();
2031  if(CHECK_PROOFS) {
2032  CHECK_SOUND(isGrayShadow(theShadow),
2033  "ArithTheoremProducerOld::expandGrayShadowConst0:"
2034  " not GRAY_SHADOW: " +
2035  theShadow.toString());
2036  CHECK_SOUND(theShadow[2] == theShadow[3],
2037  "ArithTheoremProducerOld::expandGrayShadow0: c1!=c2: " +
2038  theShadow.toString());
2039  }
2040  Proof pf;
2041  if(withProof()) pf = newPf("expand_gray_shadowconst0", theShadow,
2042  grayShadow.getProof());
2043  const Expr& v = theShadow[0];
2044  const Expr& e = theShadow[1];
2045  return newRWTheorem(v, e + theShadow[2], grayShadow.getAssumptionsRef(), pf);
2046 }
2047 
2048 
2049 // G ==> (G1 or G2) and (!G1 or !G2),
2050 // where G = G(x, e, c1, c2),
2051 // G1 = G(x,e,c1,c)
2052 // G2 = G(x,e,c+1,c2),
2053 // and c = floor((c1+c2)/2)
2054 Theorem ArithTheoremProducerOld::splitGrayShadow(const Theorem& gThm) {
2055  const Expr& theShadow = gThm.getExpr();
2056  if(CHECK_PROOFS) {
2057  CHECK_SOUND(isGrayShadow(theShadow),
2058  "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
2059  theShadow.toString());
2060  }
2061 
2062  const Rational& c1 = theShadow[2].getRational();
2063  const Rational& c2 = theShadow[3].getRational();
2064 
2065  if(CHECK_PROOFS) {
2066  CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
2067  "ArithTheoremProducerOld::expandGrayShadow: " +
2068  theShadow.toString());
2069  }
2070 
2071  const Expr& v = theShadow[0];
2072  const Expr& e = theShadow[1];
2073 
2074  Proof pf;
2075  Rational c(floor((c1+c2) / 2));
2076  Expr g1(grayShadow(v, e, c1, c));
2077  Expr g2(grayShadow(v, e, c+1, c2));
2078 
2079  if(withProof()){
2080  vector<Expr> exprs;
2081  exprs.push_back(theShadow);
2082  exprs.push_back(g1);
2083  exprs.push_back(g2);
2084  pf = newPf("split_gray_shadow", exprs, gThm.getProof());
2085  }
2086 
2087  return newTheorem((g1 || g2) && (!g1 || !g2), gThm.getAssumptionsRef(), pf);
2088 }
2089 
2090 
2091 Theorem ArithTheoremProducerOld::expandGrayShadow(const Theorem& gThm) {
2092  const Expr& theShadow = gThm.getExpr();
2093  if(CHECK_PROOFS) {
2094  CHECK_SOUND(isGrayShadow(theShadow),
2095  "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
2096  theShadow.toString());
2097  }
2098 
2099  const Rational& c1 = theShadow[2].getRational();
2100  const Rational& c2 = theShadow[3].getRational();
2101 
2102  if(CHECK_PROOFS) {
2103  CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
2104  "ArithTheoremProducerOld::expandGrayShadow: " +
2105  theShadow.toString());
2106  }
2107 
2108  const Expr& v = theShadow[0];
2109  const Expr& e = theShadow[1];
2110 
2111  Proof pf;
2112  if(withProof())
2113  pf = newPf("expand_gray_shadow", theShadow, gThm.getProof());
2114  Expr ineq1(leExpr(e+rat(c1), v));
2115  Expr ineq2(leExpr(v, e+rat(c2)));
2116  return newTheorem(ineq1 && ineq2, gThm.getAssumptionsRef(), pf);
2117 }
2118 
2119 
2120 // Expanding GRAY_SHADOW(a*x, c, b), where c is a constant
2121 Theorem
2122 ArithTheoremProducerOld::expandGrayShadowConst(const Theorem& gThm) {
2123  const Expr& theShadow = gThm.getExpr();
2124  const Expr& ax = theShadow[0];
2125  const Expr& cExpr = theShadow[1];
2126  const Expr& bExpr = theShadow[2];
2127 
2128  if(CHECK_PROOFS) {
2129  CHECK_SOUND(!isMult(ax) || ax[0].isRational(),
2130  "ArithTheoremProducerOld::expandGrayShadowConst: "
2131  "'a' in a*x is not a const: " +theShadow.toString());
2132  }
2133 
2134  Rational a = isMult(ax)? ax[0].getRational() : 1;
2135 
2136  if(CHECK_PROOFS) {
2137  CHECK_SOUND(isGrayShadow(theShadow),
2138  "ArithTheoremProducerOld::expandGrayShadowConst: "
2139  "not a GRAY_SHADOW: " +theShadow.toString());
2140  CHECK_SOUND(a.isInteger() && a >= 1,
2141  "ArithTheoremProducerOld::expandGrayShadowConst: "
2142  "'a' is not integer: " +theShadow.toString());
2143  CHECK_SOUND(cExpr.isRational(),
2144  "ArithTheoremProducerOld::expandGrayShadowConst: "
2145  "'c' is not rational" +theShadow.toString());
2146  CHECK_SOUND(bExpr.isRational() && bExpr.getRational().isInteger(),
2147  "ArithTheoremProducerOld::expandGrayShadowConst: b not integer: "
2148  +theShadow.toString());
2149  }
2150 
2151  const Rational& b = bExpr.getRational();
2152  const Rational& c = cExpr.getRational();
2153  Rational j = constRHSGrayShadow(c,b,a);
2154  // Compute sign(b)*j(c,b,a)
2155  Rational signB = (b>0)? 1 : -1;
2156  // |b| (absolute value of b)
2157  Rational bAbs = abs(b);
2158 
2159  const Assumptions& assump(gThm.getAssumptionsRef());
2160  Proof pf;
2161  Theorem conc; // Conclusion of the rule
2162 
2163  if(bAbs < j) {
2164  if(withProof())
2165  pf = newPf("expand_gray_shadow_const_0", theShadow,
2166  gThm.getProof());
2167  conc = newTheorem(d_em->falseExpr(), assump, pf);
2168  } else if(bAbs < a+j) {
2169  if(withProof())
2170  pf = newPf("expand_gray_shadow_const_1", theShadow,
2171  gThm.getProof());
2172  conc = newRWTheorem(ax, rat(c+b-signB*j), assump, pf);
2173  } else {
2174  if(withProof())
2175  pf = newPf("expand_gray_shadow_const", theShadow,
2176  gThm.getProof());
2177  Expr newGrayShadow(Expr(GRAY_SHADOW, ax, cExpr, rat(b-signB*(a+j))));
2178  conc = newTheorem(ax.eqExpr(rat(c+b-signB*j)).orExpr(newGrayShadow),
2179  assump, pf);
2180  }
2181 
2182  return conc;
2183 }
2184 
2185 
2186 Theorem
2187 ArithTheoremProducerOld::grayShadowConst(const Theorem& gThm) {
2188  const Expr& g = gThm.getExpr();
2189  bool checkProofs(CHECK_PROOFS);
2190  if(checkProofs) {
2191  CHECK_SOUND(isGrayShadow(g), "ArithTheoremProducerOld::grayShadowConst("
2192  +g.toString()+")");
2193  }
2194 
2195  const Expr& ax = g[0];
2196  const Expr& e = g[1];
2197  const Rational& c1 = g[2].getRational();
2198  const Rational& c2 = g[3].getRational();
2199  Expr aExpr, x;
2200  d_theoryArith->separateMonomial(ax, aExpr, x);
2201 
2202  if(checkProofs) {
2204  "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
2205  CHECK_SOUND(aExpr.isRational(),
2206  "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
2207  }
2208 
2209  const Rational& a = aExpr.getRational();
2210  const Rational& c = e.getRational();
2211 
2212  if(checkProofs) {
2213  CHECK_SOUND(a.isInteger() && a >= 2,
2214  "ArithTheoremProducerOld::grayShadowConst("+g.toString()+")");
2215  }
2216 
2217  Rational newC1 = ceil((c1+c)/a), newC2 = floor((c2+c)/a);
2218  Expr newG((newC1 > newC2)? d_em->falseExpr()
2219  : grayShadow(x, rat(0), newC1, newC2));
2220  Proof pf;
2221  if(withProof())
2222  pf = newPf("gray_shadow_const", g, newG, gThm.getProof());
2223  return newTheorem(newG, gThm.getAssumptionsRef(), pf);
2224 }
2225 
2226 
2227 Rational ArithTheoremProducerOld::constRHSGrayShadow(const Rational& c,
2228  const Rational& b,
2229  const Rational& a) {
2230  DebugAssert(c.isInteger() &&
2231  b.isInteger() &&
2232  a.isInteger() &&
2233  b != 0,
2234  "ArithTheoremProducerOld::constRHSGrayShadow: a, b, c must be ints");
2235  if (b > 0)
2236  return mod(c+b, a);
2237  else
2238  return mod(a-(c+b), a);
2239 }
2240 
2241 /*! Takes a Theorem(\\alpha < \\beta) and returns
2242  * Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1)
2243  * where \\alpha and \\beta are integer expressions
2244  */
2245 Theorem ArithTheoremProducerOld::lessThanToLE(const Theorem& less,
2246  const Theorem& isIntLHS,
2247  const Theorem& isIntRHS,
2248  bool changeRight) {
2249  const Expr& ineq = less.getExpr();
2250  const Expr& isIntLHSexpr = isIntLHS.getExpr();
2251  const Expr& isIntRHSexpr = isIntRHS.getExpr();
2252 
2253  if(CHECK_PROOFS) {
2254  CHECK_SOUND(isLT(ineq),
2255  "ArithTheoremProducerOld::LTtoLE: ineq must be <");
2256  // Integrality check
2257  CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0],
2258  "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
2259  " ineq = "+ineq.toString()+"\n isIntLHS = "
2260  +isIntLHSexpr.toString());
2261  CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1],
2262  "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
2263  " ineq = "+ineq.toString()+"\n isIntRHS = "
2264  +isIntRHSexpr.toString());
2265  }
2266  vector<Theorem> thms;
2267  thms.push_back(less);
2268  thms.push_back(isIntLHS);
2269  thms.push_back(isIntRHS);
2270  Assumptions a(thms);
2271  Proof pf;
2272  Expr le = changeRight?
2273  leExpr(ineq[0], ineq[1] + rat(-1))
2274  : leExpr(ineq[0] + rat(1), ineq[1]);
2275  if(withProof()) {
2276  vector<Proof> pfs;
2277  pfs.push_back(less.getProof());
2278  pfs.push_back(isIntLHS.getProof());
2279  pfs.push_back(isIntRHS.getProof());
2280  pf = newPf(changeRight? "lessThan_To_LE_rhs" : "lessThan_To_LE_lhs",
2281  ineq,le, pfs);
2282  }
2283 
2284  return newRWTheorem(ineq, le, a, pf);
2285 }
2286 
2287 
2288 /*! \param eqn is an equation 0 = a.x or 0 = c + a.x
2289  * \param isIntx is a proof of IS_INTEGER(x)
2290  *
2291  * \return the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else
2292  * return the theorem 0 = c + a.x <==> false.
2293  *
2294  * It also handles the special case of 0 = a.x <==> x = 0
2295  */
2296 Theorem
2297 ArithTheoremProducerOld::intVarEqnConst(const Expr& eqn,
2298  const Theorem& isIntx) {
2299  const Expr& left(eqn[0]);
2300  const Expr& right(eqn[1]);
2301  const Expr& isIntxexpr(isIntx.getExpr());
2302 
2303  if(CHECK_PROOFS) {
2304  CHECK_SOUND((isMult(right) && right[0].isRational())
2305  || (right.arity() == 2 && isPlus(right)
2306  && right[0].isRational()
2307  && ((!isMult(right[1]) || right[1][0].isRational()))),
2308  "ArithTheoremProducerOld::intVarEqnConst: "
2309  "rhs has a wrong format: " + right.toString());
2310  CHECK_SOUND(left.isRational() && 0 == left.getRational(),
2311  "ArithTheoremProducerOld:intVarEqnConst:left is not a zero: " +
2312  left.toString());
2313  }
2314  // Integrality constraint
2315  Expr x(right);
2316  Rational a(1), c(0);
2317  if(isMult(right)) {
2318  Expr aExpr;
2319  d_theoryArith->separateMonomial(right, aExpr, x);
2320  a = aExpr.getRational();
2321  } else { // right is a PLUS
2322  c = right[0].getRational();
2323  Expr aExpr;
2324  d_theoryArith->separateMonomial(right[1], aExpr, x);
2325  a = aExpr.getRational();
2326  }
2327  if(CHECK_PROOFS) {
2328  CHECK_SOUND(isIntPred(isIntxexpr) && isIntxexpr[0] == x,
2329  "ArithTheoremProducerOld:intVarEqnConst: "
2330  "bad integrality constraint:\n right = " +
2331  right.toString()+"\n isIntx = "+isIntxexpr.toString());
2332  CHECK_SOUND(a!=0, "ArithTheoremProducerOld:intVarEqnConst: eqn = "
2333  +eqn.toString());
2334  }
2335  const Assumptions& assump(isIntx.getAssumptionsRef());
2336 
2337  /*
2338  Proof pf;
2339  if(withProof())
2340  pf = newPf("int_const_eq", eqn, isIntx.getProof());
2341 
2342  // Solve for x: x = r = -c/a
2343  Rational r(-c/a);
2344 
2345  if(r.isInteger()){
2346  return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf);
2347  else
2348  return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
2349  */
2350 
2351  Proof pf;
2352  // Solve for x: x = r = -c/a
2353  Rational r(-c/a);
2354 
2355  if(r.isInteger()){
2356  if(withProof())
2357  pf = newPf("int_const_eq", eqn, x.eqExpr(rat(r)),isIntx.getProof());
2358  return newRWTheorem(eqn, x.eqExpr(rat(r)), assump, pf);
2359  }
2360  else{
2361  if(withProof())
2362  pf = newPf("int_const_eq", eqn, d_em->falseExpr(),isIntx.getProof());
2363  return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
2364  }
2365 }
2366 
2367 
2368 Expr
2369 ArithTheoremProducerOld::create_t(const Expr& eqn) {
2370  const Expr& lhs = eqn[0];
2371  DebugAssert(isMult(lhs),
2372  CLASS_NAME "create_t : lhs must be a MULT"
2373  + lhs.toString());
2374  const Expr& x = lhs[1];
2375  Rational m = lhs[0].getRational()+1;
2376  DebugAssert(m > 0, "ArithTheoremProducerOld::create_t: m = "+m.toString());
2377  vector<Expr> kids;
2378  if(isPlus(eqn[1]))
2379  sumModM(kids, eqn[1], m, m);
2380  else
2381  kids.push_back(monomialModM(eqn[1], m, m));
2382 
2383  kids.push_back(multExpr(rat(1/m), x));
2384  return plusExpr(kids);
2385 }
2386 
2387 Expr
2388 ArithTheoremProducerOld::create_t2(const Expr& lhs, const Expr& rhs,
2389  const Expr& sigma) {
2390  Rational m = lhs[0].getRational()+1;
2391  DebugAssert(m > 0, "ArithTheoremProducerOld::create_t2: m = "+m.toString());
2392  vector<Expr> kids;
2393  if(isPlus(rhs))
2394  sumModM(kids, rhs, m, -1);
2395  else {
2396  kids.push_back(rat(0)); // For canonical form
2397  Expr monom = monomialModM(rhs, m, -1);
2398  if(!monom.isRational())
2399  kids.push_back(monom);
2400  else
2401  DebugAssert(monom.getRational() == 0, "");
2402  }
2403  kids.push_back(rat(m)*sigma);
2404  return plusExpr(kids);
2405 }
2406 
2407 Expr
2408 ArithTheoremProducerOld::create_t3(const Expr& lhs, const Expr& rhs,
2409  const Expr& sigma) {
2410  const Rational& a = lhs[0].getRational();
2411  Rational m = a+1;
2412  DebugAssert(m > 0, "ArithTheoremProducerOld::create_t3: m = "+m.toString());
2413  vector<Expr> kids;
2414  if(isPlus(rhs))
2415  sumMulF(kids, rhs, m, 1);
2416  else {
2417  kids.push_back(rat(0)); // For canonical form
2418  Expr monom = monomialMulF(rhs, m, 1);
2419  if(!monom.isRational())
2420  kids.push_back(monom);
2421  else
2422  DebugAssert(monom.getRational() == 0, "");
2423  }
2424  kids.push_back(rat(-a)*sigma);
2425  return plusExpr(kids);
2426 }
2427 
2428 Rational
2429 ArithTheoremProducerOld::modEq(const Rational& i, const Rational& m) {
2430  DebugAssert(m > 0, "ArithTheoremProducerOld::modEq: m = "+m.toString());
2431  Rational half(1,2);
2432  Rational res((i - m*(floor((i/m) + half))));
2433  TRACE("arith eq", "modEq("+i.toString()+", "+m.toString()+") = ", res, "");
2434  return res;
2435 }
2436 
2437 Rational
2438 ArithTheoremProducerOld::f(const Rational& i, const Rational& m) {
2439  DebugAssert(m > 0, "ArithTheoremProducerOld::f: m = "+m.toString());
2440  Rational half(1,2);
2441  return (floor(i/m + half)+modEq(i,m));
2442 }
2443 
2444 void
2445 ArithTheoremProducerOld::sumModM(vector<Expr>& summands, const Expr& sum,
2446  const Rational& m, const Rational& divisor) {
2447  DebugAssert(divisor != 0, "ArithTheoremProducerOld::sumModM: divisor = "
2448  +divisor.toString());
2449  Expr::iterator i = sum.begin();
2450  DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
2451  Rational C = i->getRational();
2452  C = modEq(C,m)/divisor;
2453  summands.push_back(rat(C));
2454  i++;
2455  for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
2456  Expr monom = monomialModM(*i, m, divisor);
2457  if(!monom.isRational())
2458  summands.push_back(monom);
2459  else
2460  DebugAssert(monom.getRational() == 0, "");
2461  }
2462 }
2463 
2464 Expr
2465 ArithTheoremProducerOld::monomialModM(const Expr& i,
2466  const Rational& m, const Rational& divisor)
2467 {
2468  DebugAssert(divisor != 0, "ArithTheoremProducerOld::monomialModM: divisor = "
2469  +divisor.toString());
2470  Expr res;
2471  if(isMult(i)) {
2472  Rational ai = i[0].getRational();
2473  ai = modEq(ai,m)/divisor;
2474  if(0 == ai) res = rat(0);
2475  else if(1 == ai && i.arity() == 2) res = i[1];
2476  else {
2477  vector<Expr> kids = i.getKids();
2478  kids[0] = rat(ai);
2479  res = multExpr(kids);
2480  }
2481  } else { // It's a single variable
2482  Rational ai = modEq(1,m)/divisor;
2483  if(1 == ai) res = i;
2484  else res = rat(ai)*i;
2485  }
2486  DebugAssert(!res.isNull(), "ArithTheoremProducerOld::monomialModM()");
2487  TRACE("arith eq", "monomialModM(i="+i.toString()+", m="+m.toString()
2488  +", div="+divisor.toString()+") = ", res, "");
2489  return res;
2490 }
2491 
2492 void
2493 ArithTheoremProducerOld::sumMulF(vector<Expr>& summands, const Expr& sum,
2494  const Rational& m, const Rational& divisor) {
2495  DebugAssert(divisor != 0, "ArithTheoremProducerOld::sumMulF: divisor = "
2496  +divisor.toString());
2497  Expr::iterator i = sum.begin();
2498  DebugAssert(i != sum.end(), CLASS_NAME "::sumModM");
2499  Rational C = i->getRational();
2500  C = f(C,m)/divisor;
2501  summands.push_back(rat(C));
2502  i++;
2503  for(Expr::iterator iend=sum.end(); i!=iend; ++i) {
2504  Expr monom = monomialMulF(*i, m, divisor);
2505  if(!monom.isRational())
2506  summands.push_back(monom);
2507  else
2508  DebugAssert(monom.getRational() == 0, "");
2509  }
2510 }
2511 
2512 Expr
2513 ArithTheoremProducerOld::monomialMulF(const Expr& i,
2514  const Rational& m, const Rational& divisor)
2515 {
2516  DebugAssert(divisor != 0, "ArithTheoremProducerOld::monomialMulF: divisor = "
2517  +divisor.toString());
2518  Rational ai = isMult(i) ? (i)[0].getRational() : 1;
2519  Expr xi = isMult(i) ? (i)[1] : (i);
2520  ai = f(ai,m)/divisor;
2521  if(0 == ai) return rat(0);
2522  if(1 == ai) return xi;
2523  return multExpr(rat(ai), xi);
2524 }
2525 
2526 // This recursive function accepts a term, t, and a 'map' of
2527 // substitutions [x1/t1, x2/t2,...,xn/tn]. it returns a t' which is
2528 // basically t[x1/t1,x2/t2...xn/tn]
2529 Expr
2530 ArithTheoremProducerOld::substitute(const Expr& term, ExprMap<Expr>& eMap)
2531 {
2532  ExprMap<Expr>::iterator i, iend = eMap.end();
2533 
2534  i = eMap.find(term);
2535  if(iend != i)
2536  return (*i).second;
2537 
2538  if (isMult(term)) {
2539  //in this case term is of the form c.x
2540  i = eMap.find(term[1]);
2541  if(iend != i)
2542  return term[0]*(*i).second;
2543  else
2544  return term;
2545  }
2546 
2547  if(isPlus(term)) {
2548  vector<Expr> output;
2549  for(Expr::iterator j = term.begin(), jend = term.end(); j != jend; ++j)
2550  output.push_back(substitute(*j, eMap));
2551  return plusExpr(output);
2552  }
2553  return term;
2554 }
2555 
2556 bool ArithTheoremProducerOld::greaterthan(const Expr & l, const Expr & r)
2557 {
2558  // DebugAssert(l != r, "");
2559  if (l==r) return false;
2560 
2561  switch(l.getKind()) {
2562  case RATIONAL_EXPR:
2563  DebugAssert(!r.isRational(), "");
2564  return true;
2565  break;
2566  case POW:
2567  switch (r.getKind()) {
2568  case RATIONAL_EXPR:
2569  // TODO:
2570  // alternately I could return (not greaterthan(r,l))
2571  return false;
2572  break;
2573  case POW:
2574  // x^n > y^n if x > y
2575  // x^n1 > x^n2 if n1 > n2
2576  return
2577  ((r[1] < l[1]) ||
2578  ((r[1]==l[1]) && (r[0].getRational() < l[0].getRational())));
2579  break;
2580 
2581  case MULT:
2582  DebugAssert(r.arity() > 1, "");
2583  DebugAssert((r.arity() > 2) || (r[1] != l), "");
2584  if (r[1] == l) return false;
2585  return greaterthan(l, r[1]);
2586  break;
2587  case PLUS:
2588  DebugAssert(false, "");
2589  return true;
2590  break;
2591  default:
2592  // leaf
2593  return ((r < l[1]) || ((r == l[1]) && l[0].getRational() > 1));
2594  break;
2595  }
2596  break;
2597  case MULT:
2598  DebugAssert(l.arity() > 1, "");
2599  switch (r.getKind()) {
2600  case RATIONAL_EXPR:
2601  return false;
2602  break;
2603  case POW:
2604  DebugAssert(l.arity() > 1, "");
2605  DebugAssert((l.arity() > 2) || (l[1] != r), "");
2606  // TODO:
2607  // alternately return (not greaterthan(r,l)
2608  return ((l[1] == r) || greaterthan(l[1], r));
2609  break;
2610  case MULT:
2611  {
2612 
2613  DebugAssert(r.arity() > 1, "");
2614  Expr::iterator i = l.begin();
2615  Expr::iterator j = r.begin();
2616  ++i;
2617  ++j;
2618  for (; i != l.end() && j != r.end(); ++i, ++j) {
2619  if (*i == *j)
2620  continue;
2621  return greaterthan(*i,*j);
2622  }
2623  DebugAssert(i != l.end() || j != r.end(), "");
2624  if (i == l.end()) {
2625  // r is bigger
2626  return false;
2627  }
2628  else
2629  {
2630  // l is bigger
2631  return true;
2632  }
2633  }
2634  break;
2635  case PLUS:
2636  DebugAssert(false, "");
2637  return true;
2638  break;
2639  default:
2640  // leaf
2641  DebugAssert((l.arity() > 2) || (l[1] != r), "");
2642  return ((l[1] == r) || greaterthan(l[1], r));
2643  break;
2644  }
2645  break;
2646  case PLUS:
2647  DebugAssert(false, "");
2648  return true;
2649  break;
2650  default:
2651  // leaf
2652  switch (r.getKind()) {
2653  case RATIONAL_EXPR:
2654  return false;
2655  break;
2656  case POW:
2657  return ((r[1] < l) || ((r[1] == l) && (r[0].getRational() < 1)));
2658  break;
2659  case MULT:
2660  DebugAssert(r.arity() > 1, "");
2661  DebugAssert((r.arity() > 2) || (r[1] != l), "");
2662  if (l == r[1]) return false;
2663  return greaterthan(l,r[1]);
2664  break;
2665  case PLUS:
2666  DebugAssert(false, "");
2667  return true;
2668  break;
2669  default:
2670  // leaf
2671  return (r < l);
2672  break;
2673  }
2674  break;
2675  }
2676 }
2677 
2678 
2679 /*! IS_INTEGER(x) |= EXISTS (y : INT) y = x
2680  * where x is not already known to be an integer.
2681  */
2682 Theorem ArithTheoremProducerOld::IsIntegerElim(const Theorem& isIntx)
2683 {
2684  Expr expr = isIntx.getExpr();
2685  if (CHECK_PROOFS) {
2686  CHECK_SOUND(expr.getKind() == IS_INTEGER,
2687  "Expected IS_INTEGER predicate");
2688  }
2689  expr = expr[0];
2690  DebugAssert(!d_theoryArith->isInteger(expr), "Expected non-integer");
2691 
2692  Assumptions a(isIntx);
2693  Proof pf;
2694 
2695  if (withProof())
2696  {
2697  pf = newPf("isIntElim", isIntx.getProof());
2698  }
2699 
2700  Expr newVar = d_em->newBoundVarExpr(d_theoryArith->intType());
2701  Expr res = d_em->newClosureExpr(EXISTS, newVar, newVar.eqExpr(expr));
2702 
2703  return newTheorem(res, a, pf);
2704 }
2705 
2706 
2707 Theorem
2708 ArithTheoremProducerOld::eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
2709  const vector<Theorem>& isIntVars) {
2710  TRACE("arith eq", "eqElimIntRule(", eqn.getExpr(), ") {");
2711  Proof pf;
2712 
2713  if(CHECK_PROOFS)
2714  CHECK_SOUND(eqn.isRewrite(),
2715  "ArithTheoremProducerOld::eqElimInt: input must be an equation" +
2716  eqn.toString());
2717 
2718  const Expr& lhs = eqn.getLHS();
2719  const Expr& rhs = eqn.getRHS();
2720  Expr a, x;
2721  d_theoryArith->separateMonomial(lhs, a, x);
2722 
2723  if(CHECK_PROOFS) {
2724  // Checking LHS
2725  const Expr& isIntxe = isIntx.getExpr();
2726  CHECK_SOUND(isIntPred(isIntxe) && isIntxe[0] == x,
2727  "ArithTheoremProducerOld::eqElimInt\n eqn = "
2728  +eqn.getExpr().toString()
2729  +"\n isIntx = "+isIntxe.toString());
2731  && a.getRational() >= 2,
2732  "ArithTheoremProducerOld::eqElimInt:\n lhs = "+lhs.toString());
2733  // Checking RHS
2734  // It cannot be a division (we don't handle it)
2735  CHECK_SOUND(!isDivide(rhs),
2736  "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.toString());
2737  // If it's a single monomial, then it's the only "variable"
2738  if(!isPlus(rhs)) {
2739  Expr c, v;
2740  d_theoryArith->separateMonomial(rhs, c, v);
2741  CHECK_SOUND(isIntVars.size() == 1
2742  && isIntPred(isIntVars[0].getExpr())
2743  && isIntVars[0].getExpr()[0] == v
2744  && isRational(c) && c.getRational().isInteger(),
2745  "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.toString()
2746  +"isIntVars.size = "+int2string(isIntVars.size()));
2747  } else { // RHS is a plus
2748  CHECK_SOUND(isIntVars.size() + 1 == (size_t)rhs.arity(),
2749  "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.toString());
2750  // Check the free constant
2751  CHECK_SOUND(isRational(rhs[0]) && rhs[0].getRational().isInteger(),
2752  "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.toString());
2753  // Check the vars
2754  for(size_t i=0, iend=isIntVars.size(); i<iend; ++i) {
2755  Expr c, v;
2756  d_theoryArith->separateMonomial(rhs[i+1], c, v);
2757  const Expr& isInt(isIntVars[i].getExpr());
2758  CHECK_SOUND(isIntPred(isInt) && isInt[0] == v
2759  && isRational(c) && c.getRational().isInteger(),
2760  "ArithTheoremProducerOld::eqElimInt:\n rhs["+int2string(i+1)
2761  +"] = "+rhs[i+1].toString()
2762  +"\n isInt = "+isInt.toString());
2763  }
2764  }
2765  }
2766 
2767  // Creating a fresh bound variable
2768  static int varCount(0);
2769  Expr newVar = d_em->newBoundVarExpr("_int_var", int2string(varCount++));
2770  newVar.setType(intType());
2771  Expr t2 = create_t2(lhs, rhs, newVar);
2772  Expr t3 = create_t3(lhs, rhs, newVar);
2773  vector<Expr> vars;
2774  vars.push_back(newVar);
2775  Expr res = d_em->newClosureExpr(EXISTS, vars,
2776  x.eqExpr(t2) && rat(0).eqExpr(t3));
2777 
2778  vector<Theorem> thms(isIntVars);
2779  thms.push_back(isIntx);
2780  thms.push_back(eqn);
2781  Assumptions assump(thms);
2782 
2783  if(withProof()) {
2784  vector<Proof> pfs;
2785  pfs.push_back(eqn.getProof());
2786  pfs.push_back(isIntx.getProof());
2787  vector<Theorem>::const_iterator i=isIntVars.begin(), iend=isIntVars.end();
2788  for(; i!=iend; ++i)
2789  pfs.push_back(i->getProof());
2790  pf = newPf("eq_elim_int", eqn.getExpr(), res, pfs);
2791  }
2792 
2793  Theorem thm(newTheorem(res, assump, pf));
2794  TRACE("arith eq", "eqElimIntRule => ", thm.getExpr(), " }");
2795  return thm;
2796 }
2797 
2798 
2799 Theorem
2800 ArithTheoremProducerOld::isIntConst(const Expr& e) {
2801  Proof pf;
2802 
2803  if(CHECK_PROOFS) {
2804  CHECK_SOUND(isIntPred(e) && e[0].isRational(),
2805  "ArithTheoremProducerOld::isIntConst(e = "
2806  +e.toString()+")");
2807  }
2808  if(withProof())
2809  pf = newPf("is_int_const", e);
2810  bool isInt = e[0].getRational().isInteger();
2811  return newRWTheorem(e, isInt? d_em->trueExpr() : d_em->falseExpr(), Assumptions::emptyAssump(), pf);
2812 }
2813 
2814 
2815 Theorem
2816 ArithTheoremProducerOld::equalLeaves1(const Theorem& thm)
2817 {
2818  Proof pf;
2819  const Expr& e = thm.getRHS();
2820 
2821  if (CHECK_PROOFS) {
2822  CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
2823  e[1].getRational() == Rational(0) &&
2824  e[0].getKind() == PLUS &&
2825  e[0].arity() == 3 &&
2826  e[0][0].getKind() == RATIONAL_EXPR &&
2827  e[0][0].getRational() == Rational(0) &&
2828  e[0][1].getKind() == MULT &&
2829  e[0][1].arity() == 2 &&
2830  e[0][1][0].getKind() == RATIONAL_EXPR &&
2831  e[0][1][0].getRational() == Rational(-1),
2832  "equalLeaves1");
2833  }
2834  if (withProof())
2835  {
2836  vector<Proof> pfs;
2837  pfs.push_back(thm.getProof());
2838  pf = newPf("equalLeaves1", e, pfs);
2839  }
2840  return newRWTheorem(e, e[0][1][1].eqExpr(e[0][2]), thm.getAssumptionsRef(), pf);
2841 }
2842 
2843 
2844 Theorem
2845 ArithTheoremProducerOld::equalLeaves2(const Theorem& thm)
2846 {
2847  Proof pf;
2848  const Expr& e = thm.getRHS();
2849 
2850  if (CHECK_PROOFS) {
2851  CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
2852  e[0].getRational() == Rational(0) &&
2853  e[1].getKind() == PLUS &&
2854  e[1].arity() == 3 &&
2855  e[1][0].getKind() == RATIONAL_EXPR &&
2856  e[1][0].getRational() == Rational(0) &&
2857  e[1][1].getKind() == MULT &&
2858  e[1][1].arity() == 2 &&
2859  e[1][1][0].getKind() == RATIONAL_EXPR &&
2860  e[1][1][0].getRational() == Rational(-1),
2861  "equalLeaves2");
2862  }
2863  if (withProof())
2864  {
2865  vector<Proof> pfs;
2866  pfs.push_back(thm.getProof());
2867  pf = newPf("equalLeaves2", e, pfs);
2868  }
2869  return newRWTheorem(e, e[1][1][1].eqExpr(e[1][2]), thm.getAssumptionsRef(), pf);
2870 }
2871 
2872 
2873 Theorem
2874 ArithTheoremProducerOld::equalLeaves3(const Theorem& thm)
2875 {
2876  Proof pf;
2877  const Expr& e = thm.getRHS();
2878 
2879  if (CHECK_PROOFS) {
2880  CHECK_SOUND(e[1].getKind() == RATIONAL_EXPR &&
2881  e[1].getRational() == Rational(0) &&
2882  e[0].getKind() == PLUS &&
2883  e[0].arity() == 3 &&
2884  e[0][0].getKind() == RATIONAL_EXPR &&
2885  e[0][0].getRational() == Rational(0) &&
2886  e[0][2].getKind() == MULT &&
2887  e[0][2].arity() == 2 &&
2888  e[0][2][0].getKind() == RATIONAL_EXPR &&
2889  e[0][2][0].getRational() == Rational(-1),
2890  "equalLeaves3");
2891  }
2892  if (withProof())
2893  {
2894  vector<Proof> pfs;
2895  pfs.push_back(thm.getProof());
2896  pf = newPf("equalLeaves3", e, pfs);
2897  }
2898  return newRWTheorem(e, e[0][2][1].eqExpr(e[0][1]), thm.getAssumptionsRef(), pf);
2899 }
2900 
2901 
2902 Theorem
2903 ArithTheoremProducerOld::equalLeaves4(const Theorem& thm)
2904 {
2905  Proof pf;
2906  const Expr& e = thm.getRHS();
2907 
2908  if (CHECK_PROOFS) {
2909  CHECK_SOUND(e[0].getKind() == RATIONAL_EXPR &&
2910  e[0].getRational() == Rational(0) &&
2911  e[1].getKind() == PLUS &&
2912  e[1].arity() == 3 &&
2913  e[1][0].getKind() == RATIONAL_EXPR &&
2914  e[1][0].getRational() == Rational(0) &&
2915  e[1][2].getKind() == MULT &&
2916  e[1][2].arity() == 2 &&
2917  e[1][2][0].getKind() == RATIONAL_EXPR &&
2918  e[1][2][0].getRational() == Rational(-1),
2919  "equalLeaves4");
2920  }
2921  if (withProof())
2922  {
2923  vector<Proof> pfs;
2924  pfs.push_back(thm.getProof());
2925  pf = newPf("equalLeaves4", e, pfs);
2926  }
2927  return newRWTheorem(e, e[1][2][1].eqExpr(e[1][1]), thm.getAssumptionsRef(), pf);
2928 }
2929 
2930 Theorem
2931 ArithTheoremProducerOld::diseqToIneq(const Theorem& diseq) {
2932  Proof pf;
2933 
2934  const Expr& e = diseq.getExpr();
2935 
2936  if(CHECK_PROOFS) {
2937  CHECK_SOUND(e.isNot() && e[0].isEq(),
2938  "ArithTheoremProducerOld::diseqToIneq: expected disequality:\n"
2939  " e = "+e.toString());
2940  }
2941 
2942  const Expr& x = e[0][0];
2943  const Expr& y = e[0][1];
2944 
2945  if(withProof())
2946  pf = newPf(e, diseq.getProof());
2947  return newTheorem(ltExpr(x,y).orExpr(gtExpr(x,y)), diseq.getAssumptionsRef(), pf);
2948 }
2949 
2950 Theorem ArithTheoremProducerOld::dummyTheorem(const Expr& e) {
2951  Proof pf;
2952  return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
2953 }
2954 
2955 Theorem ArithTheoremProducerOld::oneElimination(const Expr& e) {
2956 
2957  // Check soundness
2958  if (CHECK_PROOFS)
2959  CHECK_SOUND(isMult(e) &&
2960  e.arity() == 2 &&
2961  e[0].isRational() &&
2962  e[0].getRational() == 1,
2963  "oneElimination: input must be a multiplication by one" + e.toString());
2964 
2965  // The proof object that we will us
2966  Proof pf;
2967 
2968  // Setup the proof if needed
2969  if (withProof())
2970  pf = newPf("oneElimination", e);
2971 
2972  // Return the rewrite theorem that explains the phenomenon
2973  return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
2974 }
2975 
2976 Theorem ArithTheoremProducerOld::clashingBounds(const Theorem& lowerBound, const Theorem& upperBound) {
2977 
2978  // Get the expressions
2979  const Expr& lowerBoundExpr = lowerBound.getExpr();
2980  const Expr& upperBoundExpr = upperBound.getExpr();
2981 
2982  // Check soundness
2983  if (CHECK_PROOFS) {
2984  CHECK_SOUND(isLE(lowerBoundExpr) || isLT(lowerBoundExpr), "clashingBounds: lowerBound should be >= or > " + lowerBoundExpr.toString());
2985  CHECK_SOUND(isGE(upperBoundExpr) || isGT(upperBoundExpr), "clashingBounds: upperBound should be <= or < " + upperBoundExpr.toString());
2986  CHECK_SOUND(lowerBoundExpr[0].isRational(), "clashingBounds: lowerBound left side should be a rational " + lowerBoundExpr.toString());
2987  CHECK_SOUND(upperBoundExpr[0].isRational(), "clashingBounds: upperBound left side should be a rational " + upperBoundExpr.toString());
2988  CHECK_SOUND(lowerBoundExpr[1] == upperBoundExpr[1], "clashingBounds: bounds not on the same term " + lowerBoundExpr.toString() + ", " + upperBoundExpr.toString());
2989 
2990  // Get the bounds
2991  Rational lowerBoundR = lowerBoundExpr[0].getRational();
2992  Rational upperBoundR = upperBoundExpr[0].getRational();
2993 
2994  if (isLE(lowerBoundExpr) && isGE(upperBoundExpr)) {
2995  CHECK_SOUND(upperBoundR < lowerBoundR, "clashingBounds: bounds are satisfiable");
2996  } else {
2997  CHECK_SOUND(upperBoundR <= lowerBoundR, "clashingBounds: bounds are satisfiable");
2998  }
2999  }
3000 
3001  // The proof object that we will use
3002  Proof pf;
3003  // Setup the proof if needed
3004  if (withProof())
3005  pf = newPf("clashingBounds", lowerBoundExpr, upperBoundExpr);
3006 
3007  // Put the bounds expressions in the assumptions
3008  Assumptions assumptions;
3009  assumptions.add(lowerBound);
3010  assumptions.add(upperBound);
3011 
3012  // Return the theorem
3013  return newTheorem(d_em->falseExpr(), assumptions, pf);
3014 }
3015 
3016 Theorem ArithTheoremProducerOld::addInequalities(const Theorem& thm1, const Theorem& thm2) {
3017 
3018  // Get the expressions of the theorem
3019  const Expr& expr1 = thm1.getExpr();
3020  const Expr& expr2 = thm2.getExpr();
3021 
3022  // Check soundness
3023  if (CHECK_PROOFS) {
3024 
3025  CHECK_SOUND(isIneq(expr1), "addInequalities: expecting an inequality for thm1, got " + expr1.toString());
3026  CHECK_SOUND(isIneq(expr2), "addInequalities: expecting an inequality for thm2, got " + expr2.toString());
3027 
3028  if (isLE(expr1) || isLT(expr1))
3029  CHECK_SOUND(isLE(expr2) || isLT(expr2), "addInequalities: expr2 should be <(=) also " + expr2.toString());
3030  if (isGE(expr1) || isGT(expr1))
3031  CHECK_SOUND(isGE(expr2) || isGT(expr2), "addInequalities: expr2 should be >(=) also" + expr2.toString());
3032  }
3033 
3034  // Create the assumptions
3035  Assumptions a(thm1, thm2);
3036 
3037  // Get the kinds of the inequalitites
3038  int kind1 = expr1.getKind();
3039  int kind2 = expr2.getKind();
3040 
3041  // Set-up the resulting inequality
3042  int kind = (kind1 == kind2) ? kind1 : ((kind1 == LT) || (kind2 == LT))? LT : GT;
3043 
3044  // Create the proof object
3045  Proof pf;
3046  if(withProof()) {
3047  vector<Proof> pfs;
3048  pfs.push_back(thm1.getProof());
3049  pfs.push_back(thm2.getProof());
3050  pf = newPf("addInequalities", expr1, expr2, pfs);
3051  }
3052 
3053  // Create the new expressions
3054  Expr leftSide = plusExpr(expr1[0], expr2[0]);
3055  Expr rightSide = plusExpr(expr1[1], expr2[1]);
3056 
3057  // Return the theorem
3058  return newTheorem(Expr(kind, leftSide, rightSide), a, pf);
3059 }
3060 
3061 //
3062 // 0 <= c1 + t
3063 // ==> 0 <= c2 + t
3064 // if c2 > c1
3065 Theorem ArithTheoremProducerOld::implyWeakerInequality(const Expr& expr1, const Expr& expr2) {
3066 
3067  // Check soundness
3068  if (CHECK_PROOFS) {
3069 
3070  // Both must be inequalitites
3071  CHECK_SOUND(isIneq(expr1), "implyWeakerInequality: expr1 should be an inequality" + expr1.toString());
3072  CHECK_SOUND(isIneq(expr2), "implyWeakerInequality: expr1 should be an inequality" + expr2.toString());
3073 
3074  // Left sides must be zero
3075  CHECK_SOUND(expr1[0].isRational() && expr1[0].getRational() == 0, "implyWeakerInequality: expr1 should have a rational on the left side" + expr1.toString());
3076  CHECK_SOUND(expr2[0].isRational() && expr2[0].getRational() == 0, "implyWeakerInequality: expr2 should have a rational on the left side" + expr2.toString());
3077 
3078  // Get the expr1 monomials and constant 0 <= c1 + t1
3079  Rational c1 = 0;
3080  vector<Expr> t1_children;
3081  if (isPlus(expr1[1])) {
3082  int start_i = 0;
3083  if (expr1[1][0].isRational()) {
3084  start_i = 1;
3085  c1 = expr1[1][0].getRational();
3086  }
3087  int end_i = expr1[1].arity();
3088  for(int i = start_i; i < end_i; i ++) {
3089  const Expr& term = expr1[1][i];
3090  t1_children.push_back(term);
3091  }
3092  } else
3093  t1_children.push_back(expr1[1]);
3094  Expr t1 = (t1_children.size() > 1 ? plusExpr(t1_children) : t1_children[0]);
3095 
3096  // Get the expr1 monomials and constant 0 <= c1 + t1
3097  Rational c2 = 0;
3098  vector<Expr> t2_children;
3099  if (isPlus(expr2[1])) {
3100  int start_i = 0;
3101  if (expr2[1][0].isRational()) {
3102  start_i = 1;
3103  c2 = expr2[1][0].getRational();
3104  }
3105  int end_i = expr2[1].arity();
3106  for(int i = start_i; i < end_i; i ++) {
3107  const Expr& term = expr2[1][i];
3108  t2_children.push_back(term);
3109  }
3110  } else
3111  t2_children.push_back(expr2[1]);
3112  Expr t2 = (t2_children.size() > 1 ? plusExpr(t2_children) : t2_children[0]);
3113 
3114  CHECK_SOUND(t2 == t1, "implyWeakerInequality: terms different " + t1.toString() + " vs " + t2.toString());
3115  CHECK_SOUND(c2 > c1 || (c2 == c1 && !(expr1.getKind() == LE && expr2.getKind() == LT)), "implyWeakerInequality: c2 is not bigger than c1" + expr1.toString() + " --> " + expr2.toString());
3116  }
3117  // Create the proof object
3118  Proof pf;
3119  if(withProof()) pf = newPf("implyWeakerInequality", expr1, expr2);
3120 
3121  // Return the theorem
3122  return newTheorem(expr1.impExpr(expr2), Assumptions::emptyAssump(), pf);
3123 }
3124 
3125 // Takes
3126 // Expr1: 0 <= c1 + t1
3127 // Expr2: 0 <= c2 + t2 (t2 is -t1)
3128 // if c1 + c2 < 0 then Expr1 => !Expr2
3129 //
3130 
3131 Theorem ArithTheoremProducerOld::implyNegatedInequality(const Expr& expr1, const Expr& expr2) {
3132 
3133  // Check soundness
3134  // Check soundness
3135  if (CHECK_PROOFS) {
3136 
3137  // Both must be inequalitites
3138  CHECK_SOUND(isIneq(expr1), "implyNegatedInequality: expr1 should be an inequality" + expr1.toString());
3139  CHECK_SOUND(isIneq(expr2), "implyNegatedInequality: expr1 should be an inequality" + expr2.toString());
3140 
3141  // Left sides must be zero
3142  CHECK_SOUND(expr1[0].isRational() && expr1[0].getRational() == 0, "implyNegatedInequality: expr1 should have a rational on the left side" + expr1.toString());
3143  CHECK_SOUND(expr2[0].isRational() && expr2[0].getRational() == 0, "implyNegatedInequality: expr2 should have a rational on the left side" + expr2.toString());
3144 
3145  // Get the expr1 monomials and constant 0 <= c1 + t1
3146  Rational c1 = 0;
3147  vector<Expr> t1_children;
3148  if (isPlus(expr1[1])) {
3149  int start_i = 0;
3150  if (expr1[1][0].isRational()) {
3151  start_i = 1;
3152  c1 = expr1[1][0].getRational();
3153  }
3154  int end_i = expr1[1].arity();
3155  for(int i = start_i; i < end_i; i ++) {
3156  const Expr& term = expr1[1][i];
3157  t1_children.push_back(term);
3158  }
3159  } else
3160  t1_children.push_back(expr1[1]);
3161  Expr t1 = (t1_children.size() > 1 ? plusExpr(t1_children) : t1_children[0]);
3162 
3163  // Get the expr1 monomials and constant 0 <= c1 + t1
3164  Rational c2 = 0;
3165  vector<Expr> t2_children;
3166  if (isPlus(expr2[1])) {
3167  int start_i = 0;
3168  if (expr2[1][0].isRational()) {
3169  start_i = 1;
3170  c2 = expr2[1][0].getRational();
3171  }
3172  int end_i = expr2[1].arity();
3173  for(int i = start_i; i < end_i; i ++) {
3174  const Expr& term = expr2[1][i];
3175  t2_children.push_back(term);
3176  }
3177  } else
3178  t2_children.push_back(expr2[1]);
3179  Expr t2 = (t2_children.size() > 1 ? plusExpr(t2_children) : t2_children[0]);
3180 
3181  // t1 shoud be -t2
3182  if (isPlus(t1) && isPlus(t2)) {
3183  CHECK_SOUND(t1.arity() == t2.arity(), "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString());
3184  for (int i = 0; i < t1.arity(); i++) {
3185  Expr term_t1 = t1[i];
3186  Expr term_t2 = t2[i];
3187  Rational t1_c = (isMult(term_t1) ? term_t1[0].getRational() : 1);
3188  term_t1 = (isMult(term_t1) ? term_t1[1] : term_t1);
3189  Rational t2_c = (isMult(term_t2) ? term_t2[0].getRational() : 1);
3190  term_t2 = (isMult(term_t2) ? term_t2[1] : term_t2);
3191  CHECK_SOUND(t1_c == - t2_c, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString());
3192  CHECK_SOUND(term_t1 == term_t2, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString());
3193  }
3194  } else {
3195  Rational t1_c = (isMult(t1) ? t1[0].getRational() : 1);
3196  Expr term_t1 = (isMult(t1) ? t1[1] : t1);
3197  Rational t2_c = (isMult(t2) ? t2[0].getRational() : 1);
3198  Expr term_t2 = (isMult(t2) ? t2[1] : t2);
3199  CHECK_SOUND(t1_c == - t2_c, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString());
3200  CHECK_SOUND(term_t1 == term_t2, "implyNegatedInequality: t1 should be -t2 : " + t1.toString() + " vs " + t2.toString());
3201  }
3202 
3203  int kind1 = expr1.getKind();
3204  int kind2 = expr2.getKind();
3205  bool bothStrict = kind1 == LT && kind2 == LT;
3206  CHECK_SOUND(c1 + c2 < 0 || (c1 + c2 == 0 && bothStrict), "implyNegatedInequality: sum of constants not negative!");
3207  }
3208 
3209  // The proof object that we will use
3210  Proof pf;
3211  if (withProof()) pf = newPf("implyNegatedInequality", expr1, expr2, expr2.negate());
3212 
3213  // Return the theorem
3214  return newTheorem(expr1.impExpr(expr2.negate()), Assumptions::emptyAssump(), pf);
3215 }
3216 
3217 Theorem ArithTheoremProducerOld::trustedRewrite(const Expr& expr1, const Expr& expr2) {
3218 
3219  // The proof object that we will us
3220  Proof pf;
3221 
3222  // Setup the proof if needed
3223  if (withProof()) pf = newPf("trustedRewrite", expr1, expr2);
3224 
3225  // Return the rewrite theorem that explains the phenomenon
3226  return newRWTheorem(expr1, expr2, Assumptions::emptyAssump(), pf);
3227 
3228 }
3229 
3230 Theorem ArithTheoremProducerOld::integerSplit(const Expr& intVar, const Rational& intPoint) {
3231 
3232  // Check soundness
3233  if (CHECK_PROOFS) {
3234  CHECK_SOUND(intPoint.isInteger(), "integerSplit: we can only split on integer points, given" + intPoint.toString());
3235  }
3236 
3237  // Create the expression
3238  const Expr& split = Expr(IS_INTEGER, intVar).impExpr(leExpr(intVar, rat(intPoint)).orExpr(geExpr(intVar, rat(intPoint + 1))));
3239 
3240  // The proof object that we will use
3241  Proof pf;
3242  if (withProof()) pf = newPf("integerSplit", intVar, rat(intPoint));
3243 
3244  // Return the theorem
3245  return newTheorem(split, Assumptions::emptyAssump(), pf);
3246 }
3247 
3248 //
3249 // Changed from the new arithmetic, takes
3250 // 0 op c + t, where t is an integer expression but c is a rational
3251 // or 0 op x, where x is a leaf
3252 //
3253 Theorem ArithTheoremProducerOld::rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr) {
3254 
3255  // Check soundness
3256  if (CHECK_PROOFS) {
3257  // Right side of the constraint should correspond to the proved integer expression
3258  CHECK_SOUND(isIneq(constr), "rafineStrictInteger: expected a constraint got : " + constr.toString());
3259  CHECK_SOUND(constr[0].isRational() && constr[0].getRational() == 0, "rafineStrictInteger: left hand side must be 0");
3260  CHECK_SOUND(d_theoryArith->isLeaf(constr[1]) || constr[1][0].isRational(), "rafineStrictInteger: right side of the constraint must be a leaf or a sum, with the first one a rational");
3261 
3262  // We have to check that the non-constant children of inequality correspond to the integrality theorem's children
3263  Expr intSum = isIntConstrThm.getExpr()[0];
3264  Expr ineqSum = constr[1];
3265  if (isPlus(intSum)) {
3266  int i, j;
3267  for (i = 0, j = 1; i < intSum.arity() && j < ineqSum.arity(); i ++, j ++)
3268  if (!(intSum[i] == ineqSum[j])) break;
3269  CHECK_SOUND(i == intSum.arity() && j == ineqSum.arity(), "rafineStrictInteger: proof of intger doesn't correspond to the constarint right side");
3270  } else
3271  CHECK_SOUND(intSum == ineqSum || intSum == ineqSum[1], "rafineStrictInteger: proof of intger doesn't correspond to the constarint right side:" + intSum.getString() + " vs " + ineqSum[1].getString());
3272  }
3273 
3274  // Get the contraint bound
3275  Rational c = (isPlus(constr[1]) ? constr[1][0].getRational() : 0);
3276 
3277  // Get the kind of the constraint
3278  int kind = constr.getKind();
3279 
3280  // If the bound is strict, make it non-strict
3281  switch (kind) {
3282  case LT:
3283  kind = LE;
3284  if (c.isInteger()) c --; // 0 < 3 + x --> 0 <= 2 + x
3285  else c = floor(c); // 0 < 3.4 + x --> 0 <= 3 + x
3286  break;
3287  case LE:
3288  kind = LE;
3289  if (!c.isInteger()) c = floor(c); // 0 <= 3.5 + x --> 0 <= 3 + x
3290  break;
3291  case GT:
3292  kind = GE;
3293  if (c.isInteger()) c ++; // 0 > 3 + x --> 0 >= 4 + x
3294  else c = ceil(c); // 0 > 3.4 + x --> 0 >= 4 + x
3295  break;
3296  case GE:
3297  kind = GE;
3298  if (!c.isInteger()) c = ceil(c); // 0 >= 3.4 + x --> 4 >= x
3299  break;
3300  }
3301 
3302  // The new constraint
3303  vector<Expr> newChildren;
3304  if (isPlus(constr[1])) {
3305  for (int i = 0; i < constr[1].arity(); i ++)
3306  if (constr[1][i].isRational()) newChildren.push_back(rat(c));
3307  else newChildren.push_back(constr[1][i]);
3308  } else {
3309  if (c != 0) newChildren.push_back(rat(c));
3310  newChildren.push_back(constr[1]);
3311  }
3312  Expr newSum = newChildren.size() > 1 ? plusExpr(newChildren) : newChildren[0];
3313  Expr newConstr(kind, rat(0), newSum);
3314 
3315  // Pick up the assumptions from the integer proof
3316  const Assumptions& assump(isIntConstrThm.getAssumptionsRef());
3317 
3318  // Construct the proof object if necessary
3319  Proof pf;
3320  if (withProof())
3321  pf = newPf("rafineStrictInteger", constr,newConstr, isIntConstrThm.getProof());
3322 
3323  // Return the rewrite theorem that explains the phenomenon
3324  return newRWTheorem(constr, newConstr, assump, pf);
3325 }
3326 
3327 
3328 // Given:
3329 // 0 = c + t
3330 // where t is integer and c is not
3331 // deduce bot
3332 Theorem ArithTheoremProducerOld::intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr) {
3333 
3334  // Check soundness
3335  if (CHECK_PROOFS) {
3336  // Right side of the constraint should correspond to the proved integer expression
3337  CHECK_SOUND(constr.getKind() == EQ, "intEqualityRationalConstant: expected a constraint got : " + constr.toString());
3338  bool sum_on_rhs = (constr[0].isRational() && constr[0].getRational() == 0);
3339  bool sum_on_lhs = (constr[1].isRational() && constr[1].getRational() == 0);
3340  CHECK_SOUND((sum_on_rhs && !sum_on_lhs) ||(!sum_on_rhs && sum_on_lhs),
3341  "intEqualityRationalConstant: left or right hand side must be 0");
3342  CHECK_SOUND((sum_on_rhs && constr[1][0].isRational() && !constr[1][0].getRational().isInteger()) ||
3343  (sum_on_lhs && constr[0][0].isRational() && !constr[0][0].getRational().isInteger()),
3344  "intEqualityRationalConstant: left or right side of the constraint must be a sum, with the first one a rational (non integer)");
3345 
3346  // We have to check that the non-constant children of inequality correspond to the integrality theorem's children
3347  Expr intSum = isIntConstrThm.getExpr()[0];
3348  Expr eqSum = (sum_on_lhs ? constr[0] : constr[1]);
3349  if (isPlus(intSum)) {
3350  int i, j;
3351  for (i = 0, j = 1; i < intSum.arity() && j < eqSum.arity(); i ++, j ++)
3352  if (!(intSum[i] == eqSum[j])) break;
3353  CHECK_SOUND(i == intSum.arity() && j == eqSum.arity(), "intEqualityRationalConstant: proof of intger doesn't correspond to the constarint right side");
3354  } else
3355  CHECK_SOUND(intSum == eqSum[1], "intEqualityRationalConstant: proof of intger doesn't correspond to the constarint right side:" + intSum.getString() + " vs " + eqSum[1].getString());
3356  }
3357 
3358  const Assumptions& assump(isIntConstrThm.getAssumptionsRef());
3359 
3360  // Construct the proof object if necessary
3361  Proof pf;
3362  if (withProof())
3363  pf = newPf("intEqualityRationalConstant", constr, isIntConstrThm.getProof());
3364 
3365  // Return the rewrite theorem that explains the phenomenon
3366  return newRWTheorem(constr, d_em->falseExpr(), assump, pf);
3367 }
3368 
3369 Theorem ArithTheoremProducerOld::cycleConflict(const vector<Theorem>& inequalitites) {
3370  Proof pf;
3371  if(withProof()) {
3372  vector<Expr> es;
3373  vector<Proof> pfs;
3374  for(unsigned i = 0; i < inequalitites.size(); i++) {
3375  es.push_back(inequalitites[i].getExpr());
3376  pfs.push_back(inequalitites[i].getProof());
3377  }
3378  pf = newPf("cycleConflict", es, pfs);
3379  }
3380 
3381  Assumptions a;
3382  for(unsigned i = 0; i < inequalitites.size(); i ++)
3383  a.add(inequalitites[i]);
3384 
3385  return newTheorem(d_em->falseExpr(), a, pf);
3386 }
3387 
3388 Theorem ArithTheoremProducerOld::implyEqualities(const std::vector<Theorem>& inequalities) {
3389  Assumptions a;
3390  vector<Expr> conjuncts;
3391  for(unsigned i = 0; i < inequalities.size(); i ++) {
3392  a.add(inequalities[i]);
3393  Expr inequality = inequalities[i].getExpr();
3394  Expr equality = inequality[0].eqExpr(inequality[1]);
3395  conjuncts.push_back(equality);
3396  }
3397 
3398  Proof pf;
3399  if(withProof()) {
3400  vector<Expr> es;
3401  vector<Proof> pfs;
3402  for(unsigned i = 0; i < inequalities.size(); i++) {
3403  es.push_back(inequalities[i].getExpr());
3404  pfs.push_back(inequalities[i].getProof());
3405  }
3406  pf = newPf("implyEqualities", Expr(RAW_LIST,conjuncts),Expr(RAW_LIST,es), pfs);
3407  }
3408 
3409  return newTheorem(andExpr(conjuncts), a, pf);
3410 }
3411 
3412 /*! Takes a Theorem(\\alpha < \\beta) and returns
3413  * Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1)
3414  * where \\alpha and \\beta are integer expressions
3415  */
3416 Theorem ArithTheoremProducerOld::lessThanToLERewrite(const Expr& ineq,
3417  const Theorem& isIntLHS,
3418  const Theorem& isIntRHS,
3419  bool changeRight) {
3420 
3421  const Expr& isIntLHSexpr = isIntLHS.getExpr();
3422  const Expr& isIntRHSexpr = isIntRHS.getExpr();
3423 
3424  if(CHECK_PROOFS) {
3425  CHECK_SOUND(isLT(ineq), "ArithTheoremProducerOld::LTtoLE: ineq must be <");
3426  // Integrality check
3427  CHECK_SOUND(isIntPred(isIntLHSexpr) && isIntLHSexpr[0] == ineq[0],
3428  "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
3429  " ineq = "+ineq.toString()+"\n isIntLHS = "
3430  +isIntLHSexpr.toString());
3431  CHECK_SOUND(isIntPred(isIntRHSexpr) && isIntRHSexpr[0] == ineq[1],
3432  "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
3433  " ineq = "+ineq.toString()+"\n isIntRHS = "
3434  +isIntRHSexpr.toString());
3435  }
3436 
3437  vector<Theorem> thms;
3438  thms.push_back(isIntLHS);
3439  thms.push_back(isIntRHS);
3440  Assumptions a(thms);
3441  Proof pf;
3442  Expr le = changeRight? leExpr(ineq[0], ineq[1] + rat(-1)) : leExpr(ineq[0] + rat(1), ineq[1]);
3443  if(withProof()) {
3444  vector<Proof> pfs;
3445  pfs.push_back(isIntLHS.getProof());
3446  pfs.push_back(isIntRHS.getProof());
3447  pf = newPf(changeRight? "lessThan_To_LE_rhs_rwr" : "lessThan_To_LE_lhs_rwr", ineq, le, pfs);
3448  }
3449 
3450  return newRWTheorem(ineq, le, a, pf);
3451 }
3452 
3453 // G ==> (G1 or G2) and (!G1 or !G2),
3454 // where G = G(x, e, c1, c2),
3455 // V x = e + i, for i in c1 .. c2
3456 Theorem ArithTheoremProducerOld::splitGrayShadowSmall(const Theorem& gThm) {
3457  const Expr& theShadow = gThm.getExpr();
3458  if(CHECK_PROOFS) {
3459  CHECK_SOUND(isGrayShadow(theShadow),
3460  "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
3461  theShadow.toString());
3462  }
3463 
3464  const Rational& c1 = theShadow[2].getRational();
3465  const Rational& c2 = theShadow[3].getRational();
3466 
3467  if(CHECK_PROOFS) {
3468  CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
3469  "ArithTheoremProducerOld::expandGrayShadow: " +
3470  theShadow.toString());
3471  }
3472 
3473  const Expr& v = theShadow[0];
3474  const Expr& e = theShadow[1];
3475 
3476  vector<Expr> disjuncts;
3477  for (int i = c1.getInt(); i <= c2.getInt(); i ++) {
3478  Expr disjunct = v.eqExpr(e + rat(i));
3479  disjuncts.push_back(disjunct);
3480  }
3481  Expr bigOr = orExpr(disjuncts);
3482 
3483  Proof pf;
3484  if(withProof()){
3485  vector<Expr> exprs;
3486  exprs.push_back(theShadow);
3487  exprs.push_back(bigOr);
3488  pf = newPf("split_gray_shadow", exprs, gThm.getProof());
3489  }
3490 
3491  return newTheorem(bigOr, gThm.getAssumptionsRef(), pf);
3492 }
3493 
3494 Theorem ArithTheoremProducerOld::implyWeakerInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) {
3495  Proof pf;
3496 
3497  if(withProof()) {
3498  vector<Expr> es;
3499  vector<Proof> pfs;
3500  for(unsigned i = 0; i < antecedentThms.size(); i++) {
3501  es.push_back(antecedentThms[i].getExpr());
3502  pfs.push_back(antecedentThms[i].getProof());
3503  }
3504  pf = newPf("implyWeakerInequalityDiffLogic", implied, Expr(RAW_LIST,es), pfs);
3505  }
3506 
3507  Assumptions a;
3508  for(unsigned i = 0; i < antecedentThms.size(); i ++) {
3509  a.add(antecedentThms[i]);
3510  }
3511 
3512  return newTheorem(implied, a, pf);
3513 
3514 }
3515 
3516 Theorem ArithTheoremProducerOld::implyNegatedInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) {
3517  Proof pf;
3518 
3519  if(withProof()) {
3520  vector<Expr> es;
3521  vector<Proof> pfs;
3522  for(unsigned i = 0; i < antecedentThms.size(); i++) {
3523  es.push_back(antecedentThms[i].getExpr());
3524  pfs.push_back(antecedentThms[i].getProof());
3525  }
3526  pf = newPf("implyNegatedInequalityDiffLogic",implied.notExpr(), Expr(RAW_LIST, es), pfs);
3527  }
3528 
3529  Assumptions a;
3530  for(unsigned i = 0; i < antecedentThms.size(); i ++) {
3531  a.add(antecedentThms[i]);
3532  }
3533 
3534  return newTheorem(implied.notExpr(), a, pf);
3535 
3536 }
3537 
3538 
3539 Theorem ArithTheoremProducerOld::expandGrayShadowRewrite(const Expr& theShadow) {
3540 
3541  if(CHECK_PROOFS) {
3542  CHECK_SOUND(isGrayShadow(theShadow),
3543  "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
3544  theShadow.toString());
3545  }
3546 
3547  const Rational& c1 = theShadow[2].getRational();
3548  const Rational& c2 = theShadow[3].getRational();
3549 
3550  if(CHECK_PROOFS) {
3551  CHECK_SOUND(c1.isInteger() && c2.isInteger() && c1 < c2,
3552  "ArithTheoremProducerOld::expandGrayShadow: " +
3553  theShadow.toString());
3554  }
3555 
3556  const Expr& v = theShadow[0];
3557  const Expr& e = theShadow[1];
3558 
3559  Proof pf;
3560  if(withProof())
3561  pf = newPf("expand_gray_shadow", theShadow);
3562  Expr ineq1(leExpr(e+rat(c1), v));
3563  Expr ineq2(leExpr(v, e+rat(c2)));
3564  return newRWTheorem(theShadow, ineq1 && ineq2, Assumptions::emptyAssump(), pf);
3565 }
3566 
3567 Theorem ArithTheoremProducerOld::compactNonLinearTerm(const Expr& nonLinear) {
3568 
3569  // The set of common leaves
3570  multiset<Expr> commonLeaves;
3571  bool first = true;
3572 
3573  // Go through the terms and intersect the leaf sets
3574  for (int i = 0; i < nonLinear.arity(); i ++) {
3575  if (!nonLinear[i].isRational()) {
3576  // Get the current monomial
3577  Expr monomial = nonLinear[i];
3578 
3579  // A set to keep the variables
3580  multiset<Expr> currentLeaves;
3581 
3582  // Get the set of leaves in this term
3583  if (isMult(monomial)) {
3584  for (int j = 0; j < monomial.arity(); j ++)
3585  if (!monomial[j].isRational()) {
3586  if (isPow(monomial[j])) {
3587  for (int p = 0; p < monomial[j][0].getRational().getInt(); p ++)
3588  currentLeaves.insert(monomial[j][1]);
3589  } else
3590  currentLeaves.insert(monomial[j]);
3591  }
3592  } else if (isPow(monomial)) {
3593  for (int p = 0; p < monomial[0].getRational().getInt(); p ++)
3594  currentLeaves.insert(monomial[1]);
3595  } else
3596  currentLeaves.insert(monomial);
3597 
3598  // And intersect them
3599  if (first) {
3600  commonLeaves.swap(currentLeaves);
3601  first = false;
3602  } else {
3603  multiset<Expr> intersectLeaves;
3604  set_intersection(currentLeaves.begin(), currentLeaves.end(),
3605  commonLeaves.begin(), commonLeaves.end(),
3606  insert_iterator< multiset<Expr> >
3607  (intersectLeaves, intersectLeaves.begin()));
3608  intersectLeaves.swap(commonLeaves);
3609  }
3610  }
3611  }
3612 
3613  Expr result;
3614  if (commonLeaves.size() > 0) {
3615 
3616  // The constant to add in the beginnings
3617  Expr constant = rat(0);
3618 
3619  // The sum of of the rest when we pullout the common factors
3620  vector<Expr> sumChildren;
3621 
3622  // Go through them again and construct the sum of the rest
3623  for (int i = 0; i < nonLinear.arity(); i ++) {
3624  if (!nonLinear[i].isRational()) {
3625  // Get the current monomial
3626  Expr monomial = nonLinear[i];
3627 
3628  // A set to keep the variables
3629  multiset<Expr> currentChildren;
3630 
3631  // Get the set of childrent of this multiplication
3632  if (isMult(monomial)) {
3633  for (int j = 0; j < monomial.arity(); j ++)
3634  if (isPow(monomial[j])) {
3635  for (int p = 0; p < monomial[j][0].getRational().getInt(); p ++)
3636  currentChildren.insert(monomial[j][1]);
3637  } else
3638  currentChildren.insert(monomial[j]);
3639  } else if (isPow(monomial)) {
3640  for (int p = 0; p < monomial[0].getRational().getInt(); p ++)
3641  currentChildren.insert(monomial[1]);
3642  } else
3643  currentChildren.insert(monomial);
3644 
3645  // Take the difference and construct a multiplication
3646  multiset<Expr> diffChildren;
3647  set_difference(currentChildren.begin(), currentChildren.end(),
3648  commonLeaves.begin(), commonLeaves.end(),
3649  insert_iterator< multiset<Expr> >
3650  (diffChildren, diffChildren.begin()));
3651 
3652  // Go create another sumChildren element
3653  if (diffChildren.size() == 1) {
3654  sumChildren.push_back(*diffChildren.begin());
3655  } else if (diffChildren.size() == 0) {
3656  sumChildren.push_back(rat(1));
3657  } else {
3658  multiset<Expr>::iterator it = diffChildren.begin();
3659  multiset<Expr>::iterator it_end = diffChildren.end();
3660  vector<Expr> multChildren;
3661  while (it != it_end) {
3662  multChildren.push_back(*it);
3663  it ++;
3664  }
3665  sumChildren.push_back(multExpr(multChildren));
3666  }
3667  } else
3668  constant = nonLinear[i];
3669  }
3670 
3671  // The children of the final multiplication
3672  vector<Expr> multChildren;
3673  multChildren.push_back(plusExpr(sumChildren));
3674  multiset<Expr>::iterator it = commonLeaves.begin();
3675  multiset<Expr>::iterator it_end = commonLeaves.end();
3676  for (; it != it_end; it ++)
3677  multChildren.push_back(*it);
3678  result = plusExpr(constant, multExpr(multChildren));
3679  } else {
3680  // We have no common leaves to take out
3681  result = nonLinear;
3682  }
3683 
3684  Proof pf;
3685  if(withProof())
3686  pf = newPf("compactNonlinear", nonLinear, result);
3687 
3688  return newRWTheorem(nonLinear, result, Assumptions::emptyAssump(), pf);
3689 }
3690 
3691 //
3692 // -c <= x1*x2*...*xn
3693 // if c = 0 then "only even number of x_i's can be negative" or one of them is zero
3694 // x1 = 0 or x2 = 0 or ... or xn = 0
3695 // or (x1
3696 // else "only only even number of x_i's can be negative" and none of them is zero"
3697 Theorem ArithTheoremProducerOld::nonLinearIneqSignSplit(const Theorem& ineqThm) {
3698 
3699  // Get the inequality
3700  Expr ineq = ineqThm.getExpr();
3701  Expr rhs = ineq[1];
3702 
3703  // Get the constant
3704  Rational c = (isMult(rhs) ? 0 : rhs[0].getRational());
3705  if(CHECK_PROOFS) {
3706  CHECK_SOUND(c <= 0, "ArithTheoremProducerOld::nonLinearIneqSignSplit: " + ineq.toString());
3707  CHECK_SOUND(isMult(rhs) || (isPlus(rhs) && rhs.arity() == 2), "ArithTheoremProducerOld::nonLinearIneqSignSplit: " + ineq.toString());
3708  }
3709 
3710  Expr signXor = d_em->trueExpr();
3711  Expr mult = (isMult(rhs) ? rhs : rhs[1]);
3712  for (int i = 0; i < mult.arity(); i ++) {
3713  Expr term = mult[i];
3714  if (isPow(term) && term[0].getRational() < 0)
3715  term = Expr(POW, -term[0], term[1]);
3716  signXor = Expr(XOR, signXor, ltExpr(term, rat(0)));
3717  }
3718 
3719  if (c == 0 && ineq.getKind() == LE) {
3720  Expr zeroOr = d_em->falseExpr();
3721  for (int i = 0; i < mult.arity(); i ++) {
3722  Expr term = mult[i];
3723  zeroOr = zeroOr.orExpr(term.eqExpr(rat(0)));
3724  }
3725  signXor = zeroOr.orExpr(signXor);
3726  }
3727 
3728  Proof pf;
3729  if(withProof()) {
3730  vector<Expr> exprs;
3731  exprs.push_back(ineq);
3732  exprs.push_back(signXor);
3733  pf = newPf("nonLinearIneqSignSplit", exprs, ineqThm.getProof());
3734  }
3735 
3736  Assumptions assumptions;
3737  assumptions.add(ineqThm);
3738 
3739  return newTheorem(signXor, assumptions, pf);
3740 }
3741 
3742 Theorem ArithTheoremProducerOld::implyDiffLogicBothBounds(const Expr& x,
3743  std::vector<Theorem>& c1_le_x, Rational c1,
3744  std::vector<Theorem>& x_le_c2, Rational c2)
3745 {
3746  Proof pf;
3747 
3748  if(withProof()) {
3749  vector<Expr> es;
3750  vector<Proof> pfs;
3751  for(unsigned i = 0; i < c1_le_x.size(); i++) {
3752  es.push_back(c1_le_x[i].getExpr());
3753  pfs.push_back(c1_le_x[i].getProof());
3754  }
3755  for(unsigned i = 0; i < x_le_c2.size(); i++) {
3756  es.push_back(x_le_c2[i].getExpr());
3757  pfs.push_back(x_le_c2[i].getProof());
3758  }
3759  pf = newPf("implyDiffLogicBothBounds", es, pfs);
3760  }
3761 
3762  Assumptions a;
3763  for(unsigned i = 0; i < x_le_c2.size(); i ++) {
3764  a.add(c1_le_x[i]);
3765  }
3766  for(unsigned i = 0; i < x_le_c2.size(); i ++) {
3767  a.add(c1_le_x[i]);
3768  }
3769 
3770  Expr implied = grayShadow(x, rat(0), c1, c2);
3771 
3772  return newTheorem(implied, a, pf);
3773 }
3774 
3775 Theorem ArithTheoremProducerOld::addInequalities(const vector<Theorem>& thms) {
3776 
3777  // Check soundness
3778  if (CHECK_PROOFS) {
3779  for (unsigned i = 0; i < thms.size(); i ++) {
3780  Expr expr = thms[i].getExpr();
3781  CHECK_SOUND(isIneq(expr), "addInequalities: expecting an inequality for, got " + expr.toString());
3782  CHECK_SOUND(isLE(expr) || isLT(expr), "addInequalities: expr should be <(=) " + expr.toString());
3783  }
3784  }
3785 
3786  // Create the assumptions
3787  Assumptions a;
3788  for (unsigned i = 0; i < thms.size(); i ++)
3789  a.add(thms[i]);
3790 
3791  // Get the kinds of the inequalitites
3792  int kind = LE;
3793  for (unsigned i = 0; i < thms.size(); i ++)
3794  if (thms[i].getExpr().getKind() == LT) kind = LT;
3795 
3796  // Create the proof object
3797  Proof pf;
3798  if(withProof()) {
3799  vector<Proof> pfs;
3800  vector<Expr> exps;
3801  for (unsigned i = 0; i < thms.size(); i ++) {
3802  pfs.push_back(thms[i].getProof());
3803  exps.push_back(thms[i].getExpr());
3804  }
3805  pf = newPf("addInequalities", exps, pfs);
3806  }
3807 
3808  // Create the new expressions
3809  vector<Expr> summandsLeft;
3810  vector<Expr> summandsRight;
3811  for (unsigned i = 0; i < thms.size(); i ++) {
3812  summandsLeft.push_back(thms[i].getExpr()[0]);
3813  summandsRight.push_back(thms[i].getExpr()[1]);
3814  }
3815  Expr leftSide = plusExpr(summandsLeft);
3816  Expr rightSide = plusExpr(summandsRight);
3817 
3818  // Return the theorem
3819  return newTheorem(Expr(kind, leftSide, rightSide), a, pf);
3820 }
3821 
3822 // x^1 <-> x
3823 Theorem ArithTheoremProducerOld::powerOfOne(const Expr& e) {
3824 
3825  if(CHECK_PROOFS) {
3826  CHECK_SOUND(isPow(e), "ArithTheoremProducerOld::powerOfOne: not a power expression" + e.toString());
3827  CHECK_SOUND(e[0].isRational() && e[0].getRational() == 1, "ArithTheoremProducerOld::powerOfOne: not a power of 1" + e.toString());
3828  }
3829 
3830  Proof pf;
3831  if(withProof())
3832  pf = newPf("power_of_one", e);
3833 
3834  return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
3835 }
3836 
3837 
3838 void ArithTheoremProducerOld::getLeaves(const Expr& e, set<Rational>& s, ExprHashMap<bool>& cache)
3839 {
3840  if (e.isRational()) {
3841  s.insert(e.getRational());
3842  return;
3843  }
3844 
3845  if (e.isAtomic() && d_theoryArith->isLeaf(e)) {
3846  return;
3847  }
3848 
3849  ExprHashMap<bool>::iterator it = cache.find(e);
3850  if (it != cache.end()) return;
3851 
3852  cache[e] = true;
3853 
3854  DebugAssert(e.arity() > 0, "Expected non-zero arity");
3855  int k = 0;
3856 
3857  if (e.isITE()) {
3858  k = 1;
3859  }
3860 
3861  for (; k < e.arity(); ++k) {
3862  getLeaves(e[k], s, cache);
3863  }
3864 }
3865 
3866 
3867 Theorem ArithTheoremProducerOld::rewriteLeavesConst(const Expr& e)
3868 {
3869  DebugAssert(e.isPropAtom() && d_theoryArith->leavesAreNumConst(e),
3870  "invariant violated");
3871  DebugAssert(e.getKind() == EQ || e.getKind() == LT || e.getKind() == LE || e.getKind() == GT || e.getKind() == GE,
3872  "Unexpected kind");
3873  set<Rational> lhs, rhs;
3874  ExprHashMap<bool> cache;
3875  getLeaves(e[0], lhs, cache);
3876 
3877  cache.clear();
3878  getLeaves(e[1], rhs, cache);
3879 
3880  Expr res;
3881  switch (e.getKind()) {
3882  case EQ: {
3883  set<Rational> common;
3884  set_intersection(lhs.begin(), lhs.end(), rhs.begin(), rhs.end(),
3885  inserter(common, common.begin()));
3886  if (common.empty()) {
3887  res = d_em->falseExpr();
3888  }
3889  break;
3890  }
3891  case LT: {
3892  set<Rational>::iterator it;
3893  it = lhs.end();
3894  --it;
3895  if ((*it) < (*(rhs.begin()))) {
3896  res = d_em->trueExpr();
3897  } else {
3898  it = rhs.end();
3899  --it;
3900  if ((*it) <= (*(lhs.begin()))) {
3901  res = d_em->falseExpr();
3902  }
3903  }
3904  break;
3905  }
3906  case LE: {
3907  set<Rational>::iterator it;
3908  it = lhs.end();
3909  --it;
3910  if ((*it) <= (*(rhs.begin()))) {
3911  res = d_em->trueExpr();
3912  }
3913  else {
3914  it = rhs.end();
3915  --it;
3916  if ((*it) < (*(lhs.begin()))) {
3917  res = d_em->falseExpr();
3918  break;
3919  }
3920  }
3921  break;
3922  }
3923  case GT: {
3924  set<Rational>::iterator it;
3925  it = rhs.end();
3926  --it;
3927  if ((*(lhs.begin())) > (*it)) {
3928  res = d_em->trueExpr();
3929  } else {
3930  it = lhs.end();
3931  --it;
3932  if ((*(rhs.begin())) >= (*it)) {
3933  res = d_em->falseExpr();
3934  }
3935  }
3936  break;
3937  }
3938  case GE: {
3939  set<Rational>::iterator it;
3940  it = rhs.end();
3941  --it;
3942  if ((*(lhs.begin())) >= (*it)) {
3943  res = d_em->trueExpr();
3944  } else {
3945  it = lhs.end();
3946  --it;
3947  if ((*(rhs.begin())) > (*it)) {
3948  res = d_em->falseExpr();
3949  }
3950  }
3951  break;
3952  }
3953  default:
3954  break;
3955  }
3956  if (res.isNull()) return d_theoryArith->reflexivityRule(e);
3957  else {
3958  Proof pf;
3959  if(withProof())
3960  pf = newPf("rewrite_leaves_const", e);
3961  return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
3962  }
3963 }
Expr minusExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:205
int arity() const
Definition: expr.h:1201
bool isNull() const
Definition: expr.h:1223
iterator begin() const
Begin iterator.
Definition: expr.h:1211
bool isEq() const
Definition: expr.h:419
bool isAtomic() const
Test if e is atomic.
Definition: expr.cpp:550
bool isInt(Type t)
Definition: theory_arith.h:174
Expr ltExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:221
Data structure of expressions in CVC3.
Definition: expr.h:133
bool isRational() const
Definition: expr.h:431
bool isIntPred(const Expr &e)
Definition: theory_arith.h:194
bool isITE() const
Definition: expr.h:423
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
Definition: expr.h:1135
iterator find(const Expr &e)
Definition: expr_map.h:194
void add(const std::vector< Theorem > &thms)
bool isLE(const Expr &e)
Definition: theory_arith.h:187
bool isPropAtom() const
True iff expr is not a Bool connective.
Definition: expr.h:411
Definition: kinds.h:85
iterator begin()
Definition: expr_map.h:190
bool isGE(const Expr &e)
Definition: theory_arith.h:189
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
std::string toString(int base=10) const
Expr gtExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:225
#define DebugAssert(cond, str)
Definition: debug.h:408
#define CHECK_SOUND(cond, msg)
#define CHECK_PROOFS
bool isGT(const Expr &e)
Definition: theory_arith.h:188
bool isIntx(const Expr &e, const Rational &x)
bool isPlus(const Expr &e)
Definition: theory_arith.h:181
const std::vector< Expr > & getKids() const
Definition: expr.h:1162
Expr andExpr(const Expr &right) const
Definition: expr.h:941
bool isRational(const Expr &e)
Definition: theory_arith.h:177
Expr orExpr(const std::vector< Expr > &children)
Definition: expr.h:955
Expr impExpr(const Expr &right) const
Definition: expr.h:969
Op getOp() const
Get operator from expression.
Definition: expr.h:1183
bool isNot() const
Definition: expr.h:420
size_t count(const Expr &e) const
Definition: expr_map.h:173
Definition: kinds.h:44
#define CLASS_NAME
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
bool isInteger() const
std::string toString() const
Definition: theorem.h:404
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
static int left(int i)
Definition: minisat_heap.h:53
Expr iffExpr(const Expr &right) const
Definition: expr.h:965
Expr negate() const
Definition: expr.h:937
Definition: kinds.h:68
int getKind() const
Definition: expr.h:1168
T abs(T t)
Definition: cvc_util.h:53
std::string int2string(int n)
Definition: cvc_util.h:46
const Expr & getRHS() const
Definition: theorem.cpp:246
Expr powExpr(const Expr &pow, const Expr &base)
Power (x^n, or base^{pow}) expressions.
Definition: theory_arith.h:216
Proof getProof() const
Definition: theorem.cpp:402
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
Expr notExpr() const
Definition: expr.h:933
Expr getExpr() const
Definition: theorem.cpp:230
bool isIneq(const Expr &e)
Definition: theory_arith.h:192
Expr orExpr(const Expr &right) const
Definition: expr.h:951
Definition: kinds.h:69
bool operator()(const Expr &e1, const Expr &e2) const
bool isDarkShadow(const Expr &e)
Definition: theory_arith.h:190
void setType(const Type &t) const
Set the cached type.
Definition: expr.h:1427
static int right(int i)
Definition: minisat_heap.h:54
map< Expr, Rational, MonomialLess > MonomMap
bool isDivide(const Expr &e)
Definition: theory_arith.h:184
bool isVar() const
Definition: expr.h:1005
iterator find(const Expr &e)
Definition: expr_map.h:329
TRUSTED implementation of arithmetic proof rules.
bool isLT(const Expr &e)
Definition: theory_arith.h:186
Expr plusExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:199
bool isGrayShadow(const Expr &e)
Definition: theory_arith.h:191
const Expr & getLHS() const
Definition: theorem.cpp:240
Expr geExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:227
Definition: kinds.h:61
const std::string & getString() const
Definition: expr.h:1055
Rational pow(Rational pow, const Rational &base)
Raise 'base' into the power of 'pow' (pow must be an integer)
Definition: rational.h:159
bool isPow(const Expr &e)
Definition: theory_arith.h:185
Definition: kinds.h:99
Expr leExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:223
bool isRewrite() const
Definition: theorem.cpp:224
map< Expr, Rational, MonomialLess > MonomMap
bool isMult(const Expr &e)
Definition: theory_arith.h:183
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
iterator end()
Definition: expr_map.h:191
Rational ratRoot(const Rational &base, unsigned long int n)
take nth root of base, return result if it is exact, 0 otherwise
Definition: rational.h:172
int getInt() const
Expr multExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:207
iterator end()
Definition: expr_map.h:326
iterator end() const
End iterator.
Definition: expr.h:1217