1 /********************* */
2 /*! \file arith_rewriter.cpp
4 ** Original author: taking
5 ** Major contributors: dejan
6 ** Minor contributors (to current version): mdeters
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
);
100 RewriteResponse
ArithRewriter::postRewriteTerm(TNode t
){
101 if(t
.getMetaKind() == kind::metakind::CONSTANT
){
102 return rewriteConstant(t
);
103 }else if(isVariable(t
)){
104 return rewriteVariable(t
);
105 }else if(t
.getKind() == kind::MINUS
){
106 return rewriteMinus(t
, false);
107 }else if(t
.getKind() == kind::UMINUS
){
108 return rewriteUMinus(t
, false);
109 }else if(t
.getKind() == kind::DIVISION
){
110 return rewriteDivByConstant(t
, false);
111 }else if(t
.getKind() == kind::PLUS
){
112 return postRewritePlus(t
);
113 }else if(t
.getKind() == kind::MULT
){
114 return postRewriteMult(t
);
120 RewriteResponse
ArithRewriter::preRewriteMult(TNode t
){
121 Assert(t
.getKind()== kind::MULT
);
123 // Rewrite multiplications with a 0 argument and to 0
128 for(TNode::iterator i
= t
.begin(); i
!= t
.end(); ++i
) {
129 if((*i
).getKind() == kind::CONST_RATIONAL
) {
130 if((*i
).getConst
<Rational
>() == qZero
) {
131 return RewriteResponse(REWRITE_DONE
, mkRationalNode(qZero
));
133 } else if((*i
).getKind() == kind::CONST_INTEGER
) {
134 if((*i
).getConst
<Integer
>() == intZero
) {
135 if(t
.getType().isInteger()) {
136 return RewriteResponse(REWRITE_DONE
, NodeManager::currentNM()->mkConst(intZero
));
138 return RewriteResponse(REWRITE_DONE
, mkRationalNode(qZero
));
143 return RewriteResponse(REWRITE_DONE
, t
);
145 RewriteResponse
ArithRewriter::preRewritePlus(TNode t
){
146 Assert(t
.getKind()== kind::PLUS
);
148 return RewriteResponse(REWRITE_DONE
, t
);
151 RewriteResponse
ArithRewriter::postRewritePlus(TNode t
){
152 Assert(t
.getKind()== kind::PLUS
);
154 Polynomial res
= Polynomial::mkZero();
156 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
158 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
160 res
= res
+ currPoly
;
163 return RewriteResponse(REWRITE_DONE
, res
.getNode());
166 RewriteResponse
ArithRewriter::postRewriteMult(TNode t
){
167 Assert(t
.getKind()== kind::MULT
);
169 Polynomial res
= Polynomial::mkOne();
171 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
173 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
175 res
= res
* currPoly
;
178 return RewriteResponse(REWRITE_DONE
, res
.getNode());
181 RewriteResponse
ArithRewriter::postRewriteAtomConstantRHS(TNode t
){
185 Comparison cmp
= Comparison::mkComparison(t
.getKind(), Polynomial::parsePolynomial(left
), Constant(right
));
188 return RewriteResponse(REWRITE_DONE
, cmp
.getNode());
191 if(cmp
.getLeft().containsConstant()){
192 Monomial constantHead
= cmp
.getLeft().getHead();
193 Assert(constantHead
.isConstant());
195 Constant constant
= constantHead
.getConstant();
197 Constant negativeConstantHead
= -constant
;
199 cmp
= cmp
.addConstant(negativeConstantHead
);
201 Assert(!cmp
.getLeft().containsConstant());
203 if(!cmp
.getLeft().getHead().coefficientIsOne()){
204 Monomial constantHead
= cmp
.getLeft().getHead();
205 Assert(!constantHead
.isConstant());
206 Constant constant
= constantHead
.getConstant();
208 Constant inverse
= Constant::mkConstant(constant
.getValue().inverse());
210 cmp
= cmp
.multiplyConstant(inverse
);
212 Assert(cmp
.getLeft().getHead().coefficientIsOne());
214 Assert(cmp
.isBoolean() || cmp
.isNormalForm());
215 return RewriteResponse(REWRITE_DONE
, cmp
.getNode());
218 RewriteResponse
ArithRewriter::postRewriteAtom(TNode atom
){
220 TNode left
= atom
[0];
221 TNode right
= atom
[1];
223 if(right
.getMetaKind() == kind::metakind::CONSTANT
){
224 return postRewriteAtomConstantRHS(atom
);
226 //Transform this to: (left - right) |><| 0
227 Node diff
= makeSubtractionNode(left
, right
);
229 Node reduction
= NodeManager::currentNM()->mkNode(atom
.getKind(), diff
, mkRationalNode(qZero
));
230 return RewriteResponse(REWRITE_AGAIN_FULL
, reduction
);
234 RewriteResponse
ArithRewriter::preRewriteAtom(TNode atom
){
235 Assert(isAtom(atom
));
237 NodeManager
* currNM
= NodeManager::currentNM();
239 if(atom
.getKind() == kind::EQUAL
) {
240 if(atom
[0] == atom
[1]) {
241 return RewriteResponse(REWRITE_DONE
, currNM
->mkConst(true));
245 Node reduction
= atom
;
247 if(atom
[1].getMetaKind() != kind::metakind::CONSTANT
) {
249 TNode left
= atom
[0];
250 TNode right
= atom
[1];
252 //Transform this to: (left - right) |><| 0
253 Node diff
= makeSubtractionNode(left
, right
);
255 reduction
= currNM
->mkNode(atom
.getKind(), diff
, mkRationalNode(qZero
));
258 if(reduction
.getKind() == kind::GT
){
259 Node leq
= currNM
->mkNode(kind::LEQ
, reduction
[0], reduction
[1]);
260 reduction
= currNM
->mkNode(kind::NOT
, leq
);
261 }else if(reduction
.getKind() == kind::LT
){
262 Node geq
= currNM
->mkNode(kind::GEQ
, reduction
[0], reduction
[1]);
263 reduction
= currNM
->mkNode(kind::NOT
, geq
);
265 /* BREADCRUMB : Move this rewrite into preprocessing
266 else if( Options::current()->rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
267 Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
268 Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]);
269 reduction = currNM->mkNode(kind::AND, geq, leq);
274 return RewriteResponse(REWRITE_DONE
, reduction
);
277 RewriteResponse
ArithRewriter::postRewrite(TNode t
){
279 RewriteResponse response
= postRewriteTerm(t
);
280 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
281 Polynomial::parsePolynomial(response
.node
);
285 RewriteResponse response
= postRewriteAtom(t
);
286 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
287 Comparison::parseNormalForm(response
.node
);
292 return RewriteResponse(REWRITE_DONE
, Node::null());
296 RewriteResponse
ArithRewriter::preRewrite(TNode t
){
298 return preRewriteTerm(t
);
300 return preRewriteAtom(t
);
303 return RewriteResponse(REWRITE_DONE
, Node::null());
307 Node
ArithRewriter::makeUnaryMinusNode(TNode n
){
308 Rational
qNegOne(-1);
309 return NodeManager::currentNM()->mkNode(kind::MULT
, mkRationalNode(qNegOne
),n
);
312 Node
ArithRewriter::makeSubtractionNode(TNode l
, TNode r
){
313 Node negR
= makeUnaryMinusNode(r
);
314 Node diff
= NodeManager::currentNM()->mkNode(kind::PLUS
, l
, negR
);
319 RewriteResponse
ArithRewriter::rewriteDivByConstant(TNode t
, bool pre
){
320 Assert(t
.getKind()== kind::DIVISION
);
324 Assert(right
.getKind()== kind::CONST_RATIONAL
);
327 const Rational
& den
= right
.getConst
<Rational
>();
329 Assert(den
!= Rational(0));
331 Rational div
= den
.inverse();
333 Node result
= mkRationalNode(div
);
335 Node mult
= NodeManager::currentNM()->mkNode(kind::MULT
,left
,result
);
337 return RewriteResponse(REWRITE_DONE
, mult
);
339 return RewriteResponse(REWRITE_AGAIN
, mult
);