From 6a61c1a75b08867c7c06623b8c03084056b6bed7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 5 Jun 2020 19:04:10 -0500 Subject: [PATCH] Smt2 parsing support for nested recursive datatypes (#4575) Also includes some minor improvement to expand definitions in TheoryDatatypes leftover from the branch. Adds 3 regressions using the option --dt-nested-rec. --- src/parser/parser.cpp | 9 +++++ src/parser/parser.h | 7 ++++ src/parser/smt2/Smt2.g | 36 +++++++++++++++++-- src/theory/datatypes/theory_datatypes.cpp | 19 +++++----- test/regress/CMakeLists.txt | 3 ++ .../datatypes/non-simple-rec-mut-unsat.smt2 | 18 ++++++++++ .../datatypes/non-simple-rec-param.smt2 | 15 ++++++++ .../datatypes/non-simple-rec-set.smt2 | 10 ++++++ .../regress1/datatypes/non-simple-rec.smt2 | 11 ++++++ 9 files changed, 115 insertions(+), 13 deletions(-) create mode 100644 test/regress/regress1/datatypes/non-simple-rec-mut-unsat.smt2 create mode 100644 test/regress/regress1/datatypes/non-simple-rec-param.smt2 create mode 100644 test/regress/regress1/datatypes/non-simple-rec-set.smt2 create mode 100644 test/regress/regress1/datatypes/non-simple-rec.smt2 diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index b24f9ae9d..5ad773c9c 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -387,6 +387,15 @@ api::Sort Parser::mkUnresolvedTypeConstructor( return unresolved; } +api::Sort Parser::mkUnresolvedType(const std::string& name, size_t arity) +{ + if (arity == 0) + { + return mkUnresolvedType(name); + } + return mkUnresolvedTypeConstructor(name, arity); +} + bool Parser::isUnresolvedType(const std::string& name) { if (!isDeclared(name, SYM_SORT)) { return false; diff --git a/src/parser/parser.h b/src/parser/parser.h index b5dc83902..681404efa 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -588,6 +588,13 @@ public: api::Sort mkUnresolvedTypeConstructor(const std::string& name, const std::vector& params); + /** + * Creates a new unresolved (parameterized) type constructor of the given + * arity. Calls either mkUnresolvedType or mkUnresolvedTypeConstructor + * depending on the arity. + */ + api::Sort mkUnresolvedType(const std::string& name, size_t arity); + /** * Returns true IFF name is an unresolved type. */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index ec3e874df..436700826 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1530,7 +1530,10 @@ datatypesDefCommand[bool isCo, std::unique_ptr* cmd] /** * Read a list of datatype definitions for datatypes with names dnames and * parametric arities arities. A negative value in arities indicates that the - * arity for the corresponding datatype has not been fixed. + * arity for the corresponding datatype has not been fixed: notice that we do + * not know the arity of datatypes in the declare-datatype command prior to + * parsing their body, whereas the arity of datatypes in declare-datatypes is + * given in the preamble of that command and thus is known prior to this call. */ datatypesDef[bool isCo, const std::vector& dnames, @@ -1541,7 +1544,26 @@ datatypesDef[bool isCo, std::string name; std::vector params; } - : { PARSER_STATE->pushScope(true); } + : { PARSER_STATE->pushScope(true); + // Declare the datatypes that are currently being defined as unresolved + // types. If we do not know the arity of the datatype yet, we wait to + // define it until parsing the preamble of its body, which may optionally + // involve `par`. This is limited to the case of single datatypes defined + // via declare-datatype, and hence no datatype body is parsed without + // having all types declared. This ensures we can parse datatypes with + // nested recursion, e.g. datatypes D having a subfield type + // (Array Int D). + for (unsigned i=0, dsize=dnames.size(); i(arities[i]); + PARSER_STATE->mkUnresolvedType(dnames[i], arity); + } + } ( LPAREN_TOK { params.clear(); Debug("parser-dt") << "Processing datatype #" << dts.size() << std::endl; @@ -1559,6 +1581,11 @@ datatypesDef[bool isCo, if( arities[dts.size()]>=0 && static_cast(params.size())!=arities[dts.size()] ){ PARSER_STATE->parseError("Wrong number of parameters for datatype."); } + if (arities[dts.size()]<0) + { + // now declare it as an unresolved type + PARSER_STATE->mkUnresolvedType(dnames[dts.size()], params.size()); + } Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl; dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()], params, isCo)); } @@ -1569,6 +1596,11 @@ datatypesDef[bool isCo, if( arities[dts.size()]>0 ){ PARSER_STATE->parseError("No parameters given for datatype."); } + else if (arities[dts.size()]<0) + { + // now declare it as an unresolved type + PARSER_STATE->mkUnresolvedType(dnames[dts.size()], 0); + } Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl; dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()], params, diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 6e5b028a7..b0164265d 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -587,7 +587,6 @@ Node TheoryDatatypes::expandDefinition(Node n) { case kind::APPLY_SELECTOR: { - Trace("dt-expand") << "Dt Expand definition : " << n << std::endl; Node selector = n.getOperator(); // APPLY_SELECTOR always applies to an external selector, cindexOf is // legal here @@ -643,30 +642,28 @@ Node TheoryDatatypes::expandDefinition(Node n) case TUPLE_UPDATE: case RECORD_UPDATE: { - TypeNode t = n.getType(); - Assert(t.isDatatype()); - const DType& dt = t.getDType(); + Assert(tn.isDatatype()); + const DType& dt = tn.getDType(); NodeBuilder<> b(APPLY_CONSTRUCTOR); b << dt[0].getConstructor(); size_t size, updateIndex; if (n.getKind() == TUPLE_UPDATE) { - Assert(t.isTuple()); - size = t.getTupleLength(); + Assert(tn.isTuple()); + size = tn.getTupleLength(); updateIndex = n.getOperator().getConst().getIndex(); } else { - Assert(t.toType().isRecord()); - const Record& record = - DatatypeType(t.toType()).getRecord(); + Assert(tn.toType().isRecord()); + const Record& record = DatatypeType(tn.toType()).getRecord(); size = record.getNumFields(); updateIndex = record.getIndex( n.getOperator().getConst().getField()); } Debug("tuprec") << "expr is " << n << std::endl; Debug("tuprec") << "updateIndex is " << updateIndex << std::endl; - Debug("tuprec") << "t is " << t << std::endl; + Debug("tuprec") << "t is " << tn << std::endl; Debug("tuprec") << "t has arity " << size << std::endl; for (size_t i = 0; i < size; ++i) { @@ -679,7 +676,7 @@ Node TheoryDatatypes::expandDefinition(Node n) else { b << nm->mkNode( - APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(t, i), n[0]); + APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, i), n[0]); Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f6bc70cd0..4bc9d2705 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1275,6 +1275,9 @@ set(regress_1_tests regress1/datatypes/issue3266-small.smt2 regress1/datatypes/issue-variant-dt-zero.smt2 regress1/datatypes/manos-model.smt2 + regress1/datatypes/non-simple-rec.smt2 + regress1/datatypes/non-simple-rec-mut-unsat.smt2 + regress1/datatypes/non-simple-rec-param.smt2 regress1/decision/error3.smtv1.smt2 regress1/decision/quant-Arrays_Q1-noinfer.smt2 regress1/decision/quant-symmetric_unsat_7.smt2 diff --git a/test/regress/regress1/datatypes/non-simple-rec-mut-unsat.smt2 b/test/regress/regress1/datatypes/non-simple-rec-mut-unsat.smt2 new file mode 100644 index 000000000..35e06a0d3 --- /dev/null +++ b/test/regress/regress1/datatypes/non-simple-rec-mut-unsat.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --dt-nested-rec +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((E 0)(T 0)) ( +((Yes) (No)) +((FMap (m (Array E E))) (Map (mm (Array E T))) (None) ) +)) +(declare-fun a () T) +(declare-fun b () T) +(declare-fun c () T) +(assert (distinct a b c)) +(assert ((_ is FMap) a)) +(assert ((_ is FMap) b)) +(assert ((_ is FMap) c)) +(assert (= (select (m a) Yes) (select (m b) Yes))) +(assert (= (select (m b) Yes) (select (m c) Yes))) +(check-sat) diff --git a/test/regress/regress1/datatypes/non-simple-rec-param.smt2 b/test/regress/regress1/datatypes/non-simple-rec-param.smt2 new file mode 100644 index 000000000..8db92b0fd --- /dev/null +++ b/test/regress/regress1/datatypes/non-simple-rec-param.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --dt-nested-rec +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((T 1)) ( +(par (x) ((Data (s x)) (Map (m (Array Int (T (T Int)))) ) ) )) +) +(declare-fun a () (T Int)) +(declare-fun b () (T Int)) +(declare-fun c () (T Int)) +(declare-fun d () (T Int)) +(assert (distinct a b c d)) +(assert (= (select (m a) 5) (Data b))) +(assert (not (= (s b) 0))) +(check-sat) diff --git a/test/regress/regress1/datatypes/non-simple-rec-set.smt2 b/test/regress/regress1/datatypes/non-simple-rec-set.smt2 new file mode 100644 index 000000000..a6c4f6695 --- /dev/null +++ b/test/regress/regress1/datatypes/non-simple-rec-set.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --dt-nested-rec +; EXPECT: unsat +(set-logic ALL) +(declare-datatype T +((Emp) (Container (s (Set T)) ) +)) +(declare-fun a () T) +(assert (not ((_ is Emp) a))) +(assert (= (s a) (singleton a))) +(check-sat) diff --git a/test/regress/regress1/datatypes/non-simple-rec.smt2 b/test/regress/regress1/datatypes/non-simple-rec.smt2 new file mode 100644 index 000000000..f6b8ede3f --- /dev/null +++ b/test/regress/regress1/datatypes/non-simple-rec.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --dt-nested-rec +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((T 0)) (((Nil) (Map (m (Array Int T)) ) ) )) +(declare-fun a () T) +(declare-fun b () T) +(declare-fun c () T) +(declare-fun d () T) +(assert (distinct a b c d)) +(check-sat) -- 2.30.2