Add recursive function definitions to subsolver in sygus (#6824)

This passes recursive function definitions to the verification subsolver in sygus, with a default bounded limit of 3. This required improving the interface for setting up subsolvers by allowing custom options; the sygus solver statically computes an instance of the options that it uses in all calls.

This allows us to solve non-PBE sygus problems with recursive function definitions. The PR adds an example.

13 files changed, 147 insertions, 13 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 45341a6a6..cfb678991 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1317,6 +1317,14 @@ name   = "Quantifiers"
   default    = "1000"
   help       = "use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)"
 
+[[option]]
+  name       = "sygusVerifyInstMaxRounds"
+  category   = "regular"
+  long       = "sygus-verify-inst-max-rounds=N"
+  type       = "int"
+  default    = "3"
+  help       = "maximum number of instantiation rounds for sygus verification calls (-1 == no limit, default is 3)"
+
 # Internal uses of sygus
 
 [[option]]
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index a46452004..027ba71ec 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -84,7 +84,7 @@ std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
   std::unique_ptr<SmtEngine> optChecker;
   // initializeSubSolver will copy the options and theories enabled
   // from the current solver to optChecker and adds timeout
-  theory::initializeSubsolver(optChecker, needsTimeout, timeout);
+  theory::initializeSubsolver(optChecker, nullptr, needsTimeout, timeout);
   // we need to be in incremental mode for multiple objectives since we need to
   // push pop we need to produce models to inrement on our objective
   optChecker->setOption("incremental", "true");
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 14bc05335..72605e9d1 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -78,7 +78,8 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
   Assert (!query.isNull());
   if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
   {
-    initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout());
+    initializeSubsolver(
+        checker, nullptr, true, options::sygusExprMinerCheckTimeout());
   }
   else
   {
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
index beb2a33cd..36f557db8 100644
--- a/src/theory/quantifiers/fun_def_evaluator.cpp
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -41,7 +41,9 @@ void FunDefEvaluator::assertDefinition(Node q)
   Node f = h.hasOperator() ? h.getOperator() : h;
   Assert(d_funDefMap.find(f) == d_funDefMap.end())
       << "FunDefEvaluator::assertDefinition: function already defined";
+  d_funDefs.push_back(q);
   FunDefInfo& fdi = d_funDefMap[f];
+  fdi.d_quant = q;
   fdi.d_body = QuantAttributes::getFunDefBody(q);
   Assert(!fdi.d_body.isNull());
   fdi.d_args.insert(fdi.d_args.end(), q[0].begin(), q[0].end());
@@ -251,6 +253,20 @@ Node FunDefEvaluator::evaluate(Node n) const
 
 bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
 
+const std::vector<Node>& FunDefEvaluator::getDefinitions() const
+{
+  return d_funDefs;
+}
+Node FunDefEvaluator::getDefinitionFor(Node f) const
+{
+  std::map<Node, FunDefInfo>::const_iterator it = d_funDefMap.find(f);
+  if (it != d_funDefMap.end())
+  {
+    return it->second.d_quant;
+  }
+  return Node::null();
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/quantifiers/fun_def_evaluator.h b/src/theory/quantifiers/fun_def_evaluator.h
index 54565b4ee..a3b79bec7 100644
--- a/src/theory/quantifiers/fun_def_evaluator.h
+++ b/src/theory/quantifiers/fun_def_evaluator.h
@@ -53,11 +53,18 @@ class FunDefEvaluator
    */
   bool hasDefinitions() const;
 
+  /** Get definitions */
+  const std::vector<Node>& getDefinitions() const;
+  /** Get definition for function symbol f, if it is cached by this class */
+  Node getDefinitionFor(Node f) const;
+
  private:
   /** information cached per function definition */
   class FunDefInfo
   {
    public:
+    /** the quantified formula */
+    Node d_quant;
     /** the body */
     Node d_body;
     /** the formal argument list */
@@ -65,6 +72,8 @@ class FunDefEvaluator
   };
   /** maps functions to the above information */
   std::map<Node, FunDefInfo> d_funDefMap;
+  /** list of all definitions */
+  std::vector<Node> d_funDefs;
   /** evaluator utility */
   Evaluator d_eval;
 };
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 0b5d06bd2..739e9ab0d 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -233,9 +233,11 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   // make the satisfiability query
   std::unique_ptr<SmtEngine> repcChecker;
   // initialize the subsolver using the standard method
-  initializeSubsolver(repcChecker,
-                      Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
-                      options::sygusRepairConstTimeout());
+  initializeSubsolver(
+      repcChecker,
+      nullptr,
+      Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
+      options::sygusRepairConstTimeout());
   // renable options disabled by sygus
   repcChecker->setOption("miniscope-quant", "true");
   repcChecker->setOption("miniscope-quant-fv", "true");
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 62c61fe1e..4e8d7d46d 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 
 #include "base/configuration.h"
+#include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
@@ -87,6 +88,18 @@ SynthConjecture::SynthConjecture(QuantifiersState& qs,
     d_modules.push_back(d_sygus_ccore.get());
   }
   d_modules.push_back(d_ceg_cegis.get());
+  // determine the options to use for the verification subsolvers we spawn
+  // we start with the options of the current SmtEngine
+  SmtEngine* smtCurr = smt::currentSmtEngine();
+  d_subOptions.copyValues(smtCurr->getOptions());
+  // limit the number of instantiation rounds on subcalls
+  d_subOptions.quantifiers.instMaxRounds =
+      d_subOptions.quantifiers.sygusVerifyInstMaxRounds;
+  // Disable sygus on the subsolver. This is particularly important since it
+  // ensures that recursive function definitions have the standard ownership
+  // instead of being claimed by sygus in the subsolver.
+  d_subOptions.base.inputLanguage = language::input::LANG_SMTLIB_V2_6;
+  d_subOptions.quantifiers.sygus = false;
 }
 
 SynthConjecture::~SynthConjecture() {}
@@ -580,8 +593,34 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
 
   if (!query.isConst() || query.getConst<bool>())
   {
+    // add recursive function definitions
+    FunDefEvaluator* feval = d_tds->getFunDefEvaluator();
+    const std::vector<Node>& fdefs = feval->getDefinitions();
+    if (!fdefs.empty())
+    {
+      // Get the relevant definitions based on the symbols in the query.
+      // Notice in some cases, this may have the effect of making the subcall
+      // involve no recursive function definitions at all, in which case the
+      // subcall to verification may be decidable, in which case the call
+      // below is guaranteed to generate a new counterexample point.
+      std::unordered_set<Node> syms;
+      expr::getSymbols(query, syms);
+      std::vector<Node> qconj;
+      qconj.push_back(query);
+      for (const Node& f : syms)
+      {
+        Node q = feval->getDefinitionFor(f);
+        if (!q.isNull())
+        {
+          qconj.push_back(q);
+        }
+      }
+      query = nm->mkAnd(qconj);
+      Trace("cegqi-debug") << "query is " << query << std::endl;
+    }
     Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
-    Result r = checkWithSubsolver(query, d_ce_sk_vars, d_ce_sk_var_mvs);
+    Result r =
+        checkWithSubsolver(query, d_ce_sk_vars, d_ce_sk_var_mvs, &d_subOptions);
     Trace("sygus-engine") << "  ...got " << r << std::endl;
     if (r.asSatisfiabilityResult().isSat() == Result::SAT)
     {
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 4329a9c60..bf3e7b31d 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -423,6 +423,8 @@ class SynthConjecture
    * rewrite rules.
    */
   std::map<Node, ExpressionMinerManager> d_exprm;
+  /** The options for subsolver calls */
+  Options d_subOptions;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 86c3f62d0..1792f9386 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -164,7 +164,7 @@ void SynthEngine::checkOwnership(Node q)
   // take ownership of quantified formulas with sygus attribute, and function
   // definitions when options::sygusRecFun is true.
   QuantAttributes& qa = d_qreg.getQuantAttributes();
-  if (qa.isSygus(q) || (options::sygusRecFun() && qa.isFunDef(q)))
+  if (qa.isSygus(q) || (qa.isFunDef(q) && options::sygusRecFun()))
   {
     d_qreg.setOwner(q, this, 2);
   }
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 1c76f0205..5f285dc07 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -42,13 +42,18 @@ Result quickCheck(Node& query)
 }
 
 void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+                         Options* opts,
                          bool needsTimeout,
                          unsigned long timeout)
 {
   NodeManager* nm = NodeManager::currentNM();
   SmtEngine* smtCurr = smt::currentSmtEngine();
-  // must copy the options
-  smte.reset(new SmtEngine(nm, &smtCurr->getOptions()));
+  if (opts == nullptr)
+  {
+    // must copy the options
+    opts = &smtCurr->getOptions();
+  }
+  smte.reset(new SmtEngine(nm, opts));
   smte->setIsInternalSubsolver();
   smte->setLogic(smtCurr->getLogicInfo());
   // set the options
@@ -60,6 +65,7 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
 
 Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
                           Node query,
+                          Options* opts,
                           bool needsTimeout,
                           unsigned long timeout)
 {
@@ -69,21 +75,26 @@ Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
   {
     return r;
   }
-  initializeSubsolver(smte, needsTimeout, timeout);
+  initializeSubsolver(smte, opts, needsTimeout, timeout);
   smte->assertFormula(query);
   return smte->checkSat();
 }
 
