diff options
Diffstat (limited to 'src')
-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 |
3 files changed, 36 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. |