Split SmtSolver from SmtEngine (#4880)

This class is responsible for maintaining TheoryEngine and PropEngine and implementing the check-sat command. It also has an interface for processing/pushing the current assertions into the PropEngine.

This class will be used directly by other extension solvers (for abduction, interpolation, qe, sygus, etc.).

1 files changed, 12 insertions, 27 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 4df57accb..1c71e371e 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -103,6 +103,7 @@ class SmtNodeManagerListener;
 class OptionsManager;
 class Preprocessor;
 /** Subsolvers */
+class SmtSolver;
 class AbductionSolver;
 /**
  * Representation of a defined function.  We keep these around in
@@ -149,6 +150,7 @@ class CVC4_PUBLIC SmtEngine
   friend class ::CVC4::smt::SmtEngineState;
   friend class ::CVC4::smt::SmtScope;
   friend class ::CVC4::smt::ProcessAssertions;
+  friend class ::CVC4::smt::SmtSolver;
   friend ProofManager* ::CVC4::smt::currentProofManager();
   friend class ::CVC4::LogicRequest;
   friend class ::CVC4::theory::TheoryModel;
@@ -908,10 +910,10 @@ class CVC4_PUBLIC SmtEngine
   context::Context* getContext();
 
   /** Get a pointer to the TheoryEngine owned by this SmtEngine. */
-  TheoryEngine* getTheoryEngine() { return d_theoryEngine.get(); }
+  TheoryEngine* getTheoryEngine();
 
   /** Get a pointer to the PropEngine owned by this SmtEngine. */
-  prop::PropEngine* getPropEngine() { return d_propEngine.get(); }
+  prop::PropEngine* getPropEngine();
 
   /** Get a pointer to the ProofManager owned by this SmtEngine. */
   ProofManager* getProofManager() { return d_proofManager.get(); };
@@ -989,12 +991,6 @@ class CVC4_PUBLIC SmtEngine
   void shutdown();
 
   /**
-   * Full check of consistency in current context.  Returns true iff
-   * consistent.
-   */
-  Result check();
-
-  /**
    * Quick check of consistency in current context: calls
    * processAssertionList() then look for inconsistency (based only on
    * that).
@@ -1050,14 +1046,6 @@ class CVC4_PUBLIC SmtEngine
   void setLogicInternal();
 
   /**
-   * Process the assertions that have been asserted. This moves the set of
-   * assertions that have been buffered into the smt::Assertions object,
-   * preprocesses them, pushes them into the SMT solver, and clears the
-   * buffer.
-   */
-  void processAssertionsInternal();
-
-  /**
    * Add to Model command.  This is used for recording a command
    * that should be reported during a get-model call.
    */
@@ -1066,13 +1054,12 @@ class CVC4_PUBLIC SmtEngine
                                 bool userVisible = true,
                                 const char* dumpTag = "declarations");
 
-  /* Check satisfiability (used to check satisfiability and entailment). */
-  Result checkSatisfiability(const Node& assumption,
-                             bool inUnsatCore,
-                             bool isEntailmentCheck);
-  Result checkSatisfiability(const std::vector<Node>& assumptions,
-                             bool inUnsatCore,
-                             bool isEntailmentCheck);
+  /*
+   * Check satisfiability (used to check satisfiability and entailment).
+   */
+  Result checkSatInternal(const std::vector<Node>& assumptions,
+                          bool inUnsatCore,
+                          bool isEntailmentCheck);
 
   /**
    * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
@@ -1125,10 +1112,8 @@ class CVC4_PUBLIC SmtEngine
   /** Node manager listener */
   std::unique_ptr<smt::SmtNodeManagerListener> d_snmListener;
 
-  /** The theory engine */
-  std::unique_ptr<TheoryEngine> d_theoryEngine;
-  /** The propositional engine */
-  std::unique_ptr<prop::PropEngine> d_propEngine;
+  /** The SMT solver */
+  std::unique_ptr<smt::SmtSolver> d_smtSolver;
 
   /** The proof manager */
   std::unique_ptr<ProofManager> d_proofManager;