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 arith::ArithConstants
* ArithRewriter::s_constants
= NULL
;
35 bool isVariable(TNode t
){
36 return t
.getMetaKind() == kind::metakind::VARIABLE
;
39 RewriteResponse
ArithRewriter::rewriteConstant(TNode t
){
40 Assert(t
.getMetaKind() == kind::metakind::CONSTANT
);
41 Node val
= coerceToRationalNode(t
);
43 return RewriteResponse(REWRITE_DONE
, val
);
46 RewriteResponse
ArithRewriter::rewriteVariable(TNode t
){
47 Assert(isVariable(t
));
49 return RewriteResponse(REWRITE_DONE
, t
);
52 RewriteResponse
ArithRewriter::rewriteMinus(TNode t
, bool pre
){
53 Assert(t
.getKind()== kind::MINUS
);
55 if(t
[0] == t
[1]) return RewriteResponse(REWRITE_DONE
, s_constants
->d_ZERO_NODE
);
57 Node noMinus
= makeSubtractionNode(t
[0],t
[1]);
59 return RewriteResponse(REWRITE_DONE
, noMinus
);
61 return RewriteResponse(REWRITE_AGAIN_FULL
, noMinus
);
65 RewriteResponse
ArithRewriter::rewriteUMinus(TNode t
, bool pre
){
66 Assert(t
.getKind()== kind::UMINUS
);
68 Node noUminus
= makeUnaryMinusNode(t
[0]);
70 return RewriteResponse(REWRITE_DONE
, noUminus
);
72 return RewriteResponse(REWRITE_AGAIN
, noUminus
);
75 RewriteResponse
ArithRewriter::preRewriteTerm(TNode t
){
76 if(t
.getMetaKind() == kind::metakind::CONSTANT
){
77 return rewriteConstant(t
);
78 }else if(isVariable(t
)){
79 return rewriteVariable(t
);
80 }else if(t
.getKind() == kind::MINUS
){
81 return rewriteMinus(t
, true);
82 }else if(t
.getKind() == kind::UMINUS
){
83 return rewriteUMinus(t
, true);
84 }else if(t
.getKind() == kind::DIVISION
){
85 if(t
[0].getKind()== kind::CONST_RATIONAL
){
86 return rewriteDivByConstant(t
, true);
88 return RewriteResponse(REWRITE_DONE
, t
);
90 }else if(t
.getKind() == kind::PLUS
){
91 return preRewritePlus(t
);
92 }else if(t
.getKind() == kind::MULT
){
93 return preRewriteMult(t
);
98 RewriteResponse
ArithRewriter::postRewriteTerm(TNode t
){
99 if(t
.getMetaKind() == kind::metakind::CONSTANT
){
100 return rewriteConstant(t
);
101 }else if(isVariable(t
)){
102 return rewriteVariable(t
);
103 }else if(t
.getKind() == kind::MINUS
){
104 return rewriteMinus(t
, false);
105 }else if(t
.getKind() == kind::UMINUS
){
106 return rewriteUMinus(t
, false);
107 }else if(t
.getKind() == kind::DIVISION
){
108 return rewriteDivByConstant(t
, false);
109 }else if(t
.getKind() == kind::PLUS
){
110 return postRewritePlus(t
);
111 }else if(t
.getKind() == kind::MULT
){
112 return postRewriteMult(t
);
118 RewriteResponse
ArithRewriter::preRewriteMult(TNode t
){
119 Assert(t
.getKind()== kind::MULT
);
121 // Rewrite multiplications with a 0 argument and to 0
124 for(TNode::iterator i
= t
.begin(); i
!= t
.end(); ++i
) {
125 if((*i
).getKind() == kind::CONST_RATIONAL
) {
126 if((*i
).getConst
<Rational
>() == s_constants
->d_ZERO
) {
127 return RewriteResponse(REWRITE_DONE
, s_constants
->d_ZERO_NODE
);
129 } else if((*i
).getKind() == kind::CONST_INTEGER
) {
130 if((*i
).getConst
<Integer
>() == intZero
) {
131 if(t
.getType().isInteger()) {
132 return RewriteResponse(REWRITE_DONE
, NodeManager::currentNM()->mkConst(intZero
));
134 return RewriteResponse(REWRITE_DONE
, s_constants
->d_ZERO_NODE
);
139 return RewriteResponse(REWRITE_DONE
, t
);
141 RewriteResponse
ArithRewriter::preRewritePlus(TNode t
){
142 Assert(t
.getKind()== kind::PLUS
);
144 return RewriteResponse(REWRITE_DONE
, t
);
147 RewriteResponse
ArithRewriter::postRewritePlus(TNode t
){
148 Assert(t
.getKind()== kind::PLUS
);
150 Polynomial res
= Polynomial::mkZero();
152 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
154 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
156 res
= res
+ currPoly
;
159 return RewriteResponse(REWRITE_DONE
, res
.getNode());
162 RewriteResponse
ArithRewriter::postRewriteMult(TNode t
){
163 Assert(t
.getKind()== kind::MULT
);
165 Polynomial res
= Polynomial::mkOne();
167 for(TNode::iterator i
= t
.begin(), end
= t
.end(); i
!= end
; ++i
){
169 Polynomial currPoly
= Polynomial::parsePolynomial(curr
);
171 res
= res
* currPoly
;
174 return RewriteResponse(REWRITE_DONE
, res
.getNode());
177 RewriteResponse
ArithRewriter::postRewriteAtomConstantRHS(TNode t
){
182 Comparison cmp
= Comparison::mkComparison(t
.getKind(), Polynomial::parsePolynomial(left
), Constant(right
));
185 return RewriteResponse(REWRITE_DONE
, cmp
.getNode());
188 if(cmp
.getLeft().containsConstant()){
189 Monomial constantHead
= cmp
.getLeft().getHead();
190 Assert(constantHead
.isConstant());
192 Constant constant
= constantHead
.getConstant();
194 Constant negativeConstantHead
= -constant
;
196 cmp
= cmp
.addConstant(negativeConstantHead
);
198 Assert(!cmp
.getLeft().containsConstant());
200 if(!cmp
.getLeft().getHead().coefficientIsOne()){
201 Monomial constantHead
= cmp
.getLeft().getHead();
202 Assert(!constantHead
.isConstant());
203 Constant constant
= constantHead
.getConstant();
205 Constant inverse
= Constant::mkConstant(constant
.getValue().inverse());
207 cmp
= cmp
.multiplyConstant(inverse
);
209 Assert(cmp
.getLeft().getHead().coefficientIsOne());
211 Assert(cmp
.isBoolean() || cmp
.isNormalForm());
212 return RewriteResponse(REWRITE_DONE
, cmp
.getNode());
215 RewriteResponse
ArithRewriter::postRewriteAtom(TNode atom
){
217 TNode left
= atom
[0];
218 TNode right
= atom
[1];
220 if(right
.getMetaKind() == kind::metakind::CONSTANT
){
221 return postRewriteAtomConstantRHS(atom
);
223 //Transform this to: (left - right) |><| 0
224 Node diff
= makeSubtractionNode(left
, right
);
225 Node reduction
= NodeManager::currentNM()->mkNode(atom
.getKind(), diff
, s_constants
->d_ZERO_NODE
);
226 return RewriteResponse(REWRITE_AGAIN_FULL
, reduction
);
230 RewriteResponse
ArithRewriter::preRewriteAtom(TNode atom
){
231 Assert(isAtom(atom
));
232 NodeManager
* currNM
= NodeManager::currentNM();
234 if(atom
.getKind() == kind::EQUAL
) {
235 if(atom
[0] == atom
[1]) {
236 return RewriteResponse(REWRITE_DONE
, currNM
->mkConst(true));
240 Node reduction
= atom
;
242 if(atom
[1].getMetaKind() != kind::metakind::CONSTANT
){
244 TNode left
= atom
[0];
245 TNode right
= atom
[1];
247 //Transform this to: (left - right) |><| 0
248 Node diff
= makeSubtractionNode(left
, right
);
249 reduction
= currNM
->mkNode(atom
.getKind(), diff
, s_constants
->d_ZERO_NODE
);
252 if(reduction
.getKind() == kind::GT
){
253 Node leq
= currNM
->mkNode(kind::LEQ
, reduction
[0], reduction
[1]);
254 reduction
= currNM
->mkNode(kind::NOT
, leq
);
255 }else if(reduction
.getKind() == kind::LT
){
256 Node geq
= currNM
->mkNode(kind::GEQ
, reduction
[0], reduction
[1]);
257 reduction
= currNM
->mkNode(kind::NOT
, geq
);
260 return RewriteResponse(REWRITE_DONE
, reduction
);
263 RewriteResponse
ArithRewriter::postRewrite(TNode t
){
265 RewriteResponse response
= postRewriteTerm(t
);
266 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
267 Polynomial::parsePolynomial(response
.node
);
271 RewriteResponse response
= postRewriteAtom(t
);
272 if(Debug
.isOn("arith::rewriter") && response
.status
== REWRITE_DONE
) {
273 Comparison::parseNormalForm(response
.node
);
278 return RewriteResponse(REWRITE_DONE
, Node::null());
282 RewriteResponse
ArithRewriter::preRewrite(TNode t
){
284 return preRewriteTerm(t
);
286 return preRewriteAtom(t
);
289 return RewriteResponse(REWRITE_DONE
, Node::null());
293 Node
ArithRewriter::makeUnaryMinusNode(TNode n
){
294 return NodeManager::currentNM()->mkNode(kind::MULT
,s_constants
->d_NEGATIVE_ONE_NODE
,n
);
297 Node
ArithRewriter::makeSubtractionNode(TNode l
, TNode r
){
298 Node negR
= makeUnaryMinusNode(r
);
299 Node diff
= NodeManager::currentNM()->mkNode(kind::PLUS
, l
, negR
);
304 RewriteResponse
ArithRewriter::rewriteDivByConstant(TNode t
, bool pre
){
305 Assert(t
.getKind()== kind::DIVISION
);
309 Assert(right
.getKind()== kind::CONST_RATIONAL
);
312 const Rational
& den
= right
.getConst
<Rational
>();
314 Assert(den
!= s_constants
->d_ZERO
);
316 Rational div
= den
.inverse();
318 Node result
= mkRationalNode(div
);
320 Node mult
= NodeManager::currentNM()->mkNode(kind::MULT
,left
,result
);
322 return RewriteResponse(REWRITE_DONE
, mult
);
324 return RewriteResponse(REWRITE_AGAIN
, mult
);