diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-04-01 19:35:25 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-01 19:35:25 -0700 |
commit | 3915eb7b497bd185385048f8c7f2b4c8f2bf7c03 (patch) | |
tree | 8686d5ceea120ebda1ea65c0a8696ab1bdf78543 /test | |
parent | 936e9c442443799c866a65c6ca3fbdcd3ac9aab8 (diff) |
Initialize theory rewriters in theories (#4197)
Until now, the `Rewriter` was responsible for creating `TheoryRewriter`
instances. This commit adds a method `mkTheoryRewriter()` that theories
override to create an instance of their corresponding theory rewriter.
The advantage is that the theories can pass additional information to
their theory rewriter (e.g. a statistics object).
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/preprocessing/pass_bv_gauss_white.h | 7 | ||||
-rw-r--r-- | test/unit/theory/evaluator_white.h | 1 | ||||
-rw-r--r-- | test/unit/theory/regexp_operation_black.h | 4 | ||||
-rw-r--r-- | test/unit/theory/sequences_rewriter_white.h | 1 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 15 | ||||
-rw-r--r-- | test/unit/theory/theory_bv_rewriter_white.h | 1 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 144 | ||||
-rw-r--r-- | test/unit/theory/theory_quantifiers_bv_instantiator_white.h | 1 | ||||
-rw-r--r-- | test/unit/theory/theory_sets_type_enumerator_white.h | 22 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_skolem_cache_black.h | 20 | ||||
-rw-r--r-- | test/unit/theory/theory_white.h | 7 | ||||
-rw-r--r-- | test/unit/theory/type_enumerator_white.h | 17 |
12 files changed, 118 insertions, 122 deletions
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h index 4037c7191..bd21ed69c 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.h +++ b/test/unit/preprocessing/pass_bv_gauss_white.h @@ -176,6 +176,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); + d_smt->finalOptionsAreSet(); d_zero = bv::utils::mkZero(16); @@ -2373,7 +2374,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite AssertionPipeline apipe; apipe.push_back(a); - passes::BVGauss bgauss(nullptr); + passes::BVGauss bgauss(nullptr, "bv-gauss-unit"); std::unordered_map<Node, Node, NodeHashFunction> res; PreprocessingPassResult pres = bgauss.applyInternal(&apipe); TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT); @@ -2457,7 +2458,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite apipe.push_back(a); apipe.push_back(eq4); apipe.push_back(eq5); - passes::BVGauss bgauss(nullptr); + passes::BVGauss bgauss(nullptr, "bv-gauss-unit"); std::unordered_map<Node, Node, NodeHashFunction> res; PreprocessingPassResult pres = bgauss.applyInternal(&apipe); TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT); @@ -2507,7 +2508,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite AssertionPipeline apipe; apipe.push_back(eq1); apipe.push_back(eq2); - passes::BVGauss bgauss(nullptr); + passes::BVGauss bgauss(nullptr, "bv-gauss-unit"); std::unordered_map<Node, Node, NodeHashFunction> res; PreprocessingPassResult pres = bgauss.applyInternal(&apipe); TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT); diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h index c02aaaed8..547ce27cf 100644 --- a/test/unit/theory/evaluator_white.h +++ b/test/unit/theory/evaluator_white.h @@ -52,6 +52,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); + d_smt->finalOptionsAreSet(); } void tearDown() override diff --git a/test/unit/theory/regexp_operation_black.h b/test/unit/theory/regexp_operation_black.h index 81f5cf34a..826e14a31 100644 --- a/test/unit/theory/regexp_operation_black.h +++ b/test/unit/theory/regexp_operation_black.h @@ -45,6 +45,10 @@ class RegexpOperationBlack : public CxxTest::TestSuite d_scope = new SmtScope(d_smt); d_regExpOpr = new RegExpOpr(); + // Ensure that the SMT engine is fully initialized (required for the + // rewriter) + d_smt->push(); + d_nm = NodeManager::currentNM(); } diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h index 200a36d0b..c823c0704 100644 --- a/test/unit/theory/sequences_rewriter_white.h +++ b/test/unit/theory/sequences_rewriter_white.h @@ -45,6 +45,7 @@ class SequencesRewriterWhite : public CxxTest::TestSuite d_em = new ExprManager(opts); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); + d_smt->finalOptionsAreSet(); d_rewriter = new ExtendedRewriter(true); d_nm = NodeManager::currentNM(); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 8ae90c4c3..72b74a7b9 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -37,19 +37,15 @@ using namespace CVC4::theory; using namespace CVC4::smt; class TheoryBlack : public CxxTest::TestSuite { -private: - - ExprManager* d_em; - SmtEngine* d_smt; - NodeManager* d_nm; - SmtScope* d_scope; - public: void setUp() override { d_em = new ExprManager(); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); + // Ensure that the SMT engine is fully initialized (required for the + // rewriter) + d_smt->push(); d_nm = NodeManager::fromExprManager(d_em); } @@ -152,4 +148,9 @@ private: } + private: + ExprManager* d_em; + SmtEngine* d_smt; + NodeManager* d_nm; + SmtScope* d_scope; }; diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h index bf0ca73b3..b6348339b 100644 --- a/test/unit/theory/theory_bv_rewriter_white.h +++ b/test/unit/theory/theory_bv_rewriter_white.h @@ -43,6 +43,7 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite d_em = new ExprManager(opts); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); + d_smt->finalOptionsAreSet(); d_nm = NodeManager::currentNM(); } diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 5af670d5e..4a019ac08 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -38,6 +38,7 @@ #include "theory/rewriter.h" #include "theory/theory.h" #include "theory/theory_engine.h" +#include "theory/theory_rewriter.h" #include "theory/valuation.h" #include "util/integer.h" #include "util/proof.h" @@ -91,118 +92,72 @@ struct RewriteItem { bool d_topLevel; };/* struct RewriteItem */ +class FakeTheoryRewriter : public TheoryRewriter +{ + public: + RewriteResponse preRewrite(TNode n) override + { + return RewriteResponse(REWRITE_DONE, n); + } + + RewriteResponse postRewrite(TNode n) override + { + return RewriteResponse(REWRITE_DONE, n); + } +}; + /** - * Fake Theory interface. Looks like a Theory, but really all it does is note when and - * how rewriting behavior is requested. + * Fake Theory interface. Looks like a Theory, but really all it does is note + * when and how rewriting behavior is requested. */ -template<TheoryId theoryId> -class FakeTheory : public Theory { +template <TheoryId theoryId> +class FakeTheory : public Theory +{ /** - * This fake theory class is equally useful for bool, uf, arith, etc. It keeps an - * identifier to identify itself. + * This fake theory class is equally useful for bool, uf, arith, etc. It + * keeps an identifier to identify itself. */ std::string d_id; /** - * The expected sequence of rewrite calls. Filled by FakeTheory::expect() and consumed - * by FakeTheory::preRewrite() and FakeTheory::postRewrite(). + * The expected sequence of rewrite calls. Filled by FakeTheory::expect() and + * consumed by FakeTheory::preRewrite() and FakeTheory::postRewrite(). */ // static std::deque<RewriteItem> s_expected; -public: - FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo) - { } - - /** Register an expected rewrite call */ - static void expect(RewriteType type, FakeTheory* thy, TNode n, bool topLevel) - throw() + public: + FakeTheory(context::Context* ctxt, + context::UserContext* uctxt, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo) + : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo) { - RewriteItem item = { type, thy, n, topLevel }; - //s_expected.push_back(item); } - /** - * Returns whether the expected queue is empty. This is done after a call into - * the rewriter to ensure that the actual set of observed rewrite calls completed - * the sequence of expected rewrite calls. - */ - static bool nothingMoreExpected() throw() { - return true; // s_expected.empty(); + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override + { + return std::unique_ptr<TheoryRewriter>(new FakeTheoryRewriter()); } - /** - * Overrides Theory::preRewrite(). This "fake theory" version ensures that - * this actual, observed pre-rewrite call matches the next "expected" call set up - * by the test. - */ - RewriteResponse preRewrite(TNode n, bool topLevel) { -// if(false) { //s_expected.empty()) { -// cout << std::endl -// << "didn't expect anything more, but got" << std::endl -// << " PRE " << topLevel << " " << identify() << " " << n -// << std::endl; -// } -// TS_ASSERT(!s_expected.empty()); -// -// RewriteItem expected = s_expected.front(); -// s_expected.pop_front(); -// -// if(expected.d_type != PRE || -//// expected.d_theory != this || -// expected.d_node != n || -// expected.d_topLevel != topLevel) { -// cout << std::endl -// << "HAVE PRE " << topLevel << " " << identify() << " " << n -// << std::endl -// << "WANT " << (expected.d_type == PRE ? "PRE " : "POST ") -// // << expected.d_topLevel << " " << expected.d_theory->identify() -// << " " << expected.d_node << std::endl << std::endl; -// } -// -// TS_ASSERT_EQUALS(expected.d_type, PRE); -//// TS_ASSERT_EQUALS(expected.d_theory, this); -// TS_ASSERT_EQUALS(expected.d_node, n); -// TS_ASSERT_EQUALS(expected.d_topLevel, topLevel); - - return RewriteResponse(REWRITE_DONE, n); + /** Register an expected rewrite call */ + static void expect(RewriteType type, + FakeTheory* thy, + TNode n, + bool topLevel) throw() + { + RewriteItem item = {type, thy, n, topLevel}; + // s_expected.push_back(item); } /** - * Overrides Theory::postRewrite(). This "fake theory" version ensures that - * this actual, observed post-rewrite call matches the next "expected" call set up - * by the test. + * Returns whether the expected queue is empty. This is done after a call + * into the rewriter to ensure that the actual set of observed rewrite calls + * completed the sequence of expected rewrite calls. */ - RewriteResponse postRewrite(TNode n, bool topLevel) { -// if(s_expected.empty()) { -// cout << std::endl -// << "didn't expect anything more, but got" << std::endl -// << " POST " << topLevel << " " << identify() << " " << n -// << std::endl; -// } -// TS_ASSERT(!s_expected.empty()); -// -// RewriteItem expected = s_expected.front(); -// s_expected.pop_front(); -// -// if(expected.d_type != POST || -//// expected.d_theory != this || -// expected.d_node != n || -// expected.d_topLevel != topLevel) { -// cout << std::endl -// << "HAVE POST " << topLevel << " " << identify() << " " << n -// << std::endl -// << "WANT " << (expected.d_type == PRE ? "PRE " : "POST ") -//// << expected.d_topLevel << " " << expected.d_theory->identify() -// << " " << expected.d_node << std::endl << std::endl; -// } -// -// TS_ASSERT_EQUALS(expected.d_type, POST); -// TS_ASSERT_EQUALS(expected.d_theory, this); -// TS_ASSERT_EQUALS(expected.d_node, n); -// TS_ASSERT_EQUALS(expected.d_topLevel, topLevel); - - return RewriteResponse(REWRITE_DONE, n); + static bool nothingMoreExpected() throw() + { + return true; // s_expected.empty(); } std::string identify() const override { @@ -221,8 +176,7 @@ public: return Node::null(); } Node getValue(TNode n) { return Node::null(); } -};/* class FakeTheory */ - +}; /* class FakeTheory */ /* definition of the s_expected static field in FakeTheory; see above */ // std::deque<RewriteItem> FakeTheory::s_expected; diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h index 0fa7a3f82..7c37b1a85 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h @@ -65,6 +65,7 @@ void BvInstantiatorWhite::setUp() d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); + d_smt->finalOptionsAreSet(); } void BvInstantiatorWhite::tearDown() diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h index 3b5016fad..0ece5a056 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.h +++ b/test/unit/theory/theory_sets_type_enumerator_white.h @@ -18,9 +18,12 @@ #include <cxxtest/TestSuite.h> +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "theory/sets/theory_sets_type_enumerator.h" using namespace CVC4; +using namespace CVC4::smt; using namespace CVC4::theory; using namespace CVC4::kind; using namespace CVC4::theory::sets; @@ -28,21 +31,20 @@ using namespace std; class SetEnumeratorWhite : public CxxTest::TestSuite { - ExprManager* d_em; - NodeManager* d_nm; - NodeManagerScope* d_scope; - public: void setUp() override { d_em = new ExprManager(); + d_smt = new SmtEngine(d_em); d_nm = NodeManager::fromExprManager(d_em); - d_scope = new NodeManagerScope(d_nm); + d_scope = new SmtScope(d_smt); + d_smt->finalOptionsAreSet(); } void tearDown() override { delete d_scope; + delete d_smt; delete d_em; } @@ -68,8 +70,9 @@ class SetEnumeratorWhite : public CxxTest::TestSuite TS_ASSERT_EQUALS(expected2, actual2); TS_ASSERT(!setEnumerator.isFinished()); - Node actual3 = *++setEnumerator; - Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2); + Node actual3 = Rewriter::rewrite(*++setEnumerator); + Node expected3 = + Rewriter::rewrite(d_nm->mkNode(Kind::UNION, expected1, expected2)); TS_ASSERT_EQUALS(expected3, actual3); TS_ASSERT(!setEnumerator.isFinished()); @@ -301,4 +304,9 @@ class SetEnumeratorWhite : public CxxTest::TestSuite TS_ASSERT(setEnumerator.isFinished()); } + private: + ExprManager* d_em; + SmtEngine* d_smt; + NodeManager* d_nm; + SmtScope* d_scope; }; /* class SetEnumeratorWhite */ diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h index e1b84492c..8f41153f3 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.h +++ b/test/unit/theory/theory_strings_skolem_cache_black.h @@ -16,13 +16,17 @@ #include <memory> +#include "expr/expr_manager.h" #include "expr/node.h" #include "expr/node_manager.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "theory/strings/skolem_cache.h" #include "util/rational.h" #include "util/string.h" using namespace CVC4; +using namespace CVC4::smt; using namespace CVC4::theory::strings; class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite @@ -30,8 +34,14 @@ class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite public: void setUp() override { - d_nm.reset(new NodeManager(nullptr)); - d_scope.reset(new NodeManagerScope(d_nm.get())); + d_em.reset(new ExprManager()); + d_smt.reset(new SmtEngine(d_em.get())); + d_scope.reset(new SmtScope(d_smt.get())); + // Ensure that the SMT engine is fully initialized (required for the + // rewriter) + d_smt->push(); + + d_nm = NodeManager::fromExprManager(d_em.get()); } void tearDown() override {} @@ -87,6 +97,8 @@ class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite } private: - std::unique_ptr<NodeManager> d_nm; - std::unique_ptr<NodeManagerScope> d_scope; + std::unique_ptr<ExprManager> d_em; + std::unique_ptr<SmtEngine> d_smt; + NodeManager* d_nm; + std::unique_ptr<SmtScope> d_scope; }; diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 0dd52be8c..eb43e00cb 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -93,7 +93,7 @@ class TestOutputChannel : public OutputChannel { }; class DummyTheory : public Theory { -public: + public: set<Node> d_registered; vector<Node> d_getSequence; @@ -102,6 +102,11 @@ public: : Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo) {} + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() + { + return std::unique_ptr<TheoryRewriter>(); + } + void registerTerm(TNode n) { // check that we registerTerm() a term only once TS_ASSERT(d_registered.find(n) == d_registered.end()); diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index da915b7ee..58dadd27a 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -25,30 +25,32 @@ #include "expr/node_manager.h" #include "expr/type_node.h" #include "options/language.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "theory/type_enumerator.h" using namespace CVC4; +using namespace CVC4::smt; using namespace CVC4::theory; using namespace CVC4::kind; using namespace std; class TypeEnumeratorWhite : public CxxTest::TestSuite { - ExprManager* d_em; - NodeManager* d_nm; - NodeManagerScope* d_scope; - public: void setUp() override { d_em = new ExprManager(); + d_smt = new SmtEngine(d_em); d_nm = NodeManager::fromExprManager(d_em); - d_scope = new NodeManagerScope(d_nm); + d_scope = new SmtScope(d_smt); + d_smt->finalOptionsAreSet(); } void tearDown() override { delete d_scope; + delete d_smt; delete d_em; } @@ -272,4 +274,9 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite { TS_ASSERT_THROWS(*++te, NoMoreValuesException&); } + private: + ExprManager* d_em; + SmtEngine* d_smt; + NodeManager* d_nm; + SmtScope* d_scope; };/* class TypeEnumeratorWhite */ |