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.

2 files changed, 1 insertions, 202 deletions

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<TheoryArith*>(
         d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_ARITH]);
 
-    d_preregistered.reset(new std::set<Node>());
-
-    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<Node> toPreregister;
-
-    toPreregister.push_back(rewrite);
-    for (std::list<Node>::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<Node>::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<std::set<Node>> d_preregistered;
-  std::unique_ptr<TypeNode> d_booleanType;
   std::unique_ptr<TypeNode> d_realType;
   std::unique_ptr<TypeNode> 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<Rational>(d_zero);
-  Node c1 = d_nodeManager->mkConst<Rational>(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<Rational>(d_zero);
-  Node c1 = d_nodeManager->mkConst<Rational>(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<Rational>(d_zero);
-  Node c1 = d_nodeManager->mkConst<Rational>(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);