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 isVariable(TNode t
){
34 return t
.getMetaKind() == kind::metakind::VARIABLE
;
37 bool ArithRewriter::isAtom(TNode n
) {
38 return arith::isRelationOperator(n
.getKind());
41 RewriteResponse
ArithRewriter::rewriteConstant(TNode t
){
42 Assert(t
.getMetaKind() == kind::metakind::CONSTANT
);
43 Node val
= coerceToRationalNode(t
);
45 return RewriteResponse(REWRITE_DONE
, val
);
48 RewriteResponse
ArithRewriter::rewriteVariable(TNode t
){
49 Assert(isVariable(t
));
51 return RewriteResponse(REWRITE_DONE
, t
);
54 RewriteResponse
ArithRewriter::rewriteMinus(TNode t
, bool pre
){
55 Assert(t
.getKind()== kind::MINUS
);
60 Node zeroNode
= mkRationalNode(zero
);
61 return RewriteResponse(REWRITE_DONE
, zeroNode
);
63 Node noMinus
= makeSubtractionNode(t
[0],t
[1]);
64 return RewriteResponse(REWRITE_DONE
, noMinus
);
67 Polynomial minuend
= Polynomial::parsePolynomial(t
[0]);
68 Polynomial subtrahend
= Polynomial::parsePolynomial(t
[0]);
69 Polynomial diff
= minuend
- subtrahend
;
70 return RewriteResponse(REWRITE_DONE
, diff
.getNode());
74 RewriteResponse
ArithRewriter::rewriteUMinus(TNode t
, bool pre
){
75 Assert(t
.getKind()== kind::UMINUS
);
77 Node noUminus
= makeUnaryMinusNode(t
[0]);
79 return RewriteResponse(REWRITE_DONE
, noUminus
);
81 return RewriteResponse(REWRITE_AGAIN
, noUminus
);
84 RewriteResponse
ArithRewriter::preRewriteTerm(TNode t
){
85 if(t
.getMetaKind() == kind::metakind::CONSTANT
){
86 return rewriteConstant(t
);
87 }else if(isVariable(t
)){
88 return rewriteVariable(t
);
89 }else if(t
.getKind() == kind::MINUS
){
90 return rewriteMinus(t
, true);
91 }else if(t
.getKind() == kind::UMINUS
){
92 return rewriteUMinus(t
, true);
93 }else if(t
.getKind() == kind::DIVISION
){
94 if(t
[0].getKind()== kind::CONST_RATIONAL
){
95 return rewriteDivByConstant(t
, true);
97 return RewriteResponse(REWRITE_DONE
, t
);
99 }else if(t
.getKind() == kind::PLUS
){
100 return preRewritePlus(t
);
101 }else if(t
.getKind() == kind::MULT
){
102 return preRewriteMult(t
);
103 }else if(t
.getKind() == kind::INTS_DIVISION
){
105 if(t
[1].getKind()== kind::CONST_INTEGER
&& t
[1].getConst
<Integer
>() == intOne
){
106 return RewriteResponse(REWRITE_AGAIN
, t
[0]);
108 return RewriteResponse(REWRITE_DONE
, t
);
110 }else if(t
.getKind() == kind::INTS_MODULUS
){
112 if(t
[1].getKind()== kind::CONST_INTEGER
&& t
[1].getConst
<Integer
>() == intOne
){
114 return RewriteResponse(REWRITE_AGAIN
, mkIntegerNode(intZero
));
116 return RewriteResponse(REWRITE_DONE
, t
);
122 RewriteResponse
ArithRewriter::postRewriteTerm(TNode t
){
123 if(t
.getMetaKind() == kind::metakind::CONSTANT
){
124 return rewriteConstant(t
);
125 }else if(isVariable(t
)){
126 return rewriteVariable(t
);
127 }else if(t
.getKind() == kind::MINUS
){
128 return rewriteMinus(t
, false);
129 }else if(t
.getKind() == kind::UMINUS
){
130 return rewriteUMinus(t
, false);
131 }else if(t
.getKind() == kind::DIVISION
){
132 return rewriteDivByConstant(t
, false);
133 }else if(t
.getKind() == kind::PLUS
){
134 return postRewritePlus(t
);
135 }else if(t
.getKind() == kind::MULT
){
136 return postRewriteMult(t
);
137 }else if(t
.getKind() == kind::INTS_DIVISION
){
138 return RewriteResponse(REWRITE_DONE
, t
);
139 }else if(t
.getKind() == kind::INTS_MODULUS
){
140 return RewriteResponse(REWRITE_DONE
, t
);
146 RewriteResponse
ArithRewriter::preRewriteMult(TNode t
){
147 Assert(t
.getKind()== kind::MULT
);
149 // Rewrite multiplications with a 0 argument and to 0
154 for(TNode::iterator i
= t
.begin(); i
!= t
.end(); ++i
) {
155 if((*i
).getKind() == kind::CONST_RATIONAL
) {
156 if((*i
).getConst
<Rational
>() == qZero
) {
157 return RewriteResponse(REWRITE_DONE
, mkRationalNode(qZero
));
159 } else if((*i
).getKind() == kind::CONST_INTEGER
) {
160 if((*i
).getConst
<Integer
>() == intZero
) {
161 if(t
.getType().isInteger()) {
162 return RewriteResponse(REWRITE_DONE
, NodeManager::currentNM()->mkConst(intZero
));
164 return RewriteResponse(REWRITE_DONE
, mkRationalNode(qZero
));
169 return RewriteResponse(REWRITE_DONE
, t
);
171 RewriteResponse
ArithRewriter::preRewritePlus(TNode t
){
172 Assert(t
.getKind()== kind::PLUS
);
174 return RewriteResponse(REWRITE_DONE
, t
);
177 RewriteResponse
ArithRewriter::postRewritePlus(TNode t
){
178 Assert(t
.getKind()== kind::PLUS
);
180 Polynomial res
= Polynomial::mkZero();
182 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
184 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
186 res
= res
+ currPoly
;
189 return RewriteResponse(REWRITE_DONE
, res
.getNode());
192 RewriteResponse
ArithRewriter::postRewriteMult(TNode t
){
193 Assert(t
.getKind()== kind::MULT
);
195 Polynomial res
= Polynomial::mkOne();
197 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
199 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
201 res
= res
* currPoly
;
204 return RewriteResponse(REWRITE_DONE
, res
.getNode());
207 RewriteResponse
ArithRewriter::postRewriteAtomConstantRHS(TNode t
){
211 Comparison cmp
= Comparison::mkNormalComparison(t
.getKind(), Polynomial::parsePolynomial(left
), Constant(right
));
213 Assert(cmp
.isNormalForm());
214 return RewriteResponse(REWRITE_DONE
, cmp
.getNode());
217 RewriteResponse
ArithRewriter::postRewriteAtom(TNode atom
){
219 TNode left
= atom
[0];
220 TNode right
= atom
[1];
222 if(right
.getMetaKind() == kind::metakind::CONSTANT
){
223 return postRewriteAtomConstantRHS(atom
);
225 Polynomial pleft
= Polynomial::parsePolynomial(left
);
226 Polynomial pright
= Polynomial::parsePolynomial(right
);
228 Polynomial diff
= pleft
- pright
;
230 Constant cZero
= Constant::mkConstant(Rational(0));
231 Node reduction
= NodeManager::currentNM()->mkNode(atom
.getKind(), diff
.getNode(), cZero
.getNode());
233 return postRewriteAtomConstantRHS(reduction
);
237 RewriteResponse
ArithRewriter::preRewriteAtom(TNode atom
){
238 Assert(isAtom(atom
));
240 NodeManager
* currNM
= NodeManager::currentNM();
242 if(atom
.getKind() == kind::EQUAL
) {
243 if(atom
[0] == atom
[1]) {
244 return RewriteResponse(REWRITE_DONE
, currNM
->mkConst(true));
246 }else if(atom
.getKind() == kind::GT
){
247 Node leq
= currNM
->mkNode(kind::LEQ
, atom
[0], atom
[1]);
248 return RewriteResponse(REWRITE_DONE
, currNM
->mkNode(kind::NOT
, leq
));
249 }else if(atom
.getKind() == kind::LT
){
250 Node geq
= currNM
->mkNode(kind::GEQ
, atom
[0], atom
[1]);
251 return RewriteResponse(REWRITE_DONE
, currNM
->mkNode(kind::NOT
, geq
));
254 return RewriteResponse(REWRITE_DONE
, atom
);
257 RewriteResponse
ArithRewriter::postRewrite(TNode t
){
259 RewriteResponse response
= postRewriteTerm(t
);
260 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
261 Polynomial::parsePolynomial(response
.node
);
265 RewriteResponse response
= postRewriteAtom(t
);
266 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
267 Comparison::parseNormalForm(response
.node
);
272 return RewriteResponse(REWRITE_DONE
, Node::null());
276 RewriteResponse
ArithRewriter::preRewrite(TNode t
){
278 return preRewriteTerm(t
);
280 return preRewriteAtom(t
);
283 return RewriteResponse(REWRITE_DONE
, Node::null());
287 Node
ArithRewriter::makeUnaryMinusNode(TNode n
){
288 Rational
qNegOne(-1);
289 return NodeManager::currentNM()->mkNode(kind::MULT
, mkRationalNode(qNegOne
),n
);
292 Node
ArithRewriter::makeSubtractionNode(TNode l
, TNode r
){
293 Node negR
= makeUnaryMinusNode(r
);
294 Node diff
= NodeManager::currentNM()->mkNode(kind::PLUS
, l
, negR
);
299 RewriteResponse
ArithRewriter::rewriteDivByConstant(TNode t
, bool pre
){
300 Assert(t
.getKind()== kind::DIVISION
);
304 Assert(right
.getKind()== kind::CONST_RATIONAL
);
307 const Rational
& den
= right
.getConst
<Rational
>();
309 Assert(den
!= Rational(0));
311 Rational div
= den
.inverse();
313 Node result
= mkRationalNode(div
);
315 Node mult
= NodeManager::currentNM()->mkNode(kind::MULT
,left
,result
);
317 return RewriteResponse(REWRITE_DONE
, mult
);
319 return RewriteResponse(REWRITE_AGAIN
, mult
);
323 }/* CVC4::theory::arith namespace */
324 }/* CVC4::theory namespace */
325 }/* CVC4 namespace */