From 89384c9a4aad291ce5ca26917507e4fd47c6ec4f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 7 Apr 2021 20:40:42 -0500 Subject: Initial support for parametric datatypes in sygus (#6304) Fixes #6298. Enables parsing of par in the sygus parser, and adds support for default grammar construction. Also fixes a bug related to single invocation for non-function types. --- src/expr/dtype_cons.cpp | 9 +++++-- src/parser/smt2/Smt2.g | 2 +- src/theory/quantifiers/single_inv_partition.cpp | 4 +-- .../quantifiers/sygus/sygus_grammar_cons.cpp | 30 ++++++++++++++-------- test/regress/CMakeLists.txt | 1 + test/regress/regress0/sygus/issue6298-par.sy | 6 +++++ 6 files changed, 37 insertions(+), 15 deletions(-) create mode 100644 test/regress/regress0/sygus/issue6298-par.sy diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 927c48dda..c358aa2e8 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -120,15 +120,20 @@ TypeNode DTypeConstructor::getSpecializedConstructorType( << "DTypeConstructor::getSpecializedConstructorType: expected datatype, " "got " << returnType; + TypeNode ctn = d_constructor.getType(); const DType& dt = DType::datatypeOf(d_constructor); - Assert(dt.isParametric()); + if (!dt.isParametric()) + { + // if the datatype is not parametric, then no specialization is needed + return ctn; + } TypeNode dtt = dt.getTypeNode(); TypeMatcher m(dtt); m.doMatching(dtt, returnType); std::vector subst; m.getMatches(subst); std::vector params = dt.getParameters(); - return d_constructor.getType().substitute( + return ctn.substitute( params.begin(), params.end(), subst.begin(), subst.end()); } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 3302533e6..00cf8e75a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2217,7 +2217,7 @@ DECLARE_DATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) DECLARE_DATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-datatypes'; DECLARE_CODATATYPES_2_5_TOK : { !( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) }?'declare-codatatypes'; DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'declare-codatatypes'; -PAR_TOK : { PARSER_STATE->v2_6() }?'par'; +PAR_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'par'; COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) }?'comprehension'; TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'is'; MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'match'; diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 7a1a6fb45..6885bb01b 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -139,7 +139,7 @@ bool SingleInvocationPartition::init(std::vector& funcs, Node n) if (!funcs.empty()) { TypeNode tn0 = funcs[0].getType(); - if (tn0.getNumChildren() > 0) + if (tn0.isFunction()) { for (unsigned i = 0, nargs = tn0.getNumChildren() - 1; i < nargs; i++) { @@ -155,7 +155,7 @@ bool SingleInvocationPartition::init(std::vector& funcs, Node n) Trace("si-prt") << "...type mismatch" << std::endl; return false; } - else if (tni.getNumChildren() > 0) + else if (tni.isFunction()) { for (unsigned j = 0, nargs = tni.getNumChildren() - 1; j < nargs; j++) { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 1c96b1346..d1a1315c9 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -458,11 +458,13 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor( const DType& dt = range.getDType(); for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i) { - for (unsigned j = 0, size_args = dt[i].getNumArgs(); j < size_args; - ++j) + // get the specialized constructor type, which accounts for + // parametric datatypes + TypeNode ctn = dt[i].getSpecializedConstructorType(range); + std::vector argTypes = ctn.getArgTypes(); + for (size_t j = 0, nargs = argTypes.size(); j < nargs; ++j) { - TypeNode tn = dt[i][j].getRangeType(); - collectSygusGrammarTypesFor(tn, types); + collectSygusGrammarTypesFor(argTypes[j], types); } } } @@ -988,6 +990,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Trace("sygus-grammar-def") << "...for " << dt[l].getName() << std::endl; Node cop = dt[l].getConstructor(); + TypeNode tspec = dt[l].getSpecializedConstructorType(types[i]); + // must specialize if a parametric datatype + if (dt.isParametric()) + { + cop = nm->mkNode( + APPLY_TYPE_ASCRIPTION, nm->mkConst(AscriptionType(tspec)), cop); + } if (dt[l].getNumArgs() == 0) { // Nullary constructors are interpreted as terms, not operators. @@ -996,11 +1005,15 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } std::vector cargsCons; Trace("sygus-grammar-def") << "...add for selectors" << std::endl; - for (unsigned j = 0, size_j = dt[l].getNumArgs(); j < size_j; ++j) + // iterate over the arguments of the specialized constructor type, + // which accounts for parametric datatypes + std::vector tsargs = tspec.getArgTypes(); + TypeNode selDomain = type_to_unres[types[i]]; + for (unsigned j = 0, size_j = tsargs.size(); j < size_j; ++j) { Trace("sygus-grammar-def") << "...for " << dt[l][j].getName() << std::endl; - TypeNode crange = dt[l][j].getRangeType(); + TypeNode crange = tsargs[j]; Assert(type_to_unres.find(crange) != type_to_unres.end()); cargsCons.push_back(type_to_unres[crange]); // add to the selector type the selector operator @@ -1008,11 +1021,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Assert(std::find(types.begin(), types.end(), crange) != types.end()); unsigned i_selType = std::distance( types.begin(), std::find(types.begin(), types.end(), crange)); - TypeNode arg_type = dt[l][j].getType(); - arg_type = arg_type.getSelectorDomainType(); - Assert(type_to_unres.find(arg_type) != type_to_unres.end()); std::vector cargsSel; - cargsSel.push_back(type_to_unres[arg_type]); + cargsSel.push_back(selDomain); Node sel = dt[l][j].getSelector(); sdts[i_selType].addConstructor(sel, dt[l][j].getName(), cargsSel); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c7c311079..83f1c7d84 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1172,6 +1172,7 @@ set(regress_0_tests regress0/sygus/issue4383-cache-fv-id.sy regress0/sygus/issue4790-dtd.sy regress0/sygus/issue5512-vvv.sy + regress0/sygus/issue6298-par.sy regress0/sygus/let-ringer.sy regress0/sygus/let-simp.sy regress0/sygus/no-logic.sy diff --git a/test/regress/regress0/sygus/issue6298-par.sy b/test/regress/regress0/sygus/issue6298-par.sy new file mode 100644 index 000000000..bffa02b29 --- /dev/null +++ b/test/regress/regress0/sygus/issue6298-par.sy @@ -0,0 +1,6 @@ +; EXPECT: unsat +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic ALL) +(declare-datatypes (( List 1)) ( (par (T) ((nil) (cons (head T) (tail (List T))))))) +(synth-fun f () (List Int)) +(check-synth) -- cgit v1.2.3