Also includes some minor improvement to expand definitions in TheoryDatatypes leftover from the branch.
Adds 3 regressions using the option --dt-nested-rec.
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;
api::Sort mkUnresolvedTypeConstructor(const std::string& name,
const std::vector<api::Sort>& 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.
*/
/**
* 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<std::string>& dnames,
std::string name;
std::vector<api::Sort> 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<dsize; i++)
+ {
+ if( arities[i]<0 )
+ {
+ // do not know the arity yet
+ continue;
+ }
+ unsigned arity = static_cast<unsigned>(arities[i]);
+ PARSER_STATE->mkUnresolvedType(dnames[i], arity);
+ }
+ }
( LPAREN_TOK {
params.clear();
Debug("parser-dt") << "Processing datatype #" << dts.size() << std::endl;
if( arities[dts.size()]>=0 && static_cast<int>(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));
}
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,
{
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
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<TupleUpdate>().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<RecordUpdate>().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)
{
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;
}
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
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff