diff options
Diffstat (limited to 'src/theory/booleans/theory_bool.cpp')
| -rw-r--r-- | src/theory/booleans/theory_bool.cpp | 141 |
1 files changed, 140 insertions, 1 deletions
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 878b18478..b06972a2e 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -18,7 +18,15 @@ #include "theory/theory.h" #include "theory/booleans/theory_bool.h" +#include "theory/booleans/circuit_propagator.h" #include "theory/valuation.h" +#include "util/boolean_simplification.h" + +#include <vector> +#include <stack> +#include "util/hash.h" + +using namespace std; namespace CVC4 { namespace theory { @@ -89,6 +97,137 @@ Node TheoryBool::getValue(TNode n) { } } +static void +findAtoms(TNode in, vector<TNode>& atoms, + hash_map<TNode, vector<TNode>, TNodeHashFunction>& backEdges) { + Kind k = 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); + } + } + } + } +} + +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; + } + + // 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; + } + } 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; + } + } + } + + 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); + } + } + n = b; + } + Debug("simplify") << "final boolean simplification returned: " << n << endl; + return n; +} + + }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |