diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 11:47:05 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-26 11:47:05 -0600 |
| commit | 2a274c84867a2974abc0b626349b934d520339b0 (patch) | |
| tree | ba38f050cc21927407ec45bd9b14e8d9ab97b0ec /src/theory/quantifiers/sygus/sygus_grammar_norm.cpp | |
| parent | 40807e2f5f3b9d07e66dc2d2a7dde4c8aac98720 (diff) | |
Use default consts when not using any const during grammar normalization (#3807)
Fixes #3802.
If we decide not to add the any constant constructor due to insufficient cegqi algorithms (or if the sort is Boolean), then we should add the default constants for a sort.
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_grammar_norm.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_norm.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index b2e7d2681..f00fd0092 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine_scope.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_grammar_red.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -557,6 +558,19 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, // same level as constants. to.d_sdt.addAnyConstantConstructor(dtn); } + else + { + // add default constant constructors + std::vector<Node> ops; + CegGrammarConstructor::mkSygusConstantsForType(sygus_type, ops); + for (const Node& op : ops) + { + std::stringstream ss; + ss << op; + std::vector<TypeNode> ctypes; + to.d_sdt.addConstructor(op, ss.str(), ctypes); + } + } } /* Determine normalization transformation based on sygus type and given |