diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-21 16:34:29 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-21 16:34:29 -0400 |
commit | 7cb22c139978c154b13f0159a9308922a36ac6db (patch) | |
tree | 09d963a654745100a1ba54fa74a4a36219c4be36 /src | |
parent | 86d625587d37858ea0f28cf608a635eaba271760 (diff) | |
parent | 48d863e95d753c0bd477e7e36d0e683e3ec7b27f (diff) |
Merge branch '1.2.x'
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 37 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 28 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 3 |
3 files changed, 64 insertions, 4 deletions
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index fcb6c3cd5..f5d7f9235 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -52,6 +52,8 @@ namespace CVC4 { namespace theory { namespace uf { +using namespace ::CVC4::context; + SymmetryBreaker::Template::Template() : d_template(), d_sets(), @@ -165,7 +167,10 @@ void SymmetryBreaker::Template::reset() { d_reps.clear(); } -SymmetryBreaker::SymmetryBreaker() : +SymmetryBreaker::SymmetryBreaker(context::Context* context) : + ContextNotifyObj(context), + d_assertionsToRerun(context), + d_rerunningAssertions(false), d_phi(), d_phiSet(), d_permutations(), @@ -175,6 +180,31 @@ SymmetryBreaker::SymmetryBreaker() : d_termEqs() { } +class SBGuard { + bool& d_ref; + bool d_old; +public: + SBGuard(bool& b) : d_ref(b), d_old(b) {} + ~SBGuard() { Debug("uf") << "reset to " << d_old << std::endl; d_ref = d_old; } +};/* class SBGuard */ + +void SymmetryBreaker::rerunAssertionsIfNecessary() { + if(d_rerunningAssertions || !d_phi.empty() || d_assertionsToRerun.empty()) { + return; + } + + SBGuard g(d_rerunningAssertions); + d_rerunningAssertions = true; + + Debug("ufsymm") << "UFSYMM: rerunning assertions..." << std::endl; + for(CDList<Node>::const_iterator i = d_assertionsToRerun.begin(); + i != d_assertionsToRerun.end(); + ++i) { + assertFormula(*i); + } + Debug("ufsymm") << "UFSYMM: DONE rerunning assertions..." << std::endl; +} + Node SymmetryBreaker::norm(TNode phi) { Node n = Rewriter::rewrite(phi); return normInternal(n); @@ -254,6 +284,10 @@ Node SymmetryBreaker::normInternal(TNode n) { } void SymmetryBreaker::assertFormula(TNode phi) { + rerunAssertionsIfNecessary(); + if(!d_rerunningAssertions) { + d_assertionsToRerun.push_back(phi); + } // use d_phi, put into d_permutations Debug("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl; d_phi.push_back(phi); @@ -322,6 +356,7 @@ void SymmetryBreaker::clear() { } void SymmetryBreaker::apply(std::vector<Node>& newClauses) { + rerunAssertionsIfNecessary(); guessPermutations(); Debug("ufsymm") << "UFSYMM =====================================================" << endl << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl; diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index cf54b62c2..d04da048a 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -50,13 +50,15 @@ #include "expr/node.h" #include "expr/node_builder.h" +#include "context/context.h" +#include "context/cdlist.h" #include "util/statistics_registry.h" namespace CVC4 { namespace theory { namespace uf { -class SymmetryBreaker { +class SymmetryBreaker : public context::ContextNotifyObj { class Template { Node d_template; @@ -92,6 +94,19 @@ public: private: + /** + * This class wasn't initially built to be incremental. It should + * be attached to a UserContext so that it clears everything when + * a pop occurs. This "assertionsToRerun" is a set of assertions to + * feed back through assertFormula() when we started getting things + * again. It's not just a matter of effectiveness, but also soundness; + * if some assertions (still in scope) are not seen by a symmetry-breaking + * round, then some symmetries that don't actually exist might be broken, + * leading to unsound results! + */ + context::CDList<Node> d_assertionsToRerun; + bool d_rerunningAssertions; + std::vector<Node> d_phi; std::set<TNode> d_phiSet; Permutations d_permutations; @@ -101,6 +116,7 @@ private: TermEqs d_termEqs; void clear(); + void rerunAssertionsIfNecessary(); void guessPermutations(); bool invariantByPermutations(const Permutation& p); @@ -140,9 +156,17 @@ private: d_initNormalizationTimer, "theory::uf::symmetry_breaker::timers::initNormalization"); +protected: + + void contextNotifyPop() { + Debug("ufsymm") << "UFSYMM: clearing state due to pop" << std::endl; + clear(); + } + public: - SymmetryBreaker(); + SymmetryBreaker(context::Context* context); + ~SymmetryBreaker() throw() {} void assertFormula(TNode phi); void apply(std::vector<Node>& newClauses); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 69a963360..41935984f 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -38,7 +38,8 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), - d_functionsTerms(c) + d_functionsTerms(c), + d_symb(u) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); |