summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/Makefile.am1
-rw-r--r--src/theory/arith/arith_rewriter.cpp3
-rw-r--r--src/theory/arith/arith_static_learner.cpp88
-rw-r--r--src/theory/arith/arith_static_learner.h9
-rw-r--r--src/theory/arith/theory_arith.cpp78
-rw-r--r--src/theory/arith/theory_arith.h3
-rw-r--r--src/theory/booleans/circuit_propagator.cpp619
-rw-r--r--src/theory/booleans/circuit_propagator.h207
-rw-r--r--src/theory/booleans/theory_bool.cpp137
-rw-r--r--src/theory/booleans/theory_bool.h2
-rw-r--r--src/theory/booleans/theory_bool_rewriter.cpp53
-rw-r--r--src/theory/builtin/theory_builtin.cpp41
-rw-r--r--src/theory/builtin/theory_builtin.h1
-rw-r--r--src/theory/bv/theory_bv.h2
-rw-r--r--src/theory/substitutions.cpp165
-rw-r--r--src/theory/substitutions.h54
-rw-r--r--src/theory/theory.h62
-rw-r--r--src/theory/theory_engine.cpp208
-rw-r--r--src/theory/theory_engine.h75
-rw-r--r--src/theory/valuation.cpp8
-rw-r--r--src/theory/valuation.h14
21 files changed, 1051 insertions, 779 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index d720d5136..9e31bd7a3 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -24,6 +24,7 @@ libtheory_la_SOURCES = \
rewriter_attributes.h \
rewriter.cpp \
substitutions.h \
+ substitutions.cpp \
valuation.h \
valuation.cpp
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index bc8604e85..d2ecaffe4 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -234,6 +234,7 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){
RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
Assert(isAtom(atom));
+
NodeManager* currNM = NodeManager::currentNM();
if(atom.getKind() == kind::EQUAL) {
@@ -244,7 +245,7 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
Node reduction = atom;
- if(atom[1].getMetaKind() != kind::metakind::CONSTANT){
+ if(atom[1].getMetaKind() != kind::metakind::CONSTANT) {
// left |><| right
TNode left = atom[0];
TNode right = atom[1];
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 315c6ce94..77a89b54b 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -112,7 +112,7 @@ void ArithStaticLearner::clear(){
void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue){
- Debug("arith::static") << "===================== looking at" << n << endl;
+ Debug("arith::static") << "===================== looking at " << n << endl;
switch(n.getKind()){
case ITE:
@@ -121,8 +121,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
iteMinMax(n, learned);
}
- if((n[1].getKind() == CONST_RATIONAL || n[1].getKind() == CONST_INTEGER) &&
- (n[2].getKind() == CONST_RATIONAL || n[2].getKind() == CONST_INTEGER)) {
+ if((d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) ||
+ (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end())) {
iteConstant(n, learned);
}
break;
@@ -145,6 +145,12 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
}
}
break;
+ case CONST_RATIONAL:
+ case CONST_INTEGER:
+ // Mark constants as minmax
+ d_minMap[n] = coerceToRational(n);
+ d_maxMap[n] = coerceToRational(n);
+ break;
default: // Do nothing
break;
}
@@ -198,19 +204,42 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
Assert(n.getKind() == ITE);
- Assert(n[1].getKind() == CONST_RATIONAL || n[1].getKind() == CONST_INTEGER );
- Assert(n[2].getKind() == CONST_RATIONAL || n[2].getKind() == CONST_INTEGER );
- Rational t = coerceToRational(n[1]);
- Rational e = coerceToRational(n[2]);
- TNode min = (t <= e) ? n[1] : n[2];
- TNode max = (t >= e) ? n[1] : n[2];
+ Debug("arith::static") << "iteConstant(" << n << ")" << endl;
- Node nGeqMin = NodeBuilder<2>(GEQ) << n << min;
- Node nLeqMax = NodeBuilder<2>(LEQ) << n << max;
- Debug("arith::static") << n << " iteConstant" << nGeqMin << nLeqMax << endl;
- learned << nGeqMin << nLeqMax;
- ++(d_statistics.d_iteConstantApplications);
+ if (d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) {
+ DeltaRational min = std::min(d_minMap[n[1]], d_minMap[n[2]]);
+ NodeToMinMaxMap::iterator minFind = d_minMap.find(n);
+ if (minFind == d_minMap.end() || minFind->second < min) {
+ d_minMap[n] = min;
+ Node nGeqMin;
+ if (min.getInfinitesimalPart() == 0) {
+ nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart());
+ } else {
+ nGeqMin = NodeBuilder<2>(kind::GT) << n << mkRationalNode(min.getNoninfinitesimalPart());
+ }
+ learned << nGeqMin;
+ Debug("arith::static") << n << " iteConstant" << nGeqMin << endl;
+ ++(d_statistics.d_iteConstantApplications);
+ }
+ }
+
+ if (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end()) {
+ DeltaRational max = std::max(d_maxMap[n[1]], d_maxMap[n[2]]);
+ NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n);
+ if (maxFind == d_maxMap.end() || maxFind->second > max) {
+ d_maxMap[n] = max;
+ Node nLeqMax;
+ if (max.getInfinitesimalPart() == 0) {
+ nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart());
+ } else {
+ nLeqMax = NodeBuilder<2>(kind::LT) << n << mkRationalNode(max.getNoninfinitesimalPart());
+ }
+ learned << nLeqMax;
+ Debug("arith::static") << n << " iteConstant" << nLeqMax << endl;
+ ++(d_statistics.d_iteConstantApplications);
+ }
+ }
}
@@ -311,3 +340,34 @@ void ArithStaticLearner::miplibTrick(TNode var, set<Rational>& values, NodeBuild
learned << excludedMiddle;
}
}
+
+void ArithStaticLearner::addBound(TNode n) {
+
+ NodeToMinMaxMap::iterator minFind = d_minMap.find(n[0]);
+ NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n[0]);
+
+ Rational constant = coerceToRational(n[1]);
+ DeltaRational bound = constant;
+
+ switch(n.getKind()) {
+ case kind::LT:
+ bound = DeltaRational(constant, -1);
+ case kind::LEQ:
+ if (maxFind == d_maxMap.end() || maxFind->second > bound) {
+ d_maxMap[n[0]] = bound;
+ Debug("arith::static") << "adding bound " << n << endl;
+ }
+ break;
+ case kind::GT:
+ bound = DeltaRational(constant, 1);
+ case kind::GEQ:
+ if (minFind == d_minMap.end() || minFind->second < bound) {
+ d_minMap[n[0]] = bound;
+ Debug("arith::static") << "adding bound " << n << endl;
+ }
+ break;
+ default:
+ // nothing else
+ break;
+ }
+}
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index f2405cd5c..0ed9cbe85 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -44,10 +44,19 @@ private:
VarToNodeSetMap d_miplibTrick;
std::list<TNode> d_miplibTrickKeys;
+ /**
+ * Map from a node to it's minimum and maximum.
+ */
+ typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap;
+ NodeToMinMaxMap d_minMap;
+ NodeToMinMaxMap d_maxMap;
+
public:
ArithStaticLearner();
void staticLearning(TNode n, NodeBuilder<>& learned);
+ void addBound(TNode n);
+
void clear();
private:
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index a4c9f3ce0..34cb4d666 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -130,10 +130,82 @@ TheoryArith::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_restartTimer);
}
-Node TheoryArith::simplify(TNode in, std::vector< std::pair<Node, Node> >& outSubstitutions) {
+Node TheoryArith::preprocess(TNode atom) {
+ if (atom.getKind() == kind::EQUAL) {
+ Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
+ Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
+ return Rewriter::rewrite(leq.andNode(geq));
+ } else {
+ return atom;
+ }
+}
+
+Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutions) {
TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
- Trace("simplify:arith") << "arith-simplifying: " << in << endl;
- return d_valuation.rewrite(in);
+ Debug("simplify") << "TheoryArith::solve(" << in << ")" << endl;
+
+ // Solve equalities
+ Rational minConstant = 0;
+ Node minMonomial;
+ Node minVar;
+ unsigned nVars = 0;
+ if (in.getKind() == kind::EQUAL) {
+ Assert(in[1].getKind() == kind::CONST_RATIONAL);
+ // Find the variable with the smallest coefficient
+ Polynomial p = Polynomial::parsePolynomial(in[0]);
+ Polynomial::iterator it = p.begin(), it_end = p.end();
+ for (; it != it_end; ++ it) {
+ Monomial m = *it;
+ // Skip the constant
+ if (m.isConstant()) continue;
+ // This is a ''variable''
+ nVars ++;
+ // Skip the non-linear stuff
+ if (!m.getVarList().singleton()) continue;
+ // Get the minimal one
+ Rational constant = m.getConstant().getValue();
+ Rational absSconstant = constant > 0 ? constant : -constant;
+ if (minVar.isNull() || absSconstant < minConstant) {
+ Node var = m.getVarList().getNode();
+ if (var.getKind() == kind::VARIABLE) {
+ minVar = var;
+ minMonomial = m.getNode();
+ minConstant = constant;
+ }
+ }
+ }
+
+ // Solve for variable
+ if (!minVar.isNull()) {
+ // ax + p = c -> (ax + p) -ax - c = -ax
+ Node eliminateVar = NodeManager::currentNM()->mkNode(kind::MINUS, in[0], minMonomial);
+ if (in[1].getConst<Rational>() != 0) {
+ eliminateVar = NodeManager::currentNM()->mkNode(kind::MINUS, eliminateVar, in[1]);
+ }
+ // x = (p - ax - c) * -1/a
+ eliminateVar = NodeManager::currentNM()->mkNode(kind::MULT, eliminateVar, mkRationalNode(- minConstant.inverse()));
+ // Add the substitution
+ outSubstitutions.addSubstitution(minVar, Rewriter::rewrite(eliminateVar));
+ return SOLVE_STATUS_SOLVED;
+ }
+ }
+
+ // If a relation, remember the bound
+ switch(in.getKind()) {
+ case kind::LEQ:
+ case kind::LT:
+ case kind::GEQ:
+ case kind::GT:
+ if (in[0].getKind() == kind::VARIABLE) {
+ learner.addBound(in);
+ }
+ break;
+ default:
+ // Do nothing
+ break;
+ }
+
+ return SOLVE_STATUS_UNSOLVED;
}
void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 241ef8075..255e2a304 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -152,7 +152,8 @@ public:
void presolve();
void notifyRestart();
- Node simplify(TNode in, std::vector< std::pair<Node, Node> >& outSubstitutions);
+ SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions);
+ Node preprocess(TNode atom);
void staticLearning(TNode in, NodeBuilder<>& learned);
std::string identify() const { return std::string("TheoryArith"); }
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index e5055c164..fd44ec13b 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -19,6 +19,7 @@
#include "theory/booleans/circuit_propagator.h"
#include "util/utility.h"
+#include <stack>
#include <vector>
#include <algorithm>
@@ -28,353 +29,363 @@ namespace CVC4 {
namespace theory {
namespace booleans {
-void CircuitPropagator::propagateBackward(TNode in, bool polarity, vector<TNode>& changed) {
- if(!isPropagatedBackward(in)) {
- Debug("circuit-prop") << push << "propagateBackward(" << polarity << "): " << in << endl;
- setPropagatedBackward(in);
- // backward rules
- switch(Kind k = in.getKind()) {
+void CircuitPropagator::assert(TNode assertion)
+{
+ if (assertion.getKind() == kind::AND) {
+ for (unsigned i = 0; i < assertion.getNumChildren(); ++ i) {
+ assert(assertion[i]);
+ }
+ } else {
+ // Analyze the assertion for back-edges and all that
+ computeBackEdges(assertion);
+ // Assign the given assertion to true
+ assignAndEnqueue(assertion, true);
+ }
+}
+
+void CircuitPropagator::computeBackEdges(TNode node) {
+
+ Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")" << endl;
+
+ // Vector of nodes to visit
+ vector<TNode> toVisit;
+
+ // Start with the top node
+ if (d_seen.find(node) == d_seen.end()) {
+ toVisit.push_back(node);
+ d_seen.insert(node);
+ }
+
+ // Initialize the back-edges for the root, so we don't have a special case
+ d_backEdges[node];
+
+ // Go through the visit list
+ for (unsigned i = 0; i < toVisit.size(); ++ i) {
+ // Node we need to visit
+ TNode current = toVisit[i];
+ Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(): processing " << current << endl;
+ Assert(d_seen.find(current) != d_seen.end());
+
+ // If this not an atom visit all the children and compute the back edges
+ if (Theory::theoryOf(current) == THEORY_BOOL) {
+ for (unsigned child = 0, child_end = current.getNumChildren(); child < child_end; ++ child) {
+ TNode childNode = current[child];
+ // Add the back edge
+ d_backEdges[childNode].push_back(current);
+ // Add to the queue if not seen yet
+ if (d_seen.find(childNode) == d_seen.end()) {
+ toVisit.push_back(childNode);
+ d_seen.insert(childNode);
+ }
+ }
+ }
+ }
+}
+
+void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) {
+
+ Debug("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent << ", " << parentAssignment << ")" << endl;
+
+ // backward rules
+ switch(parent.getKind()) {
+ case kind::AND:
+ if (parentAssignment) {
+ // AND = TRUE: forall children c, assign(c = TRUE)
+ for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) {
+ assignAndEnqueue(*i, true);
+ }
+ } else {
+ // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE)
+ TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, true)));
+ if (holdout != parent.end()) {
+ assignAndEnqueue(*holdout, false);
+ }
+ }
+ break;
+ case kind::OR:
+ if (parentAssignment) {
+ // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE)
+ TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, false)));
+ if (holdout != parent.end()) {
+ assignAndEnqueue(*holdout, true);
+ }
+ } else {
+ // OR = FALSE: forall children c, assign(c = FALSE)
+ for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) {
+ assignAndEnqueue(*i, false);
+ }
+ }
+ break;
+ case kind::NOT:
+ // NOT = b: assign(c = !b)
+ assignAndEnqueue(parent[0], !parentAssignment);
+ break;
+ case kind::ITE:
+ if (isAssignedTo(parent[0], true)) {
+ // ITE c x y = v: if c is assigned and TRUE, assign(x = v)
+ assignAndEnqueue(parent[1], parentAssignment);
+ } else if (isAssignedTo(parent[0], false)) {
+ // ITE c x y = v: if c is assigned and FALSE, assign(y = v)
+ assignAndEnqueue(parent[2], parentAssignment);
+ } else if (isAssigned(parent[1]) && isAssigned(parent[2])) {
+ if (getAssignment(parent[1]) == parentAssignment && getAssignment(parent[2]) != parentAssignment) {
+ // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE)
+ assignAndEnqueue(parent[0], true);
+ } else if (getAssignment(parent[1]) != parentAssignment && getAssignment(parent[2]) == parentAssignment) {
+ // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE)
+ assignAndEnqueue(parent[0], false);
+ }
+ }
+ break;
+ case kind::IFF:
+ if (parentAssignment) {
+ // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment])
+ if (isAssigned(parent[0])) {
+ assignAndEnqueue(parent[1], getAssignment(parent[0]));
+ } else if (isAssigned(parent[1])) {
+ assignAndEnqueue(parent[0], getAssignment(parent[1]));
+ }
+ } else {
+ // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment])
+ if (isAssigned(parent[0])) {
+ assignAndEnqueue(parent[1], !getAssignment(parent[0]));
+ } else if (isAssigned(parent[1])) {
+ assignAndEnqueue(parent[0], !getAssignment(parent[1]));
+ }
+ }
+ break;
+ case kind::IMPLIES:
+ if (parentAssignment) {
+ if (isAssignedTo(parent[0], true)) {
+ // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE)
+ assignAndEnqueue(parent[1], true);
+ }
+ if (isAssignedTo(parent[1], false)) {
+ // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE)
+ assignAndEnqueue(parent[0], false);
+ }
+ } else {
+ // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE)
+ assignAndEnqueue(parent[0], true);
+ assignAndEnqueue(parent[1], false);
+ }
+ break;
+ case kind::XOR:
+ if (parentAssignment) {
+ if (isAssigned(parent[0])) {
+ // XOR x y = TRUE, and x assigned, assign(y = !assignment(x))
+ assignAndEnqueue(parent[1], !getAssignment(parent[0]));
+ } else if (isAssigned(parent[1])) {
+ // XOR x y = TRUE, and y assigned, assign(x = !assignment(y))
+ assignAndEnqueue(parent[0], !getAssignment(parent[1]));
+ }
+ } else {
+ if (isAssigned(parent[0])) {
+ // XOR x y = FALSE, and x assigned, assign(y = assignment(x))
+ assignAndEnqueue(parent[1], getAssignment(parent[0]));
+ } else if (isAssigned(parent[1])) {
+ // XOR x y = FALSE, and y assigned, assign(x = assignment(y))
+ assignAndEnqueue(parent[0], getAssignment(parent[1]));
+ }
+ }
+ break;
+ default:
+ Unhandled();
+ }
+}
+
+
+void CircuitPropagator::propagateForward(TNode child, bool childAssignment) {
+
+ // The assignment we have
+ Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child << ", " << childAssignment << ")" << endl;
+
+ // Get the back any nodes where this is child
+ const vector<TNode>& parents = d_backEdges.find(child)->second;
+
+ // Go through the parents and see if there is anything to propagate
+ vector<TNode>::const_iterator parent_it = parents.begin();
+ vector<TNode>::const_iterator parent_it_end = parents.end();
+ for(; parent_it != parent_it_end && !d_conflict; ++ parent_it) {
+ // The current parent of the child
+ TNode parent = *parent_it;
+ Assert(parent.hasSubterm(child));
+
+ // Forward rules
+ switch(parent.getKind()) {
case kind::AND:
- if(polarity) {
- // AND = TRUE: forall children c, assign(c = TRUE)
- for(TNode::iterator i = in.begin(), i_end = in.end(); i != i_end; ++i) {
- Debug("circuit-prop") << "bAND1" << endl;
- assign(*i, true, changed);
+ if (childAssignment) {
+ TNode::iterator holdout;
+ holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, true)));
+ if (holdout == parent.end()) { // all children are assigned TRUE
+ // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE)
+ assignAndEnqueue(parent, true);
+ } else if (isAssignedTo(parent, false)) {// the AND is FALSE
+ // is the holdout unique ?
+ TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, true)));
+ if (other == parent.end()) { // the holdout is unique
+ // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE)
+ assignAndEnqueue(*holdout, false);
+ }
}
} else {
- // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE)
- TNode::iterator holdout = find_if_unique(in.begin(), in.end(), not1(IsAssignedTo(*this, true)));
- if(holdout != in.end()) {
- Debug("circuit-prop") << "bAND2" << endl;
- assign(*holdout, false, changed);
- }
+ // AND ...(x=FALSE)...: assign(AND = FALSE)
+ assignAndEnqueue(parent, false);
}
break;
case kind::OR:
- if(polarity) {
- // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE)
- TNode::iterator holdout = find_if_unique(in.begin(), in.end(), not1(IsAssignedTo(*this, false)));
- if(holdout != in.end()) {
- Debug("circuit-prop") << "bOR1" << endl;
- assign(*holdout, true, changed);
- }
+ if (childAssignment) {
+ // OR ...(x=TRUE)...: assign(OR = TRUE)
+ assignAndEnqueue(parent, true);
} else {
- // OR = FALSE: forall children c, assign(c = FALSE)
- for(TNode::iterator i = in.begin(), i_end = in.end(); i != i_end; ++i) {
- Debug("circuit-prop") << "bOR2" << endl;
- assign(*i, false, changed);
+ TNode::iterator holdout;
+ holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, false)));
+ if (holdout == parent.end()) { // all children are assigned FALSE
+ // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE)
+ assignAndEnqueue(parent, false);
+ } else if (isAssignedTo(parent, true)) {// the OR is TRUE
+ // is the holdout unique ?
+ TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, false)));
+ if (other == parent.end()) { // the holdout is unique
+ // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE)
+ assignAndEnqueue(*holdout, true);
+ }
}
}
break;
+
case kind::NOT:
- // NOT = b: assign(c = !b)
- Debug("circuit-prop") << "bNOT" << endl;
- assign(in[0], !polarity, changed);
+ // NOT (x=b): assign(NOT = !b)
+ assignAndEnqueue(parent, !childAssignment);
break;
+
case kind::ITE:
- if(isAssignedTo(in[0], true)) {
- // ITE c x y = v: if c is assigned and TRUE, assign(x = v)
- Debug("circuit-prop") << "bITE1" << endl;
- assign(in[1], polarity, changed);
- } else if(isAssignedTo(in[0], false)) {
- // ITE c x y = v: if c is assigned and FALSE, assign(y = v)
- Debug("circuit-prop") << "bITE2" << endl;
- assign(in[2], polarity, changed);
- } else if(isAssigned(in[1]) && isAssigned(in[2])) {
- if(assignment(in[1]) == polarity && assignment(in[2]) != polarity) {
- // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE)
- Debug("circuit-prop") << "bITE3" << endl;
- assign(in[0], true, changed);
- } else if(assignment(in[1]) == !polarity && assignment(in[2]) == polarity) {
- // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE)
- Debug("circuit-prop") << "bITE4" << endl;
- assign(in[0], true, changed);
+ if (child == parent[0]) {
+ if (childAssignment) {
+ if (isAssigned(parent[1])) {
+ // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment)
+ assignAndEnqueue(parent, getAssignment(parent[1]));
+ }
+ } else {
+ if (isAssigned(parent[2])) {
+ // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment)
+ assignAndEnqueue(parent, getAssignment(parent[2]));
+ }
+ }
+ }
+ if (child == parent[1]) {
+ if (isAssignedTo(parent[0], true)) {
+ // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v)
+ assignAndEnqueue(parent, childAssignment);
+ }
+ }
+ if (child == parent[2]) {
+ Assert(child == parent[2]);
+ if (isAssignedTo(parent[0], false)) {
+ // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v)
+ assignAndEnqueue(parent, childAssignment);
}
}
break;
case kind::IFF:
- if(polarity) {
- // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment])
- if(isAssigned(in[0])) {
- assign(in[1], assignment(in[0]), changed);
- Debug("circuit-prop") << "bIFF1" << endl;
- } else if(isAssigned(in[1])) {
- Debug("circuit-prop") << "bIFF2" << endl;
- assign(in[0], assignment(in[1]), changed);
- }
+ if (isAssigned(parent[0]) && isAssigned(parent[1])) {
+ // IFF x y: if x or y is assigned, assign(IFF = (x.assignment <=> y.assignment))
+ assignAndEnqueue(parent, getAssignment(parent[0]) == getAssignment(parent[1]));
} else {
- // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment])
- if(isAssigned(in[0])) {
- Debug("circuit-prop") << "bIFF3" << endl;
- assign(in[1], !assignment(in[0]), changed);
- } else if(isAssigned(in[1])) {
- Debug("circuit-prop") << "bIFF4" << endl;
- assign(in[0], !assignment(in[1]), changed);
+ if (isAssigned(parent)) {
+ if (child == parent[0]) {
+ if (getAssignment(parent)) {
+ // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b)
+ assignAndEnqueue(parent[1], childAssignment);
+ } else {
+ // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b)
+ assignAndEnqueue(parent[1], !childAssignment);
+ }
+ } else {
+ Assert(child == parent[1]);
+ if (getAssignment(parent)) {
+ // IFF x y = b: if IFF is assigned to TRUE, assign(x = b)
+ assignAndEnqueue(parent[0], childAssignment);
+ } else {
+ // IFF x y = b y: if IFF is assigned to TRUE, assign(x = !b)
+ assignAndEnqueue(parent[0], !childAssignment);
+ }
+ }
}
}
break;
case kind::IMPLIES:
- if(polarity) {
- if(isAssignedTo(in[0], true)) {
- // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE)
- Debug("circuit-prop") << "bIMPLIES1" << endl;
- assign(in[1], true, changed);
+ if (isAssigned(parent[0]) && isAssigned(parent[1])) {
+ // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2))
+ assignAndEnqueue(parent, !getAssignment(parent[0]) || getAssignment(parent[1]));
+ } else {
+ if (child == parent[0] && childAssignment && isAssignedTo(parent, true)) {
+ // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE)
+ assignAndEnqueue(parent[1], true);
}
- if(isAssignedTo(in[1], false)) {
- // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE)
- Debug("circuit-prop") << "bIMPLIES2" << endl;
- assign(in[0], false, changed);
+ if (child == parent[1] && !childAssignment && isAssignedTo(parent, true)) {
+ // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE)
+ assignAndEnqueue(parent[0], false);
}
- } else {
- // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE)
- Debug("circuit-prop") << "bIMPLIES3" << endl;
- assign(in[0], true, changed);
- assign(in[1], false, changed);
+ // Note that IMPLIES == FALSE doesn't need any cases here
+ // because if that assignment has been done, we've already
+ // propagated all the children (in back-propagation).
}
break;
case kind::XOR:
- if(polarity) {
- if(isAssigned(in[0])) {
- // XOR x y = TRUE, and x assigned, assign(y = !assignment(x))
- Debug("circuit-prop") << "bXOR1" << endl;
- assign(in[1], !assignment(in[0]), changed);
- } else if(isAssigned(in[1])) {
- // XOR x y = TRUE, and y assigned, assign(x = !assignment(y))
- Debug("circuit-prop") << "bXOR2" << endl;
- assign(in[0], !assignment(in[1]), changed);
- }
- } else {
- if(isAssigned(in[0])) {
- // XOR x y = FALSE, and x assigned, assign(y = assignment(x))
- Debug("circuit-prop") << "bXOR3" << endl;
- assign(in[1], assignment(in[0]), changed);
- } else if(isAssigned(in[1])) {
- // XOR x y = FALSE, and y assigned, assign(x = assignment(y))
- Debug("circuit-prop") << "bXOR4" << endl;
- assign(in[0], assignment(in[1]), changed);
+ if (isAssigned(parent)) {
+ if (child == parent[0]) {
+ // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR)
+ assignAndEnqueue(parent[1], childAssignment != getAssignment(parent));
+ } else {
+ Assert(child == parent[1]);
+ // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR))
+ assignAndEnqueue(parent[0], childAssignment != getAssignment(parent));
}
}
- break;
- case kind::CONST_BOOLEAN:
- // nothing to do
+ if (isAssigned(parent[0]) && isAssigned(parent[1])) {
+ assignAndEnqueue(parent, getAssignment(parent[0]) != getAssignment(parent[1]));
+ }
break;
default:
- Unhandled(k);
+ Unhandled();
}
- Debug("circuit-prop") << pop;
}
}
+bool CircuitPropagator::propagate() {
-void CircuitPropagator::propagateForward(TNode child, bool polarity, vector<TNode>& changed) {
- if(!isPropagatedForward(child)) {
- IndentedScope(Debug("circuit-prop"));
- Debug("circuit-prop") << "propagateForward (" << polarity << "): " << child << endl;
- std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>::const_iterator iter = d_backEdges.find(child);
- if(d_backEdges.find(child) == d_backEdges.end()) {
- Debug("circuit-prop") << "no backedges, must be ROOT?: " << child << endl;
- return;
- }
- const vector<TNode>& uses = (*iter).second;
- setPropagatedForward(child);
- for(vector<TNode>::const_iterator useIter = uses.begin(), useIter_end = uses.end(); useIter != useIter_end; ++useIter) {
- TNode in = *useIter; // this is the outer node
- Debug("circuit-prop") << "considering use: " << in << endl;
- IndentedScope(Debug("circuit-prop"));
- // forward rules
- switch(Kind k = in.getKind()) {
- case kind::AND:
- if(polarity) {
- TNode::iterator holdout;
- holdout = find_if(in.begin(), in.end(), not1(IsAssignedTo(*this, true)));
- if(holdout == in.end()) { // all children are assigned TRUE
- // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE)
- Debug("circuit-prop") << "fAND1" << endl;
- assign(in, true, changed);
- } else if(isAssignedTo(in, false)) {// the AND is FALSE
- // is the holdout unique ?
- TNode::iterator other = find_if(holdout, in.end(), not1(IsAssignedTo(*this, true)));
- if(other == in.end()) { // the holdout is unique
- // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE)
- Debug("circuit-prop") << "fAND2" << endl;
- assign(*holdout, false, changed);
- }
- }
- } else {
- // AND ...(x=FALSE)...: assign(AND = FALSE)
- Debug("circuit-prop") << "fAND3" << endl;
- assign(in, false, changed);
- }
- break;
- case kind::OR:
- if(polarity) {
- // OR ...(x=TRUE)...: assign(OR = TRUE)
- Debug("circuit-prop") << "fOR1" << endl;
- assign(in, true, changed);
- } else {
- TNode::iterator holdout;
- holdout = find_if(in.begin(), in.end(), not1(IsAssignedTo(*this, false)));
- if(holdout == in.end()) { // all children are assigned FALSE
- // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE)
- Debug("circuit-prop") << "fOR2" << endl;
- assign(in, false, changed);
- } else if(isAssignedTo(in, true)) {// the OR is TRUE
- // is the holdout unique ?
- TNode::iterator other = find_if(holdout, in.end(), not1(IsAssignedTo(*this, false)));
- if(other == in.end()) { // the holdout is unique
- // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE)
- Debug("circuit-prop") << "fOR3" << endl;
- assign(*holdout, true, changed);
- }
- }
- }
- break;
-
- case kind::NOT:
- // NOT (x=b): assign(NOT = !b)
- Debug("circuit-prop") << "fNOT" << endl;
- assign(in, !polarity, changed);
- break;
- case kind::ITE:
- if(child == in[0]) {
- if(polarity) {
- if(isAssigned(in[1])) {
- // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment)
- Debug("circuit-prop") << "fITE1" << endl;
- assign(in, assignment(in[1]), changed);
- }
- } else {
- if(isAssigned(in[2])) {
- // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment)
- Debug("circuit-prop") << "fITE2" << endl;
- assign(in, assignment(in[2]), changed);
- }
- }
- } else if(child == in[1]) {
- if(isAssignedTo(in[0], true)) {
- // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v)
- Debug("circuit-prop") << "fITE3" << endl;
- assign(in, assignment(in[1]), changed);
- }
- } else {
- Assert(child == in[2]);
- if(isAssignedTo(in[0], false)) {
- // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v)
- Debug("circuit-prop") << "fITE4" << endl;
- assign(in, assignment(in[2]), changed);
- }
- }
- break;
- case kind::IFF:
- if(child == in[0]) {
- if(isAssigned(in[1])) {
- // IFF (x=b) y: if y is assigned, assign(IFF = (x.assignment <=> y.assignment))
- Debug("circuit-prop") << "fIFF1" << endl;
- assign(in, assignment(in[0]) == assignment(in[1]), changed);
- } else if(isAssigned(in)) {
- // IFF (x=b) y: if IFF is assigned, assign(y = (b <=> IFF.assignment))
- Debug("circuit-prop") << "fIFF2" << endl;
- assign(in[1], polarity == assignment(in), changed);
- }
- } else {
- Assert(child == in[1]);
- if(isAssigned(in[0])) {
- // IFF x (y=b): if x is assigned, assign(IFF = (x.assignment <=> y.assignment))
- Debug("circuit-prop") << "fIFF3" << endl;
- assign(in, assignment(in[0]) == assignment(in[1]), changed);
- } else if(isAssigned(in)) {
- // IFF x (y=b): if IFF is assigned, assign(x = (b <=> IFF.assignment))
- Debug("circuit-prop") << "fIFF4" << endl;
- assign(in[0], polarity == assignment(in), changed);
- }
- }
- break;
- case kind::IMPLIES:
- if(isAssigned(in[0]) && isAssigned(in[1])) {
- // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2))
- assign(in, !assignment(in[0]) || assignment(in[1]), changed);
- Debug("circuit-prop") << "fIMPLIES1" << endl;
- } else {
- if(child == in[0] && assignment(in[0]) && isAssignedTo(in, true)) {
- // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE)
- Debug("circuit-prop") << "fIMPLIES2" << endl;
- assign(in[1], true, changed);
- }
- if(child == in[1] && !assignment(in[1]) && isAssignedTo(in, true)) {
- // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE)
- Debug("circuit-prop") << "fIMPLIES3" << endl;
- assign(in[0], false, changed);
- }
- // Note that IMPLIES == FALSE doesn't need any cases here
- // because if that assignment has been done, we've already
- // propagated all the children (in back-propagation).
- }
- break;
- case kind::XOR:
- if(isAssigned(in)) {
- if(child == in[0]) {
- // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR)
- Debug("circuit-prop") << "fXOR1" << endl;
- assign(in[1], polarity ^ assignment(in), changed);
- } else {
- Assert(child == in[1]);
- // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR))
- Debug("circuit-prop") << "fXOR2" << endl;
- assign(in[0], polarity ^ assignment(in), changed);
- }
- }
- if( (child == in[0] && isAssigned(in[1])) ||
- (child == in[1] && isAssigned(in[0])) ) {
- // XOR (x=v) y [with y assigned], assign(XOR = (v ^ assignment(y))
- // XOR x (y=v) [with x assigned], assign(XOR = (assignment(x) ^ v)
- Debug("circuit-prop") << "fXOR3" << endl;
- assign(in, assignment(in[0]) ^ assignment(in[1]), changed);
- }
- break;
- case kind::CONST_BOOLEAN:
- InternalError("Forward-propagating a constant Boolean value makes no sense");
- default:
- Unhandled(k);
- }
- }
- }
-}
+ Debug("circuit-prop") << "CircuitPropagator::propagate()" << std::endl;
+ for(unsigned i = 0; i < d_propagationQueue.size() && !d_conflict; ++ i) {
-bool CircuitPropagator::propagate(TNode in, bool polarity, vector<Node>& newFacts) {
- try {
- vector<TNode> changed;
+ // The current node we are propagating
+ TNode current = d_propagationQueue[i];
+ Debug("circuit-prop") << "CircuitPropagator::propagate(): processing " << current << std::endl;
+ bool assignment = getAssignment(current);
+ Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " << (assignment ? "true" : "false") << std::endl;
- Assert(kindToTheoryId(in.getKind()) == THEORY_BOOL);
+ // Is this an atom
+ bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.getMetaKind() == kind::metakind::VARIABLE;
- Debug("circuit-prop") << "B: " << (polarity ? "" : "~") << in << endl;
- propagateBackward(in, polarity, changed);
- Debug("circuit-prop") << "F: " << (polarity ? "" : "~") << in << endl;
- propagateForward(in, polarity, changed);
-
- while(!changed.empty()) {
- vector<TNode> worklist;
- worklist.swap(changed);
+ // If an atom, add to the list for simplification
+ if (atom) {
+ Debug("circuit-prop") << "CircuitPropagator::propagate(): adding to learned: " << (assignment ? (Node)current : current.notNode()) << std::endl;
+ d_learnedLiterals.push_back(assignment ? (Node)current : current.notNode());
+ }
- for(vector<TNode>::iterator i = worklist.begin(), i_end = worklist.end(); i != i_end; ++i) {
- if(kindToTheoryId((*i).getKind()) != THEORY_BOOL) {
- if(assignment(*i)) {
- newFacts.push_back(*i);
- } else {
- newFacts.push_back((*i).notNode());
- }
- } else {
- Debug("circuit-prop") << "B: " << (isAssignedTo(*i, true) ? "" : "~") << *i << endl;
- propagateBackward(*i, assignment(*i), changed);
- Debug("circuit-prop") << "F: " << (isAssignedTo(*i, true) ? "" : "~") << *i << endl;
- propagateForward(*i, assignment(*i), changed);
- }
- }
+ // Propagate this value to the children (if not an atom or a constant)
+ if (d_backwardPropagation && !atom && !current.isConst()) {
+ propagateBackward(current, assignment);
+ }
+ // Propagate this value to the parents
+ if (d_forwardPropagation) {
+ propagateForward(current, assignment);
}
- } catch(ConflictException& ce) {
- return true;
}
- return false;
+
+ // No conflict
+ return d_conflict;
}
}/* CVC4::theory::booleans namespace */
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index f9efc20af..73a5be0f8 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -33,6 +33,7 @@ namespace CVC4 {
namespace theory {
namespace booleans {
+
/**
* The main purpose of the CircuitPropagator class is to maintain the
* state of the circuit for subsequent calls to propagate(), so that
@@ -40,104 +41,103 @@ namespace booleans {
* circuit isn't propagated twice, etc.
*/
class CircuitPropagator {
- const std::vector<TNode>& d_atoms;
- const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& d_backEdges;
- class ConflictException : Exception {
- public:
- ConflictException() : Exception("A conflict was found in the CircuitPropagator") {
- }
- };/* class ConflictException */
+public:
+
+ /**
+ * Value of a particular node
+ */
+ enum AssignmentStatus {
+ /** Node is currently unassigned */
+ UNASSIGNED = 0,
+ /** Node is assigned to true */
+ ASSIGNED_TO_TRUE,
+ /** Node is assigned to false */
+ ASSIGNED_TO_FALSE,
+ };
+
+ /** Invert a set value */
+ static inline AssignmentStatus neg(AssignmentStatus value) {
+ Assert(value != UNASSIGNED);
+ if (value == ASSIGNED_TO_TRUE) return ASSIGNED_TO_FALSE;
+ else return ASSIGNED_TO_TRUE;
+ }
+
+private:
+
+ /** Back edges from nodes to where they are used */
+ typedef std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction> BackEdgesMap;
+ BackEdgesMap d_backEdges;
- enum {
- ASSIGNMENT_MASK = 1,
- IS_ASSIGNED_MASK = 2,
- IS_PROPAGATED_FORWARD_MASK = 4,
- IS_PROPAGATED_BACKWARD_MASK = 8
- };/* enum */
+ /** The propagation queue */
+ std::vector<TNode> d_propagationQueue;
+
+ /** Are we in conflict */
+ bool d_conflict;
+
+ /** Map of substitutions */
+ std::vector<Node>& d_learnedLiterals;
+
+ /** Nodes that have been attached already (computed forward edges for) */
+ // All the nodes we've visited so far
+ std::hash_set<TNode, TNodeHashFunction> d_seen;
/**
- * For each Node we care about, we have a 4-bit state:
- * Bit 0 (ASSIGNMENT_MASK) is set to indicate the current assignment
- * Bit 1 (IS_ASSIGNED_MASK) is set if a value is assigned
- * Bit 2 (IS_PROPAGATED_FORWARD) is set to indicate it's been propagated forward
- * Bit 2 (IS_PROPAGATED_BACKWARD) is set to indicate it's been propagated backward
+ * Assignment status of each node.
*/
- std::hash_map<TNode, unsigned, TNodeHashFunction> d_state;
-
- /** Assign Node in circuit with the value and add it to the changed vector; note conflicts. */
- void assign(TNode n, bool b, std::vector<TNode>& changed) {
- if(n.getMetaKind() == kind::metakind::CONSTANT) {
- bool c = n.getConst<bool>();
- if(c != b) {
- Debug("circuit-prop") << "while assigning(" << b << "): " << n
- << ", constant conflict" << std::endl;
- throw ConflictException();
- } else {
- Debug("circuit-prop") << "assigning(" << b << "): " << n
- << ", nothing to do" << std::endl;
+ typedef std::hash_map<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
+ AssignmentMap d_state;
+
+ /**
+ * Assign Node in circuit with the value and add it to the queue; note conflicts.
+ */
+ void assignAndEnqueue(TNode n, bool value) {
+
+ Debug("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl;
+
+ if (n.getKind() == kind::CONST_BOOLEAN) {
+ // Assigning a constant to the opposite value is dumb
+ if (value != n.getConst<bool>()) {
+ d_conflict = true;
+ return;
}
- return;
}
- unsigned& state = d_state[n];
- if((state & IS_ASSIGNED_MASK) != 0) {// if assigned already
- if(((state & ASSIGNMENT_MASK) != 0) != b) {// conflict
- Debug("circuit-prop") << "while assigning(" << b << "): " << n
- << ", got conflicting assignment(" << assignment(n) << "): "
- << n << std::endl;
- throw ConflictException();
- } else {
- Debug("circuit-prop") << "already assigned(" << b << "): " << n << std::endl;
+
+ // Get the current assignement
+ AssignmentStatus state = d_state[n];
+
+ if(state != UNASSIGNED) {
+ // If the node is already assigned we might have a conflict
+ if(value != (state == ASSIGNED_TO_TRUE)) {
+ d_conflict = true;
}
- } else {// if unassigned
- Debug("circuit-prop") << "assigning(" << b << "): " << n << std::endl;
- state |= IS_ASSIGNED_MASK | (b ? ASSIGNMENT_MASK : 0);
- changed.push_back(n);
+ } else {
+ // If unassigned, mark it as assigned
+ d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
+ // Add for further propagation
+ d_propagationQueue.push_back(n);
}
}
- /** True iff Node is assigned in circuit (either true or false). */
- bool isAssigned(TNode n) {
- return (d_state[n] & IS_ASSIGNED_MASK) != 0;
- }
+
/** True iff Node is assigned in circuit (either true or false). */
bool isAssigned(TNode n) const {
- std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n);
- return i != d_state.end() && ((*i).second & IS_ASSIGNED_MASK) != 0;
- }
- /** True iff Node is assigned in circuit with the value given. */
- bool isAssignedTo(TNode n, bool b) {
- unsigned state = d_state[n];
- return (state & IS_ASSIGNED_MASK) &&
- (state & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0);
+ AssignmentMap::const_iterator i = d_state.find(n);
+ return i != d_state.end() && ((*i).second != UNASSIGNED);
}
- /** True iff Node is assigned in circuit (either true or false). */
- bool isAssignedTo(TNode n, bool b) const {
- std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n);
- return i != d_state.end() &&
- ((*i).second & IS_ASSIGNED_MASK) &&
- ((*i).second & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0);
+
+ /** True iff Node is assigned to the value. */
+ bool isAssignedTo(TNode n, bool value) const {
+ AssignmentMap::const_iterator i = d_state.find(n);
+ if (i == d_state.end()) return false;
+ if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true;
+ if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
+ return false;
}
+
/** Get Node assignment in circuit. Assert-fails if Node is unassigned. */
- bool assignment(TNode n) {
- unsigned state = d_state[n];
- Assert((state & IS_ASSIGNED_MASK) != 0);
- return (state & ASSIGNMENT_MASK) != 0;
- }
- /** Has this node already been propagated forward? */
- bool isPropagatedForward(TNode n) {
- return (d_state[n] & IS_PROPAGATED_FORWARD_MASK) != 0;
- }
- /** Has this node already been propagated backward? */
- bool isPropagatedBackward(TNode n) {
- return (d_state[n] & IS_PROPAGATED_BACKWARD_MASK) != 0;
- }
- /** Mark this node as already having been propagated forward. */
- void setPropagatedForward(TNode n) {
- d_state[n] |= IS_PROPAGATED_FORWARD_MASK;
- }
- /** Mark this node as already having been propagated backward. */
- void setPropagatedBackward(TNode n) {
- d_state[n] |= IS_PROPAGATED_BACKWARD_MASK;
+ bool getAssignment(TNode n) const {
+ Assert(d_state.find(n) != d_state.end() && d_state.find(n)->second != UNASSIGNED);
+ return d_state.find(n)->second == ASSIGNED_TO_TRUE;
}
/** Predicate for use in STL functions. */
@@ -169,33 +169,52 @@ class CircuitPropagator {
};/* class IsAssignedTo */
/**
- * Propagate new information (in = polarity) forward in circuit to
+ * Compute the map from nodes to the nodes that use it.
+ */
+ void computeBackEdges(TNode node);
+
+ /**
+ * Propagate new information forward in circuit to
* the parents of "in".
*/
- void propagateForward(TNode in, bool polarity, std::vector<TNode>& newFacts);
+ void propagateForward(TNode child, bool assignment);
+
/**
- * Propagate new information (in = polarity) backward in circuit to
+ * Propagate new information backward in circuit to
* the children of "in".
*/
- void propagateBackward(TNode in, bool polarity, std::vector<TNode>& newFacts);
+ void propagateBackward(TNode parent, bool assignment);
+
+ /** Whether to perform forward propagation */
+ bool d_forwardPropagation;
+ /** Whether to perform backward propagation */
+ bool d_backwardPropagation;
+ /** Whether to perform expensive propagations */
+ bool d_expensivePropagation;
public:
/**
* Construct a new CircuitPropagator with the given atoms and backEdges.
*/
- CircuitPropagator(const std::vector<TNode>& atoms, const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& backEdges)
- : d_atoms(atoms),
- d_backEdges(backEdges) {
+ CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true, bool enableExpensive = true) :
+ d_conflict(false),
+ d_learnedLiterals(outLearnedLiterals),
+ d_forwardPropagation(enableForward),
+ d_backwardPropagation(enableBackward),
+ d_expensivePropagation(enableExpensive)
+ {
}
+ /** Assert for propagation */
+ void assert(TNode assertion);
+
/**
- * Propagate new information (in == polarity) through the circuit
- * propagator. New information discovered by the propagator are put
- * in the (output-only) newFacts vector.
+ * Propagate through the asserted circuit propagator. New information discovered by the propagator
+ * are put in the subsitutions vector used in construction.
*
* @return true iff conflict found
*/
- bool propagate(TNode in, bool polarity, std::vector<Node>& newFacts) CVC4_WARN_UNUSED_RESULT;
+ bool propagate() CVC4_WARN_UNUSED_RESULT;
};/* class CircuitPropagator */
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 836022bc2..01185281a 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -97,134 +97,29 @@ Node TheoryBool::getValue(TNode n) {
}
}
-static void
-findAtoms(TNode in, vector<TNode>& atoms,
- hash_map<TNode, vector<TNode>, TNodeHashFunction>& backEdges) {
- Kind k CVC4_UNUSED = in.getKind();
- Assert(kindToTheoryId(k) == THEORY_BOOL);
-
- stack< pair<TNode, TNode::iterator> > trail;
- hash_set<TNode, TNodeHashFunction> seen;
- trail.push(make_pair(in, in.begin()));
-
- while(!trail.empty()) {
- pair<TNode, TNode::iterator>& pr = trail.top();
- Debug("simplify") << "looking at: " << pr.first << endl;
- if(pr.second == pr.first.end()) {
- trail.pop();
- } else {
- if(pr.second == pr.first.begin()) {
- Debug("simplify") << "first visit: " << pr.first << endl;
- // first time we've visited this node?
- if(seen.find(pr.first) == seen.end()) {
- Debug("simplify") << "+ haven't seen it yet." << endl;
- seen.insert(pr.first);
- } else {
- Debug("simplify") << "+ saw it before." << endl;
- trail.pop();
- continue;
- }
- }
- TNode n = *pr.second++;
- if(seen.find(n) == seen.end()) {
- Debug("simplify") << "back edge " << n << " to " << pr.first << endl;
- backEdges[n].push_back(pr.first);
- Kind nk = n.getKind();
- if(kindToTheoryId(nk) == THEORY_BOOL) {
- trail.push(make_pair(n, n.begin()));
- } else {
- Debug("simplify") << "atom: " << n << endl;
- atoms.push_back(n);
- }
- }
- }
- }
-}
+Theory::SolveStatus TheoryBool::solve(TNode in, SubstitutionMap& outSubstitutions) {
-Node TheoryBool::simplify(TNode in, Substitutions& outSubstitutions) {
- const unsigned prev = outSubstitutions.size();
-
- if(kindToTheoryId(in.getKind()) != THEORY_BOOL) {
- Assert(in.getMetaKind() == kind::metakind::VARIABLE &&
- in.getType().isBoolean());
- return in;
+ if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) {
+ // If we get a false literal, we're in conflict
+ return SOLVE_STATUS_CONFLICT;
}
- // form back edges and atoms
- vector<TNode> atoms;
- hash_map<TNode, vector<TNode>, TNodeHashFunction> backEdges;
- Debug("simplify") << "finding atoms..." << endl << push;
- findAtoms(in, atoms, backEdges);
- Debug("simplify") << pop << "done finding atoms..." << endl;
-
- hash_map<TNode, Node, TNodeHashFunction> simplified;
-
- vector<Node> newFacts;
- CircuitPropagator circuit(atoms, backEdges);
- Debug("simplify") << "propagate..." << endl;
- if(circuit.propagate(in, true, newFacts)) {
- Notice() << "Found a conflict in nonclausal Boolean reasoning" << endl;
- return NodeManager::currentNM()->mkConst(false);
- }
- Debug("simplify") << "done w/ propagate..." << endl;
-
- for(vector<Node>::iterator i = newFacts.begin(), i_end = newFacts.end(); i != i_end; ++i) {
- TNode a = *i;
- if(a.getKind() == kind::NOT) {
- if(a[0].getMetaKind() == kind::metakind::VARIABLE ) {
- Debug("simplify") << "found bool unit ~" << a[0] << "..." << endl;
- outSubstitutions.push_back(make_pair(a[0], NodeManager::currentNM()->mkConst(false)));
- } else if(kindToTheoryId(a[0].getKind()) != THEORY_BOOL) {
- Debug("simplify") << "simplifying: " << a << endl;
- simplified[a] = d_valuation.simplify(a, outSubstitutions);
- Debug("simplify") << "done simplifying, got: " << simplified[a] << endl;
- }
+ // Add the substitution from the variable to it's value
+ if (in.getKind() == kind::NOT) {
+ if (in[0].getKind() == kind::VARIABLE) {
+ outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false));
} else {
- if(a.getMetaKind() == kind::metakind::VARIABLE) {
- Debug("simplify") << "found bool unit " << a << "..." << endl;
- outSubstitutions.push_back(make_pair(a, NodeManager::currentNM()->mkConst(true)));
- } else if(kindToTheoryId(a.getKind()) != THEORY_BOOL) {
- Debug("simplify") << "simplifying: " << a << endl;
- simplified[a] = d_valuation.simplify(a, outSubstitutions);
- Debug("simplify") << "done simplifying, got: " << simplified[a] << endl;
- }
+ return SOLVE_STATUS_UNSOLVED;
}
- }
-
- Debug("simplify") << "substituting in root..." << endl;
- Node n = in.substitute(outSubstitutions.begin(), outSubstitutions.end());
- Debug("simplify") << "got: " << n << endl;
- if(Debug.isOn("simplify")) {
- Debug("simplify") << "new substitutions:" << endl;
- copy(outSubstitutions.begin() + prev, outSubstitutions.end(),
- ostream_iterator< pair<TNode, TNode> >(Debug("simplify"), "\n"));
- Debug("simplify") << "done." << endl;
- }
- if(outSubstitutions.size() > prev) {
- NodeBuilder<> b(kind::AND);
- b << n;
- for(Substitutions::iterator i = outSubstitutions.begin() + prev,
- i_end = outSubstitutions.end();
- i != i_end;
- ++i) {
- if((*i).first.getType().isBoolean()) {
- if((*i).second.getMetaKind() == kind::metakind::CONSTANT) {
- if((*i).second.getConst<bool>()) {
- b << (*i).first;
- } else {
- b << BooleanSimplification::negate((*i).first);
- }
- } else {
- b << (*i).first.iffNode((*i).second);
- }
- } else {
- b << (*i).first.eqNode((*i).second);
- }
+ } else {
+ if (in.getKind() == kind::VARIABLE) {
+ outSubstitutions.addSubstitution(in, NodeManager::currentNM()->mkConst<bool>(true));
+ } else {
+ return SOLVE_STATUS_UNSOLVED;
}
- n = b;
}
- Debug("simplify") << "final boolean simplification returned: " << n << endl;
- return n;
+
+ return SOLVE_STATUS_SOLVED;
}
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 40bbd3308..ce9938b10 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -36,7 +36,7 @@ public:
Node getValue(TNode n);
- Node simplify(TNode in, Substitutions& outSubstitutions);
+ SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions);
std::string identify() const { return std::string("TheoryBool"); }
};/* class TheoryBool */
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index c1be3b906..18aa71667 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -36,7 +36,31 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
if (n[0].getKind() == kind::NOT) return RewriteResponse(REWRITE_AGAIN, n[0][0]);
break;
}
- case kind::IFF: {
+ case kind::OR: {
+ if (n.getNumChildren() == 2) {
+ if (n[0] == tt || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
+ if (n[0] == ff) return RewriteResponse(REWRITE_AGAIN, n[1]);
+ if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0]);
+ }
+ break;
+ }
+ case kind::AND: {
+ if (n.getNumChildren() == 2) {
+ if (n[0] == ff || n[1] == ff) return RewriteResponse(REWRITE_DONE, ff);
+ if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
+ if (n[1] == tt) return RewriteResponse(REWRITE_AGAIN, n[0]);
+ }
+ break;
+ }
+ case kind::IMPLIES: {
+ if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
+ if (n[0] == tt && n[0] == ff) return RewriteResponse(REWRITE_DONE, ff);
+ if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
+ if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+ break;
+ }
+ case kind::IFF:
+ case kind::EQUAL: {
// rewrite simple cases of IFF
if(n[0] == tt) {
// IFF true x
@@ -62,10 +86,35 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
}
break;
}
+ case kind::XOR: {
+ // rewrite simple cases of XOR
+ if(n[0] == tt) {
+ // XOR true x
+ return RewriteResponse(REWRITE_AGAIN, n[1].notNode());
+ } else if(n[1] == tt) {
+ // XCR x true
+ return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+ } else if(n[0] == ff) {
+ // XOR false x
+ return RewriteResponse(REWRITE_AGAIN, n[1]);
+ } else if(n[1] == ff) {
+ // XOR x false
+ return RewriteResponse(REWRITE_AGAIN, n[0]);
+ } else if(n[0] == n[1]) {
+ // XOR x x
+ return RewriteResponse(REWRITE_DONE, ff);
+ } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
+ // XOR (NOT x) x
+ return RewriteResponse(REWRITE_DONE, tt);
+ } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
+ // XOR x (NOT x)
+ return RewriteResponse(REWRITE_DONE, tt);
+ }
+ break;
+ }
case kind::ITE: {
// non-Boolean-valued ITEs should have been removed in place of
// a variable
- Assert(n.getType().isBoolean());
// rewrite simple cases of ITE
if(n[0] == tt) {
// ITE true x y
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index ddfd2ab59..1c779bd79 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -26,47 +26,6 @@ namespace CVC4 {
namespace theory {
namespace builtin {
-Node TheoryBuiltin::simplify(TNode in, Substitutions& outSubstitutions) {
- if(in.getKind() == kind::EQUAL) {
- Node lhs = d_valuation.simplify(in[0], outSubstitutions);
- Node rhs = d_valuation.simplify(in[1], outSubstitutions);
- Node n = lhs.eqNode(rhs);
- if( n[0].getMetaKind() == kind::metakind::VARIABLE &&
- n[1].getMetaKind() == kind::metakind::CONSTANT ) {
- Debug("simplify:builtin") << "found new substitution! "
- << n[0] << " => " << n[1] << endl;
- outSubstitutions.push_back(make_pair(n[0], n[1]));
- // with our substitutions we've subsumed the equality
- return NodeManager::currentNM()->mkConst(true);
- } else if( n[1].getMetaKind() == kind::metakind::VARIABLE &&
- n[0].getMetaKind() == kind::metakind::CONSTANT ) {
- Debug("simplify:builtin") << "found new substitution! "
- << n[1] << " => " << n[0] << endl;
- outSubstitutions.push_back(make_pair(n[1], n[0]));
- // with our substitutions we've subsumed the equality
- return NodeManager::currentNM()->mkConst(true);
- }
- } else if(in.getKind() == kind::NOT && in[0].getKind() == kind::DISTINCT) {
- TNode::iterator found = in[0].end();
- for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) {
- if((*i).getMetaKind() == kind::metakind::CONSTANT) {
- found = i;
- break;
- }
- }
- if(found != in[0].end()) {
- for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) {
- if(i != found) {
- outSubstitutions.push_back(make_pair(*i, *found));
- }
- }
- // with our substitutions we've subsumed the (NOT (DISTINCT...))
- return NodeManager::currentNM()->mkConst(true);
- }
- }
- return in;
-}
-
Node TheoryBuiltin::getValue(TNode n) {
switch(n.getKind()) {
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index a97773dce..4e62401ff 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -31,7 +31,6 @@ class TheoryBuiltin : public Theory {
public:
TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) :
Theory(THEORY_BUILTIN, c, out, valuation) {}
- Node simplify(TNode in, Substitutions& outSubstitutions);
Node getValue(TNode n);
std::string identify() const { return std::string("TheoryBuiltin"); }
};/* class TheoryBuiltin */
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 8c2b59efa..27fadce0b 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -143,8 +143,6 @@ public:
void check(Effort e);
- //void presolve() { }
-
void propagate(Effort e) { }
void explain(TNode n);
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
new file mode 100644
index 000000000..8657ed871
--- /dev/null
+++ b/src/theory/substitutions.cpp
@@ -0,0 +1,165 @@
+/********************* */
+/*! \file substitutions.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** 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 A substitution mapping for theory simplification
+ **
+ ** A substitution mapping for theory simplification.
+ **/
+
+#include "theory/substitutions.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+
+struct substitution_stack_element {
+ TNode node;
+ bool children_added;
+ substitution_stack_element(TNode node)
+ : node(node), children_added(false) {}
+};
+
+Node SubstitutionMap::internalSubstitute(TNode t, NodeMap& substitutionCache) {
+
+ Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << std::endl;
+
+ // If nothing to substitute just return the node
+ if (substitutionCache.empty()) {
+ return t;
+ }
+
+ // Do a topological sort of the subexpressions and substitute them
+ vector<substitution_stack_element> toVisit;
+ toVisit.push_back((TNode) t);
+
+ while (!toVisit.empty())
+ {
+ // The current node we are processing
+ substitution_stack_element& stackHead = toVisit.back();
+ TNode current = stackHead.node;
+
+ Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << std::endl;
+
+ // If node already in the cache we're done, pop from the stack
+ NodeMap::iterator find = substitutionCache.find(current);
+ if (find != substitutionCache.end()) {
+ toVisit.pop_back();
+ continue;
+ }
+
+ // Not yet substituted, so process
+ if (stackHead.children_added) {
+ // Children have been processed, so substitute
+ NodeBuilder<> builder(current.getKind());
+ if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << current.getOperator();
+ }
+ for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
+ Assert(substitutionCache.find(current[i]) != substitutionCache.end());
+ builder << substitutionCache[current[i]];
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+ Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << std::endl;
+ substitutionCache[current] = result;
+ toVisit.pop_back();
+ } else {
+ // Mark that we have added the children if any
+ if (current.getNumChildren() > 0) {
+ stackHead.children_added = true;
+ // We need to add the children
+ for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
+ TNode childNode = *child_it;
+ NodeMap::iterator childFind = substitutionCache.find(childNode);
+ if (childFind == substitutionCache.end()) {
+ toVisit.push_back(childNode);
+ }
+ }
+ } else {
+ // No children, so we're done
+ Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << std::endl;
+ substitutionCache[current] = current;
+ toVisit.pop_back();
+ }
+ }
+ }
+
+ // Return the substituted version
+ return substitutionCache[t];
+}
+
+void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) {
+ Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl;
+ Assert(d_substitutions.find(x) == d_substitutions.end());
+
+ // Temporary substitution cache
+ NodeMap tempCache;
+ tempCache[x] = t;
+
+ // Put in the new substitutions into the old ones
+ NodeMap::iterator it = d_substitutions.begin();
+ NodeMap::iterator it_end = d_substitutions.end();
+ for(; it != it_end; ++ it) {
+ it->second = internalSubstitute(it->second, tempCache);
+ }
+
+ // Put the new substitution in
+ d_substitutions[x] = t;
+
+ // Also invalidate the cache
+ if (invalidateCache) {
+ d_cacheInvalidated = true;
+ }
+}
+
+bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
+ SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
+ SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end();
+ for (; it != it_end; ++ it) {
+ if (node.hasSubterm(it->first)) {
+ return false;
+ }
+ }
+ return true;
+}
+
+Node SubstitutionMap::apply(TNode t) {
+
+ Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << std::endl;
+
+ // Setup the cache
+ if (d_cacheInvalidated) {
+ d_substitutionCache = d_substitutions;
+ d_cacheInvalidated = false;
+ }
+
+ // Perform the substitution
+ Node result = internalSubstitute(t, d_substitutionCache);
+ Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << std::endl;
+
+ Assert(check(result, d_substitutions));
+
+ return result;
+}
+
+void SubstitutionMap::print(ostream& out) const {
+ NodeMap::const_iterator it = d_substitutions.begin();
+ NodeMap::const_iterator it_end = d_substitutions.end();
+ for (; it != it_end; ++ it) {
+ out << it->first << " -> " << it->second << endl;
+ }
+}
+
+}
+}
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 32e1599ea..513300a32 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -34,7 +34,59 @@ namespace theory {
* Valuation::simplify(). This is in its own header to avoid circular
* dependences between those three.
*/
-typedef std::vector< std::pair<Node, Node> > Substitutions;
+class SubstitutionMap {
+
+public:
+
+ typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+
+private:
+
+ /** The variables, in order of addition */
+ NodeMap d_substitutions;
+
+ /** Cache of the already performed substitutions */
+ NodeMap d_substitutionCache;
+
+ /** Has the cache been invalidated */
+ bool d_cacheInvalidated;
+
+ /** Internaal method that performs substitution */
+ Node internalSubstitute(TNode t, NodeMap& substitutionCache);
+
+public:
+
+ SubstitutionMap(): d_cacheInvalidated(true) {}
+
+ /**
+ * Adds a substitution from x to t
+ */
+ void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
+
+
+ /**
+ * Apply the substitutions to the node.
+ */
+ Node apply(TNode t);
+
+ /**
+ * Apply the substitutions to the node.
+ */
+ Node apply(TNode t) const {
+ return const_cast<SubstitutionMap*>(this)->apply(t);
+ }
+
+ /**
+ * Print to the output stream
+ */
+ void print(std::ostream& out) const;
+
+};
+
+inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subst) {
+ subst.print(out);
+ return out;
+}
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index e97e603e5..252d18844 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -141,7 +141,7 @@ protected:
d_wasSharedTermFact = false;
d_factsHead = d_factsHead + 1;
Debug("theory") << "Theory::get() => " << fact
- << "(" << d_facts.size() << " left)" << std::endl;
+ << " (" << d_facts.size() << " left)" << std::endl;
d_out->newFact(fact);
return fact;
}
@@ -407,19 +407,43 @@ public:
*/
virtual void staticLearning(TNode in, NodeBuilder<>& learned) { }
+ enum SolveStatus {
+ /** Atom has been solved */
+ SOLVE_STATUS_SOLVED,
+ /** Atom has not been solved */
+ SOLVE_STATUS_UNSOLVED,
+ /** Atom is inconsistent */
+ SOLVE_STATUS_CONFLICT
+ };
+
+ /**
+ * Given a literal, add the solved substitutions to the map, if any.
+ * The method should return true if the literal can be safely removed.
+ */
+ virtual SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions) {
+ if (in.getKind() == kind::EQUAL) {
+ if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
+ outSubstitutions.addSubstitution(in[0], in[1]);
+ return SOLVE_STATUS_SOLVED;
+ }
+ if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
+ outSubstitutions.addSubstitution(in[1], in[0]);
+ }
+ if (in[0].getMetaKind() == kind::metakind::CONSTANT && in[1].getMetaKind() == kind::metakind::CONSTANT) {
+ if (in[0] != in[1]) {
+ return SOLVE_STATUS_CONFLICT;
+ }
+ }
+ }
+
+ return SOLVE_STATUS_UNSOLVED;
+ }
+
/**
- * Simplify a node in a theory-specific way. The node is a theory
- * operation or its negation, or an equality between theory-typed
- * terms or its negation. Add to "outSubstitutions" any
- * replacements you want to make for the entire subterm; if you add
- * [x,y] to the vector, the enclosing Boolean formula (call it
- * "phi") will be replaced with (AND phi[x->y] (x = y)). Use
- * Valuation::simplify() to simplify subterms (it maintains a cache
- * and dispatches to the appropriate theory).
+ * Given an atom of the theory, that comes from the input formula, this is method can rewrite the atom
+ * into an equivalent form. This is only called just before an input atom to the engine.
*/
- virtual Node simplify(TNode in, Substitutions& outSubstitutions) {
- return in;
- }
+ virtual Node preprocess(TNode atom) { return atom; }
/**
* A Theory is called with presolve exactly one time per user
@@ -457,6 +481,20 @@ inline std::ostream& operator<<(std::ostream& out,
return out << theory.identify();
}
+inline std::ostream& operator << (std::ostream& out, theory::Theory::SolveStatus status) {
+ switch (status) {
+ case theory::Theory::SOLVE_STATUS_SOLVED:
+ out << "SOLVE_STATUS_SOLVED"; break;
+ case theory::Theory::SOLVE_STATUS_UNSOLVED:
+ out << "SOLVE_STATUS_UNSOLVED"; break;
+ case theory::Theory::SOLVE_STATUS_CONFLICT:
+ out << "SOLVE_STATUS_CONFLICT"; break;
+ default:
+ Unhandled();
+ }
+ return out;
+}
+
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__THEORY_H */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index db22d8981..fa885590b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -29,6 +29,8 @@
#include "theory/rewriter.h"
#include "theory/theory_traits.h"
+#include "util/ite_removal.h"
+
using namespace std;
using namespace CVC4;
@@ -46,9 +48,6 @@ typedef CVC4::expr::CDAttribute<RegisteredAttrTag, bool> RegisteredAttr;
struct PreRegisteredAttrTag {};
typedef expr::Attribute<PreRegisteredAttrTag, bool> PreRegistered;
-struct IteRewriteAttrTag {};
-typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr;
-
}/* CVC4::theory namespace */
void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
@@ -125,11 +124,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
// traversing a DAG as a tree and that can really blow up @CB
if(! n.getAttribute(RegisteredAttr())) {
n.setAttribute(RegisteredAttr(), true);
- if (n.getKind() == kind::EQUAL) {
- d_engine->theoryOf(n[0])->registerTerm(n);
- } else {
- d_engine->theoryOf(n)->registerTerm(n);
- }
+ d_engine->theoryOf(n)->registerTerm(n);
}
}
}/* Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr()) */
@@ -167,24 +162,13 @@ TheoryEngine::~TheoryEngine() {
delete d_sharedTermManager;
}
-struct preprocess_stack_element {
+struct preregister_stack_element {
TNode node;
bool children_added;
- preprocess_stack_element(TNode node)
+ preregister_stack_element(TNode node)
: node(node), children_added(false) {}
};/* struct preprocess_stack_element */
-Node TheoryEngine::preprocess(TNode node) {
- // Make sure the node is type-checked first (some rewrites depend on
- // typechecking having succeeded to be safe).
- if(Options::current()->typeChecking) {
- node.getType(true);
- }
- // Remove ITEs and rewrite the node
- Node preprocessed = Rewriter::rewrite(removeITEs(node));
- return preprocessed;
-}
-
void TheoryEngine::preRegister(TNode preprocessed) {
// If we are pre-registered already we are done
if (preprocessed.getAttribute(PreRegistered())) {
@@ -192,10 +176,10 @@ void TheoryEngine::preRegister(TNode preprocessed) {
}
// Do a topological sort of the subexpressions and preregister them
- vector<preprocess_stack_element> toVisit;
+ vector<preregister_stack_element> toVisit;
toVisit.push_back((TNode) preprocessed);
while (!toVisit.empty()) {
- preprocess_stack_element& stackHead = toVisit.back();
+ preregister_stack_element& stackHead = toVisit.back();
// The current node we are processing
TNode current = stackHead.node;
// If we already added all the children its time to register or just pop from the stack
@@ -208,22 +192,11 @@ void TheoryEngine::preRegister(TNode preprocessed) {
if(d_logic == "QF_AX") {
d_theoryTable[theory::THEORY_ARRAY]->preRegisterTerm(current);
} else {
- TheoryId theoryLHS = Theory::theoryOf(current[0]);
+ Theory* theory = theoryOf(current);
+ TheoryId theoryLHS = theory->getId();
Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl;
markActive(theoryLHS);
- d_theoryTable[theoryLHS]->preRegisterTerm(current);
-// TheoryId theoryRHS = Theory::theoryOf(current[1]);
-// if (theoryLHS != theoryRHS) {
-// markActive(theoryRHS);
-// d_theoryTable[theoryRHS]->preRegisterTerm(current);
-// Debug("register") << "preregistering " << current << " with " << theoryRHS << std::endl;
-// }
-// TheoryId typeTheory = Theory::theoryOf(current[0].getType());
-// if (typeTheory != theoryLHS && typeTheory != theoryRHS) {
-// markActive(typeTheory);
-// d_theoryTable[typeTheory]->preRegisterTerm(current);
-// Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl;
-// }
+ theory->preRegisterTerm(current);
}
} else {
TheoryId theory = Theory::theoryOf(current);
@@ -297,68 +270,6 @@ void TheoryEngine::propagate() {
CVC4_FOR_EACH_THEORY;
}
-/* Our goal is to tease out any ITE's sitting under a theory operator. */
-Node TheoryEngine::removeITEs(TNode node) {
- Debug("ite") << "removeITEs(" << node << ")" << endl;
-
- /* The result may be cached already */
- Node cachedRewrite;
- NodeManager *nodeManager = NodeManager::currentNM();
- if(nodeManager->getAttribute(node, theory::IteRewriteAttr(), cachedRewrite)) {
- Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
- return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
- }
-
- if(node.getKind() == kind::ITE){
- Assert( node.getNumChildren() == 3 );
- TypeNode nodeType = node.getType();
- if(!nodeType.isBoolean()){
- Node skolem = nodeManager->mkVar(nodeType);
- Node newAssertion =
- nodeManager->mkNode(kind::ITE,
- node[0],
- nodeManager->mkNode(kind::EQUAL, skolem, node[1]),
- nodeManager->mkNode(kind::EQUAL, skolem, node[2]));
- nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem);
-
- Debug("ite") << "removeITEs([" << node.getId() << "," << node << "," << nodeType << "])"
- << "->"
- << "[" << newAssertion.getId() << "," << newAssertion << "]"
- << endl;
-
- Node preprocessed = preprocess(newAssertion);
- d_propEngine->assertFormula(preprocessed);
-
- return skolem;
- }
- }
- vector<Node> newChildren;
- bool somethingChanged = false;
- if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- // Make sure to push operator or it will be missing in new
- // (reformed) node. This was crashing on the very simple input
- // "(f (ite c 0 1))"
- newChildren.push_back(node.getOperator());
- }
- for(TNode::const_iterator it = node.begin(), end = node.end();
- it != end;
- ++it) {
- Node newChild = removeITEs(*it);
- somethingChanged |= (newChild != *it);
- newChildren.push_back(newChild);
- }
-
- if(somethingChanged) {
- cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
- nodeManager->setAttribute(node, theory::IteRewriteAttr(), cachedRewrite);
- return cachedRewrite;
- } else {
- nodeManager->setAttribute(node, theory::IteRewriteAttr(), Node::null());
- return node;
- }
-}
-
-
Node TheoryEngine::getValue(TNode node) {
kind::MetaKind metakind = node.getMetaKind();
// special case: prop engine handles boolean vars
@@ -451,36 +362,91 @@ bool TheoryEngine::hasRegisterTerm(TheoryId th) const {
}
}
-Node TheoryEngine::simplify(TNode in, theory::Substitutions& outSubstitutions) {
- SimplifyCache::Scope cache(d_simplifyCache, in);
- if(cache) {
- outSubstitutions.insert(outSubstitutions.end(),
- cache.get().second.begin(),
- cache.get().second.end());
- return cache.get().first;
- }
+theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) {
+ TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
+ Debug("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl;
+ Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitionOut);
+ Debug("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << std::endl;
+ return solveStatus;
+}
+
+struct preprocess_stack_element {
+ TNode node;
+ bool children_added;
+ preprocess_stack_element(TNode node)
+ : node(node), children_added(false) {}
+};/* struct preprocess_stack_element */
- size_t prevSize = outSubstitutions.size();
- TNode atom = in.getKind() == kind::NOT ? in[0] : in;
+Node TheoryEngine::preprocess(TNode assertion) {
+
+ Debug("theory") << "TheoryEngine::preprocess(" << assertion << ")" << std::endl;
+
+ // Do a topological sort of the subexpressions and substitute them
+ vector<preprocess_stack_element> toVisit;
+ toVisit.push_back(assertion);
+
+ while (!toVisit.empty())
+ {
+ // The current node we are processing
+ preprocess_stack_element& stackHead = toVisit.back();
+ TNode current = stackHead.node;
- theory::Theory* theory = theoryOf(atom);
+ Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << std::endl;
- Debug("simplify") << push << "simplifying " << in << " to " << theory->identify() << std::endl;
- Node n = theory->simplify(in, outSubstitutions);
- Debug("simplify") << "got from " << theory->identify() << " : " << n << std::endl << pop;
+ // If node already in the cache we're done, pop from the stack
+ NodeMap::iterator find = d_atomPreprocessingCache.find(current);
+ if (find != d_atomPreprocessingCache.end()) {
+ toVisit.pop_back();
+ continue;
+ }
- atom = n.getKind() == kind::NOT ? n[0] : n;
+ // If this is an atom, we preprocess it with the theory
+ if (Theory::theoryOf(current) != THEORY_BOOL) {
+ d_atomPreprocessingCache[current] = theoryOf(current)->preprocess(current);
+ continue;
+ }
- if(atom.getKind() == kind::EQUAL) {
- theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType());
- Debug("simplify") << push << "simplifying " << n << " to " << typeTheory << std::endl;
- n = d_theoryTable[typeTheory]->simplify(n, outSubstitutions);
- Debug("simplify") << "got from " << d_theoryTable[typeTheory]->identify() << " : " << n << std::endl << pop;
+ // Not yet substituted, so process
+ if (stackHead.children_added) {
+ // Children have been processed, so substitute
+ NodeBuilder<> builder(current.getKind());
+ if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << current.getOperator();
+ }
+ for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
+ Assert(d_atomPreprocessingCache.find(current[i]) != d_atomPreprocessingCache.end());
+ builder << d_atomPreprocessingCache[current[i]];
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+ Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << std::endl;
+ d_atomPreprocessingCache[current] = result;
+ toVisit.pop_back();
+ } else {
+ // Mark that we have added the children if any
+ if (current.getNumChildren() > 0) {
+ stackHead.children_added = true;
+ // We need to add the children
+ for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
+ TNode childNode = *child_it;
+ NodeMap::iterator childFind = d_atomPreprocessingCache.find(childNode);
+ if (childFind == d_atomPreprocessingCache.end()) {
+ toVisit.push_back(childNode);
+ }
+ }
+ } else {
+ // No children, so we're done
+ Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << std::endl;
+ d_atomPreprocessingCache[current] = current;
+ toVisit.pop_back();
+ }
+ }
}
- cache(std::make_pair(n, theory::Substitutions(outSubstitutions.begin() + prevSize, outSubstitutions.end())));
- return n;
+ // Return the substituted version
+ return d_atomPreprocessingCache[assertion];
}
+
}/* CVC4 namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 852eea0c4..5b724a7c7 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -29,6 +29,7 @@
#include "prop/prop_engine.h"
#include "theory/shared_term_manager.h"
#include "theory/theory.h"
+#include "theory/substitutions.h"
#include "theory/rewriter.h"
#include "theory/substitutions.h"
#include "theory/valuation.h"
@@ -36,6 +37,7 @@
#include "util/stats.h"
#include "util/hash.h"
#include "util/cache.h"
+#include "util/ite_removal.h"
namespace CVC4 {
@@ -81,14 +83,10 @@ class TheoryEngine {
bool d_needRegistration;
/**
- * The type of the simplification cache.
- */
- typedef Cache<Node, std::pair<Node, theory::Substitutions>, NodeHashFunction> SimplifyCache;
-
- /**
- * A cache for simplification.
+ * Cache from proprocessing of atoms.
*/
- SimplifyCache d_simplifyCache;
+ typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ NodeMap d_atomPreprocessingCache;
/**
* An output channel for Theory that passes messages
@@ -191,11 +189,6 @@ class TheoryEngine {
context::CDO<bool> d_incomplete;
/**
- * Replace ITE forms in a node.
- */
- Node removeITEs(TNode t);
-
- /**
* Mark a theory active if it's not already.
*/
void markActive(theory::TheoryId th) {
@@ -256,6 +249,12 @@ public:
}
/**
+ * Runs theory specific preprocesssing on the non-Boolean parts of the formula.
+ * This is only called on input assertions, after ITEs have been removed.
+ */
+ Node preprocess(TNode node);
+
+ /**
* Return whether or not we are incomplete (in the current context).
*/
bool isIncomplete() {
@@ -290,7 +289,11 @@ public:
* of built-in type.
*/
inline theory::Theory* theoryOf(TNode node) {
- return d_theoryTable[theory::Theory::theoryOf(node)];
+ if (node.getKind() == kind::EQUAL) {
+ return d_theoryTable[theory::Theory::theoryOf(node[0])];
+ } else {
+ return d_theoryTable[theory::Theory::theoryOf(node)];
+ }
}
/**
@@ -304,12 +307,9 @@ public:
}
/**
- * Preprocess a node. This involves ITE removal and theory-specific
- * rewriting.
- *
- * @param n the node to preprocess
+ * Solve the given literal with a theory that owns it.
*/
- Node preprocess(TNode n);
+ theory::Theory::SolveStatus solve(TNode literal, theory::SubstitutionMap& substitionOut);
/**
* Preregister a Theory atom with the responsible theory (or
@@ -318,6 +318,15 @@ public:
void preRegister(TNode preprocessed);
/**
+ * Call the theories to perform one last rewrite on the theory atoms
+ * if they wish. This last rewrite is only performed on the input atoms.
+ * At this point it is ensured that atoms do not contain any Boolean
+ * strucure, i.e. there is no ITE nodes in them.
+ *
+ */
+ Node preCheckRewrite(TNode node);
+
+ /**
* Assert the formula to the appropriate theory.
* @param node the assertion
*/
@@ -339,19 +348,9 @@ public:
//Debug("theory")<< "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays \n";
d_theoryTable[theory::THEORY_ARRAY]->assertFact(node);
} else {
- theory::TheoryId theoryLHS = theory::Theory::theoryOf(atom[0]);
- Debug("theory") << "asserting " << node << " to " << theoryLHS << std::endl;
- d_theoryTable[theoryLHS]->assertFact(node);
-// theory::TheoryId theoryRHS = theory::Theory::theoryOf(atom[1]);
-// if (theoryLHS != theoryRHS) {
-// Debug("theory") << "asserting " << node << " to " << theoryRHS << std::endl;
-// d_theoryTable[theoryRHS]->assertFact(node);
-// }
-// theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType());
-// if (typeTheory!= theoryLHS && typeTheory != theoryRHS) {
-// Debug("theory") << "asserting " << node << " to " << typeTheory << std::endl;
-// d_theoryTable[typeTheory]->assertFact(node);
-// }
+ theory::Theory* theory = theoryOf(atom);
+ Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl;
+ theory->assertFact(node);
}
} else {
theory::Theory* theory = theoryOf(atom);
@@ -373,12 +372,6 @@ public:
void staticLearning(TNode in, NodeBuilder<>& learned);
/**
- * Calls simplify() on all theories, accumulating their combined
- * contributions in the "outSubstitutions" vector.
- */
- Node simplify(TNode in, theory::Substitutions& outSubstitutions);
-
- /**
* Calls presolve() on all active theories and returns true
* if one of the theories discovers a conflict.
*/
@@ -398,7 +391,13 @@ public:
}
inline void newLemma(TNode node) {
- d_propEngine->assertLemma(preprocess(node));
+ // Remove the ITEs and assert to prop engine
+ std::vector<Node> additionalLemmas;
+ additionalLemmas.push_back(node);
+ RemoveITE::run(additionalLemmas);
+ for (unsigned i = 0; i < additionalLemmas.size(); ++ i) {
+ d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i]));
+ }
}
/**
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 604ae21e1..536255c2d 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -41,13 +41,5 @@ Node Valuation::getSatValue(TNode n) const{
}
}
-Node Valuation::simplify(TNode in, Substitutions& outSubstitutions) {
- return d_engine->simplify(in, outSubstitutions);
-}
-
-Node Valuation::rewrite(TNode in) {
- return d_engine->preprocess(in);
-}
-
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index d46b9aab1..2346b6d32 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -51,20 +51,6 @@ public:
*/
Node getSatValue(TNode n) const;
- /**
- * Simplify a node. Intended to be used by a theory's simplify()
- * function to simplify subterms (TheoryEngine will cache the
- * results and make sure that the request is directed to the correct
- * theory).
- */
- Node simplify(TNode in, Substitutions& outSubstitutions);
-
- /**
- * Rewrite a node. Intended to be used by a theory to have the
- * TheoryEngine fully rewrite a node.
- */
- Node rewrite(TNode in);
-
};/* class Valuation */
}/* CVC4::theory namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback