Support get-abduct smt2 command (#3122)

4 files changed, 298 insertions, 19 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index b1936d8cc..044062f77 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2033,6 +2033,90 @@ std::string GetSynthSolutionCommand::getCommandName() const
   return "get-instantiations";
 }
 
+GetAbductCommand::GetAbductCommand() {}
+GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj)
+    : d_name(name), d_conj(conj), d_resultStatus(false)
+{
+}
+GetAbductCommand::GetAbductCommand(const std::string& name,
+                                   Expr conj,
+                                   const Type& gtype)
+    : d_name(name),
+      d_conj(conj),
+      d_sygus_grammar_type(gtype),
+      d_resultStatus(false)
+{
+}
+
+Expr GetAbductCommand::getConjecture() const { return d_conj; }
+Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; }
+Expr GetAbductCommand::getResult() const { return d_result; }
+
+void GetAbductCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    if (d_sygus_grammar_type.isNull())
+    {
+      d_resultStatus = smtEngine->getAbduct(d_conj, d_result);
+    }
+    else
+    {
+      d_resultStatus =
+          smtEngine->getAbduct(d_conj, d_sygus_grammar_type, d_result);
+    }
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+  if (!ok())
+  {
+    this->Command::printResult(out, verbosity);
+  }
+  else
+  {
+    expr::ExprDag::Scope scope(out, false);
+    if (d_resultStatus)
+    {
+      out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+          << std::endl;
+    }
+    else
+    {
+      out << "none" << std::endl;
+    }
+  }
+}
+
+Command* GetAbductCommand::exportTo(ExprManager* exprManager,
+                                    ExprManagerMapCollection& variableMap)
+{
+  GetAbductCommand* c =
+      new GetAbductCommand(d_name, d_conj.exportTo(exprManager, variableMap));
+  c->d_sygus_grammar_type =
+      d_sygus_grammar_type.exportTo(exprManager, variableMap);
+  c->d_result = d_result.exportTo(exprManager, variableMap);
+  c->d_resultStatus = d_resultStatus;
+  return c;
+}
+
+Command* GetAbductCommand::clone() const
+{
+  GetAbductCommand* c = new GetAbductCommand(d_name, d_conj);
+  c->d_sygus_grammar_type = d_sygus_grammar_type;
+  c->d_result = d_result;
+  c->d_resultStatus = d_resultStatus;
+  return c;
+}
+
+std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
+
 /* -------------------------------------------------------------------------- */
 /* class GetQuantifierEliminationCommand                                      */
 /* -------------------------------------------------------------------------- */
diff --git a/src/smt/command.h b/src/smt/command.h
index 68f9d1881..eb3199944 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1009,6 +1009,56 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
   SmtEngine* d_smtEngine;
 }; /* class GetSynthSolutionCommand */
 
