Support UF in default sygus grammars (#3319)

8 files changed, 107 insertions, 32 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 96c79e69d..47a1f6142 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -143,14 +143,15 @@ void CegSingleInv::initialize(Node q)
   }
   // if we are doing invariant templates, then construct the template
   Trace("cegqi-si") << "- Do transition inference..." << std::endl;
-  d_ti[q].process(qq);
+  d_ti[q].process(qq, q[0][0]);
   Trace("cegqi-inv") << std::endl;
   Node prog = d_ti[q].getFunction();
-  if (prog.isNull())
+  if (!d_ti[q].isComplete())
   {
     // the invariant could not be inferred
     return;
   }
+  Assert(prog == q[0][0]);
   NodeManager* nm = NodeManager::currentNM();
   // map the program back via non-single invocation map
   std::vector<Node> prog_templ_vars;
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index 047a78d11..529ef037f 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -55,20 +55,20 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
   for (const Node& s : symset)
   {
     TypeNode tn = s.getType();
-    if (tn.isFirstClass())
-    {
-      std::stringstream ss;
-      ss << s;
-      Node var = nm->mkBoundVar(tn);
-      syms.push_back(s);
-      vars.push_back(var);
-      Node vlv = nm->mkBoundVar(ss.str(), tn);
-      varlist.push_back(vlv);
-      varlistTypes.push_back(tn);
-      // set that this variable encodes the term s
-      SygusVarToTermAttribute sta;
-      vlv.setAttribute(sta, s);
-    }
+    // Notice that we allow for non-first class (e.g. function) variables here.
+    // This is applicable to the case where we are doing get-abduct in a logic
+    // with UF.
+    std::stringstream ss;
+    ss << s;
+    Node var = nm->mkBoundVar(tn);
+    syms.push_back(s);
+    vars.push_back(var);
+    Node vlv = nm->mkBoundVar(ss.str(), tn);
+    varlist.push_back(vlv);
+    varlistTypes.push_back(tn);
+    // set that this variable encodes the term s
+    SygusVarToTermAttribute sta;
+    vlv.setAttribute(sta, s);
   }
   // make the sygus variable list
   Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist);
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index ba55db132..43696bff0 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
+#include "printer/sygus_print_callback.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
@@ -428,6 +429,15 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor(
         TypeNode intType = NodeManager::currentNM()->integerType();
         collectSygusGrammarTypesFor(intType,types);
       }
+      else if (range.isFunction())
+      {
+        std::vector<TypeNode> atypes = range.getArgTypes();
+        for (unsigned i = 0, ntypes = atypes.size(); i < ntypes; i++)
+        {
+          collectSygusGrammarTypesFor(atypes[i], types);
+        }
+        collectSygusGrammarTypesFor(range.getRangeType(), types);
+      }
     }
   }
 }
@@ -533,18 +543,42 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
     Type unres_t = unres_types[i];
     //add variables
-    for (unsigned j = 0, size_j = sygus_vars.size(); j < size_j; ++j)
+    for (const Node& sv : sygus_vars)
     {
-      if( sygus_vars[j].getType()==types[i] ){
+      TypeNode svt = sv.getType();
+      if (svt == types[i])
+      {
         std::stringstream ss;
-        ss << sygus_vars[j];
-        Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
-        ops[i].push_back( sygus_vars[j].toExpr() );
+        ss << sv;
+        Trace("sygus-grammar-def")
+            << "...add for variable " << ss.str() << std::endl;
+        ops[i].push_back(sv.toExpr());
         cnames[i].push_back(ss.str());
         cargs[i].push_back(std::vector<Type>());
         pcs[i].push_back(nullptr);
         weights[i].push_back(-1);
       }
+      else if (svt.isFunction() && svt.getRangeType() == types[i])
+      {
+        // We add an APPLY_UF for all function whose return type is this type
+        // whose argument types are the other sygus types we are constructing.
+        std::vector<TypeNode> argTypes = svt.getArgTypes();
+        std::vector<Type> stypes;
+        for (unsigned k = 0, ntypes = argTypes.size(); k < ntypes; k++)
+        {
+          unsigned index =
+              std::distance(types.begin(),
+                            std::find(types.begin(), types.end(), argTypes[k]));
+          stypes.push_back(unres_types[index]);
+        }
+        std::stringstream ss;
+        ss << "apply_" << sv;
+        ops[i].push_back(sv.toExpr());
+        cnames[i].push_back(ss.str());
+        cargs[i].push_back(stypes);
+        pcs[i].push_back(nullptr);
+        weights[i].push_back(-1);
+      }
     }
     //add constants
     std::vector< Node > consts;
@@ -812,7 +846,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         pcs[i].push_back(nullptr);
         weights[i].push_back(-1);
       }
