diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 34 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 7 |
2 files changed, 34 insertions, 7 deletions
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index b530edeaa..85ff5c896 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -685,6 +685,14 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { }else{ // no arguments to synthesis functions } + // register connected types + for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) + { + registerSygusType(getArgType(dt[i], j)); + } + } //iterate over constructors for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ Expr sop = dt[i].getSygusOp(); @@ -701,6 +709,26 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { d_consts[tn][n] = i; d_arg_const[tn][i] = n; } + else if (sop.getKind() == LAMBDA) + { + // do type checking + Assert(sop[0].getNumChildren() == dt[i].getNumArgs()); + for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) + { + TypeNode ct = TypeNode::fromType(dt[i].getArgType(j)); + TypeNode cbt = sygusToBuiltinType(ct); + TypeNode lat = TypeNode::fromType(sop[0][j].getType()); + CVC4_CHECK(cbt.isSubtypeOf(lat)) + << "In sygus datatype " << dt.getName() + << ", argument to a lambda constructor is not " << lat + << std::endl; + } + } + // TODO (as part of #1170): we still do not properly catch type + // errors in sygus grammars for arguments of builtin operators. + // The challenge is that we easily ask for expected argument types of + // builtin operators e.g. PLUS. Hence the call to mkGeneric below + // will throw a type exception. d_ops[tn][n] = i; d_arg_ops[tn][i] = n; Trace("sygus-db") << std::endl; @@ -714,12 +742,6 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { << "Sygus datatype " << dt.getName() << " encodes terms that are not of type " << btn << std::endl; } - //register connected types - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ - registerSygusType( getArgType( dt[i], j ) ); - } - } } } } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 9466a6a10..a9e17fdf9 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -189,6 +189,12 @@ class TermDbSygus { * and constants c1...cn. */ bool isEvaluationPoint(Node n) const; + /** return the builtin type of tn + * + * The type tn should be a sygus datatype type that has been registered to + * this database. + */ + TypeNode sygusToBuiltinType(TypeNode tn); //-----------------------------end conversion from sygus to builtin private: @@ -285,7 +291,6 @@ private: unsigned getSelectorWeight(TypeNode tn, Node sel); public: - TypeNode sygusToBuiltinType( TypeNode tn ); int getKindConsNum( TypeNode tn, Kind k ); int getConstConsNum( TypeNode tn, Node n ); int getOpConsNum( TypeNode tn, Node n ); |