Do not make SyGuS subsolver in unsat state after solving (#7759)

This makes subsolvers answer "unknown" instead of "unsat" when solving SyGuS inputs, by setting unknown when a SyGuS input is solved instead of asserting the negation of the input. Knowing whether the call was successful is simply obtained by calling getSynthSolutions.

This will allow for multiple solutions for the same conjecture.

12 files changed, 81 insertions, 50 deletions

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 7ebb3ab80..cdbd6099e 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -301,15 +301,13 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions,
   Trace("sygus-infer") << "*** Check sat..." << std::endl;
   Result r = rrSygus->checkSat();
   Trace("sygus-infer") << "...result : " << r << std::endl;
-  if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+  // get the synthesis solutions
+  std::map<Node, Node> synth_sols;
+  if (!rrSygus->getSubsolverSynthSolutions(synth_sols))
   {
     // failed, conjecture was infeasible
     return false;
   }
-  // get the synthesis solutions
-  std::map<Node, Node> synth_sols;
-  bool sinferSol = rrSygus->getSubsolverSynthSolutions(synth_sols);
-  AlwaysAssert(sinferSol) << "Failed to get solutions for sygus-inference";
 
   std::vector<Node> final_ff;
   std::vector<Node> final_ff_sol;
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index a5a180ffb..f17e768c9 100644
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -94,13 +94,12 @@ bool AbductionSolver::getAbductInternal(const std::vector<Node>& axioms,
   Result r = d_subsolver->checkSat();
   Trace("sygus-abduct") << "  SolverEngine::getAbduct result: " << r
                         << std::endl;
-  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+  // get the synthesis solution
+  std::map<Node, Node> sols;
+  // use the "getSubsolverSynthSolutions" interface, since we asserted the
+  // internal form of the SyGuS conjecture and used check-sat.
+  if (d_subsolver->getSubsolverSynthSolutions(sols))
   {
-    // get the synthesis solution
-    std::map<Node, Node> sols;
-    // use the "getSubsolverSynthSolutions" interface, since we asserted the
-    // internal form of the SyGuS conjecture and used check-sat.
-    d_subsolver->getSubsolverSynthSolutions(sols);
     Assert(sols.size() == 1);
     std::map<Node, Node>::iterator its = sols.find(d_sssf);
     if (its != sols.end())
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index d9108a28c..25c6f5f9f 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -158,6 +158,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as,
   d_env.verbose(2) << "solving..." << std::endl;
   Trace("smt") << "SmtSolver::check(): running check" << endl;
   Result result = d_propEngine->checkSat();
+  Trace("smt") << "SmtSolver::check(): result " << result << std::endl;
 
   rm->endCall();
   Trace("limit") << "SmtSolver::check(): cumulative millis "
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 12a178814..70ad65644 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -261,11 +261,46 @@ Result SygusSolver::checkSynth(Assertions& as)
     query.push_back(d_conj);
     r = d_smtSolver.checkSatisfiability(as, query, false);
   }
-  // Check that synthesis solutions satisfy the conjecture
-  if (options().smt.checkSynthSol
-      && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+  // The result returned by the above call is typically "unknown", which may
+  // or may not correspond to a state in which we solved the conjecture
+  // successfully. Instead we call getSynthSolutions below. If this returns
+  // true, then we were successful. In this case, we set the result to "unsat",
+  // since the synthesis conjecture was negated when asserted to the subsolver.
+  //
+  // This behavior is done for 2 reasons:
+  // (1) if we do not negate the synthesis conjecture, the subsolver in some
+  // cases cannot answer "sat", e.g. in the presence of recursive function
+  // definitions. Instead the SyGuS language standard itself indicates that
+  // a correct solution for a conjecture is one where the synthesis conjecture
+  // is *T-valid* (in the presence of defined recursive functions). In other
+  // words, a SyGuS query asks to prove that the conjecture is valid when
+  // witnessed by the given solution.
+  // (2) we do not want the solver to explicitly answer "unsat" by giving an
+  // unsatisfiable set of formulas to the underlying PropEngine, or otherwise
+  // we will not be able to ask for further solutions. This is critical for
+  // incremental solving where multiple solutions are returned for the same
+  // set of constraints. Thus, the internal SyGuS solver will mark unknown
+  // with IncompleteId::QUANTIFIERS_SYGUS_SOLVED. Furthermore, this id may be
+  // overwritten by other means of incompleteness, so we cannot rely on this
+  // identifier being the final reason for unknown.
+  //
+  // Thus, we use getSynthSolutions as means of knowing the conjecture was
+  // solved.
+  std::map<Node, Node> sol_map;
+  if (getSynthSolutions(sol_map))
+  {
+    // if we have solutions, we return "unsat" by convention
+    r = Result(Result::UNSAT);
+    // Check that synthesis solutions satisfy the conjecture
+    if (options().smt.checkSynthSol)
+    {
+      checkSynthSolution(as, sol_map);
+    }
+  }
+  else
   {
-    checkSynthSolution(as);
+    // otherwise, we return "unknown"
+    r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
   }
   return r;
 }
@@ -301,21 +336,14 @@ bool SygusSolver::getSubsolverSynthSolutions(std::map<Node, Node>& solMap)
   return true;
 }
 
-void SygusSolver::checkSynthSolution(Assertions& as)
+void SygusSolver::checkSynthSolution(Assertions& as,
+                                     const std::map<Node, Node>& sol_map)
 {
   if (isVerboseOn(1))
   {
     verbose(1) << "SyGuS::checkSynthSolution: checking synthesis solution"
                << std::endl;
   }
-  std::map<Node, Node> sol_map;
-  // Get solutions and build auxiliary vectors for substituting
-  if (!getSynthSolutions(sol_map))
-  {
-    InternalError()
-        << "SygusSolver::checkSynthSolution(): No solution to check!";
-    return;
-  }
   if (sol_map.empty())
   {
     InternalError() << "SygusSolver::checkSynthSolution(): Got empty solution!";
diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index 9fe9f7a36..4e7a04364 100644
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -169,8 +169,13 @@ class SygusSolver : protected EnvObj
    * conjecture in which the functions-to-synthesize have been replaced by the
    * synthesized solutions, which is a quantifier-free formula, is
    * unsatisfiable. If not, then the found solutions are wrong.
+   *
+   * @param as The background assertions, which may include define-fun and
+   * define-fun-rec,
+   * @param sol_map Map from functions-to-synthesize to their solution (of the
+   * same type) for the asserted synthesis conjecture.
    */
-  void checkSynthSolution(Assertions& as);
+  void checkSynthSolution(Assertions& as, const std::map<Node, Node>& solMap);
   /**
    * Expand definitions in sygus datatype tn, which ensures that all
    * sygus constructors that are used to build values of sygus datatype
diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp
index c763fb9a0..b1071b5ae 100644
--- a/src/theory/incomplete_id.cpp
+++ b/src/theory/incomplete_id.cpp
@@ -35,6 +35,8 @@ const char* toString(IncompleteId i)
       return "QUANTIFIERS_RECORDED_INST";
     case IncompleteId::QUANTIFIERS_MAX_INST_ROUNDS:
       return "QUANTIFIERS_MAX_INST_ROUNDS";
+    case IncompleteId::QUANTIFIERS_SYGUS_SOLVED:
+      return "QUANTIFIERS_SYGUS_SOLVED";
     case IncompleteId::SEP: return "SEP";
     case IncompleteId::SETS_RELS_CARD: return "SETS_RELS_CARD";
     case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP";
diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h
index aaa458d8e..1e8bf155a 100644
--- a/src/theory/incomplete_id.h
+++ b/src/theory/incomplete_id.h
@@ -44,6 +44,9 @@ enum class IncompleteId
   QUANTIFIERS_RECORDED_INST,
   // incomplete due to limited number of allowed instantiation rounds
   QUANTIFIERS_MAX_INST_ROUNDS,
+  // we solved a negated synthesis conjecture and will terminate as a subsolver
+  // with unknown
+  QUANTIFIERS_SYGUS_SOLVED,
   // incomplete due to separation logic
   SEP,
   // relations were used in combination with set cardinality constraints
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 56d2f0500..b525d1c53 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -229,12 +229,6 @@ const char* toString(InferenceId i)
       return "QUANTIFIERS_SYGUS_EXCLUDE_CURRENT";
     case InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT:
       return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT";
-    case InferenceId::QUANTIFIERS_SYGUS_SI_SOLVED:
-      return "QUANTIFIERS_SYGUS_SI_SOLVED";
-    case InferenceId::QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED:
-      return "QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED";
-    case InferenceId::QUANTIFIERS_SYGUS_VERIFY_SOLVED:
-      return "QUANTIFIERS_SYGUS_VERIFY_SOLVED";
     case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA:
       return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA";
     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB:
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index d98d3ff25..f6e826ac3 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -342,12 +342,6 @@ enum class InferenceId
   QUANTIFIERS_SYGUS_EXCLUDE_CURRENT,
   // manual exclusion of a current solution for sygus-stream
   QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT,
-  // Q where Q was solved by a subcall to the single invocation module
-  QUANTIFIERS_SYGUS_SI_SOLVED,
-  // Q where Q was (trusted) solved by sampling
-  QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED,
-  // Q where Q was solved by a verification subcall
-  QUANTIFIERS_SYGUS_VERIFY_SOLVED,
   // ~Q where Q is a PBE conjecture with conflicting examples
   QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA,
   // unif+pi symmetry breaking between multiple enumerators
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index a90551a0f..e5dfe408b 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -306,6 +306,10 @@ bool SynthConjecture::needsCheck()
 
 bool SynthConjecture::doCheck()
 {
+  if (d_hasSolution)
+  {
+    return true;
+  }
   if (isSingleInvocation())
   {
     // We now try to solve with the single invocation solver, which may or may
@@ -314,14 +318,12 @@ bool SynthConjecture::doCheck()
     if (d_ceg_si->solve())
     {
       d_hasSolution = true;
-      // the conjecture has a solution, so its negation holds
-      Node qn = d_quant.negate();
-      d_qim.addPendingLemma(qn, InferenceId::QUANTIFIERS_SYGUS_SI_SOLVED);
+      // the conjecture has a solution, we set incomplete
+      d_qim.setIncomplete(IncompleteId::QUANTIFIERS_SYGUS_SOLVED);
     }
     return true;
   }
   Assert(d_master != nullptr);
-  Assert(!d_hasSolution);
 
   // get the list of terms that the master strategy is interested in
   std::vector<Node> terms;
@@ -506,11 +508,10 @@ bool SynthConjecture::doCheck()
   if (options().quantifiers.cegisSample == options::CegisSampleMode::TRUST)
   {
     // we have that the current candidate passed a sample test
-    // since we trust sampling in this mode, we assert there is no
-    // counterexample to the conjecture here.
-    Node qn = d_quant.negate();
-    d_qim.addPendingLemma(qn,
-                          InferenceId::QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED);
+    // since we trust sampling in this mode, we assume there is a solution here
+    // and set incomplete.
+    d_hasSolution = true;
+    d_qim.setIncomplete(IncompleteId::QUANTIFIERS_SYGUS_SOLVED);
     recordSolution(candidate_values);
     return true;
   }
@@ -573,10 +574,8 @@ bool SynthConjecture::doCheck()
     d_hasSolution = false;
     return false;
   }
-  // Use lemma to terminate with "unsat", this is justified by the verification
-  // check above, which confirms the synthesis conjecture is solved.
-  Node qn = d_quant.negate();
-  d_qim.addPendingLemma(qn, InferenceId::QUANTIFIERS_SYGUS_VERIFY_SOLVED);
+  // We set incomplete and terminate with unknown.
+  d_qim.setIncomplete(IncompleteId::QUANTIFIERS_SYGUS_SOLVED);
   return true;
 }
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8421107a4..dd1d96767 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1097,6 +1097,11 @@ void TheoryEngine::getDifficultyMap(std::map<Node, Node>& dmap)
   d_relManager->getDifficultyMap(dmap);
 }
 
+theory::IncompleteId TheoryEngine::getIncompleteId() const
+{
+  return d_incompleteId.get();
+}
+
 Node TheoryEngine::getModelValue(TNode var) {
   if (var.isConst())
   {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 03f7555b7..f1e178055 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -384,6 +384,9 @@ class TheoryEngine : protected EnvObj
    */
   void getDifficultyMap(std::map<Node, Node>& dmap);
 
+  /** Get incomplete id, valid immediately after an `unknown` response. */
+  theory::IncompleteId getIncompleteId() const;
+
   /**
    * Forwards an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().