1 /********************* */
4 ** Original author: dejan
5 ** Major contributors: cconway
6 ** Minor contributors (to current version): mdeters
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
20 #include "cvc4_private.h"
22 #ifndef __CVC4__BOOLEAN_SIMPLIFICATION_H
23 #define __CVC4__BOOLEAN_SIMPLIFICATION_H
25 #include "expr/node.h"
26 #include "util/Assert.h"
32 class BooleanSimplification
{
35 static const uint32_t DUPLICATE_REMOVAL_THRESHOLD
= 10;
37 static void removeDuplicates(std::vector
<Node
>& buffer
){
38 if(buffer
.size() < DUPLICATE_REMOVAL_THRESHOLD
){
39 std::sort(buffer
.begin(), buffer
.end());
40 std::vector
<Node
>::iterator new_end
= std::unique(buffer
.begin(), buffer
.end());
41 buffer
.erase(new_end
, buffer
.end());
45 static Node
simplifyConflict(Node andNode
){
46 Assert(andNode
.getKind() == kind::AND
);
47 std::vector
<Node
> buffer
;
48 push_back_associative_commute(andNode
, buffer
, kind::AND
, kind::OR
, false);
50 removeDuplicates(buffer
);
52 NodeBuilder
<> nb(kind::AND
);
57 static Node
simplifyClause(Node orNode
){
58 Assert(orNode
.getKind() == kind::OR
);
59 std::vector
<Node
> buffer
;
60 push_back_associative_commute(orNode
, buffer
, kind::OR
, kind::AND
, false);
62 removeDuplicates(buffer
);
64 NodeBuilder
<> nb(kind::OR
);
69 static Node
simplifyHornClause(Node implication
){
70 Assert(implication
.getKind() == kind::IMPLIES
);
71 TNode left
= implication
[0];
72 TNode right
= implication
[1];
73 Node notLeft
= NodeBuilder
<1>(kind::NOT
)<<left
;
74 Node clause
= NodeBuilder
<2>(kind::OR
)<< notLeft
<< right
;
75 return simplifyClause(clause
);
78 static void push_back_associative_commute(Node n
, std::vector
<Node
>& buffer
, Kind k
, Kind notK
, bool negateNode
){
79 Node::iterator i
= n
.begin(), end
= n
.end();
82 if(child
.getKind() == k
){
83 push_back_associative_commute(child
, buffer
, k
, notK
, negateNode
);
84 }else if(child
.getKind() == kind::NOT
&& child
[0].getKind() == notK
){
85 push_back_associative_commute(child
, buffer
, notK
, k
, !negateNode
);
88 buffer
.push_back(negate(child
));
90 buffer
.push_back(child
);
96 static Node
negate(TNode n
){
99 while(base
.getKind() == kind::NOT
){
101 polarity
= !polarity
;
104 return base
.notNode();
110 };/* class BitVector */
114 }/* CVC4 namespace */
116 #endif /* __CVC4__BITVECTOR_H */