diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-08 18:06:16 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-08 16:06:16 -0700 |
commit | 1b6784fe52f4fb745262842e0406d6dd34053cb2 (patch) | |
tree | 6c64a7485612f8af60631fde4dd827222d17215d /src/preprocessing | |
parent | 16b54708ff83a1bf6393203b79da6dc059fd2025 (diff) |
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.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 21 |
1 files changed, 20 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; |