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
canonRec(const Expr & e)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
printRational(ExprStream & os,const Rational & r,bool printAsReal)54 void TheoryArith::printRational(ExprStream& os, const Rational& r,
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
isAtomicArithTerm(const Expr & e)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
isAtomicArithFormula(const Expr & e)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
isSyntacticRational(const Expr & e,Rational & r)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
rewriteToDiff(const Expr & e)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
canonSimp(const Expr & e)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
recursiveCanonSimpCheck(const Expr & e)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
leavesAreNumConst(const Expr & e)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
332