CVC3  2.4.1
theory_arith.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_arith.cpp
4  *
5  * Author: Clark Barrett, Vijay Ganesh.
6  *
7  * Created: Fri Jan 17 18:39:18 2003
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 
21 
22 #include "theory_arith.h"
23 #include "theory_core.h"
24 #include "translator.h"
25 
26 
27 using namespace std;
28 using namespace CVC3;
29 
30 
31 Theorem TheoryArith::canonRec(const Expr& e)
32 {
33  if (isLeaf(e)) return reflexivityRule(e);
34  int ar = e.arity();
35  if (ar > 0) {
36  vector<Theorem> newChildrenThm;
37  vector<unsigned> changed;
38  for(int k = 0; k < ar; ++k) {
39  // Recursively canonize the kids
40  Theorem thm = canonRec(e[k]);
41  if (thm.getLHS() != thm.getRHS()) {
42  newChildrenThm.push_back(thm);
43  changed.push_back(k);
44  }
45  }
46  if(changed.size() > 0) {
47  return canonThm(substitutivityRule(e, changed, newChildrenThm));
48  }
49  }
50  return canon(e);
51 }
52 
53 
55  bool printAsReal)
56 {
57  // Print rational
58  if (r.isInteger()) {
59  if (r < 0) {
60  if (os.lang() == SPASS_LANG) {
61  os << "-" << (-r).toString();
62  if (printAsReal) os << ".0";
63  } else {
64  os << "(" << push;
65  if (os.lang() == SMTLIB_LANG) {
66  os << "~";
67  }
68  else {
69  os << "-";
70  }
71  os << space << (-r).toString();
72  if (printAsReal) os << ".0";
73  os << push << ")";
74  }
75  }
76  else {
77  os << r.toString();
78  if (printAsReal) os << ".0";
79  }
80  }
81  else {
82  os << "(" << push << "/ ";
83  Rational tmp = r.getNumerator();
84  if (tmp < 0) {
85  if (os.lang() == SPASS_LANG) {
86  os << "-" << (-tmp).toString();
87  if (printAsReal) os << ".0";
88  } else {
89  os << "(" << push;
90  if (os.lang() == SMTLIB_LANG) {
91  os << "~";
92  }
93  else {
94  os << "-";
95  }
96  os << space << (-tmp).toString();
97  if (printAsReal) os << ".0";
98  os << push << ")";
99  }
100  }
101  else {
102  os << tmp.toString();
103  if (printAsReal) os << ".0";
104  }
105  os << space;
106  tmp = r.getDenominator();
107  DebugAssert(tmp > 0 && tmp.isInteger(), "Unexpected rational denominator");
108  os << tmp.toString();
109  if (printAsReal) os << ".0";
110  os << push << ")";
111  }
112 }
113 
114 
115 bool TheoryArith::isAtomicArithTerm(const Expr& e)
116 {
117  switch (e.getKind()) {
118  case RATIONAL_EXPR:
119  return true;
120  case ITE:
121  return false;
122  case UMINUS:
123  case PLUS:
124  case MINUS:
125  case MULT:
126  case DIVIDE:
127  case POW:
128  case INTDIV:
129  case MOD: {
130  int i=0, iend=e.arity();
131  for(; i!=iend; ++i) {
132  if (!isAtomicArithTerm(e[i])) return false;
133  }
134  break;
135  }
136  default:
137  break;
138  }
139  return true;
140 }
141 
142 
143 bool TheoryArith::isAtomicArithFormula(const Expr& e)
144 {
145  switch (e.getKind()) {
146  case LT:
147  case GT:
148  case LE:
149  case GE:
150  case EQ:
151  return isAtomicArithTerm(e[0]) && isAtomicArithTerm(e[1]);
152  }
153  return false;
154 }
155 
156 
157 bool TheoryArith::isSyntacticRational(const Expr& e, Rational& r)
158 {
159  if (e.getKind() == REAL_CONST) {
160  r = e[0].getRational();
161  return true;
162  }
163  else if (e.isRational()) {
164  r = e.getRational();
165  return true;
166  }
167  else if (isUMinus(e)) {
168  if (isSyntacticRational(e[0], r)) {
169  r = -r;
170  return true;
171  }
172  }
173  else if (isDivide(e)) {
174  Rational num;
175  if (isSyntacticRational(e[0], num)) {
176  Rational den;
177  if (isSyntacticRational(e[1], den)) {
178  if (den != 0) {
179  r = num / den;
180  return true;
181  }
182  }
183  }
184  }
185  return false;
186 }
187 
188 
189 Expr TheoryArith::rewriteToDiff(const Expr& e)
190 {
191  Expr tmp = e[0] - e[1];
192  tmp = canonRec(tmp).getRHS();
193  switch (tmp.getKind()) {
194  case RATIONAL_EXPR: {
195  Rational r = tmp.getRational();
196  switch (e.getKind()) {
197  case LT:
198  if (r < 0) return trueExpr();
199  else return falseExpr();
200  case LE:
201  if (r <= 0) return trueExpr();
202  else return falseExpr();
203  case GT:
204  if (r > 0) return trueExpr();
205  else return falseExpr();
206  case GE:
207  if (r >= 0) return trueExpr();
208  else return falseExpr();
209  case EQ:
210  if (r == 0) return trueExpr();
211  else return falseExpr();
212  }
213  }
214  case MULT:
215  DebugAssert(tmp[0].isRational(), "Unexpected term structure from canon");
216  if (tmp[0].getRational() != -1) return e;
217  return Expr(e.getOp(), theoryCore()->getTranslator()->zeroVar() - tmp[1], rat(0));
218  case PLUS: {
219  DebugAssert(tmp[0].isRational(), "Unexpected term structure from canon");
220  Rational c = tmp[0].getRational();
221  Expr x, y;
222  if (tmp.arity() == 2) {
223  if (tmp[1].getKind() == MULT) {
224  x = theoryCore()->getTranslator()->zeroVar();
225  y = tmp[1];
226  }
227  else {
228  x = tmp[1];
229  y = rat(-1) * theoryCore()->getTranslator()->zeroVar();
230  }
231  }
232  else if (tmp.arity() == 3) {
233  if (tmp[1].getKind() == MULT) {
234  x = tmp[2];
235  y = tmp[1];
236  }
237  else if (tmp[2].getKind() == MULT) {
238  x = tmp[1];
239  y = tmp[2];
240  }
241  else return e;
242  }
243  else return e;
244  if (x.getKind() == MULT) return e;
245  DebugAssert(y[0].isRational(), "Unexpected term structure from canon");
246  if (y[0].getRational() != -1) return e;
247  return Expr(e.getOp(), x - y[1], getEM()->newRatExpr(-c));
248  }
249  default:
250  return Expr(e.getOp(), tmp - theoryCore()->getTranslator()->zeroVar(), rat(0));
251  break;
252  }
253  return e;
254 }
255 
256 
257 Theorem TheoryArith::canonSimp(const Expr& e)
258 {
259  DebugAssert(canonRec(e).getRHS() == e, "canonSimp expects input to be canonized");
260  int ar = e.arity();
261  if (isLeaf(e)) return find(e);
262  if (ar > 0) {
263  vector<Theorem> newChildrenThm;
264  vector<unsigned> changed;
265  Theorem thm;
266  for (int k = 0; k < ar; ++k) {
267  thm = canonSimp(e[k]);
268  if (thm.getLHS() != thm.getRHS()) {
269  newChildrenThm.push_back(thm);
270  changed.push_back(k);
271  }
272  }
273  if(changed.size() > 0) {
274  thm = canonThm(substitutivityRule(e, changed, newChildrenThm));
275  return transitivityRule(thm, find(thm.getRHS()));
276  }
277  else return find(e);
278  }
279  return find(e);
280 }
281 
282 
283 bool TheoryArith::recursiveCanonSimpCheck(const Expr& e)
284 {
285  if (e.hasFind()) return true;
286  if (e != canonSimp(e).getRHS()) return false;
287  Expr::iterator i = e.begin(), iend = e.end();
288  for (; i != iend; ++i)
289  if (!recursiveCanonSimpCheck(*i)) return false;
290  return true;
291 }
292 
293 
294 bool TheoryArith::leavesAreNumConst(const Expr& e)
295 {
296  DebugAssert(e.isTerm() ||
297  (e.isPropAtom() && theoryOf(e) == this),
298  "Expected term or arith prop atom");
299 
300  if (e.validTerminalsConstFlag()) {
301  return e.getTerminalsConstFlag();
302  }
303 
304  if (e.isRational()) {
305  e.setTerminalsConstFlag(true);
306  return true;
307  }
308 
309  if (e.isAtomic() && isLeaf(e)) {
310  e.setTerminalsConstFlag(false);
311  return false;
312  }
313 
314  DebugAssert(e.arity() > 0, "Expected non-zero arity");
315  int k = 0;
316 
317  if (e.isITE()) {
318  k = 1;
319  }
320 
321  for (; k < e.arity(); ++k) {
322  if (!leavesAreNumConst(e[k])) {
323  e.setTerminalsConstFlag(false);
324  return false;
325  }
326  }
327  e.setTerminalsConstFlag(true);
328  return true;
329 }
330 
331