diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 65 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/issue3645-grammar-sets.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/sets-pred-test.sy | 12 | ||||
| -rw-r--r-- | test/regress/regress2/sygus/sets-fun-test.sy | 10 |
5 files changed, 82 insertions, 15 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 259f9c642..17cc6bf9e 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -409,7 +409,7 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, { ops.push_back(nm->mkConst(String(""))); } - else if (type.isArray()) + else if (type.isArray() || type.isSet()) { // generate constant array over the first element of the constituent type Node c = type.mkGroundTerm(); @@ -443,6 +443,10 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor( collectSygusGrammarTypesFor(range.getArrayIndexType(), types); collectSygusGrammarTypesFor(range.getArrayConstituentType(), types); } + else if (range.isSet()) + { + collectSygusGrammarTypesFor(range.getSetElementType(), types); + } else if (range.isString() ) { // theory of strings shares the integer type @@ -791,22 +795,17 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Trace("sygus-grammar-def") << "...building for array type " << types[i] << "\n"; - Trace("sygus-grammar-def") << "......finding unres type for index type " - << types[i].getArrayIndexType() << "\n"; + TypeNode indexType = types[i].getArrayIndexType(); + TypeNode elemType = types[i].getArrayConstituentType(); + Trace("sygus-grammar-def") + << "......finding unres type for index type " << indexType << "\n"; // retrieve index and constituent unresolved types - Assert(std::find(types.begin(), types.end(), types[i].getArrayIndexType()) - != types.end()); - unsigned i_indexType = std::distance( - types.begin(), - std::find(types.begin(), types.end(), types[i].getArrayIndexType())); - TypeNode unres_indexType = unres_types[i_indexType]; - Assert(std::find( - types.begin(), types.end(), types[i].getArrayConstituentType()) - != types.end()); + Assert(type_to_unres.find(indexType) != type_to_unres.end()); + TypeNode unres_indexType = type_to_unres[indexType]; + Assert(std::find(types.begin(), types.end(), elemType) != types.end()); + // must get this index since we add to sdt[i_constituentType] below. unsigned i_constituentType = std::distance( - types.begin(), - std::find( - types.begin(), types.end(), types[i].getArrayConstituentType())); + types.begin(), std::find(types.begin(), types.end(), elemType)); TypeNode unres_constituentType = unres_types[i_constituentType]; // add (store ArrayType IndexType ConstituentType) Trace("sygus-grammar-def") << "...add for STORE\n"; @@ -824,6 +823,30 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargsSelect.push_back(unres_indexType); sdts[i_constituentType].addConstructor(SELECT, cargsSelect); } + else if (types[i].isSet()) + { + TypeNode etype = types[i].getSetElementType(); + // retrieve element unresolved type + Assert(type_to_unres.find(etype) != type_to_unres.end()); + TypeNode unresElemType = type_to_unres[etype]; + + // add for singleton + Trace("sygus-grammar-def") << "...add for singleton" << std::endl; + std::vector<TypeNode> cargsSingleton; + cargsSingleton.push_back(unresElemType); + sdts[i].addConstructor(SINGLETON, cargsSingleton); + + // add for union, difference, intersection + std::vector<Kind> bin_kinds = {UNION, INTERSECTION, SETMINUS}; + std::vector<TypeNode> cargsBinary; + cargsBinary.push_back(unres_t); + cargsBinary.push_back(unres_t); + for (const Kind k : bin_kinds) + { + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + sdts[i].addConstructor(k, cargsBinary); + } + } else if (types[i].isDatatype()) { Trace("sygus-grammar-def") << "...add for constructors" << std::endl; @@ -1197,6 +1220,18 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( sdtBool.addConstructor(dt[kind].getTester(), sst.str(), cargsTester); } } + else if (types[i].isSet()) + { + // add for member + TypeNode etype = types[i].getSetElementType(); + Assert(type_to_unres.find(etype) != type_to_unres.end()); + TypeNode unresElemType = type_to_unres[etype]; + std::vector<TypeNode> cargsMember; + cargsMember.push_back(unresElemType); + cargsMember.push_back(unres_types[iuse]); + Trace("sygus-grammar-def") << "...for MEMBER" << std::endl; + sdtBool.addConstructor(MEMBER, cargsMember); + } } // add Boolean connectives, if not in a degenerate case of (recursively) // having only constant constructors diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a7d931246..5eaaf3e67 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -968,6 +968,7 @@ set(regress_0_tests regress0/sygus/inv-different-var-order.sy regress0/sygus/issue3356-syg-inf-usort.smt2 regress0/sygus/issue3624.sy + regress0/sygus/issue3645-grammar-sets.smt2 regress0/sygus/let-ringer.sy regress0/sygus/let-simp.sy regress0/sygus/no-logic.sy @@ -1870,6 +1871,7 @@ set(regress_1_tests regress1/sygus/rec-fun-while-infinite.sy regress1/sygus/re-concat.sy regress1/sygus/repair-const-rl.sy + regress1/sygus/sets-pred-test.sy regress1/sygus/simple-regexp.sy regress1/sygus/stopwatch-bt.sy regress1/sygus/strings-any-term1.sy @@ -2017,6 +2019,7 @@ set(regress_2_tests regress2/sygus/process-10-vars-2fun.sy regress2/sygus/process-arg-invariance.sy regress2/sygus/real-grammar-neg.sy + regress2/sygus/sets-fun-test.sy regress2/sygus/strings-no-syntax-len.sy regress2/sygus/three.sy regress2/sygus/vcb.sy diff --git a/test/regress/regress0/sygus/issue3645-grammar-sets.smt2 b/test/regress/regress0/sygus/issue3645-grammar-sets.smt2 new file mode 100644 index 000000000..22a5e07d4 --- /dev/null +++ b/test/regress/regress0/sygus/issue3645-grammar-sets.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +; COMMAND-LINE: --sygus-inference +(set-logic ALL) +(declare-fun a () (Set (_ BitVec 2))) +(declare-fun b () (Set (_ BitVec 2))) +(assert (= a b)) +(check-sat) diff --git a/test/regress/regress1/sygus/sets-pred-test.sy b/test/regress/regress1/sygus/sets-pred-test.sy new file mode 100644 index 000000000..284325712 --- /dev/null +++ b/test/regress/regress1/sygus/sets-pred-test.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) +(synth-fun P ((x (Set Int))) Bool) + +(constraint (not (P (as emptyset (Set Int))))) +(constraint (not (P (insert 1 2 (as emptyset (Set Int)))))) +(constraint (P (insert 0 (as emptyset (Set Int))))) +(constraint (P (insert 0 4 5 (as emptyset (Set Int))))) +(constraint (not (P (singleton 45)))) + +(check-synth) diff --git a/test/regress/regress2/sygus/sets-fun-test.sy b/test/regress/regress2/sygus/sets-fun-test.sy new file mode 100644 index 000000000..987d6a792 --- /dev/null +++ b/test/regress/regress2/sygus/sets-fun-test.sy @@ -0,0 +1,10 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) +(synth-fun f ((x Int)) (Set Int)) + +(constraint (member 45 (f 45))) +(constraint (member 8 (f 8))) +(constraint (member 0 (f 3))) + +(check-synth) |