Split abduction solver from SmtEngine (#4733)

This splits everything related to abducts into its own standalone module, AbductionSolver.

It furthermore converts some of the interfaces of SmtEngine to make them take Node instead of Expr (this will be done for every method eventually).

The code for interpolation should follow a similar pattern, e.g. InterpolantSolver.

1 files changed, 32 insertions, 68 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 8db8eadd5..f6b1d08bf 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -91,23 +91,25 @@ namespace prop {
 /* -------------------------------------------------------------------------- */
 
 namespace smt {
-  /**
-   * Representation of a defined function.  We keep these around in
-   * SmtEngine to permit expanding definitions late (and lazily), to
-   * support getValue() over defined functions, to support user output
-   * in terms of defined functions, etc.
-   */
-  class DefinedFunction;
-
-  struct SmtEngineStatistics;
-  class SmtEnginePrivate;
-  class SmtScope;
-  class ProcessAssertions;
-
-  ProofManager* currentProofManager();
-
-  struct CommandCleanup;
-  typedef context::CDList<Command*, CommandCleanup> CommandList;
+/** Subsolvers */
+class AbductionSolver;
+/**
+ * Representation of a defined function.  We keep these around in
+ * SmtEngine to permit expanding definitions late (and lazily), to
+ * support getValue() over defined functions, to support user output
+ * in terms of defined functions, etc.
+ */
+class DefinedFunction;
+
+struct SmtEngineStatistics;
+class SmtEnginePrivate;
+class SmtScope;
+class ProcessAssertions;
+
+ProofManager* currentProofManager();
+
+struct CommandCleanup;
+typedef context::CDList<Command*, CommandCleanup> CommandList;
 }/* CVC4::smt namespace */
 
 /* -------------------------------------------------------------------------- */
@@ -508,7 +510,7 @@ class CVC4_PUBLIC SmtEngine
    *
    * @throw TypeCheckingException, LogicException, UnsafeInterruptException
    */
-  Expr expandDefinitions(const Expr& e);
+  Node expandDefinitions(const Node& e);
 
   /**
    * Get the assigned value of an expr (only if immediately preceded by a SAT
@@ -660,10 +662,10 @@ class CVC4_PUBLIC SmtEngine
    * This method invokes a separate copy of the SMT engine for solving the
    * corresponding sygus problem for generating such a solution.
    */
-  bool getAbduct(const Expr& conj, const Type& grammarType, Expr& abd);
+  bool getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd);
 
   /** Same as above, but without user-provided grammar restrictions */
-  bool getAbduct(const Expr& conj, Expr& abd);
+  bool getAbduct(const Node& conj, Node& abd);
 
   /**
    * Get list of quantified formulas that were instantiated on the last call
@@ -898,6 +900,13 @@ class CVC4_PUBLIC SmtEngine
 
   /** Get the resource manager of this SMT engine */
   ResourceManager* getResourceManager();
+
+  /**
+   * Get expanded assertions.
+   *
+   * Return the set of assertions, after expanding definitions.
+   */
+  std::vector<Expr> getExpandedAssertions();
   /* .......................................................................  */
  private:
   /* .......................................................................  */
@@ -994,7 +1003,7 @@ class CVC4_PUBLIC SmtEngine
    * with the abduct and the goal is UNSAT. If these criteria are not met, an
    * internal error is thrown.
    */
-  void checkAbduct(Expr a);
+  void checkAbduct(Node a);
 
   /**
    * Postprocess a value for output to the user.  Involves doing things
@@ -1111,30 +1120,12 @@ class CVC4_PUBLIC SmtEngine
                               Expr func);
 
   /**
-   * Get abduct internal.
-   *
-   * Get the next abduct from the internal subsolver d_subsolver. If
-   * successful, this method returns true and sets abd to that abduct.
-   *
-   * This method assumes d_subsolver has been initialized to do abduction
-   * problems.
-   */
-  bool getAbductInternal(Expr& abd);
-
-  /**
    * Helper method to obtain both the heap and nil from the solver. Returns a
    * std::pair where the first element is the heap expression and the second
    * element is the nil expression.
    */
   std::pair<Expr, Expr> getSepHeapAndNilExpr();
 
-  /**
-   * Get expanded assertions.
-   *
-   * Return the set of assertions, after expanding definitions.
-   */
-  std::vector<Expr> getExpandedAssertions();
-
   /* Members -------------------------------------------------------------- */
 
   /** Solver instance that owns this SmtEngine instance. */
@@ -1171,35 +1162,8 @@ class CVC4_PUBLIC SmtEngine
   /** An index of our defined functions */
   DefinedFunctionMap* d_definedFunctions;
 
-  /** The SMT engine subsolver
-   *
-   * This is a separate copy of the SMT engine which is used for making
-   * calls that cannot be answered by this copy of the SMT engine. An example
-   * of invoking this subsolver is the get-abduct command, where we wish to
-   * solve a sygus conjecture based on the current assertions. In particular,
-   * consider the input:
-   *   (assert A)
-   *   (get-abduct B)
-   * In the copy of the SMT engine where these commands are issued, we maintain
-   * A in the assertion stack. To solve the abduction problem, instead of
-   * modifying the assertion stack to remove A and add the sygus conjecture
-   * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the
-   * assertion stack unchaged. This copy of the SMT engine can be further
-   * queried for information regarding further solutions.
-   */
-  std::unique_ptr<SmtEngine> d_subsolver;
-
-  /**
-   * If applicable, the function-to-synthesize that the subsolver is solving
-   * for. This is used for the get-abduct command.
-   */
-  Expr d_sssf;
-
-  /**
-   * The conjecture of the current abduction problem. This expression is only
-   * valid while we are in mode SMT_MODE_ABDUCT.
-   */
-  Expr d_abdConj;
+  /** The solver for abduction queries */
+  std::unique_ptr<smt::AbductionSolver> d_abductSolver;
 
   /**
    * The assertion list (before any conversion) for supporting