-    }else{
+    }
+    else if (types[i].isSort() || types[i].isFunction())
+    {
+      // do nothing
+    }
+    else
+    {
       Warning()
           << "Warning: No implementation for default Sygus grammar of type "
           << types[i] << std::endl;
@@ -903,6 +943,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   // add predicates for types
   for (unsigned i = 0, size = types.size(); i < size; ++i)
   {
+    if (!types[i].isFirstClass())
+    {
+      continue;
+    }
     Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl;
     //add equality per type
     Kind k = EQUAL;
diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp
index 88ffe84b2..7db3f50f8 100644
--- a/src/theory/quantifiers/sygus/transition_inference.cpp
+++ b/src/theory/quantifiers/sygus/transition_inference.cpp
@@ -186,6 +186,13 @@ void TransitionInference::getConstantSubstitution(
   }
 }
 
+void TransitionInference::process(Node n, Node f)
+{
+  // set the function
+  d_func = f;
+  process(n);
+}
+
 void TransitionInference::process(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
@@ -404,10 +411,14 @@ bool TransitionInference::processDisjunct(
   // if another part mentions UF or a free variable, then fail
   bool lit_pol = n.getKind() != NOT;
   Node lit = n.getKind() == NOT ? n[0] : n;
-  if (lit.getKind() == APPLY_UF)
+  // is it an application of the function-to-synthesize? Yes if we haven't
+  // encountered a function or if it matches the existing d_func.
+  if (lit.getKind() == APPLY_UF
+      && (d_func.isNull() || lit.getOperator() == d_func))
   {
     Node op = lit.getOperator();
-    if (d_func.isNull())
+    // initialize the variables
+    if (d_vars.empty())
     {
       d_func = op;
       Trace("cegqi-inv-debug") << "Use " << op << " with args ";
@@ -420,13 +431,8 @@ bool TransitionInference::processDisjunct(
       }
       Trace("cegqi-inv-debug") << std::endl;
     }
-    if (op != d_func)
-    {
-      Trace("cegqi-inv-debug")
-          << "...failed, free function : " << n << std::endl;
-      return false;
-    }
-    else if (topLevel)
+    Assert(!d_func.isNull());
+    if (topLevel)
     {
       if (terms.find(lit_pol) == terms.end())
       {
diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h
index b4fb220db..8939cf6da 100644
--- a/src/theory/quantifiers/sygus/transition_inference.h
+++ b/src/theory/quantifiers/sygus/transition_inference.h
@@ -123,7 +123,13 @@ class TransitionInference
    * The node n should be the inner body of the negated synthesis conjecture,
    * prior to generating the deep embedding. That is, given:
    *   forall f. ~forall x. P( f, x ),
-   * this method expects n to be P( f, x ).
+   * this method expects n to be P( f, x ), and the argument f to be the
+   * function f above.
+   */
+  void process(Node n, Node f);
+  /**
+   * Same as above, without specifying f. This will try to infer a function f
+   * based on the body of n.
    */
   void process(Node n);
   /**
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8dba70f91..25637acdc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1690,6 +1690,7 @@ set(regress_1_tests
   regress1/sygus/hd-01-d1-prog.sy
   regress1/sygus/hd-19-d1-prog-dup-op.sy
   regress1/sygus/hd-sdiv.sy
+  regress1/sygus/ho-sygus.sy
   regress1/sygus/icfp_14.12-flip-args.sy
   regress1/sygus/icfp_14.12.sy
   regress1/sygus/icfp_14_12_diff_types.sy
@@ -1753,6 +1754,7 @@ set(regress_1_tests
   regress1/sygus/trivial-stream.sy
   regress1/sygus/twolets1.sy
   regress1/sygus/twolets2-orig.sy
+  regress1/sygus/uf-abduct.smt2
   regress1/sygus/unbdd_inv_gen_ex7.sy
   regress1/sygus/unbdd_inv_gen_winf1.sy
   regress1/sygus/univ_2-long-repeat.sy
diff --git a/test/regress/regress1/sygus/ho-sygus.sy b/test/regress/regress1/sygus/ho-sygus.sy
new file mode 100644
index 000000000..c66485817
--- /dev/null
+++ b/test/regress/regress1/sygus/ho-sygus.sy
@@ -0,0 +1,8 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --uf-ho
+(set-logic ALL)
+(synth-fun f ((y (-> Int Int)) (z Int)) Int)
+(declare-var z (-> Int Int))
+(constraint (= (f z 0) (z 1)))
+(constraint (= (f z 1) (z 2)))
+(check-synth)
diff --git a/test/regress/regress1/sygus/uf-abduct.smt2 b/test/regress/regress1/sygus/uf-abduct.smt2
new file mode 100644
index 000000000..690e57290
--- /dev/null
+++ b/test/regress/regress1/sygus/uf-abduct.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-abducts --uf-ho
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic UFLIA)
+(declare-fun f (Int) Int)
+(declare-fun a () Int)
+(assert (and (<= 0 a) (< a 4)))
+(get-abduct ensureF (or (> (f 0) 0) (> (f 1) 0) (> (f 2) 0) (> (f 3) 0)))