Remove replay and use-theory options and idl (#4186)

Towards disentangling Options / NodeManager / SmtEngine.

This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work.

The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it.

The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging.

It also removes the solver in src/theory/idl, which cannot be enabled after this commit.

5 files changed, 7 insertions, 86 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 80cce599f..f56f6a447 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -662,15 +662,6 @@ Lit Solver::pickBranchLit()
 {
     Lit nextLit;
 
-#ifdef CVC4_REPLAY
-
-    nextLit = MinisatSatSolver::toMinisatLit(d_proxy->getNextReplayDecision());
-
-    if (nextLit != lit_Undef) {
-      return nextLit;
-    }
-#endif /* CVC4_REPLAY */
-
     // Theory requests
     nextLit =
         MinisatSatSolver::toMinisatLit(d_proxy->getNextTheoryDecisionRequest());
@@ -1547,10 +1538,6 @@ lbool Solver::search(int nof_conflicts)
                     check_type = CHECK_FINAL;
                     continue;
                 }
-
-#ifdef CVC4_REPLAY
-                d_proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
-#endif /* CVC4_REPLAY */
             }
 
             // Increase decision level and enqueue 'next'
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2436aed04..89b919109 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -44,13 +44,6 @@
 using namespace std;
 using namespace CVC4::context;
 
-
-#ifdef CVC4_REPLAY
-#  define CVC4_USE_REPLAY true
-#else /* CVC4_REPLAY */
-#  define CVC4_USE_REPLAY false
-#endif /* CVC4_REPLAY */
-
 namespace CVC4 {
 namespace prop {
 
@@ -76,9 +69,7 @@ public:
 
 PropEngine::PropEngine(TheoryEngine* te,
                        Context* satContext,
-                       UserContext* userContext,
-                       std::ostream* replayLog,
-                       ExprStream* replayStream)
+                       UserContext* userContext)
     : d_inCheckSat(false),
       d_theoryEngine(te),
       d_context(satContext),
@@ -101,13 +92,8 @@ PropEngine::PropEngine(TheoryEngine* te,
   d_cnfStream = new CVC4::prop::TseitinCnfStream(
       d_satSolver, d_registrar, userContext, true);
 
-  d_theoryProxy = new TheoryProxy(this,
-                                  d_theoryEngine,
-                                  d_decisionEngine.get(),
-                                  d_context,
-                                  d_cnfStream,
-                                  replayLog,
-                                  replayStream);
+  d_theoryProxy = new TheoryProxy(
+      this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream);
   d_satSolver->initialize(d_context, d_theoryProxy);
 
   d_decisionEngine->setSatSolver(d_satSolver);
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 707244ff5..f1d73fc92 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -24,7 +24,6 @@
 #include <sys/time.h>
 
 #include "base/modal_exception.h"
-#include "expr/expr_stream.h"
 #include "expr/node.h"
 #include "options/options.h"
 #include "preprocessing/assertion_pipeline.h"
@@ -62,9 +61,7 @@ class PropEngine
    */
   PropEngine(TheoryEngine*,
              context::Context* satContext,
-             context::UserContext* userContext,
-             std::ostream* replayLog,
-             ExprStream* replayStream);
+             context::UserContext* userContext);
 
   /**
    * Destructor.
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 557dcc413..38c99f551 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -18,7 +18,6 @@
 
 #include "context/context.h"
 #include "decision/decision_engine.h"
-#include "expr/expr_stream.h"
 #include "options/decision_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
@@ -37,24 +36,17 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
                          TheoryEngine* theoryEngine,
                          DecisionEngine* decisionEngine,
                          context::Context* context,
-                         CnfStream* cnfStream,
-                         std::ostream* replayLog,
-                         ExprStream* replayStream)
+                         CnfStream* cnfStream)
     : d_propEngine(propEngine),
       d_cnfStream(cnfStream),
       d_decisionEngine(decisionEngine),
       d_theoryEngine(theoryEngine),
-      d_replayLog(replayLog),
-      d_replayStream(replayStream),
-      d_queue(context),
-      d_replayedDecisions("prop::theoryproxy::replayedDecisions", 0)
+      d_queue(context)
 {
-  smtStatisticsRegistry()->registerStat(&d_replayedDecisions);
 }
 
 TheoryProxy::~TheoryProxy() {
   /* nothing to do for now */
-  smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions);
 }
 
 void TheoryProxy::variableNotify(SatVariable var) {
@@ -150,29 +142,6 @@ void TheoryProxy::notifyRestart() {
   d_theoryEngine->notifyRestart();
 }
 
-SatLiteral TheoryProxy::getNextReplayDecision() {
-#ifdef CVC4_REPLAY
-  if(d_replayStream != NULL) {
-    Expr e = d_replayStream->nextExpr();
-    if(!e.isNull()) { // we get null node when out of decisions to replay
-      // convert & return
-      ++d_replayedDecisions;
-      return d_cnfStream->getLiteral(e);
-    }
-  }
-#endif /* CVC4_REPLAY */
-  return undefSatLiteral;
-}
-
-void TheoryProxy::logDecision(SatLiteral lit) {
-#ifdef CVC4_REPLAY
-  if(d_replayLog != NULL) {
-    Assert(lit != undefSatLiteral) << "logging an `undef' decision ?!";
-    (*d_replayLog) << d_cnfStream->getNode(lit) << std::endl;
-  }
-#endif /* CVC4_REPLAY */
-}
-
 void TheoryProxy::spendResource(ResourceManager::Resource r)
 {
   d_theoryEngine->spendResource(r);
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 0d76b473f..089d2082d 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -27,7 +27,6 @@
 #include <unordered_set>
 
 #include "context/cdqueue.h"
-#include "expr/expr_stream.h"
 #include "expr/node.h"
 #include "prop/sat_solver.h"
 #include "theory/theory.h"
@@ -54,9 +53,7 @@ class TheoryProxy
               TheoryEngine* theoryEngine,
               DecisionEngine* decisionEngine,
               context::Context* context,
-              CnfStream* cnfStream,
-              std::ostream* replayLog,
-              ExprStream* replayStream);
+              CnfStream* cnfStream);
 
   ~TheoryProxy();
 
@@ -83,10 +80,6 @@ class TheoryProxy
 
   void notifyRestart();
 
-  SatLiteral getNextReplayDecision();
-
-  void logDecision(SatLiteral lit);
-
   void spendResource(ResourceManager::Resource r);
 
   bool isDecisionEngineDone();
@@ -111,12 +104,6 @@ class TheoryProxy
   /** The theory engine we are using. */
   TheoryEngine* d_theoryEngine;
 
-  /** Stream on which to log replay events. */
-  std::ostream* d_replayLog;
-
-  /** Stream for replaying decisions. */
-  ExprStream* d_replayStream;
-
   /** Queue of asserted facts */
   context::CDQueue<TNode> d_queue;
 
@@ -126,11 +113,6 @@ class TheoryProxy
    */
   std::unordered_set<Node, NodeHashFunction> d_shared;
 
-  /**
-   * Statistic: the number of replayed decisions (via --replay).
-   */
-  IntStat d_replayedDecisions;
-
 }; /* class SatSolver */
 
 }/* CVC4::prop namespace */