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.

1 files changed, 0 insertions, 55 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 72e175a58..cd4105cd0 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -26,7 +26,6 @@
 
 #include "api/cvc4cpp.h"
 #include "expr/expr.h"
-#include "expr/expr_stream.h"
 #include "expr/kind.h"
 #include "expr/symbol_table.h"
 #include "parser/input.h"
@@ -806,63 +805,9 @@ public:
     d_globalDeclarations = flag;
   }
 
-  /**
-   * Set the current symbol table used by this parser.
-   * From now on, this parser will perform its definitions and
-   * lookups in the declaration scope of the "parser" argument
-   * (but doesn't re-delegate if the other parser's declaration scope
-   * changes later).  A NULL argument restores this parser's
-   * "primordial" declaration scope assigned at its creation.  Calling
-   * p->useDeclarationsFrom(p) is a no-op.
-   *
-   * This feature is useful when e.g. reading out-of-band expression data:
-   * 1. Parsing --replay log files produced with --replay-log.
-   * 2. Perhaps a multi-query benchmark file is being single-stepped
-   *    with intervening queries on stdin that must reference the same
-   *    declaration scope(s).
-   *
-   * However, the feature must be used carefully.  Pushes and pops
-   * should be performed with the correct current declaration scope.
-   * Care must be taken to match up declaration scopes, of course;
-   * If variables in the deferred-to parser go out of scope, the
-   * secondary parser will give errors that they are undeclared.
-   * Also, an outer-scope variable shadowed by an inner-scope one of
-   * the same name may be temporarily inaccessible.
-   *
-   * In short, caveat emptor.
-   */
-  inline void useDeclarationsFrom(Parser* parser) {
-    if(parser == NULL) {
-      d_symtab = &d_symtabAllocated;
-    } else {
-      d_symtab = parser->d_symtab;
-    }
-  }
-
-  inline void useDeclarationsFrom(SymbolTable* symtab) {
-    d_symtab = symtab;
-  }
-
   inline SymbolTable* getSymbolTable() const {
     return d_symtab;
   }
-
-  /**
-   * An expression stream interface for a parser.  This stream simply
-   * pulls expressions from the given Parser object.
-   *
-   * Here, the ExprStream base class allows a Parser (from the parser
-   * library) and core components of CVC4 (in the core library) to
-   * communicate without polluting the public interface or having them
-   * reach into private (undocumented) interfaces.
-   */
-  class ExprStream : public CVC4::ExprStream {
-    Parser* d_parser;
-  public:
-    ExprStream(Parser* parser) : d_parser(parser) {}
-    ~ExprStream() { delete d_parser; }
-    Expr nextExpr() override { return d_parser->nextExpression().getExpr(); }
-  };/* class Parser::ExprStream */
   
   //------------------------ operator overloading
   /** is this function overloaded? */