From a22deeb091673226a1edb5a89bc8a596a3d51fc7 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 11 Mar 2021 23:48:11 +0100 Subject: Make linear arithmetic use its inference manager (#5934) This PR refactors the linear arithmetic solver to properly use its inference manager, instead of directly sending lemmas to the output channel. To do this, it introduces new InferenceIds for the various linear lemmas. --- test/unit/theory/theory_arith_white.cpp | 185 +------------------------------- test/unit/theory/theory_white.cpp | 18 ---- 2 files changed, 1 insertion(+), 202 deletions(-) (limited to 'test/unit') diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 09757a304..d0ed5718e 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -43,19 +43,9 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit TestSmtNoFinishInit::SetUp(); d_smtEngine->setOption("incremental", "false"); d_smtEngine->finishInit(); - d_context = d_smtEngine->getContext(); - d_user_context = d_smtEngine->getUserContext(); - d_outputChannel.clear(); - d_logicInfo.lock(); - d_smtEngine->getTheoryEngine() - ->d_theoryTable[THEORY_ARITH] - ->setOutputChannel(d_outputChannel); d_arith = static_cast( d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_ARITH]); - d_preregistered.reset(new std::set()); - - d_booleanType.reset(new TypeNode(d_nodeManager->booleanType())); d_realType.reset(new TypeNode(d_nodeManager->realType())); d_intType.reset(new TypeNode(d_nodeManager->integerType())); } @@ -63,57 +53,15 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit void fakeTheoryEnginePreprocess(TNode input) { Assert(input == Rewriter::rewrite(input)); - Node rewrite = input; - if (d_debug) - { - std::cout << "input " << input << " rewrite " << rewrite << std::endl; - } - - std::list toPreregister; - - toPreregister.push_back(rewrite); - for (std::list::iterator i = toPreregister.begin(); - i != toPreregister.end(); - ++i) - { - Node n = *i; - d_preregistered->insert(n); - - for (Node::iterator citer = n.begin(); citer != n.end(); ++citer) - { - Node c = *citer; - if (d_preregistered->find(c) == d_preregistered->end()) - { - toPreregister.push_back(c); - } - } - } - for (std::list::reverse_iterator i = toPreregister.rbegin(); - i != toPreregister.rend(); - ++i) - { - Node n = *i; - if (d_debug) - { - std::cout << "id " << n.getId() << " " << n << std::endl; - } - d_arith->preRegisterTerm(n); - } + d_smtEngine->getTheoryEngine()->preRegister(input); } - Context* d_context; - UserContext* d_user_context; - DummyOutputChannel d_outputChannel; - LogicInfo d_logicInfo; Theory::Effort d_level = Theory::EFFORT_FULL; TheoryArith* d_arith; - std::unique_ptr> d_preregistered; - std::unique_ptr d_booleanType; std::unique_ptr d_realType; std::unique_ptr d_intType; const Rational d_zero = 0; const Rational d_one = 1; - bool d_debug = false; }; TEST_F(TestTheoryWhiteArith, assert) @@ -128,137 +76,6 @@ TEST_F(TestTheoryWhiteArith, assert) d_arith->assertFact(leq, true); d_arith->check(d_level); - - ASSERT_EQ(d_outputChannel.getNumCalls(), 0u); -} - -TEST_F(TestTheoryWhiteArith, TPLt1) -{ - Node x = d_nodeManager->mkVar(*d_realType); - Node c0 = d_nodeManager->mkConst(d_zero); - Node c1 = d_nodeManager->mkConst(d_one); - - Node gt0 = d_nodeManager->mkNode(GT, x, c0); - Node gt1 = d_nodeManager->mkNode(GT, x, c1); - Node geq1 = d_nodeManager->mkNode(GEQ, x, c1); - Node leq0 = Rewriter::rewrite(gt0.notNode()); - Node leq1 = Rewriter::rewrite(gt1.notNode()); - Node lt1 = Rewriter::rewrite(geq1.notNode()); - - fakeTheoryEnginePreprocess(leq0); - fakeTheoryEnginePreprocess(leq1); - fakeTheoryEnginePreprocess(geq1); - - d_arith->presolve(); - d_arith->assertFact(lt1, true); - d_arith->check(d_level); - d_arith->propagate(d_level); - - Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1; - Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1; - gt0OrLt1 = Rewriter::rewrite(gt0OrLt1); - geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1); - - std::cout << d_outputChannel.getIthNode(0) << std::endl << std::endl; - std::cout << d_outputChannel.getIthNode(1) << std::endl << std::endl; - std::cout << d_outputChannel.getIthNode(2) << std::endl << std::endl; - - ASSERT_EQ(d_outputChannel.getNumCalls(), 3u); - - ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA); - ASSERT_TRUE(d_outputChannel.getIthNode(0) == gt0OrLt1); - - ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA); - ASSERT_TRUE(d_outputChannel.getIthNode(1) == geq0OrLeq1); - - ASSERT_EQ(d_outputChannel.getIthCallType(2), PROPAGATE); - ASSERT_EQ(d_outputChannel.getIthNode(2), leq1); -} - -TEST_F(TestTheoryWhiteArith, TPLeq0) -{ - Node x = d_nodeManager->mkVar(*d_realType); - Node c0 = d_nodeManager->mkConst(d_zero); - Node c1 = d_nodeManager->mkConst(d_one); - - Node gt0 = d_nodeManager->mkNode(GT, x, c0); - Node gt1 = d_nodeManager->mkNode(GT, x, c1); - Node geq1 = d_nodeManager->mkNode(GEQ, x, c1); - Node leq0 = Rewriter::rewrite(gt0.notNode()); - Node leq1 = Rewriter::rewrite(gt1.notNode()); - Node lt1 = Rewriter::rewrite(geq1.notNode()); - - fakeTheoryEnginePreprocess(leq0); - fakeTheoryEnginePreprocess(leq1); - fakeTheoryEnginePreprocess(geq1); - - d_arith->presolve(); - d_arith->assertFact(leq0, true); - d_arith->check(d_level); - d_arith->propagate(d_level); - - Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1; - Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1; - gt0OrLt1 = Rewriter::rewrite(gt0OrLt1); - geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1); - - std::cout << d_outputChannel.getIthNode(0) << std::endl; - std::cout << d_outputChannel.getIthNode(1) << std::endl; - std::cout << d_outputChannel.getIthNode(2) << std::endl; - std::cout << d_outputChannel.getIthNode(3) << std::endl; - - ASSERT_EQ(d_outputChannel.getNumCalls(), 4u); - - ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA); - ASSERT_EQ(d_outputChannel.getIthNode(0), gt0OrLt1); - - ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA); - ASSERT_EQ(d_outputChannel.getIthNode(1), geq0OrLeq1); - - ASSERT_EQ(d_outputChannel.getIthCallType(2), PROPAGATE); - ASSERT_EQ(d_outputChannel.getIthNode(2), lt1); - - ASSERT_EQ(d_outputChannel.getIthCallType(3), PROPAGATE); - ASSERT_EQ(d_outputChannel.getIthNode(3), leq1); -} - -TEST_F(TestTheoryWhiteArith, TPLeq1) -{ - Node x = d_nodeManager->mkVar(*d_realType); - Node c0 = d_nodeManager->mkConst(d_zero); - Node c1 = d_nodeManager->mkConst(d_one); - - Node gt0 = d_nodeManager->mkNode(GT, x, c0); - Node gt1 = d_nodeManager->mkNode(GT, x, c1); - Node geq1 = d_nodeManager->mkNode(GEQ, x, c1); - Node leq0 = Rewriter::rewrite(gt0.notNode()); - Node leq1 = Rewriter::rewrite(gt1.notNode()); - Node lt1 = Rewriter::rewrite(geq1.notNode()); - - fakeTheoryEnginePreprocess(leq0); - fakeTheoryEnginePreprocess(leq1); - fakeTheoryEnginePreprocess(geq1); - - d_arith->presolve(); - d_arith->assertFact(leq1, true); - d_arith->check(d_level); - d_arith->propagate(d_level); - - Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1; - Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1; - gt0OrLt1 = Rewriter::rewrite(gt0OrLt1); - geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1); - - std::cout << d_outputChannel.getIthNode(0) << std::endl; - std::cout << d_outputChannel.getIthNode(1) << std::endl; - - ASSERT_EQ(d_outputChannel.getNumCalls(), 2u); - - ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA); - ASSERT_EQ(d_outputChannel.getIthNode(0), gt0OrLt1); - - ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA); - ASSERT_EQ(d_outputChannel.getIthNode(1), geq0OrLeq1); } TEST_F(TestTheoryWhiteArith, int_normal_form) diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp index f66d81b94..048fac5ac 100644 --- a/test/unit/theory/theory_white.cpp +++ b/test/unit/theory/theory_white.cpp @@ -97,24 +97,6 @@ TEST_F(TestTheoryWhite, done) ASSERT_TRUE(d_dummy_theory->done()); } -TEST_F(TestTheoryWhite, outputChannel_accessors) -{ - /* void setOutputChannel(OutputChannel& out) */ - /* OutputChannel& getOutputChannel() */ - - DummyOutputChannel theOtherChannel; - - ASSERT_EQ(&(d_dummy_theory->getOutputChannel()), &d_outputChannel); - - d_dummy_theory->setOutputChannel(theOtherChannel); - - ASSERT_EQ(&(d_dummy_theory->getOutputChannel()), &theOtherChannel); - - const OutputChannel& oc = d_dummy_theory->getOutputChannel(); - - ASSERT_EQ(&oc, &theOtherChannel); -} - TEST_F(TestTheoryWhite, outputChannel) { Node n = d_atom0.orNode(d_atom1); -- cgit v1.2.3