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
);
83 }else if(t
.getKind() == kind::MINUS
){
84 return rewriteMinus(t
, true);
85 }else if(t
.getKind() == kind::UMINUS
){
86 return rewriteUMinus(t
, true);
87 }else if(t
.getKind() == kind::DIVISION
){
88 return RewriteResponse(REWRITE_DONE
, t
); // wait until t[1] is rewritten
89 }else if(t
.getKind() == kind::DIVISION_TOTAL
){
90 if(t
[1].getKind()== kind::CONST_RATIONAL
&&
91 t
[1].getConst
<Rational
>().isZero()){
92 return RewriteResponse(REWRITE_DONE
, mkRationalNode(0));
94 return RewriteResponse(REWRITE_DONE
, t
); // wait until t[1] is rewritten
96 }else if(t
.getKind() == kind::PLUS
){
97 return preRewritePlus(t
);
98 }else if(t
.getKind() == kind::MULT
){
99 return preRewriteMult(t
);
100 }else if(t
.getKind() == kind::INTS_DIVISION
){
102 if(t
[1].getKind()== kind::CONST_RATIONAL
&&
103 t
[1].getConst
<Rational
>().isOne()){
104 return RewriteResponse(REWRITE_AGAIN
, t
[0]);
106 return RewriteResponse(REWRITE_DONE
, t
);
108 }else if(t
.getKind() == kind::INTS_DIVISION_TOTAL
){
109 if(t
[1].getKind()== kind::CONST_RATIONAL
){
110 Rational
intOne(1), intZero(0);
111 if(t
[1].getConst
<Rational
>().isOne()){
112 return RewriteResponse(REWRITE_AGAIN
, t
[0]);
113 } else if(t
[1].getConst
<Rational
>().isZero()){
114 return RewriteResponse(REWRITE_DONE
, mkRationalNode(0));
117 return RewriteResponse(REWRITE_DONE
, t
);
118 }else if(t
.getKind() == kind::INTS_MODULUS
){
120 if(t
[1].getKind()== kind::CONST_RATIONAL
&&
121 t
[1].getConst
<Rational
>().isOne()){
122 return RewriteResponse(REWRITE_AGAIN
, mkRationalNode(0));
124 return RewriteResponse(REWRITE_DONE
, t
);
126 }else if(t
.getKind() == kind::INTS_MODULUS_TOTAL
){
127 if(t
[1].getKind()== kind::CONST_RATIONAL
){
128 if(t
[1].getConst
<Rational
>().isOne() || t
[1].getConst
<Rational
>().isZero()){
129 return RewriteResponse(REWRITE_DONE
, mkRationalNode(0));
132 return RewriteResponse(REWRITE_DONE
, t
);
137 RewriteResponse
ArithRewriter::postRewriteTerm(TNode t
){
139 return rewriteConstant(t
);
141 return rewriteVariable(t
);
142 }else if(t
.getKind() == kind::MINUS
){
143 return rewriteMinus(t
, false);
144 }else if(t
.getKind() == kind::UMINUS
){
145 return rewriteUMinus(t
, false);
146 }else if(t
.getKind() == kind::DIVISION
||
147 t
.getKind() == kind::DIVISION_TOTAL
){
148 return rewriteDiv(t
, false);
149 }else if(t
.getKind() == kind::PLUS
){
150 return postRewritePlus(t
);
151 }else if(t
.getKind() == kind::MULT
){
152 return postRewriteMult(t
);
153 }else if(t
.getKind() == kind::INTS_DIVISION
||
154 t
.getKind() == kind::INTS_MODULUS
){
155 return RewriteResponse(REWRITE_DONE
, t
);
156 }else if(t
.getKind() == kind::INTS_DIVISION_TOTAL
||
157 t
.getKind() == kind::INTS_MODULUS_TOTAL
){
158 if(t
[1].getKind() == kind::CONST_RATIONAL
&&
159 t
[1].getConst
<Rational
>().isZero()){
160 return RewriteResponse(REWRITE_DONE
, mkRationalNode(0));
162 return RewriteResponse(REWRITE_DONE
, t
);
169 RewriteResponse
ArithRewriter::preRewriteMult(TNode t
){
170 Assert(t
.getKind()== kind::MULT
);
172 // Rewrite multiplications with a 0 argument and to 0
175 for(TNode::iterator i
= t
.begin(); i
!= t
.end(); ++i
) {
176 if((*i
).getKind() == kind::CONST_RATIONAL
) {
177 if((*i
).getConst
<Rational
>() == qZero
) {
178 return RewriteResponse(REWRITE_DONE
, mkRationalNode(qZero
));
182 return RewriteResponse(REWRITE_DONE
, t
);
184 RewriteResponse
ArithRewriter::preRewritePlus(TNode t
){
185 Assert(t
.getKind()== kind::PLUS
);
187 return RewriteResponse(REWRITE_DONE
, t
);
190 RewriteResponse
ArithRewriter::postRewritePlus(TNode t
){
191 Assert(t
.getKind()== kind::PLUS
);
193 Polynomial res
= Polynomial::mkZero();
195 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
197 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
199 res
= res
+ currPoly
;
202 return RewriteResponse(REWRITE_DONE
, res
.getNode());
205 RewriteResponse
ArithRewriter::postRewriteMult(TNode t
){
206 Assert(t
.getKind()== kind::MULT
);
208 Polynomial res
= Polynomial::mkOne();
210 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
212 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
214 res
= res
* currPoly
;
217 return RewriteResponse(REWRITE_DONE
, res
.getNode());
220 // RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){
221 // TNode left = t[0];
222 // TNode right = t[1];
224 // Polynomial pLeft = Polynomial::parsePolynomial(left);
227 // Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
229 // Assert(cmp.isNormalForm());
230 // return RewriteResponse(REWRITE_DONE, cmp.getNode());
233 RewriteResponse
ArithRewriter::postRewriteAtom(TNode atom
){
235 TNode left
= atom
[0];
236 TNode right
= atom
[1];
238 Polynomial pleft
= Polynomial::parsePolynomial(left
);
239 Polynomial pright
= Polynomial::parsePolynomial(right
);
241 Comparison cmp
= Comparison::mkComparison(atom
.getKind(), pleft
, pright
);
242 Assert(cmp
.isNormalForm());
243 return RewriteResponse(REWRITE_DONE
, cmp
.getNode());
246 RewriteResponse
ArithRewriter::preRewriteAtom(TNode atom
){
247 Assert(isAtom(atom
));
249 NodeManager
* currNM
= NodeManager::currentNM();
251 if(atom
.getKind() == kind::EQUAL
) {
252 if(atom
[0] == atom
[1]) {
253 return RewriteResponse(REWRITE_DONE
, currNM
->mkConst(true));
255 }else if(atom
.getKind() == kind::GT
){
256 Node leq
= currNM
->mkNode(kind::LEQ
, atom
[0], atom
[1]);
257 return RewriteResponse(REWRITE_DONE
, currNM
->mkNode(kind::NOT
, leq
));
258 }else if(atom
.getKind() == kind::LT
){
259 Node geq
= currNM
->mkNode(kind::GEQ
, atom
[0], atom
[1]);
260 return RewriteResponse(REWRITE_DONE
, currNM
->mkNode(kind::NOT
, geq
));
263 return RewriteResponse(REWRITE_DONE
, atom
);
266 RewriteResponse
ArithRewriter::postRewrite(TNode t
){
268 RewriteResponse response
= postRewriteTerm(t
);
269 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
270 Polynomial::parsePolynomial(response
.node
);
274 RewriteResponse response
= postRewriteAtom(t
);
275 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
276 Comparison::parseNormalForm(response
.node
);
281 return RewriteResponse(REWRITE_DONE
, Node::null());
285 RewriteResponse
ArithRewriter::preRewrite(TNode t
){
287 return preRewriteTerm(t
);
289 return preRewriteAtom(t
);
292 return RewriteResponse(REWRITE_DONE
, Node::null());
296 Node
ArithRewriter::makeUnaryMinusNode(TNode n
){
297 Rational
qNegOne(-1);
298 return NodeManager::currentNM()->mkNode(kind::MULT
, mkRationalNode(qNegOne
),n
);
301 Node
ArithRewriter::makeSubtractionNode(TNode l
, TNode r
){
302 Node negR
= makeUnaryMinusNode(r
);
303 Node diff
= NodeManager::currentNM()->mkNode(kind::PLUS
, l
, negR
);
308 RewriteResponse
ArithRewriter::rewriteDiv(TNode t
, bool pre
){
309 Assert(t
.getKind()== kind::DIVISION
|| t
.getKind() == kind::DIVISION_TOTAL
);
313 if(right
.getKind() == kind::CONST_RATIONAL
){
314 const Rational
& den
= right
.getConst
<Rational
>();
317 if(t
.getKind() == kind::DIVISION_TOTAL
){
318 return RewriteResponse(REWRITE_DONE
, mkRationalNode(0));
320 return RewriteResponse(REWRITE_DONE
, t
);
323 Assert(den
!= Rational(0));
325 Rational div
= den
.inverse();
327 Node result
= mkRationalNode(div
);
329 Node mult
= NodeManager::currentNM()->mkNode(kind::MULT
,left
,result
);
331 return RewriteResponse(REWRITE_DONE
, mult
);
333 return RewriteResponse(REWRITE_AGAIN
, mult
);
336 return RewriteResponse(REWRITE_DONE
, t
);
340 }/* CVC4::theory::arith namespace */
341 }/* CVC4::theory namespace */
342 }/* CVC4 namespace */