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"
30 using namespace CVC4::theory
;
31 using namespace CVC4::theory::arith
;
33 bool isVariable(TNode t
){
34 return t
.getMetaKind() == kind::metakind::VARIABLE
;
37 RewriteResponse
ArithRewriter::rewriteConstant(TNode t
){
38 Assert(t
.getMetaKind() == kind::metakind::CONSTANT
);
39 Node val
= coerceToRationalNode(t
);
41 return RewriteResponse(REWRITE_DONE
, val
);
44 RewriteResponse
ArithRewriter::rewriteVariable(TNode t
){
45 Assert(isVariable(t
));
47 return RewriteResponse(REWRITE_DONE
, t
);
50 RewriteResponse
ArithRewriter::rewriteMinus(TNode t
, bool pre
){
51 Assert(t
.getKind()== kind::MINUS
);
55 Node zeroNode
= mkRationalNode(zero
);
56 return RewriteResponse(REWRITE_DONE
, zeroNode
);
59 Node noMinus
= makeSubtractionNode(t
[0],t
[1]);
61 return RewriteResponse(REWRITE_DONE
, noMinus
);
63 return RewriteResponse(REWRITE_AGAIN_FULL
, noMinus
);
67 RewriteResponse
ArithRewriter::rewriteUMinus(TNode t
, bool pre
){
68 Assert(t
.getKind()== kind::UMINUS
);
70 Node noUminus
= makeUnaryMinusNode(t
[0]);
72 return RewriteResponse(REWRITE_DONE
, noUminus
);
74 return RewriteResponse(REWRITE_AGAIN
, noUminus
);
77 RewriteResponse
ArithRewriter::preRewriteTerm(TNode t
){
78 if(t
.getMetaKind() == kind::metakind::CONSTANT
){
79 return rewriteConstant(t
);
80 }else if(isVariable(t
)){
81 return rewriteVariable(t
);
82 }else if(t
.getKind() == kind::MINUS
){
83 return rewriteMinus(t
, true);
84 }else if(t
.getKind() == kind::UMINUS
){
85 return rewriteUMinus(t
, true);
86 }else if(t
.getKind() == kind::DIVISION
){
87 if(t
[0].getKind()== kind::CONST_RATIONAL
){
88 return rewriteDivByConstant(t
, true);
90 return RewriteResponse(REWRITE_DONE
, t
);
92 }else if(t
.getKind() == kind::PLUS
){
93 return preRewritePlus(t
);
94 }else if(t
.getKind() == kind::MULT
){
95 return preRewriteMult(t
);
96 }else if(t
.getKind() == kind::INTS_DIVISION
){
98 if(t
[1].getKind()== kind::CONST_INTEGER
&& t
[1].getConst
<Integer
>() == intOne
){
99 return RewriteResponse(REWRITE_AGAIN
, t
[0]);
101 return RewriteResponse(REWRITE_DONE
, t
);
103 }else if(t
.getKind() == kind::INTS_MODULUS
){
105 if(t
[1].getKind()== kind::CONST_INTEGER
&& t
[1].getConst
<Integer
>() == intOne
){
107 return RewriteResponse(REWRITE_AGAIN
, mkIntegerNode(intZero
));
109 return RewriteResponse(REWRITE_DONE
, t
);
115 RewriteResponse
ArithRewriter::postRewriteTerm(TNode t
){
116 if(t
.getMetaKind() == kind::metakind::CONSTANT
){
117 return rewriteConstant(t
);
118 }else if(isVariable(t
)){
119 return rewriteVariable(t
);
120 }else if(t
.getKind() == kind::MINUS
){
121 return rewriteMinus(t
, false);
122 }else if(t
.getKind() == kind::UMINUS
){
123 return rewriteUMinus(t
, false);
124 }else if(t
.getKind() == kind::DIVISION
){
125 return rewriteDivByConstant(t
, false);
126 }else if(t
.getKind() == kind::PLUS
){
127 return postRewritePlus(t
);
128 }else if(t
.getKind() == kind::MULT
){
129 return postRewriteMult(t
);
130 }else if(t
.getKind() == kind::INTS_DIVISION
){
131 return RewriteResponse(REWRITE_DONE
, t
);
132 }else if(t
.getKind() == kind::INTS_MODULUS
){
133 return RewriteResponse(REWRITE_DONE
, t
);
139 RewriteResponse
ArithRewriter::preRewriteMult(TNode t
){
140 Assert(t
.getKind()== kind::MULT
);
142 // Rewrite multiplications with a 0 argument and to 0
147 for(TNode::iterator i
= t
.begin(); i
!= t
.end(); ++i
) {
148 if((*i
).getKind() == kind::CONST_RATIONAL
) {
149 if((*i
).getConst
<Rational
>() == qZero
) {
150 return RewriteResponse(REWRITE_DONE
, mkRationalNode(qZero
));
152 } else if((*i
).getKind() == kind::CONST_INTEGER
) {
153 if((*i
).getConst
<Integer
>() == intZero
) {
154 if(t
.getType().isInteger()) {
155 return RewriteResponse(REWRITE_DONE
, NodeManager::currentNM()->mkConst(intZero
));
157 return RewriteResponse(REWRITE_DONE
, mkRationalNode(qZero
));
162 return RewriteResponse(REWRITE_DONE
, t
);
164 RewriteResponse
ArithRewriter::preRewritePlus(TNode t
){
165 Assert(t
.getKind()== kind::PLUS
);
167 return RewriteResponse(REWRITE_DONE
, t
);
170 RewriteResponse
ArithRewriter::postRewritePlus(TNode t
){
171 Assert(t
.getKind()== kind::PLUS
);
173 Polynomial res
= Polynomial::mkZero();
175 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
177 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
179 res
= res
+ currPoly
;
182 return RewriteResponse(REWRITE_DONE
, res
.getNode());
185 RewriteResponse
ArithRewriter::postRewriteMult(TNode t
){
186 Assert(t
.getKind()== kind::MULT
);
188 Polynomial res
= Polynomial::mkOne();
190 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
192 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
194 res
= res
* currPoly
;
197 return RewriteResponse(REWRITE_DONE
, res
.getNode());
200 RewriteResponse
ArithRewriter::postRewriteAtomConstantRHS(TNode t
){
204 Comparison cmp
= Comparison::mkNormalComparison(t
.getKind(), Polynomial::parsePolynomial(left
), Constant(right
));
206 Assert(cmp
.isNormalForm());
207 return RewriteResponse(REWRITE_DONE
, cmp
.getNode());
210 // Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
212 // if(cmp.isBoolean()){
213 // return RewriteResponse(REWRITE_DONE, cmp.getNode());
216 // if(cmp.getLeft().containsConstant()){
217 // Monomial constantHead = cmp.getLeft().getHead();
218 // Assert(constantHead.isConstant());
220 // Constant constant = constantHead.getConstant();
222 // Constant negativeConstantHead = -constant;
224 // cmp = cmp.addConstant(negativeConstantHead);
226 // Assert(!cmp.getLeft().containsConstant());
228 // if(!cmp.getLeft().getHead().coefficientIsOne()){
229 // Monomial constantHead = cmp.getLeft().getHead();
230 // Assert(!constantHead.isConstant());
231 // Constant constant = constantHead.getConstant();
233 // Constant inverse = Constant::mkConstant(constant.getValue().inverse());
235 // cmp = cmp.multiplyConstant(inverse);
237 // Assert(cmp.getLeft().getHead().coefficientIsOne());
239 // Assert(cmp.isBoolean() || cmp.isNormalForm());
240 // return RewriteResponse(REWRITE_DONE, cmp.getNode());
243 RewriteResponse
ArithRewriter::postRewriteAtom(TNode atom
){
245 TNode left
= atom
[0];
246 TNode right
= atom
[1];
248 if(right
.getMetaKind() == kind::metakind::CONSTANT
){
249 return postRewriteAtomConstantRHS(atom
);
251 //Transform this to: (left - right) |><| 0
252 Node diff
= makeSubtractionNode(left
, right
);
254 Node reduction
= NodeManager::currentNM()->mkNode(atom
.getKind(), diff
, mkRationalNode(qZero
));
255 return RewriteResponse(REWRITE_AGAIN_FULL
, reduction
);
259 RewriteResponse
ArithRewriter::preRewriteAtom(TNode atom
){
260 Assert(isAtom(atom
));
262 NodeManager
* currNM
= NodeManager::currentNM();
264 if(atom
.getKind() == kind::EQUAL
) {
265 if(atom
[0] == atom
[1]) {
266 return RewriteResponse(REWRITE_DONE
, currNM
->mkConst(true));
270 Node reduction
= atom
;
272 if(atom
[1].getMetaKind() != kind::metakind::CONSTANT
) {
274 TNode left
= atom
[0];
275 TNode right
= atom
[1];
277 //Transform this to: (left - right) |><| 0
278 Node diff
= makeSubtractionNode(left
, right
);
280 reduction
= currNM
->mkNode(atom
.getKind(), diff
, mkRationalNode(qZero
));
283 if(reduction
.getKind() == kind::GT
){
284 Node leq
= currNM
->mkNode(kind::LEQ
, reduction
[0], reduction
[1]);
285 reduction
= currNM
->mkNode(kind::NOT
, leq
);
286 }else if(reduction
.getKind() == kind::LT
){
287 Node geq
= currNM
->mkNode(kind::GEQ
, reduction
[0], reduction
[1]);
288 reduction
= currNM
->mkNode(kind::NOT
, geq
);
290 /* BREADCRUMB : Move this rewrite into preprocessing
291 else if( Options::current()->rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
292 Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
293 Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]);
294 reduction = currNM->mkNode(kind::AND, geq, leq);
299 return RewriteResponse(REWRITE_DONE
, reduction
);
302 RewriteResponse
ArithRewriter::postRewrite(TNode t
){
304 RewriteResponse response
= postRewriteTerm(t
);
305 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
306 Polynomial::parsePolynomial(response
.node
);
310 RewriteResponse response
= postRewriteAtom(t
);
311 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
312 Comparison::parseNormalForm(response
.node
);
317 return RewriteResponse(REWRITE_DONE
, Node::null());
321 RewriteResponse
ArithRewriter::preRewrite(TNode t
){
323 return preRewriteTerm(t
);
325 return preRewriteAtom(t
);
328 return RewriteResponse(REWRITE_DONE
, Node::null());
332 Node
ArithRewriter::makeUnaryMinusNode(TNode n
){
333 Rational
qNegOne(-1);
334 return NodeManager::currentNM()->mkNode(kind::MULT
, mkRationalNode(qNegOne
),n
);
337 Node
ArithRewriter::makeSubtractionNode(TNode l
, TNode r
){
338 Node negR
= makeUnaryMinusNode(r
);
339 Node diff
= NodeManager::currentNM()->mkNode(kind::PLUS
, l
, negR
);
344 RewriteResponse
ArithRewriter::rewriteDivByConstant(TNode t
, bool pre
){
345 Assert(t
.getKind()== kind::DIVISION
);
349 Assert(right
.getKind()== kind::CONST_RATIONAL
);
352 const Rational
& den
= right
.getConst
<Rational
>();
354 Assert(den
!= Rational(0));
356 Rational div
= den
.inverse();
358 Node result
= mkRationalNode(div
);
360 Node mult
= NodeManager::currentNM()->mkNode(kind::MULT
,left
,result
);
362 return RewriteResponse(REWRITE_DONE
, mult
);
364 return RewriteResponse(REWRITE_AGAIN
, mult
);