Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)

14 files changed, 139 insertions, 47 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index b3c1ffd4d..019b052bc 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1218,14 +1218,14 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "sygus-rec-fun"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "enable efficient support for recursive functions in sygus grammars"
 
 [[option]]
   name       = "sygusRecFunEvalLimit"
   category   = "regular"
   long       = "sygus-rec-fun-eval-limit=N"
-  type       = "int"
+  type       = "unsigned"
   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)"
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 073c2ebc5..dfd3c9fee 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4861,6 +4861,7 @@ void SmtEngine::checkSynthSolution()
   SmtEngine solChecker(d_exprManager);
   solChecker.setLogic(getLogicInfo());
   setOption("check-synth-sol", SExpr("false"));
+  setOption("sygus-rec-fun", SExpr("false"));
 
   Trace("check-synth-sol") << "Retrieving assertions\n";
   // Build conjecture from original assertions
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
index ffac9b2c8..8eb0ef686 100644
--- a/src/theory/quantifiers/fun_def_evaluator.cpp
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -118,7 +118,12 @@ Node FunDefEvaluator::evaluate(Node n) const
           it = visited.find(cur[0]);
           Assert(it != visited.end());
           Assert(!it->second.isNull());
-          Assert(it->second.isConst());
+          if (!it->second.isConst())
+          {
+            Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of "
+                                "ITE to const, FAIL\n";
+            return Node::null();
+          }
           // pick child to evaluate depending on condition eval
           unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
           Trace("fd-eval-debug2")
@@ -134,6 +139,7 @@ Node FunDefEvaluator::evaluate(Node n) const
                                   << cur[childIdxToEval] << "\n";
           continue;
         }
+        unsigned child CVC4_UNUSED = 0;
         for (const Node& cn : cur)
         {
           it = visited.find(cn);
@@ -141,6 +147,8 @@ Node FunDefEvaluator::evaluate(Node n) const
           Assert(!it->second.isNull());
           childChanged = childChanged || cn != it->second;
           children.push_back(it->second);
+          Trace("fd-eval-debug2") << "argument " << child++
+                                  << " eval : " << it->second << std::endl;
         }
         if (cur.getKind() == APPLY_UF)
         {
@@ -197,6 +205,8 @@ Node FunDefEvaluator::evaluate(Node n) const
           // evaluating the body.
           if (!sbody.isConst())
           {
+            Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur
+                                    << " from body " << sbody << "\n";
             visit.push_back(cur);
             visit.push_back(sbody);
           }
@@ -208,32 +218,35 @@ Node FunDefEvaluator::evaluate(Node n) const
             ret = nm->mkNode(cur.getKind(), children);
             ret = Rewriter::rewrite(ret);
           }
+          Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
           visited[cur] = ret;
         }
       }
       else if (cur != curEval && !curEval.isConst())
       {
         Trace("fd-eval-debug") << "from body " << cur << std::endl;
+        Trace("fd-eval-debug") << "and eval  " << curEval << std::endl;
         // we had to evaluate our body, which should have a definition now
         it = visited.find(curEval);
-        Assert(it != visited.end());
-        // our definition is the result of the body
-        visited[cur] = it->second;
+        if (it == visited.end())
+        {
+          Trace("fd-eval-debug2") << "eval without definition\n";
+          // this is the case where curEval was not a constant but it was
+          // irreducible, for example (DT_SYGUS_EVAL e args)
+          visited[cur] = curEval;
+        }
+        else
+        {
+          Trace("fd-eval-debug2")
+              << "eval with definition " << it->second << "\n";
+          visited[cur] = it->second;
       }
     }
+    }
   } while (!visit.empty());
-  Trace("fd-eval") << "FunDefEvaluator: return " << visited[n];
+  Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n";
   Assert(visited.find(n) != visited.end());
   Assert(!visited.find(n)->second.isNull());
-  if (!visited.find(n)->second.isConst())
-  {
-    visited[n] = Node::null();
-    Trace("fd-eval") << "\n with NONCONST\n";
-  }
-  else
-  {
-    Trace("fd-eval") << "\n with SUCCESS\n";
-  }
   return visited[n];
 }
 
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 6591e6828..da4275365 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -712,7 +712,7 @@ void SynthConjecture::doRefine(std::vector<Node>& lems)
   base_lem = base_lem.substitute(
       sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end());
   Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
-  base_lem = Rewriter::rewrite(base_lem);
+  base_lem = d_tds->rewriteNode(base_lem);
   Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
                         << "..." << std::endl;
   d_master->registerRefinementLemma(sk_vars, base_lem, lems);
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index cbe907d41..4a708e66c 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -276,28 +276,29 @@ void SynthEngine::registerQuantifier(Node q)
 {
   Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
                        << std::endl;
-  if (d_quantEngine->getOwner(q) == this)
+  if (d_quantEngine->getOwner(q) != this)
   {
-    Trace("cegqi") << "Register conjecture : " << q << std::endl;
-    if (options::sygusQePreproc())
-    {
-      d_waiting_conj.push_back(q);
-    }
-    else
-    {
-      // assign it now
-      assignConjecture(q);
-    }
+    return;
   }
-  if (options::sygusRecFun())
+  if (d_quantEngine->getQuantAttributes()->isFunDef(q))
   {
-    if (d_quantEngine->getQuantAttributes()->isFunDef(q))
-    {
-      // If it is a recursive function definition, add it to the function
-      // definition evaluator class.
-      FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
-      fde->assertDefinition(q);
-    }
+    Assert(options::sygusRecFun());
+    // If it is a recursive function definition, add it to the function
+    // definition evaluator class.
+    Trace("cegqi") << "Registering function definition : " << q << "\n";
+    FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
+    fde->assertDefinition(q);
+    return;
+  }
+  Trace("cegqi") << "Register conjecture : " << q << std::endl;
+  if (options::sygusQePreproc())
+  {
+    d_waiting_conj.push_back(q);
+  }
+  else
+  {
+    // assign it now
+    assignConjecture(q);
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 679d47779..d664a462d 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -741,9 +741,9 @@ Node TermDbSygus::rewriteNode(Node n) const
       {
         return fres;
       }
-      // It may have failed, in which case there are undefined symbols in res.
-      // In this case, we revert to the result of rewriting in the return
-      // statement below.
+      // It may have failed, in which case there are undefined symbols in res or
+      // we reached the limit of evaluations. In this case, we revert to the
+      // result of rewriting in the return statement below.
     }
   }
   return res;
@@ -1082,4 +1082,3 @@ bool TermDbSygus::isEvaluationPoint(Node n) const
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8337ba0b0..8730e3a97 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -407,14 +407,15 @@ void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa)
     // set rewrite engine as owner
     setOwner(q, d_private->d_rr_engine.get(), 2);
   }
-  if (qa.d_sygus)
+  if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull()))
   {
     if (d_private->d_synth_e.get() == nullptr)
     {
       Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
                           << q << std::endl;
     }
-    // set synth engine as owner
+    // set synth engine as owner since this is either a conjecture or a function
+    // definition to be used by sygus
     setOwner(q, d_private->d_synth_e.get(), 2);
   }
 }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fda31cfdb..2182beaa8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1744,6 +1744,7 @@ set(regress_1_tests
   regress1/sygus/qe.sy
   regress1/sygus/qf_abv.smt2
   regress1/sygus/real-grammar.sy
+  regress1/sygus/rec-fun-swap.sy
   regress1/sygus/rec-fun-sygus.sy
   regress1/sygus/rec-fun-while-1.sy
   regress1/sygus/rec-fun-while-2.sy
diff --git a/test/regress/regress1/sygus/list_recursor.sy b/test/regress/regress1/sygus/list_recursor.sy
index 53c55397e..2e10a0c71 100644
--- a/test/regress/regress1/sygus/list_recursor.sy
+++ b/test/regress/regress1/sygus/list_recursor.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 --uf-ho
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --uf-ho
 
 (set-logic ALL)
 
diff --git a/test/regress/regress1/sygus/rec-fun-swap.sy b/test/regress/regress1/sygus/rec-fun-swap.sy
new file mode 100644
index 000000000..056d6a8fc
--- /dev/null
+++ b/test/regress/regress1/sygus/rec-fun-swap.sy
@@ -0,0 +1,76 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
+
+(set-logic ALL)
+
+; The environment datatypes
+(declare-datatype NVars ((x) (y)))
+
+(declare-datatype Pair ((pair (first NVars) (second Int))))
+
+(declare-datatype Env ((cons (head Pair) (tail Env)) (nil)))
+
+(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env
+  (ite (is-nil env)
+    (cons (pair var value) env)
+    (ite (= var (first (head env)))
+      (cons (pair var value) (tail env))
+      (cons (head env) (envStore var value (tail env)))
+      )
+    )
+  )
+
+(define-fun-rec envSelect ((var NVars) (env Env)) Int
+  (ite (is-nil env)
+    (- 1)
+    (ite (= var (first (head env)))
+      (second (head env))
+      (envSelect var (tail env))
+      )
+    )
+  )
+
+; Syntax for arithmetic expressions
+(declare-datatype Aexp
+  (
+    (Val (val Int))
+    )
+  )
+
+; Function to evaluate arithmetic expressions
+(define-fun-rec evalA ((env Env) (a Aexp)) Int
+    (val a)
+      )
+
+; Syntax for commands
+(declare-datatype Com
+  (
+    (Skip)
+    (Assign (lhs NVars) (rhs Aexp))
+    (CSeq (cBef Com) (aAft Com))
+    )
+  )
+
+; Function to evaluate statements
+(define-fun-rec evalC ((env Env) (c Com)) Env
+  (ite (is-Skip c)
+    env
+    (ite (is-Assign c)
+      (envStore (lhs c) (evalA env (rhs c)) env)
+      (evalC (evalC env (cBef c)) (aAft c)))
+    )
+  )
+
+(synth-fun prog () Com
+  ((C Com) (V NVars) (A Aexp) (I Int))
+  (
+    (C Com (Skip (Assign V A) (CSeq C C)))
+    (V NVars (x y))
+    (A Aexp ((Val I)))
+    (I Int (0 1))
+    )
+)
+
+(constraint (= (evalC (cons (pair y 0) (cons (pair x 1) nil)) prog) (cons (pair y 1) (cons (pair x 0) nil))))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/rec-fun-sygus.sy b/test/regress/regress1/sygus/rec-fun-sygus.sy
index 13d4782d4..769e173de 100644
--- a/test/regress/regress1/sygus/rec-fun-sygus.sy
+++ b/test/regress/regress1/sygus/rec-fun-sygus.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
 
 (set-logic ALL)
 
diff --git a/test/regress/regress1/sygus/rec-fun-while-1.sy b/test/regress/regress1/sygus/rec-fun-while-1.sy
index c175094ee..e805fdc20 100644
--- a/test/regress/regress1/sygus/rec-fun-while-1.sy
+++ b/test/regress/regress1/sygus/rec-fun-while-1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
 
 (set-logic ALL)
 
diff --git a/test/regress/regress1/sygus/rec-fun-while-2.sy b/test/regress/regress1/sygus/rec-fun-while-2.sy
index 87a4f2a6e..7e32384b3 100644
--- a/test/regress/regress1/sygus/rec-fun-while-2.sy
+++ b/test/regress/regress1/sygus/rec-fun-while-2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
 
 (set-logic ALL)
 
diff --git a/test/regress/regress1/sygus/rec-fun-while-infinite.sy b/test/regress/regress1/sygus/rec-fun-while-infinite.sy
index 85f8268c5..b43b3d5e2 100644
--- a/test/regress/regress1/sygus/rec-fun-while-infinite.sy
+++ b/test/regress/regress1/sygus/rec-fun-while-infinite.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unknown
-; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
 
 (set-logic ALL)