1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
/********************* */
/*! \file boolean_simplification.h
** \verbatim
** Original author: taking
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "cvc4_private.h"
#ifndef __CVC4__BOOLEAN_SIMPLIFICATION_H
#define __CVC4__BOOLEAN_SIMPLIFICATION_H
#include "expr/node.h"
#include "util/Assert.h"
#include <vector>
namespace CVC4 {
class BooleanSimplification {
public:
static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10;
static void removeDuplicates(std::vector<Node>& buffer){
if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD){
std::sort(buffer.begin(), buffer.end());
std::vector<Node>::iterator new_end = std::unique(buffer.begin(), buffer.end());
buffer.erase(new_end, buffer.end());
}
}
static Node simplifyConflict(Node andNode){
Assert(andNode.getKind() == kind::AND);
std::vector<Node> buffer;
push_back_associative_commute(andNode, buffer, kind::AND, kind::OR, false);
removeDuplicates(buffer);
NodeBuilder<> nb(kind::AND);
nb.append(buffer);
return nb;
}
static Node simplifyClause(Node orNode){
Assert(orNode.getKind() == kind::OR);
std::vector<Node> buffer;
push_back_associative_commute(orNode, buffer, kind::OR, kind::AND, false);
removeDuplicates(buffer);
NodeBuilder<> nb(kind::OR);
nb.append(buffer);
return nb;
}
static Node simplifyHornClause(Node implication){
Assert(implication.getKind() == kind::IMPLIES);
TNode left = implication[0];
TNode right = implication[1];
Node notLeft = NodeBuilder<1>(kind::NOT)<<left;
Node clause = NodeBuilder<2>(kind::OR)<< notLeft << right;
return simplifyClause(clause);
}
static void push_back_associative_commute(Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode){
Node::iterator i = n.begin(), end = n.end();
for(; i != end; ++i){
Node child = *i;
if(child.getKind() == k){
push_back_associative_commute(child, buffer, k, notK, negateNode);
}else if(child.getKind() == kind::NOT && child[0].getKind() == notK){
push_back_associative_commute(child, buffer, notK, k, !negateNode);
}else{
if(negateNode){
buffer.push_back(negate(child));
}else{
buffer.push_back(child);
}
}
}
}
static Node negate(TNode n){
bool polarity = true;
TNode base = n;
while(base.getKind() == kind::NOT){
base = base[0];
polarity = !polarity;
}
if(polarity){
return base.notNode();
}else{
return base;
}
}
};/* class BooleanSimplification */
}/* CVC4 namespace */
#endif /* __CVC4__BOOLEAN_SIMPLIFICATION_H */
|
