diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-05 22:23:50 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-05 22:23:50 +0000 |
commit | fef0f8190fc7e5f3b88b33e7574b7df1e629e80f (patch) | |
tree | dfdda739bf5008096860e19f6b9275fb2a257960 /src/theory | |
parent | 90d8205a86b698c2548108ca4db124fe9c3f738a (diff) |
Merge from nonclausal-simplification-v2 branch:
* Preprocessing-time, non-clausal, Boolean simplification round to
support "quasi-non-linear rewrites" as discussed at last few meetings.
* --simplification=none is the default for now, but we'll probably
change that to --simplification=incremental. --simplification=batch
is also a possibility. See --simplification=help for details.
* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/Makefile.am | 1 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 9 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 2 | ||||
-rw-r--r-- | src/theory/booleans/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.cpp | 382 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 206 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 141 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 8 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 41 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 1 | ||||
-rwxr-xr-x | src/theory/mktheorytraits | 2 | ||||
-rw-r--r-- | src/theory/rewriter.h | 62 | ||||
-rw-r--r-- | src/theory/rewriter_attributes.h | 30 | ||||
-rw-r--r-- | src/theory/substitutions.h | 42 | ||||
-rw-r--r-- | src/theory/theory.h | 29 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 33 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 33 | ||||
-rw-r--r-- | src/theory/valuation.cpp | 8 | ||||
-rw-r--r-- | src/theory/valuation.h | 15 |
19 files changed, 1007 insertions, 42 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index eecf95875..d720d5136 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -23,6 +23,7 @@ libtheory_la_SOURCES = \ rewriter.h \ rewriter_attributes.h \ rewriter.cpp \ + substitutions.h \ valuation.h \ valuation.cpp diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e724312fa..7c72b5a28 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -83,6 +83,7 @@ TheoryArith::Statistics::Statistics(): d_statSlackVariables("theory::arith::SlackVariables", 0), d_statDisequalitySplits("theory::arith::DisequalitySplits", 0), d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0), + d_simplifyTimer("theory::arith::simplifyTimer"), d_staticLearningTimer("theory::arith::staticLearningTimer"), d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0), d_presolveTime("theory::arith::presolveTime"), @@ -96,6 +97,7 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_statSlackVariables); StatisticsRegistry::registerStat(&d_statDisequalitySplits); StatisticsRegistry::registerStat(&d_statDisequalityConflicts); + StatisticsRegistry::registerStat(&d_simplifyTimer); StatisticsRegistry::registerStat(&d_staticLearningTimer); StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables); @@ -114,6 +116,7 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_statSlackVariables); StatisticsRegistry::unregisterStat(&d_statDisequalitySplits); StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts); + StatisticsRegistry::unregisterStat(&d_simplifyTimer); StatisticsRegistry::unregisterStat(&d_staticLearningTimer); StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables); @@ -127,6 +130,12 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_restartTimer); } +Node TheoryArith::simplify(TNode in, std::vector< std::pair<Node, Node> >& outSubstitutions) { + TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer); + Trace("simplify:arith") << "arith-simplifying: " << in << endl; + return d_valuation.rewrite(in); +} + void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 9580a6c71..1c8955d35 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -149,6 +149,7 @@ public: void presolve(); void notifyRestart(); + Node simplify(TNode in, std::vector< std::pair<Node, Node> >& outSubstitutions); void staticLearning(TNode in, NodeBuilder<>& learned); std::string identify() const { return std::string("TheoryArith"); } @@ -234,6 +235,7 @@ private: IntStat d_statUserVariables, d_statSlackVariables; IntStat d_statDisequalitySplits; IntStat d_statDisequalityConflicts; + TimerStat d_simplifyTimer; TimerStat d_staticLearningTimer; IntStat d_permanentlyRemovedVariables; diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index 0263ae017..524a39b69 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -10,6 +10,8 @@ libbooleans_la_SOURCES = \ theory_bool.cpp \ theory_bool_type_rules.h \ theory_bool_rewriter.h \ - theory_bool_rewriter.cpp + theory_bool_rewriter.cpp \ + circuit_propagator.h \ + circuit_propagator.cpp EXTRA_DIST = kinds diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp new file mode 100644 index 000000000..e5055c164 --- /dev/null +++ b/src/theory/booleans/circuit_propagator.cpp @@ -0,0 +1,382 @@ +/********************* */ +/*! \file circuit_propagator.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 non-clausal circuit propagator for Boolean simplification + ** + ** A non-clausal circuit propagator for Boolean simplification. + **/ + +#include "theory/booleans/circuit_propagator.h" +#include "util/utility.h" + +#include <vector> +#include <algorithm> + +using namespace std; + +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()) { + 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); + } + } 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); + } + } + 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); + } + } 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); + } + } + break; + case kind::NOT: + // NOT = b: assign(c = !b) + Debug("circuit-prop") << "bNOT" << endl; + assign(in[0], !polarity, changed); + 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); + } + } + 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); + } + } 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); + } + } + 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(isAssignedTo(in[1], false)) { + // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE) + Debug("circuit-prop") << "bIMPLIES2" << endl; + assign(in[0], false, changed); + } + } 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); + } + 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); + } + } + break; + case kind::CONST_BOOLEAN: + // nothing to do + break; + default: + Unhandled(k); + } + Debug("circuit-prop") << pop; + } +} + + +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); + } + } + } +} + + +bool CircuitPropagator::propagate(TNode in, bool polarity, vector<Node>& newFacts) { + try { + vector<TNode> changed; + + Assert(kindToTheoryId(in.getKind()) == THEORY_BOOL); + + 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); + + 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); + } + } + } + } catch(ConflictException& ce) { + return true; + } + return false; +} + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h new file mode 100644 index 000000000..f9efc20af --- /dev/null +++ b/src/theory/booleans/circuit_propagator.h @@ -0,0 +1,206 @@ +/********************* */ +/*! \file circuit_propagator.h + ** \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 non-clausal circuit propagator for Boolean simplification + ** + ** A non-clausal circuit propagator for Boolean simplification. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H +#define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H + +#include <vector> +#include <functional> + +#include "theory/theory.h" +#include "context/context.h" +#include "util/hash.h" +#include "expr/node.h" + +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 + * the same fact is not output twice, so that the same edge in the + * 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 */ + + enum { + ASSIGNMENT_MASK = 1, + IS_ASSIGNED_MASK = 2, + IS_PROPAGATED_FORWARD_MASK = 4, + IS_PROPAGATED_BACKWARD_MASK = 8 + };/* enum */ + + /** + * 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 + */ + 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; + } + 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; + } + } else {// if unassigned + Debug("circuit-prop") << "assigning(" << b << "): " << n << std::endl; + state |= IS_ASSIGNED_MASK | (b ? ASSIGNMENT_MASK : 0); + changed.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); + } + /** 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); + } + /** 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; + } + + /** Predicate for use in STL functions. */ + class IsAssigned : public std::unary_function<TNode, bool> { + CircuitPropagator& d_circuit; + public: + IsAssigned(CircuitPropagator& circuit) : + d_circuit(circuit) { + } + + bool operator()(TNode in) const { + return d_circuit.isAssigned(in); + } + };/* class IsAssigned */ + + /** Predicate for use in STL functions. */ + class IsAssignedTo : public std::unary_function<TNode, bool> { + CircuitPropagator& d_circuit; + bool d_value; + public: + IsAssignedTo(CircuitPropagator& circuit, bool value) : + d_circuit(circuit), + d_value(value) { + } + + bool operator()(TNode in) const { + return d_circuit.isAssignedTo(in, d_value); + } + };/* class IsAssignedTo */ + + /** + * Propagate new information (in = polarity) forward in circuit to + * the parents of "in". + */ + void propagateForward(TNode in, bool polarity, std::vector<TNode>& newFacts); + /** + * Propagate new information (in = polarity) backward in circuit to + * the children of "in". + */ + void propagateBackward(TNode in, bool polarity, std::vector<TNode>& newFacts); + +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) { + } + + /** + * Propagate new information (in == polarity) through the circuit + * propagator. New information discovered by the propagator are put + * in the (output-only) newFacts vector. + * + * @return true iff conflict found + */ + bool propagate(TNode in, bool polarity, std::vector<Node>& newFacts) CVC4_WARN_UNUSED_RESULT; + +};/* class CircuitPropagator */ + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */ 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 */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index fd6d20e03..40bbd3308 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -5,13 +5,13 @@ ** Major contributors: taking ** Minor contributors (to current version): barrett ** 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 ** information.\endverbatim ** - ** \brief The theory of booleans. + ** \brief The theory of booleans ** ** The theory of booleans. **/ @@ -36,8 +36,10 @@ public: Node getValue(TNode n); + Node simplify(TNode in, Substitutions& outSubstitutions); + std::string identify() const { return std::string("TheoryBool"); } -}; +};/* class TheoryBool */ }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 1c779bd79..ddfd2ab59 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -26,6 +26,47 @@ 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 4e62401ff..a97773dce 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -31,6 +31,7 @@ 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/mktheorytraits b/src/theory/mktheorytraits index 2056c6306..45c108b72 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -131,7 +131,7 @@ struct TheoryTraits<${theory_id}> { static const bool hasPropagate = ${theory_has_propagate}; static const bool hasStaticLearning = ${theory_has_staticLearning}; static const bool hasRegisterTerm = ${theory_has_registerTerm}; - static const bool hasNotifyRestart = ${theory_has_staticLearning}; + static const bool hasNotifyRestart = ${theory_has_notifyRestart}; static const bool hasPresolve = ${theory_has_presolve}; }; " diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 403ccf755..884d0af72 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -1,9 +1,20 @@ -/* - * rewriter.h - * - * Created on: Dec 13, 2010 - * Author: dejan - */ +/********************* */ +/*! \file rewriter.h + ** \verbatim + ** Original author: dejan + ** 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 The Rewriter class + ** + ** The Rewriter class. + **/ #pragma once @@ -13,11 +24,15 @@ namespace CVC4 { namespace theory { +/** + * Theory rewriters signal whether more rewriting is needed (or not) + * by using a member of this enumeration. See RewriteResponse, below. + */ enum RewriteStatus { REWRITE_DONE, REWRITE_AGAIN, REWRITE_AGAIN_FULL -}; +};/* enum RewriteStatus */ /** * Instances of this class serve as response codes from @@ -29,9 +44,13 @@ enum RewriteStatus { struct RewriteResponse { const RewriteStatus status; const Node node; - RewriteResponse(RewriteStatus status, Node node) : status(status), node(node) {} -}; + RewriteResponse(RewriteStatus status, Node node) : + status(status), node(node) {} +};/* struct RewriteResponse */ +/** + * The main rewriter class. All functionality is static. + */ class Rewriter { /** Returns the appropriate cache for a node */ @@ -41,21 +60,28 @@ class Rewriter { static Node getPostRewriteCache(theory::TheoryId theoryId, TNode node); /** Sets the appropriate cache for a node */ - static void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache); + static void setPreRewriteCache(theory::TheoryId theoryId, + TNode node, TNode cache); /** Sets the appropriate cache for a node */ - static void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache); + static void setPostRewriteCache(theory::TheoryId theoryId, + TNode node, TNode cache); + + // disable construction of rewriters; all functionality is static + Rewriter() CVC4_UNUSED; + Rewriter(const Rewriter&) CVC4_UNUSED; public: - /** Calls the pre rewrite for the given theory */ + /** Calls the pre-rewriter for the given theory */ static RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node); - /** Calls the post rewrite for the given theory */ + /** Calls the post-rewriter for the given theory */ static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node); /** - * Rewrites the node using theoryOf to determine which rewriter to use on the node. + * Rewrites the node using theoryOf() to determine which rewriter to + * use on the node. */ static Node rewrite(Node node); @@ -65,7 +91,7 @@ public: static Node rewriteTo(theory::TheoryId theoryId, Node node); /** - * Should be called before the rewriter get's used for the first time. + * Should be called before the rewriter gets used for the first time. */ static void init(); @@ -73,7 +99,7 @@ public: * Should be called to clean up any state. */ static void shutdown(); -}; +};/* class Rewriter */ -} // Namesapce theory -} // Namespace CVC4 +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h index d33d7314e..86c2585b1 100644 --- a/src/theory/rewriter_attributes.h +++ b/src/theory/rewriter_attributes.h @@ -1,9 +1,20 @@ -/* - * rewriter_attributes.h - * - * Created on: Dec 27, 2010 - * Author: dejan - */ +/********************* */ +/*! \file rewriter_attributes.h + ** \verbatim + ** Original author: dejan + ** 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 Rewriter attributes + ** + ** Rewriter attributes. + **/ #pragma once @@ -79,8 +90,7 @@ struct RewriteAttibute { node.setAttribute(post_rewrite(), cache); } } -}; - -} // Namespace CVC4 -} // Namespace theory +};/* struct RewriteAttribute */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h new file mode 100644 index 000000000..32e1599ea --- /dev/null +++ b/src/theory/substitutions.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file substitutions.h + ** \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 "cvc4_private.h" + +#ifndef __CVC4__THEORY__SUBSTITUTIONS_H +#define __CVC4__THEORY__SUBSTITUTIONS_H + +#include <utility> +#include <vector> +#include "expr/node.h" + +namespace CVC4 { +namespace theory { + +/** + * The type for the Substitutions mapping output by + * Theory::simplify(), TheoryEngine::simplify(), and + * Valuation::simplify(). This is in its own header to avoid circular + * dependences between those three. + */ +typedef std::vector< std::pair<Node, Node> > Substitutions; + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__SUBSTITUTIONS_H */ diff --git a/src/theory/theory.h b/src/theory/theory.h index ac40c55d1..bba4c623a 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -24,6 +24,7 @@ #include "expr/node.h" #include "expr/attribute.h" #include "theory/valuation.h" +#include "theory/substitutions.h" #include "theory/output_channel.h" #include "context/context.h" #include "context/cdlist.h" @@ -159,6 +160,9 @@ protected: public: + /** + * Return the ID of the theory responsible for the given type. + */ static inline TheoryId theoryOf(TypeNode typeNode) { if (typeNode.getKind() == kind::TYPE_CONSTANT) { return typeConstantToTheoryId(typeNode.getConst<TypeConstant>()); @@ -168,10 +172,11 @@ public: } /** - * Returns the theory responsible for the node. + * Returns the ID of the theory responsible for the given node. */ static inline TheoryId theoryOf(TNode node) { - if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) { + if (node.getMetaKind() == kind::metakind::VARIABLE || + node.getMetaKind() == kind::metakind::CONSTANT) { // Constants, variables, 0-ary constructors return theoryOf(node.getType()); } else { @@ -374,13 +379,29 @@ public: } /** - * The theory should only add (via .operator<< or .append()) to the - * "learned" builder. It is a conjunction to add to the formula at + * Statically learn from assertion "in," which has been asserted + * true at the top level. The theory should only add (via + * ::operator<< or ::append()) to the "learned" builder---it should + * *never* clear it. It is a conjunction to add to the formula at * the top-level and may contain other theories' contributions. */ virtual void staticLearning(TNode in, NodeBuilder<>& learned) { } /** + * 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). + */ + virtual Node simplify(TNode in, Substitutions& outSubstitutions) { + return in; + } + + /** * A Theory is called with presolve exactly one time per user * check-sat. presolve() is called after preregistration, * rewriting, and Boolean propagation, (other theories' diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b4d6654b1..69220ad62 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -420,9 +420,40 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->staticLearning(in, learned); \ } - // notify each theory using the statement above + // static learning for each theory using the statement above CVC4_FOR_EACH_THEORY } +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; + } + + size_t prevSize = outSubstitutions.size(); + + TNode atom = in.getKind() == kind::NOT ? in[0] : in; + + theory::Theory* theory = theoryOf(atom); + + 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; + + atom = n.getKind() == kind::NOT ? n[0] : n; + + 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; + } + + cache(std::make_pair(n, theory::Substitutions(outSubstitutions.begin() + prevSize, outSubstitutions.end()))); + return n; +} }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 19374d6db..e571c2bbd 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -22,15 +22,20 @@ #define __CVC4__THEORY_ENGINE_H #include <deque> +#include <vector> +#include <utility> #include "expr/node.h" #include "prop/prop_engine.h" #include "theory/shared_term_manager.h" #include "theory/theory.h" #include "theory/rewriter.h" +#include "theory/substitutions.h" #include "theory/valuation.h" #include "util/options.h" #include "util/stats.h" +#include "util/hash.h" +#include "util/cache.h" namespace CVC4 { @@ -69,6 +74,16 @@ class TheoryEngine { size_t d_activeTheories; /** + * The type of the simplification cache. + */ + typedef Cache<Node, std::pair<Node, theory::Substitutions>, NodeHashFunction> SimplifyCache; + + /** + * A cache for simplification. + */ + SimplifyCache d_simplifyCache; + + /** * An output channel for Theory that passes messages * back to a TheoryEngine. */ @@ -273,11 +288,17 @@ public: } /** - * Preprocess a node. This involves theory-specific rewriting, then - * calling preRegister() on what's left over. + * Preprocess a node. This involves ITE removal and theory-specific + * rewriting. + * * @param n the node to preprocess */ Node preprocess(TNode n); + + /** + * Preregister a Theory atom with the responsible theory (or + * theories). + */ void preRegister(TNode preprocessed); /** @@ -325,12 +346,18 @@ public: bool check(theory::Theory::Effort effort); /** - * Calls staticLearning() on all active theories, accumulating their + * Calls staticLearning() on all theories, accumulating their * combined contributions in the "learned" builder. */ 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. */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 536255c2d..604ae21e1 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -41,5 +41,13 @@ 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 0c60ec5ea..d46b9aab1 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -24,6 +24,7 @@ #define __CVC4__THEORY__VALUATION_H #include "expr/node.h" +#include "theory/substitutions.h" namespace CVC4 { @@ -50,6 +51,20 @@ 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 */ |