1 /********************* */
2 /*! \file arith_rewriter.cpp
4 ** Original author: taking
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "theory/theory.h"
19 #include "theory/arith/normal_form.h"
20 #include "theory/arith/arith_rewriter.h"
21 #include "theory/arith/arith_utilities.h"
31 bool ArithRewriter::isAtom(TNode n
) {
32 return arith::isRelationOperator(n
.getKind());
35 RewriteResponse
ArithRewriter::rewriteConstant(TNode t
){
37 Assert(t
.getKind() == kind::CONST_RATIONAL
);
39 return RewriteResponse(REWRITE_DONE
, t
);
42 RewriteResponse
ArithRewriter::rewriteVariable(TNode t
){
45 return RewriteResponse(REWRITE_DONE
, t
);
48 RewriteResponse
ArithRewriter::rewriteMinus(TNode t
, bool pre
){
49 Assert(t
.getKind()== kind::MINUS
);
54 Node zeroNode
= mkRationalNode(zero
);
55 return RewriteResponse(REWRITE_DONE
, zeroNode
);
57 Node noMinus
= makeSubtractionNode(t
[0],t
[1]);
58 return RewriteResponse(REWRITE_DONE
, noMinus
);
61 Polynomial minuend
= Polynomial::parsePolynomial(t
[0]);
62 Polynomial subtrahend
= Polynomial::parsePolynomial(t
[1]);
63 Polynomial diff
= minuend
- subtrahend
;
64 return RewriteResponse(REWRITE_DONE
, diff
.getNode());
68 RewriteResponse
ArithRewriter::rewriteUMinus(TNode t
, bool pre
){
69 Assert(t
.getKind()== kind::UMINUS
);
71 Node noUminus
= makeUnaryMinusNode(t
[0]);
73 return RewriteResponse(REWRITE_DONE
, noUminus
);
75 return RewriteResponse(REWRITE_AGAIN
, noUminus
);
78 RewriteResponse
ArithRewriter::preRewriteTerm(TNode t
){
80 return rewriteConstant(t
);
82 return rewriteVariable(t
);
86 return rewriteMinus(t
, true);
88 return rewriteUMinus(t
, true);
90 return rewriteDiv(t
,true);
91 case kind::DIVISION_TOTAL
:
92 return rewriteDivTotal(t
,true);
94 return preRewritePlus(t
);
96 return preRewriteMult(t
);
97 //case kind::INTS_DIVISION:
98 //case kind::INTS_MODULUS:
99 case kind::INTS_DIVISION_TOTAL
:
100 case kind::INTS_MODULUS_TOTAL
:
101 return rewriteIntsDivModTotal(t
,true);
107 RewriteResponse
ArithRewriter::postRewriteTerm(TNode t
){
109 return rewriteConstant(t
);
111 return rewriteVariable(t
);
115 return rewriteMinus(t
, false);
117 return rewriteUMinus(t
, false);
119 return rewriteDiv(t
, false);
120 case kind::DIVISION_TOTAL
:
121 return rewriteDivTotal(t
, false);
123 return postRewritePlus(t
);
125 return postRewriteMult(t
);
126 //case kind::INTS_DIVISION:
127 //case kind::INTS_MODULUS:
128 case kind::INTS_DIVISION_TOTAL
:
129 case kind::INTS_MODULUS_TOTAL
:
130 return rewriteIntsDivModTotal(t
, false);
138 RewriteResponse
ArithRewriter::preRewriteMult(TNode t
){
139 Assert(t
.getKind()== kind::MULT
);
141 // Rewrite multiplications with a 0 argument and to 0
144 for(TNode::iterator i
= t
.begin(); i
!= t
.end(); ++i
) {
145 if((*i
).getKind() == kind::CONST_RATIONAL
) {
146 if((*i
).getConst
<Rational
>() == qZero
) {
147 return RewriteResponse(REWRITE_DONE
, mkRationalNode(qZero
));
151 return RewriteResponse(REWRITE_DONE
, t
);
153 RewriteResponse
ArithRewriter::preRewritePlus(TNode t
){
154 Assert(t
.getKind()== kind::PLUS
);
156 return RewriteResponse(REWRITE_DONE
, t
);
159 RewriteResponse
ArithRewriter::postRewritePlus(TNode t
){
160 Assert(t
.getKind()== kind::PLUS
);
162 Polynomial res
= Polynomial::mkZero();
164 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
166 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
168 res
= res
+ currPoly
;
171 return RewriteResponse(REWRITE_DONE
, res
.getNode());
174 RewriteResponse
ArithRewriter::postRewriteMult(TNode t
){
175 Assert(t
.getKind()== kind::MULT
);
177 Polynomial res
= Polynomial::mkOne();
179 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
181 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
183 res
= res
* currPoly
;
186 return RewriteResponse(REWRITE_DONE
, res
.getNode());
189 RewriteResponse
ArithRewriter::postRewriteAtom(TNode atom
){
191 TNode left
= atom
[0];
192 TNode right
= atom
[1];
194 Polynomial pleft
= Polynomial::parsePolynomial(left
);
195 Polynomial pright
= Polynomial::parsePolynomial(right
);
197 Comparison cmp
= Comparison::mkComparison(atom
.getKind(), pleft
, pright
);
198 Assert(cmp
.isNormalForm());
199 return RewriteResponse(REWRITE_DONE
, cmp
.getNode());
202 RewriteResponse
ArithRewriter::preRewriteAtom(TNode atom
){
203 Assert(isAtom(atom
));
205 NodeManager
* currNM
= NodeManager::currentNM();
207 if(atom
.getKind() == kind::EQUAL
) {
208 if(atom
[0] == atom
[1]) {
209 return RewriteResponse(REWRITE_DONE
, currNM
->mkConst(true));
211 }else if(atom
.getKind() == kind::GT
){
212 Node leq
= currNM
->mkNode(kind::LEQ
, atom
[0], atom
[1]);
213 return RewriteResponse(REWRITE_DONE
, currNM
->mkNode(kind::NOT
, leq
));
214 }else if(atom
.getKind() == kind::LT
){
215 Node geq
= currNM
->mkNode(kind::GEQ
, atom
[0], atom
[1]);
216 return RewriteResponse(REWRITE_DONE
, currNM
->mkNode(kind::NOT
, geq
));
219 return RewriteResponse(REWRITE_DONE
, atom
);
222 RewriteResponse
ArithRewriter::postRewrite(TNode t
){
224 RewriteResponse response
= postRewriteTerm(t
);
225 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
226 Polynomial::parsePolynomial(response
.node
);
230 RewriteResponse response
= postRewriteAtom(t
);
231 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
232 Comparison::parseNormalForm(response
.node
);
237 return RewriteResponse(REWRITE_DONE
, Node::null());
241 RewriteResponse
ArithRewriter::preRewrite(TNode t
){
243 return preRewriteTerm(t
);
245 return preRewriteAtom(t
);
248 return RewriteResponse(REWRITE_DONE
, Node::null());
252 Node
ArithRewriter::makeUnaryMinusNode(TNode n
){
253 Rational
qNegOne(-1);
254 return NodeManager::currentNM()->mkNode(kind::MULT
, mkRationalNode(qNegOne
),n
);
257 Node
ArithRewriter::makeSubtractionNode(TNode l
, TNode r
){
258 Node negR
= makeUnaryMinusNode(r
);
259 Node diff
= NodeManager::currentNM()->mkNode(kind::PLUS
, l
, negR
);
263 RewriteResponse
ArithRewriter::rewriteDiv(TNode t
, bool pre
){
264 Assert(t
.getKind()== kind::DIVISION
);
269 if(right
.getKind() == kind::CONST_RATIONAL
&&
270 left
.getKind() != kind::CONST_RATIONAL
){
272 const Rational
& den
= right
.getConst
<Rational
>();
274 Assert(!den
.isZero());
276 Rational div
= den
.inverse();
277 Node result
= mkRationalNode(div
);
278 Node mult
= NodeManager::currentNM()->mkNode(kind::MULT
,left
,result
);
280 return RewriteResponse(REWRITE_DONE
, mult
);
282 return RewriteResponse(REWRITE_AGAIN
, mult
);
287 if(right
.getKind() != kind::CONST_RATIONAL
||
288 left
.getKind() != kind::CONST_RATIONAL
){
289 return RewriteResponse(REWRITE_DONE
, t
);
293 Assert(right
.getKind() == kind::CONST_RATIONAL
);
294 Assert(left
.getKind() == kind::CONST_RATIONAL
);
296 const Rational
& den
= right
.getConst
<Rational
>();
298 Assert(!den
.isZero());
300 const Rational
& num
= left
.getConst
<Rational
>();
301 Rational div
= num
/ den
;
302 Node result
= mkRationalNode(div
);
303 return RewriteResponse(REWRITE_DONE
, result
);
306 RewriteResponse
ArithRewriter::rewriteDivTotal(TNode t
, bool pre
){
307 Assert(t
.getKind() == kind::DIVISION_TOTAL
);
312 if(right
.getKind() == kind::CONST_RATIONAL
){
313 const Rational
& den
= right
.getConst
<Rational
>();
316 return RewriteResponse(REWRITE_DONE
, mkRationalNode(0));
318 Assert(den
!= Rational(0));
320 if(left
.getKind() == kind::CONST_RATIONAL
){
321 const Rational
& num
= left
.getConst
<Rational
>();
322 Rational div
= num
/ den
;
323 Node result
= mkRationalNode(div
);
324 return RewriteResponse(REWRITE_DONE
, result
);
327 Rational div
= den
.inverse();
329 Node result
= mkRationalNode(div
);
331 Node mult
= NodeManager::currentNM()->mkNode(kind::MULT
,left
,result
);
333 return RewriteResponse(REWRITE_DONE
, mult
);
335 return RewriteResponse(REWRITE_AGAIN
, mult
);
338 return RewriteResponse(REWRITE_DONE
, t
);
342 RewriteResponse
ArithRewriter::rewriteIntsDivModTotal(TNode t
, bool pre
){
343 Kind k
= t
.getKind();
344 // Assert(k == kind::INTS_MODULUS || k == kind::INTS_MODULUS_TOTAL ||
345 // k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL);
347 //Leaving the function as before (INTS_MODULUS can be handled),
348 // but restricting its use here
349 Assert(k
== kind::INTS_MODULUS_TOTAL
|| k
== kind::INTS_DIVISION_TOTAL
);
350 TNode n
= t
[0], d
= t
[1];
351 bool dIsConstant
= d
.getKind() == kind::CONST_RATIONAL
;
352 if(dIsConstant
&& d
.getConst
<Rational
>().isZero()){
353 if(k
== kind::INTS_MODULUS_TOTAL
|| k
== kind::INTS_DIVISION_TOTAL
){
354 return RewriteResponse(REWRITE_DONE
, mkRationalNode(0));
356 // Do nothing for k == INTS_MODULUS
357 return RewriteResponse(REWRITE_DONE
, t
);
359 }else if(dIsConstant
&& d
.getConst
<Rational
>().isOne()){
360 if(k
== kind::INTS_MODULUS
|| k
== kind::INTS_MODULUS_TOTAL
){
361 return RewriteResponse(REWRITE_DONE
, mkRationalNode(0));
363 Assert(k
== kind::INTS_DIVISION
|| k
== kind::INTS_DIVISION_TOTAL
);
364 return RewriteResponse(REWRITE_AGAIN
, n
);
366 }else if(dIsConstant
&& n
.getKind() == kind::CONST_RATIONAL
){
367 Assert(d
.getConst
<Rational
>().isIntegral());
368 Assert(n
.getConst
<Rational
>().isIntegral());
369 Assert(!d
.getConst
<Rational
>().isZero());
370 Integer di
= d
.getConst
<Rational
>().getNumerator();
371 Integer ni
= n
.getConst
<Rational
>().getNumerator();
373 bool isDiv
= (k
== kind::INTS_DIVISION
|| k
== kind::INTS_DIVISION_TOTAL
);
375 Integer result
= isDiv
? ni
.floorDivideQuotient(di
) : ni
.floorDivideRemainder(di
);
377 Node resultNode
= mkRationalNode(Rational(result
));
378 return RewriteResponse(REWRITE_DONE
, resultNode
);
380 return RewriteResponse(REWRITE_DONE
, t
);
384 }/* CVC4::theory::arith namespace */
385 }/* CVC4::theory namespace */
386 }/* CVC4 namespace */