// TODO #1178 : add other missing types
}
-void CegGrammarConstructor::collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ){
+void CegGrammarConstructor::collectSygusGrammarTypesFor(
+ TypeNode range, std::vector<TypeNode>& types)
+{
if( !range.isBoolean() ){
if( std::find( types.begin(), types.end(), range )==types.end() ){
Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl;
types.push_back( range );
if( range.isDatatype() ){
- const Datatype& dt = ((DatatypeType)range.toType()).getDatatype();
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
- TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() );
- sels[crange].push_back( dt[i][j] );
- collectSygusGrammarTypesFor( crange, types, sels );
+ const Datatype& dt = range.getDatatype();
+ for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
+ {
+ for (unsigned j = 0, size_args = dt[i].getNumArgs(); j < size_args;
+ ++j)
+ {
+ collectSygusGrammarTypesFor(
+ TypeNode::fromType(static_cast<SelectorType>(dt[i][j].getType())
+ .getRangeType()),
+ types);
}
}
}
<< range << std::endl;
// collect the variables
std::vector<Node> sygus_vars;
- if( !bvl.isNull() ){
- for( unsigned i=0; i<bvl.getNumChildren(); i++ ){
+ if (!bvl.isNull())
+ {
+ for (unsigned i = 0, size = bvl.getNumChildren(); i < size; ++i)
+ {
if (term_irrelevant.find(bvl[i]) == term_irrelevant.end())
{
sygus_vars.push_back(bvl[i]);
}
else
{
- Trace("sygus-grammar-def") << "...synth var " << bvl[i]
- << " has been marked irrelevant."
- << std::endl;
+ Trace("sygus-grammar-def")
+ << "...synth var " << bvl[i] << " has been marked irrelevant."
+ << std::endl;
}
}
}
- //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
- // parseError("No default grammar for type.");
- //}
- std::vector< std::vector< Expr > > ops;
+ // operators for each constructor in type
+ std::vector<std::vector<Expr>> ops;
+ // names for the operators
+ std::vector<std::vector<std::string>> cnames;
+ // argument types of operators
+ std::vector<std::vector<std::vector<Type>>> cargs;
+ // set of callbacks for each constructor
+ std::vector<std::vector<std::shared_ptr<SygusPrintCallback>>> pcs;
+ // weights for each constructor
+ std::vector<std::vector<int>> weights;
+ // index of top datatype, i.e. the datatype for the range type
int startIndex = -1;
std::map< Type, Type > sygus_to_builtin;
- std::vector< TypeNode > types;
- std::map< TypeNode, std::vector< DatatypeConstructorArg > > sels;
- //types for each of the variables of parametric sort
- for( unsigned i=0; i<sygus_vars.size(); i++ ){
- collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels );
+ std::vector<TypeNode> types;
+ // collect connected types for each of the variables
+ for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i)
+ {
+ collectSygusGrammarTypesFor(sygus_vars[i].getType(), types);
}
- //types connected to range
- collectSygusGrammarTypesFor( range, types, sels );
+ // collect connected types to range
+ collectSygusGrammarTypesFor(range, types);
- //name of boolean sort
+ // create placeholder for boolean type (kept apart since not collected)
std::stringstream ssb;
ssb << fun << "_Bool";
std::string dbname = ssb.str();
Type unres_bt = mkUnresolvedType(ssb.str(), unres).toType();
+ // create placeholders for collected types
std::vector< Type > unres_types;
std::map< TypeNode, Type > type_to_unres;
- for( unsigned i=0; i<types.size(); i++ ){
+ for (unsigned i = 0, size = types.size(); i < size; ++i)
+ {
std::stringstream ss;
ss << fun << "_" << types[i];
std::string dname = ss.str();
datatypes.push_back(Datatype(dname));
ops.push_back(std::vector< Expr >());
+ cnames.push_back(std::vector<std::string>());
+ cargs.push_back(std::vector<std::vector<Type>>());
+ pcs.push_back(std::vector<std::shared_ptr<SygusPrintCallback>>());
+ weights.push_back(std::vector<int>());
//make unresolved type
Type unres_t = mkUnresolvedType(dname, unres).toType();
unres_types.push_back(unres_t);
type_to_unres[types[i]] = unres_t;
sygus_to_builtin[unres_t] = types[i].toType();
}
- for( unsigned i=0; i<types.size(); i++ ){
+ for (unsigned i = 0, size = types.size(); i < size; ++i)
+ {
Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
- std::vector<std::string> cnames;
- std::vector<std::vector<CVC4::Type> > cargs;
- /* Print callbacks for each constructor */
- std::vector<std::shared_ptr<SygusPrintCallback>> pcs;
- /* Weights for each constructor */
- std::vector<int> weights;
Type unres_t = unres_types[i];
//add variables
- for( unsigned j=0; j<sygus_vars.size(); j++ ){
+ for (unsigned j = 0, size_j = sygus_vars.size(); j < size_j; ++j)
+ {
if( sygus_vars[j].getType()==types[i] ){
std::stringstream ss;
ss << sygus_vars[j];
Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
ops[i].push_back( sygus_vars[j].toExpr() );
- cnames.push_back( ss.str() );
- cargs.push_back( std::vector< CVC4::Type >() );
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(ss.str());
+ cargs[i].push_back(std::vector<Type>());
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
}
//add constants
std::map< TypeNode, std::vector< Node > >::iterator itec = extra_cons.find( types[i] );
if( itec!=extra_cons.end() ){
//consts.insert( consts.end(), itec->second.begin(), itec->second.end() );
- for( unsigned j=0; j<itec->second.size(); j++ ){
+ for (unsigned j = 0, size_j = itec->second.size(); j < size_j; ++j)
+ {
if( std::find( consts.begin(), consts.end(), itec->second[j] )==consts.end() ){
consts.push_back( itec->second[j] );
}
}
}
- for( unsigned j=0; j<consts.size(); j++ ){
+ for (unsigned j = 0, size_j = consts.size(); j < size_j; ++j)
+ {
std::stringstream ss;
ss << consts[j];
Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl;
ops[i].push_back( consts[j].toExpr() );
- cnames.push_back( ss.str() );
- cargs.push_back( std::vector< CVC4::Type >() );
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(ss.str());
+ cargs[i].push_back(std::vector<Type>());
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
- //ITE
- CVC4::Kind k = kind::ITE;
+ // ITE
+ Kind k = ITE;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops[i].push_back(nm->operatorOf(k).toExpr());
- cnames.push_back( kind::kindToString(k) );
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_bt);
- cargs.back().push_back(unres_t);
- cargs.back().push_back(unres_t);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(kindToString(k));
+ cargs[i].push_back(std::vector<Type>());
+ cargs[i].back().push_back(unres_bt);
+ cargs[i].back().push_back(unres_t);
+ cargs[i].back().push_back(unres_t);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
if (types[i].isReal())
{
Kind k = j == 0 ? PLUS : MINUS;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops[i].push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kind::kindToString(k));
- cargs.push_back(std::vector<CVC4::Type>());
- cargs.back().push_back(unres_t);
- cargs.back().push_back(unres_t);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(kindToString(k));
+ cargs[i].push_back(std::vector<Type>());
+ cargs[i].back().push_back(unres_t);
+ cargs[i].back().push_back(unres_t);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
if (!types[i].isInteger())
{
- Trace("sygus-grammar-def") << "...Dedicate to Real\n";
+ Trace("sygus-grammar-def")
+ << " ...create auxiliary Positive Integers grammar\n";
/* Creating type for positive integers */
std::stringstream ss;
ss << fun << "_PosInt";
/* Add operator 1 */
Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n";
ops_pos_int.push_back(nm->mkConst(Rational(1)).toExpr());
- ss << "_1";
+ ss.str("");
+ ss << "1";
cnames_pos_int.push_back(ss.str());
cargs_pos_int.push_back(std::vector<Type>());
/* Add operator PLUS */
cargs_pos_int.back().push_back(unres_pos_int_t);
cargs_pos_int.back().push_back(unres_pos_int_t);
datatypes.back().setSygus(types[i].toType(), bvl.toExpr(), true, true);
- for (unsigned j = 0; j < ops_pos_int.size(); j++)
+ for (unsigned j = 0, size_j = ops_pos_int.size(); j < size_j; ++j)
{
datatypes.back().addSygusConstructor(
ops_pos_int[j], cnames_pos_int[j], cargs_pos_int[j]);
}
Trace("sygus-grammar-def")
- << "...built datatype " << datatypes.back() << " ";
+ << " ...built datatype " << datatypes.back() << " ";
/* Adding division at root */
k = DIVISION;
Trace("sygus-grammar-def") << "\t...add for " << k << std::endl;
ops[i].push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kindToString(k));
- cargs.push_back(std::vector<Type>());
- cargs.back().push_back(unres_t);
- cargs.back().push_back(unres_pos_int_t);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(kindToString(k));
+ cargs[i].push_back(std::vector<Type>());
+ cargs[i].back().push_back(unres_t);
+ cargs[i].back().push_back(unres_pos_int_t);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
}
else if (types[i].isBitVector())
{
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops[i].push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kindToString(k));
- cargs.push_back(std::vector<Type>());
- cargs.back().push_back(unres_t);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(kindToString(k));
+ cargs[i].push_back(std::vector<Type>());
+ cargs[i].back().push_back(unres_t);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
// binary apps
std::vector<Kind> bin_kinds = {BITVECTOR_AND,
{
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops[i].push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kindToString(k));
- cargs.push_back(std::vector<Type>());
- cargs.back().push_back(unres_t);
- cargs.back().push_back(unres_t);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames[i].push_back(kindToString(k));
+ cargs[i].push_back(std::vector<Type>());
+ cargs[i].back().push_back(unres_t);
+ cargs[i].back().push_back(unres_t);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
}
else if (types[i].isDatatype())
{
Trace("sygus-grammar-def") << "...add for constructors" << std::endl;
- const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype();
- for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
+ const Datatype& dt = types[i].getDatatype();
+ for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
+ {
Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl;
ops[i].push_back( dt[k].getConstructor() );
- cnames.push_back( dt[k].getName() );
- cargs.push_back( std::vector< CVC4::Type >() );
- for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){
- TypeNode crange = TypeNode::fromType( ((SelectorType)dt[k][j].getType()).getRangeType() );
- //Assert( type_to_unres.find(crange)!=type_to_unres.end() );
- cargs.back().push_back( type_to_unres[crange] );
+ cnames[i].push_back(dt[k].getName());
+ cargs[i].push_back(std::vector<Type>());
+ Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
+ for (unsigned j = 0, size_j = dt[k].getNumArgs(); j < size_j; ++j)
+ {
+ Trace("sygus-grammar-def")
+ << "...for " << dt[k][j].getName() << std::endl;
+ TypeNode crange = TypeNode::fromType(
+ static_cast<SelectorType>(dt[k][j].getType()).getRangeType());
+ Assert(type_to_unres.find(crange) != type_to_unres.end());
+ cargs[i].back().push_back(type_to_unres[crange]);
+ // add to the selector type the selector operator
+
+ 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 = TypeNode::fromType(
+ static_cast<SelectorType>(dt[k][j].getType()).getDomain());
+ ops[i_selType].push_back(dt[k][j].getSelector());
+ cnames[i_selType].push_back(dt[k][j].getName());
+ cargs[i_selType].push_back(std::vector<Type>());
+ Assert(type_to_unres.find(arg_type) != type_to_unres.end());
+ cargs[i_selType].back().push_back(type_to_unres[arg_type]);
+ pcs[i_selType].push_back(nullptr);
+ weights[i_selType].push_back(-1);
}
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ pcs[i].push_back(nullptr);
+ weights[i].push_back(-1);
}
}else{
std::stringstream sserr;
sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
throw LogicException(sserr.str());
}
- //add for all selectors to this type
- if( !sels[types[i]].empty() ){
- Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
- for( unsigned j=0; j<sels[types[i]].size(); j++ ){
- Trace("sygus-grammar-def") << "...for " << sels[types[i]][j].getName() << std::endl;
- TypeNode arg_type = TypeNode::fromType( ((SelectorType)sels[types[i]][j].getType()).getDomain() );
- ops[i].push_back( sels[types[i]][j].getSelector() );
- cnames.push_back( sels[types[i]][j].getName() );
- cargs.push_back( std::vector< CVC4::Type >() );
- //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() );
- cargs.back().push_back( type_to_unres[arg_type] );
- pcs.push_back(nullptr);
- weights.push_back(-1);
- }
- }
+ }
+ // make datatypes
+ for (unsigned i = 0, size = types.size(); i < size; ++i)
+ {
Trace("sygus-grammar-def") << "...make datatype " << datatypes[i] << std::endl;
datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true );
std::map<TypeNode, std::vector<Node>>::iterator itexc =
exc_cons.find(types[i]);
- for (unsigned j = 0, size = ops[i].size(); j < size; j++)
+ for (unsigned j = 0, size = ops[i].size(); j < size; ++j)
{
// add the constructor if it is not excluded
Node opn = Node::fromExpr(ops[i][j]);
== itexc->second.end())
{
datatypes[i].addSygusConstructor(
- ops[i][j], cnames[j], cargs[j], pcs[j], weights[j]);
+ ops[i][j], cnames[i][j], cargs[i][j], pcs[i][j], weights[i][j]);
}
}
- Trace("sygus-grammar-def")
- << "...built datatype " << datatypes[i] << " ";
- //sorts.push_back( types[i] );
+ Trace("sygus-grammar-def") << "...built datatype " << datatypes[i] << " ";
//set start index if applicable
if( types[i]==range ){
startIndex = i;
TypeNode btype = nm->booleanType();
datatypes.push_back(Datatype(dbname));
ops.push_back(std::vector<Expr>());
- std::vector<std::string> cnames;
- std::vector<std::vector< Type > > cargs;
- /* Print callbacks for each constructor */
- std::vector<std::shared_ptr<SygusPrintCallback>> pcs;
- /* Weights for each constructor */
- std::vector<int> weights;
+ cnames.push_back(std::vector<std::string>());
+ cargs.push_back(std::vector<std::vector<Type>>());
+ pcs.push_back(std::vector<std::shared_ptr<SygusPrintCallback>>());
+ weights.push_back(std::vector<int>());
Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl;
//add variables
- for( unsigned i=0; i<sygus_vars.size(); i++ ){
+ for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i)
+ {
if( sygus_vars[i].getType().isBoolean() ){
std::stringstream ss;
ss << sygus_vars[i];
Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
ops.back().push_back( sygus_vars[i].toExpr() );
- cnames.push_back( ss.str() );
- cargs.push_back( std::vector< CVC4::Type >() );
- pcs.push_back(nullptr);
- weights.push_back(1);
+ cnames.back().push_back(ss.str());
+ cargs.back().push_back(std::vector<Type>());
+ pcs.back().push_back(nullptr);
+ // make boolean variables weight as non-nullary constructors
+ weights.back().push_back(1);
}
}
- //add constants
+ // add constants
std::vector<Node> consts;
mkSygusConstantsForType(btype, consts);
- for (unsigned j = 0; j < consts.size(); j++)
+ for (unsigned i = 0, size = consts.size(); i < size; ++i)
{
std::stringstream ss;
- ss << consts[j];
+ ss << consts[i];
Trace("sygus-grammar-def") << "...add for constant " << ss.str()
<< std::endl;
- ops.back().push_back(consts[j].toExpr());
- cnames.push_back(ss.str());
- cargs.push_back(std::vector<CVC4::Type>());
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ ops.back().push_back(consts[i].toExpr());
+ cnames.back().push_back(ss.str());
+ cargs.back().push_back(std::vector<Type>());
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
}
- //add predicates for types
- for( unsigned i=0; i<types.size(); i++ ){
+ // add predicates for types
+ for (unsigned i = 0, size = types.size(); i < size; ++i)
+ {
Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl;
//add equality per type
- CVC4::Kind k = kind::EQUAL;
+ Kind k = EQUAL;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops.back().push_back(nm->operatorOf(k).toExpr());
std::stringstream ss;
- ss << kind::kindToString(k) << "_" << types[i];
- cnames.push_back(ss.str());
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_types[i]);
- cargs.back().push_back(unres_types[i]);
- pcs.push_back(nullptr);
- weights.push_back(-1);
- //type specific predicates
+ ss << kindToString(k) << "_" << types[i];
+ cnames.back().push_back(ss.str());
+ cargs.back().push_back(std::vector<Type>());
+ cargs.back().back().push_back(unres_types[i]);
+ cargs.back().back().push_back(unres_types[i]);
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
+ // type specific predicates
if (types[i].isReal())
{
- CVC4::Kind k = kind::LEQ;
+ Kind k = LEQ;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops.back().push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kind::kindToString(k));
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_types[i]);
- cargs.back().push_back(unres_types[i]);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames.back().push_back(kindToString(k));
+ cargs.back().push_back(std::vector<Type>());
+ cargs.back().back().push_back(unres_types[i]);
+ cargs.back().back().push_back(unres_types[i]);
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
}
else if (types[i].isBitVector())
{
Kind k = BITVECTOR_ULT;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops.back().push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kindToString(k));
- cargs.push_back(std::vector<Type>());
- cargs.back().push_back(unres_types[i]);
- cargs.back().push_back(unres_types[i]);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames.back().push_back(kindToString(k));
+ cargs.back().push_back(std::vector<Type>());
+ cargs.back().back().push_back(unres_types[i]);
+ cargs.back().back().push_back(unres_types[i]);
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
}
else if (types[i].isDatatype())
{
//add for testers
Trace("sygus-grammar-def") << "...add for testers" << std::endl;
- const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype();
- for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
+ const Datatype& dt = types[i].getDatatype();
+ for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
+ {
Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl;
ops.back().push_back(dt[k].getTester());
- cnames.push_back(dt[k].getTesterName());
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(unres_types[i]);
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ cnames.back().push_back(dt[k].getTesterName());
+ cargs.back().push_back(std::vector<Type>());
+ cargs.back().back().push_back(unres_types[i]);
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
}
}
}
}
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops.back().push_back(nm->operatorOf(k).toExpr());
- cnames.push_back(kindToString(k));
- cargs.push_back(std::vector<CVC4::Type>());
- cargs.back().push_back(unres_bt);
+ cnames.back().push_back(kindToString(k));
+ cargs.back().push_back(std::vector<Type>());
+ cargs.back().back().push_back(unres_bt);
if (k != NOT)
{
- cargs.back().push_back(unres_bt);
+ cargs.back().back().push_back(unres_bt);
if (k == ITE)
{
- cargs.back().push_back(unres_bt);
+ cargs.back().back().push_back(unres_bt);
}
}
- pcs.push_back(nullptr);
- weights.push_back(-1);
+ pcs.back().push_back(nullptr);
+ weights.back().push_back(-1);
}
}
if( range==btype ){
}
Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl;
datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true );
- for( unsigned j=0; j<ops.back().size(); j++ ){
- datatypes.back().addSygusConstructor(
- ops.back()[j], cnames[j], cargs[j], pcs[j], weights[j]);
+ for (unsigned i = 0, size = ops.back().size(); i < size; ++i)
+ {
+ datatypes.back().addSygusConstructor(ops.back()[i],
+ cnames.back()[i],
+ cargs.back()[i],
+ pcs.back()[i],
+ weights.back()[i]);
}
- //sorts.push_back( btype );
+ Trace("sygus-grammar-def") << "...built datatype " << datatypes.back() << " ";
Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl;
-
+ // make first datatype be the top level datatype
if( startIndex>0 ){
- CVC4::Datatype tmp_dt = datatypes[0];
+ Datatype tmp_dt = datatypes[0];
datatypes[0] = datatypes[startIndex];
datatypes[startIndex] = tmp_dt;
}
projects / cvc5.git / commitdiff