From bb2a0e0e12f39a1b4dea8fb0c990decba4708a1c Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 16 Nov 2010 21:11:11 +0000 Subject: [PATCH] Added Theory::presolve(). --- src/prop/prop_engine.cpp | 3 +++ src/theory/arith/theory_arith.h | 6 ++++++ src/theory/arrays/theory_arrays.h | 4 ++++ src/theory/booleans/theory_bool.h | 2 ++ src/theory/builtin/theory_builtin.h | 1 + src/theory/bv/theory_bv.h | 4 ++++ src/theory/theory.h | 10 ++++++++++ src/theory/theory_engine.cpp | 16 ++++++++++++++++ src/theory/theory_engine.h | 8 +++++++- src/theory/uf/morgan/theory_uf_morgan.h | 4 ++++ src/theory/uf/tim/theory_uf_tim.h | 4 ++++ test/unit/theory/theory_black.h | 3 +++ test/unit/theory/theory_engine_white.h | 2 ++ 13 files changed, 66 insertions(+), 1 deletion(-) diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index ab1afceba..4939ecb43 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -118,6 +118,9 @@ Result PropEngine::checkSat() { ScopedBool scopedBool(d_inCheckSat); d_inCheckSat = true; + // TODO This currently ignores conflicts (a dangerous practice). + d_theoryEngine->presolve(); + // Check the problem bool result = d_satSolver->solve(); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 81711a101..e9ff06adb 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -134,6 +134,12 @@ public: void shutdown(){ } + void presolve(){ + static int callCount = 0; + Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl; + check(FULL_EFFORT); + } + std::string identify() const { return std::string("TheoryArith"); } private: diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 89631d59f..22a0148e1 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -48,6 +48,10 @@ public: return RewriteComplete(in); } + void presolve() { + Unimplemented(); + } + void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void check(Effort e); diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 2c77c09b3..fa826539c 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -46,6 +46,8 @@ public: void propagate(Effort e) { Unimplemented(); } void explain(TNode n, Effort e) { Unimplemented(); } + void presolve(){ Unimplemented(); } + Node getValue(TNode n, TheoryEngine* engine); RewriteResponse preRewrite(TNode n, bool topLevel); diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 57c5d1558..f373d16c2 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -39,6 +39,7 @@ public: void check(Effort e) { Unreachable(); } void propagate(Effort e) { Unreachable(); } void explain(TNode n, Effort e) { Unreachable(); } + void presolve() { Unreachable(); } Node getValue(TNode n, TheoryEngine* engine); void shutdown() { } RewriteResponse preRewrite(TNode n, bool topLevel); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index c673a56b4..f6073eff9 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -71,6 +71,10 @@ public: void check(Effort e); + void presolve(){ + Unimplemented(); + } + void propagate(Effort e) {} void explain(TNode n, Effort e) { } diff --git a/src/theory/theory.h b/src/theory/theory.h index df9dcafef..de260dd99 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -443,6 +443,16 @@ public: */ virtual Node getValue(TNode n, TheoryEngine* engine) = 0; + /** + * A Theory is called with presolve exactly one time per user check-sat. + * presolve() is called after preregistration, rewriting, and Boolean propagation, + * (other theories' propagation?), but the notified Theory has not yet had its check() + * or propagate() method called yet. + * A Theory may empty its assertFact() queue using get(). + * A Theory can raise conflicts, add lemmas, and propagate literals during presolve. + */ + virtual void presolve() = 0; + /** * Identify this theory (for debugging, dynamic configuration, * etc..) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index eb4c18161..f27e61544 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -617,4 +617,20 @@ Node TheoryEngine::getValue(TNode node) { return theoryOf(node)->getValue(node, this); }/* TheoryEngine::getValue(TNode node) */ + +bool TheoryEngine::presolve(){ + d_theoryOut.d_conflictNode = Node::null(); + d_theoryOut.d_propagatedLiterals.clear(); + try { + //d_uf->presolve(); + d_arith->presolve(); + //d_arrays->presolve(); + //d_bv->presolve(); + } catch(const theory::Interrupted&) { + Debug("theory") << "TheoryEngine::presolve() => conflict" << std::endl; + } + // Return wheather we have a conflict + return d_theoryOut.d_conflictNode.get().isNull(); +} + }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7958d977e..8ee5c91d7 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -305,10 +305,16 @@ public: } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::check() => conflict" << std::endl; } - // Return wheather we have a conflict + // Return whether we have a conflict return d_theoryOut.d_conflictNode.get().isNull(); } + /** + * Calls presolve() on all active theories and returns true + * if one of the theories discovers a conflict. + */ + bool presolve(); + inline const std::vector& getPropagatedLiterals() const { return d_theoryOut.d_propagatedLiterals; } diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index 023e100a9..569f9bb49 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -130,6 +130,10 @@ public: */ void check(Effort level); + void presolve(){ + Unimplemented(); + } + /** * Rewrites a node in the theory of uninterpreted functions. * This is fairly basic and only ensures that atoms that are diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h index 4c8a1a71a..44f061c12 100644 --- a/src/theory/uf/tim/theory_uf_tim.h +++ b/src/theory/uf/tim/theory_uf_tim.h @@ -126,6 +126,10 @@ public: void check(Effort level); + void presolve() { + Unimplemented(); + } + /** * Rewrites a node in the theory of uninterpreted functions. * This is fairly basic and only ensures that atoms that are diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index f0da885c7..7387551e3 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -136,6 +136,9 @@ public: } } + void presolve() { + Unimplemented(); + } void preRegisterTerm(TNode n) {} void propagate(Effort level) {} void explain(TNode n, Effort level) {} diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index bd6ec515b..594b5646d 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -203,6 +203,8 @@ public: return "Fake" + d_id; } + void presolve() { Unimplemented(); } + void preRegisterTerm(TNode) { Unimplemented(); } void registerTerm(TNode) { Unimplemented(); } void check(Theory::Effort) { Unimplemented(); } -- 2.30.2