diff options
| -rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 21 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 14 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.h | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2 | 14 |
6 files changed, 63 insertions, 1 deletions
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 471d68ff8..930edf869 100644 --- 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 31131f23f..ba55db132 100644 --- 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 ca1b9ae37..85efddada 100644 --- 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 94f9496f3..7951a9c41 100644 --- 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 index 000000000..b35b7253c --- /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 index 000000000..bb6a63490 --- /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) |