1 /********************* */
2 /*! \file arith_rewriter.cpp
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): mdeters, dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief [[ Add one-line brief description here ]]
16 ** [[ Add lengthier description here ]]
17 ** \todo document this file
20 #include "theory/theory.h"
21 #include "theory/arith/normal_form.h"
22 #include "theory/arith/arith_rewriter.h"
23 #include "theory/arith/arith_utilities.h"
33 bool ArithRewriter::isAtom(TNode n
) {
34 return arith::isRelationOperator(n
.getKind());
37 RewriteResponse
ArithRewriter::rewriteConstant(TNode t
){
39 Assert(t
.getKind() == kind::CONST_RATIONAL
);
41 return RewriteResponse(REWRITE_DONE
, t
);
44 RewriteResponse
ArithRewriter::rewriteVariable(TNode t
){
47 return RewriteResponse(REWRITE_DONE
, t
);
50 RewriteResponse
ArithRewriter::rewriteMinus(TNode t
, bool pre
){
51 Assert(t
.getKind()== kind::MINUS
);
56 Node zeroNode
= mkRationalNode(zero
);
57 return RewriteResponse(REWRITE_DONE
, zeroNode
);
59 Node noMinus
= makeSubtractionNode(t
[0],t
[1]);
60 return RewriteResponse(REWRITE_DONE
, noMinus
);
63 Polynomial minuend
= Polynomial::parsePolynomial(t
[0]);
64 Polynomial subtrahend
= Polynomial::parsePolynomial(t
[0]);
65 Polynomial diff
= minuend
- subtrahend
;
66 return RewriteResponse(REWRITE_DONE
, diff
.getNode());
70 RewriteResponse
ArithRewriter::rewriteUMinus(TNode t
, bool pre
){
71 Assert(t
.getKind()== kind::UMINUS
);
73 Node noUminus
= makeUnaryMinusNode(t
[0]);
75 return RewriteResponse(REWRITE_DONE
, noUminus
);
77 return RewriteResponse(REWRITE_AGAIN
, noUminus
);
80 RewriteResponse
ArithRewriter::preRewriteTerm(TNode t
){
82 return rewriteConstant(t
);
84 return rewriteVariable(t
);
85 }else if(t
.getKind() == kind::MINUS
){
86 return rewriteMinus(t
, true);
87 }else if(t
.getKind() == kind::UMINUS
){
88 return rewriteUMinus(t
, true);
89 }else if(t
.getKind() == kind::DIVISION
){
90 return RewriteResponse(REWRITE_DONE
, t
); // wait until t[1] is rewritten
91 }else if(t
.getKind() == kind::PLUS
){
92 return preRewritePlus(t
);
93 }else if(t
.getKind() == kind::MULT
){
94 return preRewriteMult(t
);
95 }else if(t
.getKind() == kind::INTS_DIVISION
){
97 if(t
[1].getKind()== kind::CONST_RATIONAL
&& t
[1].getConst
<Rational
>() == intOne
){
98 return RewriteResponse(REWRITE_AGAIN
, t
[0]);
100 return RewriteResponse(REWRITE_DONE
, t
);
102 }else if(t
.getKind() == kind::INTS_MODULUS
){
104 if(t
[1].getKind()== kind::CONST_RATIONAL
&& t
[1].getConst
<Rational
>() == intOne
){
106 return RewriteResponse(REWRITE_AGAIN
, mkRationalNode(intZero
));
108 return RewriteResponse(REWRITE_DONE
, t
);
114 RewriteResponse
ArithRewriter::postRewriteTerm(TNode t
){
116 return rewriteConstant(t
);
118 return rewriteVariable(t
);
119 }else if(t
.getKind() == kind::MINUS
){
120 return rewriteMinus(t
, false);
121 }else if(t
.getKind() == kind::UMINUS
){
122 return rewriteUMinus(t
, false);
123 }else if(t
.getKind() == kind::DIVISION
){
124 return rewriteDivByConstant(t
, false);
125 }else if(t
.getKind() == kind::PLUS
){
126 return postRewritePlus(t
);
127 }else if(t
.getKind() == kind::MULT
){
128 return postRewriteMult(t
);
129 }else if(t
.getKind() == kind::INTS_DIVISION
){
130 return RewriteResponse(REWRITE_DONE
, t
);
131 }else if(t
.getKind() == kind::INTS_MODULUS
){
132 return RewriteResponse(REWRITE_DONE
, t
);
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::postRewriteAtomConstantRHS(TNode t){
190 // TNode left = t[0];
191 // TNode right = t[1];
193 // Polynomial pLeft = Polynomial::parsePolynomial(left);
196 // Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
198 // Assert(cmp.isNormalForm());
199 // return RewriteResponse(REWRITE_DONE, cmp.getNode());
202 RewriteResponse
ArithRewriter::postRewriteAtom(TNode atom
){
204 TNode left
= atom
[0];
205 TNode right
= atom
[1];
207 Polynomial pleft
= Polynomial::parsePolynomial(left
);
208 Polynomial pright
= Polynomial::parsePolynomial(right
);
210 Comparison cmp
= Comparison::mkComparison(atom
.getKind(), pleft
, pright
);
211 Assert(cmp
.isNormalForm());
212 return RewriteResponse(REWRITE_DONE
, cmp
.getNode());
215 RewriteResponse
ArithRewriter::preRewriteAtom(TNode atom
){
216 Assert(isAtom(atom
));
218 NodeManager
* currNM
= NodeManager::currentNM();
220 if(atom
.getKind() == kind::EQUAL
) {
221 if(atom
[0] == atom
[1]) {
222 return RewriteResponse(REWRITE_DONE
, currNM
->mkConst(true));
224 }else if(atom
.getKind() == kind::GT
){
225 Node leq
= currNM
->mkNode(kind::LEQ
, atom
[0], atom
[1]);
226 return RewriteResponse(REWRITE_DONE
, currNM
->mkNode(kind::NOT
, leq
));
227 }else if(atom
.getKind() == kind::LT
){
228 Node geq
= currNM
->mkNode(kind::GEQ
, atom
[0], atom
[1]);
229 return RewriteResponse(REWRITE_DONE
, currNM
->mkNode(kind::NOT
, geq
));
232 return RewriteResponse(REWRITE_DONE
, atom
);
235 RewriteResponse
ArithRewriter::postRewrite(TNode t
){
237 RewriteResponse response
= postRewriteTerm(t
);
238 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
239 Polynomial::parsePolynomial(response
.node
);
243 RewriteResponse response
= postRewriteAtom(t
);
244 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
245 Comparison::parseNormalForm(response
.node
);
250 return RewriteResponse(REWRITE_DONE
, Node::null());
254 RewriteResponse
ArithRewriter::preRewrite(TNode t
){
256 return preRewriteTerm(t
);
258 return preRewriteAtom(t
);
261 return RewriteResponse(REWRITE_DONE
, Node::null());
265 Node
ArithRewriter::makeUnaryMinusNode(TNode n
){
266 Rational
qNegOne(-1);
267 return NodeManager::currentNM()->mkNode(kind::MULT
, mkRationalNode(qNegOne
),n
);
270 Node
ArithRewriter::makeSubtractionNode(TNode l
, TNode r
){
271 Node negR
= makeUnaryMinusNode(r
);
272 Node diff
= NodeManager::currentNM()->mkNode(kind::PLUS
, l
, negR
);
277 RewriteResponse
ArithRewriter::rewriteDivByConstant(TNode t
, bool pre
){
278 Assert(t
.getKind()== kind::DIVISION
);
282 Assert(right
.getKind()== kind::CONST_RATIONAL
);
285 const Rational
& den
= right
.getConst
<Rational
>();
287 Assert(den
!= Rational(0));
289 Rational div
= den
.inverse();
291 Node result
= mkRationalNode(div
);
293 Node mult
= NodeManager::currentNM()->mkNode(kind::MULT
,left
,result
);
295 return RewriteResponse(REWRITE_DONE
, mult
);
297 return RewriteResponse(REWRITE_AGAIN
, mult
);
301 }/* CVC4::theory::arith namespace */
302 }/* CVC4::theory namespace */
303 }/* CVC4 namespace */