From: Aina Niemetz Date: Wed, 24 Feb 2021 20:25:10 +0000 (-0800) Subject: google test: theory: Migrate theory_engine_white. (#5988) X-Git-Tag: cvc5-1.0.0~2218 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cb86456081168ad0a9b3157e3981d364347847b4;p=cvc5.git google test: theory: Migrate theory_engine_white. (#5988) --- diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 4951d07b6..f87ec5e64 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -29,12 +29,12 @@ class TestSmt : public TestInternal void SetUp() override { d_nodeManager.reset(new NodeManager(nullptr)); - d_nm_scope.reset(new NodeManagerScope(d_nodeManager.get())); + d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); d_smtEngine->finishInit(); } - std::unique_ptr d_nm_scope; + std::unique_ptr d_nmScope; std::unique_ptr d_nodeManager; std::unique_ptr d_smtEngine; }; @@ -45,11 +45,11 @@ class TestSmtNoFinishInit : public TestInternal void SetUp() override { d_nodeManager.reset(new NodeManager(nullptr)); - d_scope.reset(new NodeManagerScope(d_nodeManager.get())); + d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); } - std::unique_ptr d_scope; + std::unique_ptr d_nmScope; std::unique_ptr d_nodeManager; std::unique_ptr d_smtEngine; }; diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index f972efd47..c135c4a94 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -20,7 +20,7 @@ cvc4_add_unit_test_white(theory_bags_rewriter_white theory) cvc4_add_cxx_unit_test_white(theory_bags_type_rules_white theory) cvc4_add_cxx_unit_test_white(theory_bv_rewriter_white theory) cvc4_add_cxx_unit_test_white(theory_bv_white theory) -cvc4_add_cxx_unit_test_white(theory_engine_white theory) +cvc4_add_unit_test_white(theory_engine_white theory) cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_instantiator_white theory) cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_inverter_white theory) cvc4_add_cxx_unit_test_white(theory_sets_type_enumerator_white theory) diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp new file mode 100644 index 000000000..c888fbf0d --- /dev/null +++ b/test/unit/theory/theory_engine_white.cpp @@ -0,0 +1,249 @@ +/********************* */ +/*! \file theory_engine_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters, Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief White box testing of CVC4::theory::Theory. + ** + ** White box testing of CVC4::theory::Theory. This test creates + ** "fake" theory interfaces and injects them into TheoryEngine, so we + ** can test TheoryEngine's behavior without relying on independent + ** theory behavior. This is done in TheoryEngineWhite::setUp() by + ** means of the TheoryEngineWhite::registerTheory() interface. + **/ + +#include +#include + +#include "base/check.h" +#include "context/context.h" +#include "expr/kind.h" +#include "expr/node.h" +#include "options/options.h" +#include "test_smt.h" +#include "theory/bv/theory_bv_rewrite_rules_normalization.h" +#include "theory/bv/theory_bv_rewrite_rules_simplification.h" +#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/rational.h" + +namespace CVC4 { + +using namespace theory; +using namespace expr; +using namespace context; +using namespace kind; +using namespace smt; +using namespace theory::bv; + +namespace test { + +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. + */ +template +class FakeTheory : public Theory +{ + public: + FakeTheory(context::Context* ctxt, + context::UserContext* uctxt, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, pnm) + { + } + + TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } + + std::string identify() const override { return "Fake" + d_id; } + + void presolve() override { Unimplemented(); } + + void preRegisterTerm(TNode) override { Unimplemented(); } + void registerTerm(TNode) { Unimplemented(); } + void propagate(Theory::Effort) override { Unimplemented(); } + TrustNode explain(TNode) override + { + Unimplemented(); + return TrustNode::null(); + } + Node getValue(TNode n) { return Node::null(); } + + private: + /** + * This fake theory class is equally useful for bool, uf, arith, etc. It + * keeps an identifier to identify itself. + */ + std::string d_id; + + /** The theory rewriter for this theory. */ + FakeTheoryRewriter d_rewriter; +}; + +class TestTheoryWhiteEngine : public TestSmt +{ + protected: + void SetUp() override + { + TestSmt::SetUp(); + d_context = d_smtEngine->getContext(); + d_user_context = d_smtEngine->getUserContext(); + + d_theoryEngine = d_smtEngine->getTheoryEngine(); + for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) + { + delete d_theoryEngine->d_theoryOut[id]; + delete d_theoryEngine->d_theoryTable[id]; + d_theoryEngine->d_theoryOut[id] = NULL; + d_theoryEngine->d_theoryTable[id] = NULL; + } + d_theoryEngine->addTheory >(THEORY_BUILTIN); + d_theoryEngine->addTheory >(THEORY_BOOL); + d_theoryEngine->addTheory >(THEORY_UF); + d_theoryEngine->addTheory >(THEORY_ARITH); + d_theoryEngine->addTheory >(THEORY_ARRAYS); + d_theoryEngine->addTheory >(THEORY_BV); + } + + Context* d_context; + UserContext* d_user_context; + TheoryEngine* d_theoryEngine; +}; + +TEST_F(TestTheoryWhiteEngine, rewriter_simple) +{ + Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType()); + Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType()); + Node z = d_nodeManager->mkVar("z", d_nodeManager->integerType()); + + // make the expression (PLUS x y (MULT z 0)) + Node zero = d_nodeManager->mkConst(Rational("0")); + Node zTimesZero = d_nodeManager->mkNode(MULT, z, zero); + Node n = d_nodeManager->mkNode(PLUS, x, y, zTimesZero); + + Node nExpected = n; + Node nOut; + + // do a full rewrite; FakeTheory::preRewrite() and FakeTheory::postRewrite() + // assert that the rewrite calls that are made match the expected sequence + // set up above + nOut = Rewriter::rewrite(n); + + // assert that the rewritten node is what we expect + ASSERT_EQ(nOut, nExpected); +} + +TEST_F(TestTheoryWhiteEngine, rewriter_complex) +{ + Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType()); + Node y = d_nodeManager->mkVar("y", d_nodeManager->realType()); + TypeNode u = d_nodeManager->mkSort("U"); + Node z1 = d_nodeManager->mkVar("z1", u); + Node z2 = d_nodeManager->mkVar("z2", u); + Node f = d_nodeManager->mkVar( + "f", + d_nodeManager->mkFunctionType(d_nodeManager->integerType(), + d_nodeManager->integerType())); + Node g = d_nodeManager->mkVar( + "g", + d_nodeManager->mkFunctionType(d_nodeManager->realType(), + d_nodeManager->integerType())); + Node one = d_nodeManager->mkConst(Rational("1")); + Node two = d_nodeManager->mkConst(Rational("2")); + + Node f1 = d_nodeManager->mkNode(APPLY_UF, f, one); + Node f2 = d_nodeManager->mkNode(APPLY_UF, f, two); + Node fx = d_nodeManager->mkNode(APPLY_UF, f, x); + Node ffx = d_nodeManager->mkNode(APPLY_UF, f, fx); + Node gy = d_nodeManager->mkNode(APPLY_UF, g, y); + Node z1eqz2 = d_nodeManager->mkNode(EQUAL, z1, z2); + Node f1eqf2 = d_nodeManager->mkNode(EQUAL, f1, f2); + Node ffxeqgy = d_nodeManager->mkNode(EQUAL, ffx, gy); + Node and1 = d_nodeManager->mkNode(AND, ffxeqgy, z1eqz2); + Node ffxeqf1 = d_nodeManager->mkNode(EQUAL, ffx, f1); + Node or1 = d_nodeManager->mkNode(OR, and1, ffxeqf1); + // make the expression: + // (IMPLIES (EQUAL (f 1) (f 2)) + // (OR (AND (EQUAL (f (f x)) (g y)) + // (EQUAL z1 z2)) + // (EQUAL (f (f x)) (f 1)))) + Node n = d_nodeManager->mkNode(IMPLIES, f1eqf2, or1); + Node nExpected = n; + Node nOut; + + // do a full rewrite; FakeTheory::preRewrite() and FakeTheory::postRewrite() + // assert that the rewrite calls that are made match the expected sequence + // set up above + nOut = Rewriter::rewrite(n); + + // assert that the rewritten node is what we expect + ASSERT_EQ(nOut, nExpected); +} + +TEST_F(TestTheoryWhiteEngine, rewrite_rules) +{ + TypeNode t = d_nodeManager->mkBitVectorType(8); + Node x = d_nodeManager->mkVar("x", t); + Node y = d_nodeManager->mkVar("y", t); + Node z = d_nodeManager->mkVar("z", t); + + // (x - y) * z --> (x * z) - (y * z) + Node expr = d_nodeManager->mkNode( + BITVECTOR_MULT, d_nodeManager->mkNode(BITVECTOR_SUB, x, y), z); + Node result = expr; + if (RewriteRule::applies(expr)) + { + result = RewriteRule::apply(expr); + } + Node expected = + d_nodeManager->mkNode(BITVECTOR_SUB, + d_nodeManager->mkNode(BITVECTOR_MULT, x, z), + d_nodeManager->mkNode(BITVECTOR_MULT, y, z)); + ASSERT_EQ(result, expected); + + // Try to apply MultSlice to a multiplication of two and three different + // variables, expect different results (x * y and x * y * z should not get + // rewritten to the same term). + expr = d_nodeManager->mkNode(BITVECTOR_MULT, x, y, z); + result = expr; + Node expr2 = d_nodeManager->mkNode(BITVECTOR_MULT, x, y); + Node result2 = expr; + if (RewriteRule::applies(expr)) + { + result = RewriteRule::apply(expr); + } + if (RewriteRule::applies(expr2)) + { + result2 = RewriteRule::apply(expr2); + } + ASSERT_NE(result, result2); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h deleted file mode 100644 index 04bc79b3a..000000000 --- a/test/unit/theory/theory_engine_white.h +++ /dev/null @@ -1,400 +0,0 @@ -/********************* */ -/*! \file theory_engine_white.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief White box testing of CVC4::theory::Theory. - ** - ** White box testing of CVC4::theory::Theory. This test creates - ** "fake" theory interfaces and injects them into TheoryEngine, so we - ** can test TheoryEngine's behavior without relying on independent - ** theory behavior. This is done in TheoryEngineWhite::setUp() by - ** means of the TheoryEngineWhite::registerTheory() interface. - **/ - -#include - -#include -#include -#include -#include - -#include "base/check.h" -#include "context/context.h" -#include "expr/kind.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "options/options.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/bv/theory_bv_rewrite_rules_normalization.h" -#include "theory/bv/theory_bv_rewrite_rules_simplification.h" -#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/rational.h" - -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::expr; -using namespace CVC4::context; -using namespace CVC4::kind; -using namespace CVC4::smt; -using namespace CVC4::theory::bv; - -using namespace std; - -class FakeOutputChannel : public OutputChannel { - void conflict(TNode n) override { Unimplemented(); } - bool propagate(TNode n) override { Unimplemented(); } - void lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) override - { - Unimplemented(); - } - void requirePhase(TNode, bool) override { Unimplemented(); } - void setIncomplete() override { Unimplemented(); } - void handleUserAttribute(const char* attr, Theory* t) override { - Unimplemented(); - } - void splitLemma(TNode n, bool removable) override { Unimplemented(); } -}; /* class FakeOutputChannel */ - -template -class FakeTheory; - -/** Expected rewrite calls can be PRE- or POST-rewrites */ -enum RewriteType { - PRE, - POST -};/* enum RewriteType */ - -/** - * Stores an "expected" rewrite call. The main test class will set up a sequence - * of these RewriteItems, then do a rewrite, ensuring that the actual call sequence - * matches the sequence of expected RewriteItems. */ -struct RewriteItem { - RewriteType d_type; -// FakeTheory* d_theory; - Node d_node; - 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. - */ -template -class FakeTheory : public Theory -{ - public: - FakeTheory(context::Context* ctxt, - context::UserContext* uctxt, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, pnm) - { - } - - TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } - - /** 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); - } - - /** - * 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::string identify() const override { - return "Fake" + d_id; - } - - void presolve() override { Unimplemented(); } - - void preRegisterTerm(TNode) override { Unimplemented(); } - void registerTerm(TNode) { Unimplemented(); } - void propagate(Theory::Effort) override { Unimplemented(); } - TrustNode explain(TNode) override - { - Unimplemented(); - return TrustNode::null(); - } - Node getValue(TNode n) { return Node::null(); } - - private: - /** - * This fake theory class is equally useful for bool, uf, arith, etc. It - * keeps an identifier to identify itself. - */ - std::string d_id; - - /** The theory rewriter for this theory. */ - FakeTheoryRewriter d_rewriter; -}; /* class FakeTheory */ - -/* definition of the s_expected static field in FakeTheory; see above */ -// std::deque FakeTheory::s_expected; - - -/** - * Test the TheoryEngine. - */ -class TheoryEngineWhite : public CxxTest::TestSuite { - Context* d_ctxt; - UserContext* d_uctxt; - - ExprManager* d_em; - NodeManager* d_nm; - SmtEngine* d_smt; - SmtScope* d_scope; - FakeOutputChannel *d_nullChannel; - TheoryEngine* d_theoryEngine; - -public: - - void setUp() override { - d_em = new ExprManager(); - d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_nm); - d_scope = new SmtScope(d_smt); - - d_ctxt = d_smt->getContext(); - d_uctxt = d_smt->getUserContext(); - - d_nullChannel = new FakeOutputChannel(); - - // Notice that this unit test uses the theory engine of a created SMT - // engine d_smt. We must ensure that d_smt is properly initialized via - // the following call, which constructs its underlying theory engine. - d_smt->finishInit(); - d_theoryEngine = d_smt->getTheoryEngine(); - for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) { - delete d_theoryEngine->d_theoryOut[id]; - delete d_theoryEngine->d_theoryTable[id]; - d_theoryEngine->d_theoryOut[id] = NULL; - d_theoryEngine->d_theoryTable[id] = NULL; - } - d_theoryEngine->addTheory< FakeTheory >(THEORY_BUILTIN); - d_theoryEngine->addTheory< FakeTheory >(THEORY_BOOL); - d_theoryEngine->addTheory< FakeTheory >(THEORY_UF); - d_theoryEngine->addTheory< FakeTheory >(THEORY_ARITH); - d_theoryEngine->addTheory< FakeTheory >(THEORY_ARRAYS); - d_theoryEngine->addTheory< FakeTheory >(THEORY_BV); - } - - void tearDown() override { - delete d_nullChannel; - - delete d_scope; - delete d_smt; - delete d_em; - } - - void testRewriterSimple() { - Node x = d_nm->mkVar("x", d_nm->integerType()); - Node y = d_nm->mkVar("y", d_nm->integerType()); - Node z = d_nm->mkVar("z", d_nm->integerType()); - - // make the expression (PLUS x y (MULT z 0)) - Node zero = d_nm->mkConst(Rational("0")); - Node zTimesZero = d_nm->mkNode(MULT, z, zero); - Node n = d_nm->mkNode(PLUS, x, y, zTimesZero); - - Node nExpected = n; - Node nOut; - -// // set up the expected sequence of calls -// FakeTheory::expect(PRE, d_arith, n, true); -// FakeTheory::expect(PRE, d_arith, x, false); -// FakeTheory::expect(POST, d_arith, x, false); -// FakeTheory::expect(PRE, d_arith, y, false); -// FakeTheory::expect(POST, d_arith, y, false); -// FakeTheory::expect(PRE, d_arith, zTimesZero, false); -// FakeTheory::expect(PRE, d_arith, z, false); -// FakeTheory::expect(POST, d_arith, z, false); -// FakeTheory::expect(PRE, d_arith, zero, false); -// FakeTheory::expect(POST, d_arith, zero, false); -// FakeTheory::expect(POST, d_arith, zTimesZero, false); -// FakeTheory::expect(POST, d_arith, n, true); - - // do a full rewrite; FakeTheory::preRewrite() and FakeTheory::postRewrite() - // assert that the rewrite calls that are made match the expected sequence - // set up above - nOut = Rewriter::rewrite(n); - - // assert that we consumed the sequence of expected calls completely -// TS_ASSERT(FakeTheory::nothingMoreExpected()); - - // assert that the rewritten node is what we expect -// TS_ASSERT_EQUALS(nOut, nExpected); - } - - void testRewriterComplicated() { - Node x = d_nm->mkVar("x", d_nm->integerType()); - Node y = d_nm->mkVar("y", d_nm->realType()); - TypeNode u = d_nm->mkSort("U"); - Node z1 = d_nm->mkVar("z1", u); - Node z2 = d_nm->mkVar("z2", u); - Node f = d_nm->mkVar("f", d_nm->mkFunctionType(d_nm->integerType(), - d_nm->integerType())); - Node g = d_nm->mkVar("g", d_nm->mkFunctionType(d_nm->realType(), - d_nm->integerType())); - Node one = d_nm->mkConst(Rational("1")); - Node two = d_nm->mkConst(Rational("2")); - - Node f1 = d_nm->mkNode(APPLY_UF, f, one); - Node f2 = d_nm->mkNode(APPLY_UF, f, two); - Node fx = d_nm->mkNode(APPLY_UF, f, x); - Node ffx = d_nm->mkNode(APPLY_UF, f, fx); - Node gy = d_nm->mkNode(APPLY_UF, g, y); - Node z1eqz2 = d_nm->mkNode(EQUAL, z1, z2); - Node f1eqf2 = d_nm->mkNode(EQUAL, f1, f2); - Node ffxeqgy = d_nm->mkNode(EQUAL, ffx, gy); - Node and1 = d_nm->mkNode(AND, ffxeqgy, z1eqz2); - Node ffxeqf1 = d_nm->mkNode(EQUAL, ffx, f1); - Node or1 = d_nm->mkNode(OR, and1, ffxeqf1); - // make the expression: - // (IMPLIES (EQUAL (f 1) (f 2)) - // (OR (AND (EQUAL (f (f x)) (g y)) - // (EQUAL z1 z2)) - // (EQUAL (f (f x)) (f 1)))) - Node n = d_nm->mkNode(IMPLIES, f1eqf2, or1); - Node nExpected = n; - Node nOut; - - // set up the expected sequence of calls -// FakeTheory::expect(PRE, d_bool, n, true); -// FakeTheory::expect(PRE, d_uf, f1eqf2, true); -// FakeTheory::expect(PRE, d_uf, f1, false); - //FakeTheory::expect(PRE, d_builtin, f, true); - //FakeTheory::expect(POST, d_builtin, f, true); -// FakeTheory::expect(PRE, d_arith, one, true); -// FakeTheory::expect(POST, d_arith, one, true); -// FakeTheory::expect(POST, d_uf, f1, false); -// FakeTheory::expect(PRE, d_uf, f2, false); - // these aren't called because they're in the rewrite cache - //FakeTheory::expect(PRE, d_builtin, f, true); - //FakeTheory::expect(POST, d_builtin, f, true); -// FakeTheory::expect(PRE, d_arith, two, true); -// FakeTheory::expect(POST, d_arith, two, true); -// FakeTheory::expect(POST, d_uf, f2, false); -// FakeTheory::expect(POST, d_uf, f1eqf2, true); -// FakeTheory::expect(PRE, d_bool, or1, false); -// FakeTheory::expect(PRE, d_bool, and1, false); -// FakeTheory::expect(PRE, d_uf, ffxeqgy, true); -// FakeTheory::expect(PRE, d_uf, ffx, false); -// FakeTheory::expect(PRE, d_uf, fx, false); - // these aren't called because they're in the rewrite cache - //FakeTheory::expect(PRE, d_builtin, f, true); - //FakeTheory::expect(POST, d_builtin, f, true); -// FakeTheory::expect(PRE, d_arith, x, true); -// FakeTheory::expect(POST, d_arith, x, true); -// FakeTheory::expect(POST, d_uf, fx, false); -// FakeTheory::expect(POST, d_uf, ffx, false); -// FakeTheory::expect(PRE, d_uf, gy, false); - //FakeTheory::expect(PRE, d_builtin, g, true); - //FakeTheory::expect(POST, d_builtin, g, true); -// FakeTheory::expect(PRE, d_arith, y, true); -// FakeTheory::expect(POST, d_arith, y, true); -// FakeTheory::expect(POST, d_uf, gy, false); -// FakeTheory::expect(POST, d_uf, ffxeqgy, true); -// FakeTheory::expect(PRE, d_uf, z1eqz2, true); -// FakeTheory::expect(PRE, d_uf, z1, false); -// FakeTheory::expect(POST, d_uf, z1, false); -// FakeTheory::expect(PRE, d_uf, z2, false); -// FakeTheory::expect(POST, d_uf, z2, false); -// FakeTheory::expect(POST, d_uf, z1eqz2, true); -// FakeTheory::expect(POST, d_bool, and1, false); -// FakeTheory::expect(PRE, d_uf, ffxeqf1, true); - // these aren't called because they're in the rewrite cache - //FakeTheory::expect(PRE, d_uf, ffx, false); - //FakeTheory::expect(POST, d_uf, ffx, false); - //FakeTheory::expect(PRE, d_uf, f1, false); - //FakeTheory::expect(POST, d_uf, f1, false); -// FakeTheory::expect(POST, d_uf, ffxeqf1, true); -// FakeTheory::expect(POST, d_bool, or1, false); -// FakeTheory::expect(POST, d_bool, n, true); - - // do a full rewrite; FakeTheory::preRewrite() and FakeTheory::postRewrite() - // assert that the rewrite calls that are made match the expected sequence - // set up above - nOut = Rewriter::rewrite(n); - - // assert that we consumed the sequence of expected calls completely -// TS_ASSERT(FakeTheory::nothingMoreExpected()); - - // assert that the rewritten node is what we expect -// TS_ASSERT_EQUALS(nOut, nExpected); - } - - void testRewriterRules() { - TypeNode t = d_nm->mkBitVectorType(8); - Node x = d_nm->mkVar("x", t); - Node y = d_nm->mkVar("y", t); - Node z = d_nm->mkVar("z", t); - - // (x - y) * z --> (x * z) - (y * z) - Node expr = - d_nm->mkNode(BITVECTOR_MULT, d_nm->mkNode(BITVECTOR_SUB, x, y), z); - Node result = expr; - if (RewriteRule::applies(expr)) { - result = RewriteRule::apply(expr); - } - Node expected = - d_nm->mkNode(BITVECTOR_SUB, d_nm->mkNode(BITVECTOR_MULT, x, z), - d_nm->mkNode(BITVECTOR_MULT, y, z)); - TS_ASSERT_EQUALS(result, expected); - - // Try to apply MultSlice to a multiplication of two and three different - // variables, expect different results (x * y and x * y * z should not get - // rewritten to the same term). - expr = d_nm->mkNode(BITVECTOR_MULT, x, y, z); - result = expr; - Node expr2 = d_nm->mkNode(BITVECTOR_MULT, x, y); - Node result2 = expr; - if (RewriteRule::applies(expr)) { - result = RewriteRule::apply(expr); - } - if (RewriteRule::applies(expr2)) { - result2 = RewriteRule::apply(expr2); - } - TS_ASSERT_DIFFERS(result, result2); - } -};