+/** The command (get-abduct s B (G)?)
+ *
+ * This command asks for an abduct from the current set of assertions and
+ * conjecture (goal) given by the argument B.
+ *
+ * The symbol s is the name for the abduction predicate. If we successfully
+ * find a predicate P, then the output response of this command is:
+ *   (define-fun s () Bool P)
+ *
+ * A grammar type G can be optionally provided to indicate the syntactic
+ * restrictions on the possible solutions returned.
+ */
+class CVC4_PUBLIC GetAbductCommand : public Command
+{
+ public:
+  GetAbductCommand();
+  GetAbductCommand(const std::string& name, Expr conj);
+  GetAbductCommand(const std::string& name, Expr conj, const Type& gtype);
+
+  /** Get the conjecture of the abduction query */
+  Expr getConjecture() const;
+  /** Get the grammar type given for the abduction query */
+  Type getGrammarType() const;
+  /** Get the result of the query, which is the solution to the abduction query.
+   */
+  Expr getResult() const;
+
+  void invoke(SmtEngine* smtEngine) override;
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  Command* clone() const override;
+  std::string getCommandName() const override;
+
+ protected:
+  /** The name of the abduction predicate */
+  std::string d_name;
+  /** The conjecture of the abduction query */
+  Expr d_conj;
+  /**
+   * The (optional) grammar of the abduction query, expressed as a sygus
+   * datatype type.
+   */
+  Type d_sygus_grammar_type;
+  /** the return status of the command */
+  bool d_resultStatus;
+  /** the return expression of the command */
+  Expr d_result;
+}; /* class GetAbductCommand */
+
 class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
 {
  protected:
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5e8540348..5db3fc43d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -98,6 +98,7 @@
 #include "theory/quantifiers/fun_def_process.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/single_inv_partition.h"
+#include "theory/quantifiers/sygus/sygus_abduct.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
@@ -1258,21 +1259,25 @@ void SmtEngine::setDefaults() {
   // sygus inference may require datatypes
   if (!d_isInternalSubsolver)
   {
-    if (options::sygusInference() || options::sygusRewSynthInput()
-        || options::sygusAbduct())
+    if (options::produceAbducts())
+    {
+      // we may invoke a sygus conjecture, hence we need options related to
+      // sygus
+      is_sygus = true;
+    }
+    if (options::sygusInference() || options::sygusRewSynthInput())
     {
-      d_logic = d_logic.getUnlockedCopy();
-      // sygus requires arithmetic, datatypes and quantifiers
-      d_logic.enableTheory(THEORY_ARITH);
-      d_logic.enableTheory(THEORY_DATATYPES);
-      d_logic.enableTheory(THEORY_QUANTIFIERS);
-      d_logic.lock();
       // since we are trying to recast as sygus, we assume the input is sygus
       is_sygus = true;
+      // we change the logic to incorporate sygus immediately
+      d_logic = d_logic.getUnlockedCopy();
+      d_logic.enableSygus();
+      d_logic.lock();
     }
   }
 
   if ((options::checkModels() || options::checkSynthSol()
+       || options::produceAbducts()
        || options::modelCoresMode() != MODEL_CORES_NONE)
       && !options::produceAssertions())
   {
@@ -1954,16 +1959,24 @@ void SmtEngine::setDefaults() {
         options::sygusExtRew.set(false);
       }
     }
-    if (options::sygusAbduct())
+    // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
+    // is one that is specialized for returning a single solution. Non-basic
+    // sygus algorithms currently include the PBE solver, static template
+    // inference for invariant synthesis, and single invocation techniques.
+    bool reqBasicSygus = false;
+    if (options::produceAbducts())
     {
       // if doing abduction, we should filter strong solutions
       if (!options::sygusFilterSolMode.wasSetByUser())
       {
         options::sygusFilterSolMode.set(quantifiers::SYGUS_FILTER_SOL_STRONG);
       }
+      // we must use basic sygus algorithms, since e.g. we require checking
+      // a sygus side condition for consistency with axioms.
+      reqBasicSygus = true;
     }
     if (options::sygusRewSynth() || options::sygusRewVerify()
-        || options::sygusQueryGen() || options::sygusAbduct())
+        || options::sygusQueryGen())
     {
       // rewrite rule synthesis implies that sygus stream must be true
       options::sygusStream.set(true);
@@ -1971,9 +1984,12 @@ void SmtEngine::setDefaults() {
     if (options::sygusStream())
     {
       // Streaming is incompatible with techniques that focus the search towards
-      // finding a single solution. This currently includes the PBE solver,
-      // static template inference for invariant synthesis, and single
-      // invocation techniques.
+      // finding a single solution.
+      reqBasicSygus = true;
+    }
+    // Now, disable options for non-basic sygus algorithms, if necessary.
+    if (reqBasicSygus)
+    {
       if (!options::sygusUnifPbe.wasSetByUser())
       {
         options::sygusUnifPbe.set(false);
@@ -2291,11 +2307,11 @@ void SmtEngine::setDefaults() {
           "--sygus-expr-miner-check-timeout=N requires "
           "--sygus-expr-miner-check-use-export");
     }
-    if (options::sygusRewSynthInput() || options::sygusAbduct())
+    if (options::sygusRewSynthInput() || options::produceAbducts())
     {
       std::stringstream ss;
       ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input"
-                                           : "--sygus-abduct");
+                                           : "--produce-abducts");
       ss << "requires --sygus-expr-miner-check-use-export";
       throw OptionException(ss.str());
     }
@@ -3325,10 +3341,6 @@ void SmtEnginePrivate::processAssertions() {
     {
       d_passes["sygus-infer"]->apply(&d_assertions);
     }
-    else if (options::sygusAbduct())
-    {
-      d_passes["sygus-abduct"]->apply(&d_assertions);
-    }
     else if (options::sygusRewSynthInput())
     {
       // do candidate rewrite rule synthesis
@@ -4961,6 +4973,96 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
   }
 }
 
+bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
+{
+  SmtScope smts(this);
+
+  if (!options::produceAbducts())
+  {
+    const char* msg = "Cannot get abduct when produce-abducts options is off.";
+    throw ModalException(msg);
+  }
+  Trace("sygus-abduct") << "SmtEngine::getAbduct: conjecture " << conj
+                        << std::endl;
+  std::vector<Expr> easserts = getAssertions();
+  std::vector<Node> axioms;
+  for (unsigned i = 0, size = easserts.size(); i < size; i++)
+  {
+    axioms.push_back(Node::fromExpr(easserts[i]));
+  }
+  std::vector<Node> asserts(axioms.begin(), axioms.end());
+  asserts.push_back(Node::fromExpr(conj));
+  d_sssfVarlist.clear();
+  d_sssfSyms.clear();
+  std::string name("A");
+  Node aconj = theory::quantifiers::SygusAbduct::mkAbductionConjecture(
+      name,
+      asserts,
+      axioms,
+      TypeNode::fromType(grammarType),
+      d_sssfVarlist,
+      d_sssfSyms);
+  // should be a quantified conjecture with one function-to-synthesize
+  Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1);
+  // remember the abduct-to-synthesize
+  d_sssf = aconj[0][0].toExpr();
+  Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj
+                        << ", solving for " << d_sssf << std::endl;
+  // we generate a new smt engine to do the abduction query
+  d_subsolver.reset(new SmtEngine(NodeManager::currentNM()->toExprManager()));
+  d_subsolver->setIsInternalSubsolver();
+  // get the logic
+  LogicInfo l = d_logic.getUnlockedCopy();
+  // enable everything needed for sygus
+  l.enableSygus();
+  d_subsolver->setLogic(l);
+  // assert the abduction query
+  d_subsolver->assertFormula(aconj.toExpr());
+  Trace("sygus-abduct") << "  SmtEngine::getAbduct check sat..." << std::endl;
+  Result r = d_subsolver->checkSat();
+  Trace("sygus-abduct") << "  SmtEngine::getAbduct result: " << r << std::endl;
+  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+  {
+    // get the synthesis solution
+    std::map<Expr, Expr> sols;
+    d_subsolver->getSynthSolutions(sols);
+    Assert(sols.size() == 1);
+    std::map<Expr, Expr>::iterator its = sols.find(d_sssf);
+    if (its != sols.end())
+    {
+      Node abdn = Node::fromExpr(its->second);
+      Trace("sygus-abduct")
+          << "SmtEngine::getAbduct: solution is " << abdn << std::endl;
+      if (abdn.getKind() == kind::LAMBDA)
+      {
+        abdn = abdn[1];
+      }
+      // convert back to original
+      // must replace formal arguments of abd with the free variables in the
+      // input problem that they correspond to.
+      abdn = abdn.substitute(d_sssfVarlist.begin(),
+                             d_sssfVarlist.end(),
+                             d_sssfSyms.begin(),
+                             d_sssfSyms.end());
+
+      // convert to expression
+      abd = abdn.toExpr();
+
+      return true;
+    }
+    Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!"
+                          << std::endl;
+    throw RecoverableModalException("Could not find solution for get-abduct.");
+  }
+  return false;
+}
+
+bool SmtEngine::getAbduct(const Expr& conj, Expr& abd)
+{
+  Type grammarType;
+  return getAbduct(conj, grammarType, abd);
+}
+
 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) {
   SmtScope smts(this);
   if( d_theoryEngine ){
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5913716e6..566777a89 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -147,6 +147,34 @@ class CVC4_PUBLIC SmtEngine {
   ProofManager* d_proofManager;
   /** 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 substitution to apply to the solutions from the subsolver, used for
+   * the get-abduct command.
+   */
+  std::vector<Node> d_sssfVarlist;
+  std::vector<Node> d_sssfSyms;
   /** recursive function definition abstractions for --fmf-fun */
   std::map< Node, TypeNode > d_fmfRecFunctionsAbs;
   std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete;
@@ -849,6 +877,21 @@ class CVC4_PUBLIC SmtEngine {
   Expr doQuantifierElimination(const Expr& e,
                                bool doFull,
                                bool strict = true) /* throw(Exception) */;
+  /**
+   * This method asks this SMT engine to find an abduct with respect to the
+   * current assertion stack (call it A) and the conjecture (call it B).
+   * If this method returns true, then abd is set to a formula C such that
+   * A ^ C is satisfiable, and A ^ B ^ C is unsatisfiable.
+   *
+   * The argument grammarType is a sygus datatype type that encodes the syntax
+   * restrictions on the shape of possible solutions.
+   *
+   * 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);
+  /** Same as above, but without user-provided grammar restrictions */
+  bool getAbduct(const Expr& conj, Expr& abd);
 
   /**
    * Get list of quantified formulas that were instantiated