1 /********************* */
2 /*! \file arith_rewriter.cpp
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 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
21 #include "theory/arith/arith_rewriter.h"
22 #include "theory/arith/arith_utilities.h"
30 using namespace CVC4::theory
;
31 using namespace CVC4::theory::arith
;
37 Kind
multKind(Kind k
, int sgn
);
40 * Performs a quick check to see if it is easy to rewrite to
43 * Also writes relations with constants on both sides to TRUE or FALSE.
44 * If it can, it returns true and sets res to this value.
46 * This is for optimizing rewriteAtom() to avoid the more compuationally
47 * expensive general rewriting procedure.
49 * If simplification is not done, it returns Node::null()
51 Node
almostVarOrConstEqn(TNode atom
, Kind k
, TNode left
, TNode right
){
52 Assert(atom
.getKind() == k
);
53 Assert(isRelationOperator(k
));
54 Assert(atom
[0] == left
);
55 Assert(atom
[1] == right
);
56 bool leftIsConst
= left
.getMetaKind() == kind::metakind::CONSTANT
;
57 bool rightIsConst
= right
.getMetaKind() == kind::metakind::CONSTANT
;
59 bool leftIsVar
= left
.getMetaKind() == kind::metakind::VARIABLE
;
60 bool rightIsVar
= right
.getMetaKind() == kind::metakind::VARIABLE
;
62 if(leftIsConst
&& rightIsConst
){
63 Rational lc
= coerceToRational(left
);
64 Rational rc
= coerceToRational(right
);
65 bool res
= evaluateConstantPredicate(k
,lc
, rc
);
66 return mkBoolNode(res
);
67 }else if(leftIsVar
&& rightIsConst
){
68 if(right
.getKind() == kind::CONST_RATIONAL
){
71 return NodeManager::currentNM()->mkNode(k
,left
,coerceToRationalNode(right
));
73 }else if(leftIsConst
&& rightIsVar
){
74 if(left
.getKind() == kind::CONST_RATIONAL
){
75 return NodeManager::currentNM()->mkNode(multKind(k
,-1),right
,left
);
77 Node q_left
= coerceToRationalNode(left
);
78 return NodeManager::currentNM()->mkNode(multKind(k
,-1),right
,q_left
);
85 Node
ArithRewriter::rewriteAtomCore(TNode atom
){
87 Kind k
= atom
.getKind();
88 Assert(isRelationOperator(k
));
92 TNode right
= atom
[1];
94 Node nf
= almostVarOrConstEqn(atom
, k
,left
,right
);
95 if(nf
!= Node::null() ){
100 //Transform this to: (left- right) |><| 0
101 Node diff
= makeSubtractionNode(left
, right
);
103 Node rewritten
= rewrite(diff
);
104 // rewritten =_{Reals} left - right => rewritten |><| 0
106 if(rewritten
.getMetaKind() == kind::metakind::CONSTANT
){
107 // Case 1 rewritten : c
108 Rational c
= rewritten
.getConst
<Rational
>();
109 bool res
= evaluateConstantPredicate(k
, c
, d_constants
->d_ZERO
);
110 nf
= mkBoolNode(res
);
111 }else if(rewritten
.getMetaKind() == kind::metakind::VARIABLE
){
112 // Case 2 rewritten : v
113 nf
= NodeManager::currentNM()->mkNode(k
, rewritten
, d_constants
->d_ZERO_NODE
);
115 // Case 3 rewritten : (+ c p_1 p_2 ... p_N) | not(N=1 and c=0 and p_1.d=1)
116 Rational c
= rewritten
[0].getConst
<Rational
>();
118 TNode p_1
= rewritten
[1];
119 Rational d
= p_1
[0].getConst
<Rational
>();
122 Node newRight
= mkRationalNode(c
);
123 Kind newKind
= multKind(k
, d
.sgn());
124 int N
= rewritten
.getNumChildren() - 1;
127 int M
= p_1
.getNumChildren()-1;
128 if(M
== 1){ // v |><| b
130 nf
= NodeManager::currentNM()->mkNode(newKind
, v
, newRight
);
132 Node newLeft
= multPnfByNonZero(p_1
, d
);
133 nf
= NodeManager::currentNM()->mkNode(newKind
, newLeft
, newRight
);
135 }else{ //(+ p_1 .. p_N) |><| b
136 NodeBuilder
<> plus(kind::PLUS
);
137 for(int i
=1; i
<=N
; ++i
){
138 TNode p_i
= rewritten
[i
];
139 plus
<< multPnfByNonZero(p_i
, d
);
142 nf
= NodeManager::currentNM()->mkNode(newKind
, newLeft
, newRight
);
149 Node
ArithRewriter::rewriteAtom(TNode atom
){
150 Node rewritten
= rewriteAtomCore(atom
);
151 if(rewritten
.getKind() == kind::LT
){
152 Node geq
= NodeManager::currentNM()->mkNode(kind::GEQ
, rewritten
[0], rewritten
[1]);
153 return NodeManager::currentNM()->mkNode(kind::NOT
, geq
);
154 }else if(rewritten
.getKind() == kind::GT
){
155 Node leq
= NodeManager::currentNM()->mkNode(kind::LEQ
, rewritten
[0], rewritten
[1]);
156 return NodeManager::currentNM()->mkNode(kind::NOT
, leq
);
163 /* cmp( (* d v_1 v_2 ... v_M), (* d' v'_1 v'_2 ... v'_M'):
165 * then tupleCompare(v_i, v'_i)
169 bool operator()(Node p0
, Node p1
) {
170 int p0_M
= p0
.getNumChildren() -1;
171 int p1_M
= p1
.getNumChildren() -1;
173 for(int i
=1; i
<= p0_M
; ++i
){
175 return p0
[i
] < p1
[i
];
178 return false; //p0 == p1 in this order
185 //Two pnfs are equal up to their coefficients
186 bool pnfsMatch(TNode p0
, TNode p1
){
188 unsigned M
= p0
.getNumChildren()-1;
189 if (M
+1 != p1
.getNumChildren()){
193 for(unsigned i
=1; i
<= M
; ++i
){
200 Node
addMatchingPnfs(TNode p0
, TNode p1
){
201 Assert(pnfsMatch(p0
,p1
));
203 unsigned M
= p0
.getNumChildren()-1;
205 Rational c0
= p0
[0].getConst
<Rational
>();
206 Rational c1
= p1
[0].getConst
<Rational
>();
208 Rational addedC
= c0
+ c1
;
209 Node newC
= mkRationalNode(addedC
);
210 NodeBuilder
<> nb(kind::MULT
);
212 for(unsigned i
=1; i
<= M
; ++i
){
219 void ArithRewriter::sortAndCombineCoefficients(std::vector
<Node
>& pnfs
){
222 /* combined contains exactly 1 representative per for each pnf.
223 * This is maintained by combining the coefficients for pnfs.
224 * that is equal according to pnfLessThan.
226 typedef set
<Node
, pnfLessThan
> PnfSet
;
229 for(vector
<Node
>::iterator i
=pnfs
.begin(); i
!= pnfs
.end(); ++i
){
231 PnfSet::iterator pos
= combined
.find(pnf
);
233 if(pos
== combined
.end()){
234 combined
.insert(pnf
);
237 Node sum
= addMatchingPnfs(pnf
, current
);
239 combined
.insert(sum
);
243 for(PnfSet::iterator i
=combined
.begin(); i
!= combined
.end(); ++i
){
245 if(pnf
[0].getConst
<Rational
>() != d_constants
->d_ZERO
){
246 //after combination the coefficient may be zero
252 Node
ArithRewriter::var2pnf(TNode variable
){
253 return NodeManager::currentNM()->mkNode(kind::MULT
,d_constants
->d_ONE_NODE
,variable
);
256 Node
ArithRewriter::rewritePlus(TNode t
){
259 Rational accumulator
;
262 for(TNode::iterator i
= t
.begin(); i
!= t
.end(); ++i
){
264 Node rewrittenChild
= rewrite(child
);
266 if(rewrittenChild
.getMetaKind() == kind::metakind::CONSTANT
){//c
267 Rational c
= rewrittenChild
.getConst
<Rational
>();
268 accumulator
= accumulator
+ c
;
269 }else if(rewrittenChild
.getMetaKind() == kind::metakind::VARIABLE
){ //v
270 Node pnf
= var2pnf(rewrittenChild
);
272 }else{ //(+ c p_1 p_2 ... p_N)
273 Rational c
= rewrittenChild
[0].getConst
<Rational
>();
274 accumulator
= accumulator
+ c
;
275 int N
= rewrittenChild
.getNumChildren() - 1;
276 for(int i
=1; i
<=N
; ++i
){
277 TNode pnf
= rewrittenChild
[i
];
282 sortAndCombineCoefficients(pnfs
);
283 if(pnfs
.size() == 0){
284 return mkRationalNode(accumulator
);
289 //Enforce not(N=1 and c=0 and p_1.d=1)
290 if(pnfs
.size() == 1){
291 Node p_1
= *(pnfs
.begin());
292 if(p_1
[0].getConst
<Rational
>() == d_constants
->d_ONE
){
293 if(accumulator
== d_constants
->d_ZERO
){ // 0 + (* 1 var) |-> var
300 //We must be in this case
301 //(+ c p_1 p_2 ... p_N) | not(N=1 and c=0 and p_1.d=1)
303 NodeBuilder
<> nb(kind::PLUS
);
304 nb
<< mkRationalNode(accumulator
);
305 Debug("arithrewrite") << mkRationalNode(accumulator
) << std::endl
;
306 for(vector
<Node
>::iterator i
= pnfs
.begin(); i
!= pnfs
.end(); ++i
){
308 Debug("arithrewrite") << (*i
) << std::endl
;
312 Node normalForm
= nb
;
317 //5) v_i are of metakind VARIABLE,
318 //6) v_i are in increasing (not strict) nodeOrder,
319 Node
toPnf(Rational
& c
, std::set
<Node
>& variables
){
320 NodeBuilder
<> nb(kind::MULT
);
321 nb
<< mkRationalNode(c
);
323 for(std::set
<Node
>::iterator i
= variables
.begin(); i
!= variables
.end(); ++i
){
330 Node
distribute(TNode n
, TNode sum
){
331 NodeBuilder
<> nb(kind::PLUS
);
332 for(TNode::iterator i
=sum
.begin(); i
!=sum
.end(); ++i
){
333 Node prod
= NodeManager::currentNM()->mkNode(kind::MULT
, n
, *i
);
338 Node
distributeSum(TNode sum
, TNode distribSum
){
339 NodeBuilder
<> nb(kind::PLUS
);
340 for(TNode::iterator i
=sum
.begin(); i
!=sum
.end(); ++i
){
341 Node dist
= distribute(*i
, distribSum
);
342 for(Node::iterator j
=dist
.begin(); j
!=dist
.end(); ++j
){
349 Node
ArithRewriter::rewriteMult(TNode t
){
353 Rational
accumulator(1,1);
357 //These stacks need to be kept in lock step
358 stack
<TNode
> mult_iterators_nodes
;
359 stack
<TNode::const_iterator
> mult_iterators_iters
;
361 mult_iterators_nodes
.push(t
);
362 mult_iterators_iters
.push(t
.begin());
364 while(!mult_iterators_nodes
.empty()){
365 TNode mult
= mult_iterators_nodes
.top();
366 TNode::const_iterator i
= mult_iterators_iters
.top();
368 mult_iterators_nodes
.pop();
369 mult_iterators_iters
.pop();
371 for(; i
!= mult
.end(); ++i
){
373 if(child
.getKind() == kind::MULT
){ //TODO add not rewritten already checks
375 mult_iterators_nodes
.push(mult
);
376 mult_iterators_iters
.push(i
);
378 mult_iterators_nodes
.push(child
);
379 mult_iterators_iters
.push(child
.begin());
382 Node rewrittenChild
= rewrite(child
);
384 if(rewrittenChild
.getMetaKind() == kind::metakind::CONSTANT
){//c
385 Rational c
= rewrittenChild
.getConst
<Rational
>();
386 accumulator
= accumulator
* c
;
387 if(accumulator
== d_constants
->d_ZERO
){
388 return d_constants
->d_ZERO_NODE
;
390 }else if(rewrittenChild
.getMetaKind() == kind::metakind::VARIABLE
){ //v
391 variables
.insert(rewrittenChild
);
392 }else{ //(+ c p_1 p_2 ... p_N)
393 sums
.push_back(rewrittenChild
);
397 // accumulator * (\prod var_i) *(\prod sum_j)
399 if(sums
.size() == 0){ //accumulator * (\prod var_i)
400 if(variables
.size() == 0){ //accumulator
401 return mkRationalNode(accumulator
);
402 }else if(variables
.size() == 1 && accumulator
== d_constants
->d_ONE
){ // var_1
403 Node var
= *(variables
.begin());
406 //We need to return (+ c p_1 p_2 ... p_N)
407 //To accomplish this:
408 // let pnf = pnf(accumulator * (\prod var_i)) in (+ 0 pnf)
409 Node pnf
= toPnf(accumulator
, variables
);
410 Node normalForm
= NodeManager::currentNM()->mkNode(kind::PLUS
, d_constants
->d_ZERO_NODE
, pnf
);
414 vector
<Node
>::iterator sum_iter
= sums
.begin();
417 // where A = lfp {\prod s | s \in Q \cup Variables \cup A}
418 Node distributed
= *sum_iter
;
420 while(sum_iter
!= sums
.end()){
421 Node curr
= *sum_iter
;
422 distributed
= distributeSum(curr
, distributed
);
425 if(variables
.size() >= 1){
426 Node pnf
= toPnf(accumulator
, variables
);
427 distributed
= distribute(pnf
, distributed
);
429 Node constant
= mkRationalNode(accumulator
);
430 distributed
= distribute(constant
, distributed
);
433 Node nf_distributed
= rewrite(distributed
);
434 return nf_distributed
;
438 Node
ArithRewriter::rewriteConstantDiv(TNode t
){
439 Assert(t
.getKind()== kind::DIVISION
);
441 Node reLeft
= rewrite(t
[0]);
442 Node reRight
= rewrite(t
[1]);
443 Assert(reLeft
.getKind()== kind::CONST_RATIONAL
);
444 Assert(reRight
.getKind()== kind::CONST_RATIONAL
);
446 Rational num
= reLeft
.getConst
<Rational
>();
447 Rational den
= reRight
.getConst
<Rational
>();
449 Assert(den
!= d_constants
->d_ZERO
);
451 Rational div
= num
/ den
;
453 Node result
= mkRationalNode(div
);
458 Node
ArithRewriter::rewriteTerm(TNode t
){
459 if(t
.getMetaKind() == kind::metakind::CONSTANT
){
460 return coerceToRationalNode(t
);
461 }else if(t
.getMetaKind() == kind::metakind::VARIABLE
){
463 }else if(t
.getKind() == kind::MULT
){
464 return rewriteMult(t
);
465 }else if(t
.getKind() == kind::PLUS
){
466 return rewritePlus(t
);
467 }else if(t
.getKind() == kind::DIVISION
){
468 return rewriteConstantDiv(t
);
469 }else if(t
.getKind() == kind::MINUS
){
470 Node sub
= makeSubtractionNode(t
[0],t
[1]);
472 }else if(t
.getKind() == kind::UMINUS
){
473 Node sub
= makeUnaryMinusNode(t
[0]);
483 * Given a node in PNF pnf = (* d p_1 p_2 .. p_M) and a rational q != 0
484 * constuct a node equal to q * pnf that is in pnf.
486 * The claim is that this is always okay:
487 * If d' = q*d, p' = (* d' p_1 p_2 .. p_M) =_{Reals} q * pnf.
489 Node
ArithRewriter::multPnfByNonZero(TNode pnf
, Rational
& q
){
490 Assert(q
!= d_constants
->d_ZERO
);
491 //TODO Assert(isPNF(pnf) );
493 int M
= pnf
.getNumChildren()-1;
494 Rational d
= pnf
[0].getConst
<Rational
>();
495 Rational new_d
= d
*q
;
498 NodeBuilder
<> mult(kind::MULT
);
499 mult
<< mkRationalNode(new_d
);
500 for(int i
=1; i
<=M
; ++i
){
508 Node
ArithRewriter::makeUnaryMinusNode(TNode n
){
509 Node tmp
= NodeManager::currentNM()->mkNode(kind::MULT
,d_constants
->d_NEGATIVE_ONE_NODE
,n
);
513 Node
ArithRewriter::makeSubtractionNode(TNode l
, TNode r
){
514 Node negR
= makeUnaryMinusNode(r
);
515 Node diff
= NodeManager::currentNM()->mkNode(kind::PLUS
, l
, negR
);
521 Kind
multKind(Kind k
, int sgn
){
522 using namespace kind
;
528 case LEQ
: return GEQ
;
529 case EQUAL
: return EQUAL
;
530 case GEQ
: return LEQ
;
541 Node
ArithRewriter::rewrite(TNode n
){
542 Debug("arithrewriter") << "Trace rewrite:" << n
<< std::endl
;
546 if(isRelationOperator(n
.getKind())){
547 res
= rewriteAtom(n
);
549 res
= rewriteTerm(n
);
552 Debug("arithrewriter") << "Trace rewrite:" << n
<< "|->"<< res
<< std::endl
;