diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-05 16:21:50 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-05 16:21:50 +0000 |
commit | 7342d1ca87397f3d5beb2c04b819243303e69a7c (patch) | |
tree | 9e166f1884275be7d4b33b13b8bcfe9418e61033 /src/theory/booleans/theory_bool.cpp | |
parent | af25c3f8498198dd6dd114c3b4ef39af54611e1e (diff) |
updated preprocessing and rewriting input equalities into inequalities for LRA
Diffstat (limited to 'src/theory/booleans/theory_bool.cpp')
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 137 |
1 files changed, 16 insertions, 121 deletions
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; } |