Limit cases of sygus inference based on type (#3370)

This makes `--sygus-inference` a no-op for inputs where there is a free function whose sort cannot be handled in a sygus grammar.

It also fixes an issue where skolem variables were not being treated as functions-to-synthesize.

Fixes #3250 and fixes #3356.

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 471d68ff8eac53432d0a6f52f3c49aa826c0f364..930edf869034f3f6848882dbed23bb48cdb3d10f 100644 (file)
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -19,6 +19,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -194,7 +195,7 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
             free_functions.push_back(op);
           }
         }
-        else if (cur.getKind() == VARIABLE)
+        else if (cur.isVar() && cur.getKind() != BOUND_VARIABLE)
         {
           // a free variable is a 0-argument function to synthesize
           Assert(std::find(free_functions.begin(), free_functions.end(), cur)
@@ -223,6 +224,24 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
     return false;
   }
 
+  // Ensure the type of all free functions is handled by the sygus grammar
+  // constructor utility.
+  bool typeSuccess = true;
+  for (const Node& f : free_functions)
+  {
+    TypeNode tn = f.getType();
+    if (!theory::quantifiers::CegGrammarConstructor::isHandledType(tn))
+    {
+      Trace("sygus-infer") << "...fail: unhandled type " << tn << std::endl;
+      typeSuccess = false;
+      break;
+    }
+  }
+  if (!typeSuccess)
+  {
+    return false;
+  }
+
   Assert(!processed_assertions.empty());
   // conjunction of the assertions
   Trace("sygus-infer") << "Construct body..." << std::endl;

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 31131f23fc58cdf0ce3a5b9ddd295859cf05fd11..ba55db132f56eeca39da232fc7fe34951b67576e 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -432,6 +432,20 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor(
   }
 }
 
+bool CegGrammarConstructor::isHandledType(TypeNode t)
+{
+  std::vector<TypeNode> types;
+  collectSygusGrammarTypesFor(t, types);
+  for (const TypeNode& tn : types)
+  {
+    if (tn.isSort() || tn.isFloatingPoint())
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
 void CegGrammarConstructor::mkSygusDefaultGrammar(
     TypeNode range,
     Node bvl,

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index ca1b9ae37ce10f3449aef111b81f503c42a485f7..85efddada44e26d999610dad8c27cf283e9f5072 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -154,6 +154,8 @@ public:
    * sygus grammar, add them to vector ops.
    */
   static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops);
+  /** Is it possible to construct a default grammar for type t? */
+  static bool isHandledType(TypeNode t);
   /**
    * Convert node n based on deep embedding, see Section 4 of Reynolds et al
    * CAV 2015.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 94f9496f31b6fccf6b7d0fd1d059cd7f7e5e0b76..7951a9c41c4d6532bb35f4af132159b7c0435eb8 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -905,6 +905,7 @@ set(regress_0_tests
   regress0/sygus/dt-sel-parse1.sy
   regress0/sygus/hd-05-d1-prog-nogrammar.sy
   regress0/sygus/inv-different-var-order.sy
+  regress0/sygus/issue3356-syg-inf-usort.smt2
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
   regress0/sygus/no-syntax-test-bool.sy
@@ -1383,6 +1384,7 @@ set(regress_1_tests
   regress1/quantifiers/is-even.smt2
   regress1/quantifiers/isaplanner-goal20.smt2
   regress1/quantifiers/issue2970-string-var-elim.smt2
+  regress1/quantifiers/issue3250-syg-inf-q.smt2
   regress1/quantifiers/issue3317.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2

diff --git a/test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2 b/test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2
new file mode 100644 (file)
index 0000000..b35b725
--- /dev/null
+++ b/test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --sygus-inference
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort S 1)
+(define-sort SB () (S Bool))
+(declare-fun A () (S Bool))
+(declare-fun B () SB)
+(assert (= A B))
+; do not do sygus inference due to uninterpreted sorts
+(check-sat)
+(exit)

diff --git a/test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2 b/test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2
new file mode 100644 (file)
index 0000000..bb6a634
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun a () Real)   
+(assert 
+    (and  
+        (and 
+            (exists ((?b Real)) (forall ((?c Real)) (exists ((?d Real)) 
+            (or  (and  (and  (and (and (< (+ (+ (+ 0 (* 68.0 ?c)) 0) (* 33.0 a)) 0.0) (<= 0 2.0)) 
+            (or (<= 0 (+  (*  (+ (* 55.0 ?d) 0) (* 49.0 ?b)) 0))))))))))
+        )
+    )
+) 
+
+(check-sat)