-Result checkWithSubsolver(Node query, bool needsTimeout, unsigned long timeout)
+Result checkWithSubsolver(Node query,
+                          Options* opts,
+                          bool needsTimeout,
+                          unsigned long timeout)
 {
   std::vector<Node> vars;
   std::vector<Node> modelVals;
-  return checkWithSubsolver(query, vars, modelVals, needsTimeout, timeout);
+  return checkWithSubsolver(
+      query, vars, modelVals, opts, needsTimeout, timeout);
 }
 
 Result checkWithSubsolver(Node query,
                           const std::vector<Node>& vars,
                           std::vector<Node>& modelVals,
+                          Options* opts,
                           bool needsTimeout,
                           unsigned long timeout)
 {
@@ -105,7 +116,7 @@ Result checkWithSubsolver(Node query,
     return r;
   }
   std::unique_ptr<SmtEngine> smte;
-  initializeSubsolver(smte, needsTimeout, timeout);
+  initializeSubsolver(smte, opts, needsTimeout, timeout);
   smte->assertFormula(query);
   r = smte->checkSat();
   if (r.asSatisfiabilityResult().isSat() == Result::SAT)
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index f7985d651..2d80831f2 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -41,10 +41,13 @@ namespace theory {
  * if the current SMT engine has declared a separation logic heap.
  *
  * @param smte The smt engine pointer to initialize
+ * @param opts The options for the subsolver. If nullptr, then we copy the
+ * options from the current SmtEngine in scope.
  * @param needsTimeout Whether we would like to set a timeout
  * @param timeout The timeout (in milliseconds)
  */
 void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+                         Options* opts = nullptr,
                          bool needsTimeout = false,
                          unsigned long timeout = 0);
 
@@ -56,6 +59,7 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
  */
 Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
                           Node query,
+                          Options* opts = nullptr,
                           bool needsTimeout = false,
                           unsigned long timeout = 0);
 
@@ -66,10 +70,12 @@ Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
  * concerned with the state of the SMT engine after the check.
  *
  * @param query The query to check
+ * @param opts The options for the subsolver
  * @param needsTimeout Whether we would like to set a timeout
  * @param timeout The timeout (in milliseconds)
  */
 Result checkWithSubsolver(Node query,
+                          Options* opts = nullptr,
                           bool needsTimeout = false,
                           unsigned long timeout = 0);
 
@@ -81,12 +87,14 @@ Result checkWithSubsolver(Node query,
  * @param query The query to check
  * @param vars The variables we are interesting in getting a model for.
  * @param modelVals A vector storing the model values of variables in vars.
+ * @param opts The options for the subsolver
  * @param needsTimeout Whether we would like to set a timeout
  * @param timeout The timeout (in milliseconds)
  */
 Result checkWithSubsolver(Node query,
                           const std::vector<Node>& vars,
                           std::vector<Node>& modelVals,
+                          Options* opts = nullptr,
                           bool needsTimeout = false,
                           unsigned long timeout = 0);
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e2e216567..260b0d9b7 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2521,6 +2521,7 @@ set(regress_2_tests
   regress2/sygus/process-arg-invariance.sy
   regress2/sygus/real-grammar-neg.sy
   regress2/sygus/sets-fun-test.sy
+  regress2/sygus/sumn_recur_synth.sy
   regress2/sygus/strings-no-syntax-len.sy
   regress2/sygus/three.sy
   regress2/typed_v1l50016-simp.cvc
diff --git a/test/regress/regress2/sygus/sumn_recur_synth.sy b/test/regress/regress2/sygus/sumn_recur_synth.sy
new file mode 100644
index 000000000..103992dfe
--- /dev/null
+++ b/test/regress/regress2/sygus/sumn_recur_synth.sy
@@ -0,0 +1,37 @@
+; EXPECT: unsat
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic UFLIA)
+
+(declare-var x Int)
+(declare-var x! Int)
+(declare-var y Int)
+(declare-var y! Int)
+
+(define-fun-rec sum_n ((x Int)) Int
+                  (ite (>= x 1)
+                       (+ x (sum_n (- x 1)))
+                       0))
+
+(synth-fun inv_fun ((x Int) (y Int)) Bool
+	((C Bool) (B Bool) (E Int))
+	((C Bool ((and (>= y 1) B)))
+	 (B Bool ((= (sum_n E) E) (>= E E)))
+	 (E Int (0 1 x y (+ E E))))
+)
+
+(define-fun pre_fun ((x Int) (y Int)) Bool
+	(and (= x 0) (= y 1)))
+
+(define-fun trans_fun ((x Int) (y Int) (x! Int) (y! Int)) Bool
+	(and (<= y 2) (= x! (+ x y)) (= y! (+ y 1))))
+
+(define-fun post_fun ((x Int) (y Int)) Bool
+	(= x (sum_n (- y 1)))	
+)
+
+(constraint (=> (pre_fun x y) (inv_fun x y)))
+(constraint (=> (and (inv_fun x y) (trans_fun x y x! y!)) (inv_fun x! y!)))
+(constraint (=> (inv_fun x y) (post_fun x y)))
+
+
+(check-synth)