diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-01 13:20:49 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-01 13:20:49 -0500 |
commit | 8e0fce94790249ff7aff84ff4500bb96e2ebb9e9 (patch) | |
tree | 25e65718cff712f13688e452ffc1d4b459cd7367 /src/parser | |
parent | 3506b13f4d298095e8405b32b05e838f17dbe809 (diff) |
Working memory leak free version, changes interface to pointers.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 14 | ||||
-rw-r--r-- | src/parser/parser.cpp | 8 | ||||
-rw-r--r-- | src/parser/parser.h | 3 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 29 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 60 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 18 |
6 files changed, 66 insertions, 66 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index e6d7f9d86..7ca6beb60 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -708,7 +708,7 @@ mainCommand[CVC4::Command*& cmd] SExpr sexpr; std::string id; Type t; - std::vector<CVC4::Datatype> dts; + std::vector<CVC4::Datatype*> dts; Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl; std::string s; } @@ -769,7 +769,9 @@ mainCommand[CVC4::Command*& cmd] ( COMMA datatypeDef[dts] )* END_TOK { PARSER_STATE->popScope(); - cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + std::vector<DatatypeType> dtts; + PARSER_STATE->mkMutualDatatypeTypes(dts, dtts); + cmd = new DatatypeDeclarationCommand(dtts); } | CONTEXT_TOK ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) @@ -2173,7 +2175,7 @@ iteElseTerm[CVC4::Expr& f] /** * Parses a datatype definition */ -datatypeDef[std::vector<CVC4::Datatype>& datatypes] +datatypeDef[std::vector<CVC4::Datatype*>& datatypes] @init { std::string id, id2; Type t; @@ -2193,7 +2195,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes] params.push_back( t ); } )* RBRACKET )? - { datatypes.push_back(Datatype(id, params, false)); + { datatypes.push_back(new Datatype(id, params, false)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); @@ -2207,7 +2209,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes] /** * Parses a constructor defintion for type */ -constructorDef[CVC4::Datatype& type] +constructorDef[CVC4::Datatype*& type] @init { std::string id; CVC4::DatatypeConstructor* ctor = NULL; @@ -2225,7 +2227,7 @@ constructorDef[CVC4::Datatype& type] RPAREN )? { // make the constructor - type.addConstructor(*ctor); + type->addConstructor(*ctor); Debug("parser-idt") << "constructor: " << id.c_str() << std::endl; delete ctor; } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 712494805..e46c13140 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -303,12 +303,10 @@ bool Parser::isUnresolvedType(const std::string& name) { return d_unresolved.find(getSort(name)) != d_unresolved.end(); } -std::vector<DatatypeType> -Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { +void Parser::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& types) { try { - std::vector<DatatypeType> types = - d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); + d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved, types); assert(datatypes.size() == types.size()); @@ -373,8 +371,6 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { throw ParserException(dt.getName() + " is not well-founded"); } } - - return types; } catch(IllegalArgumentException& ie) { throw ParserException(ie.getMessage()); } diff --git a/src/parser/parser.h b/src/parser/parser.h index 54f25ae74..52f8dcb86 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -501,8 +501,7 @@ public: /** * Create sorts of mutually-recursive datatypes. */ - std::vector<DatatypeType> - mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes); + void mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts); /** * Add an operator to the current legal set. diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f88b30212..0fbd454b4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -512,7 +512,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] SExpr sexpr; CommandSequence* seq; std::vector< std::vector< CVC4::SygusGTerm > > sgts; - std::vector< CVC4::Datatype > datatypes; + std::vector< CVC4::Datatype* > datatypes; std::vector< std::vector<Expr> > ops; std::vector< std::vector< std::string > > cnames; std::vector< std::vector< std::vector< CVC4::Type > > > cargs; @@ -621,14 +621,14 @@ sygusCommand returns [CVC4::Command* cmd = NULL] //swap index if necessary Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl; for( unsigned i=0; i<datatypes.size(); i++ ){ - Debug("parser-sygus") << "..." << datatypes[i].getName() << " has builtin sort " << sorts[i] << std::endl; + Debug("parser-sygus") << "..." << datatypes[i]->getName() << " has builtin sort " << sorts[i] << std::endl; } for( unsigned i=0; i<datatypes.size(); i++ ){ - Debug("parser-sygus") << "...make " << datatypes[i].getName() << " with builtin sort " << sorts[i] << std::endl; + Debug("parser-sygus") << "...make " << datatypes[i]->getName() << " with builtin sort " << sorts[i] << std::endl; if( sorts[i].isNull() ){ PARSER_STATE->parseError(std::string("Internal error : could not infer builtin sort for nested gterm.")); } - datatypes[i].setSygus( sorts[i], terms[0], allow_const[i], false ); + datatypes[i]->setSygus( sorts[i], terms[0], allow_const[i], false ); PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i], sygus_to_builtin ); } PARSER_STATE->setSygusStartIndex( fun, startIndex, datatypes, sorts, ops ); @@ -637,10 +637,11 @@ sygusCommand returns [CVC4::Command* cmd = NULL] PARSER_STATE->popScope(); Debug("parser-sygus") << "--- Make " << datatypes.size() << " mutual datatypes..." << std::endl; for( unsigned i=0; i<datatypes.size(); i++ ){ - Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName() << std::endl; + Debug("parser-sygus") << " " << i << " : " << datatypes[i]->getName() << std::endl; } seq = new CommandSequence(); - std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes); + std::vector<DatatypeType> datatypeTypes; + PARSER_STATE->mkMutualDatatypeTypes(datatypes, datatypeTypes); seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes)); std::map<DatatypeType, Expr> evals; if( sorts[0]!=range ){ @@ -1168,7 +1169,7 @@ smt25Command[CVC4::Command*& cmd] extendedCommand[CVC4::Command*& cmd] @declarations { - std::vector<CVC4::Datatype> dts; + std::vector<CVC4::Datatype*> dts; Expr e, e2; Type t; std::string name; @@ -1324,7 +1325,8 @@ extendedCommand[CVC4::Command*& cmd] datatypesDefCommand[bool isCo, CVC4::Command*& cmd] @declarations { - std::vector<CVC4::Datatype> dts; + std::vector<CVC4::Datatype*> dts; + std::vector<CVC4::DatatypeType> dtts; std::string name; std::vector<Type> sorts; } @@ -1338,7 +1340,8 @@ datatypesDefCommand[bool isCo, CVC4::Command*& cmd] RPAREN_TOK LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK { PARSER_STATE->popScope(); - cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + PARSER_STATE->mkMutualDatatypeTypes(dts, dtts); + cmd = new DatatypeDeclarationCommand(dtts); } ; rewriterulesCommand[CVC4::Command*& cmd] @@ -2472,7 +2475,7 @@ nonemptyNumeralList[std::vector<uint64_t>& numerals] /** * Parses a datatype definition */ -datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& params] +datatypeDef[bool isCo, std::vector<CVC4::Datatype*>& datatypes, std::vector< CVC4::Type >& params] @init { std::string id; } @@ -2490,7 +2493,7 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4 params.push_back( t ); } )* ']' )?*/ //AJR: this isn't necessary if we use z3's style - { datatypes.push_back(Datatype(id,params,isCo)); + { datatypes.push_back(new Datatype(id,params,isCo)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); @@ -2503,7 +2506,7 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4 /** * Parses a constructor defintion for type */ -constructorDef[CVC4::Datatype& type] +constructorDef[CVC4::Datatype*& type] @init { std::string id; CVC4::DatatypeConstructor* ctor = NULL; @@ -2517,7 +2520,7 @@ constructorDef[CVC4::Datatype& type] } ( LPAREN_TOK selector[*ctor] RPAREN_TOK )* { // make the constructor - type.addConstructor(*ctor); + type->addConstructor(*ctor); Debug("parser-idt") << "constructor: " << id.c_str() << std::endl; delete ctor; } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 8db344f92..dd48ceca7 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -563,7 +563,7 @@ void collectSygusGrammarTypesFor( Type range, std::vector< Type >& types, std::m } } -void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes, +void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector< CVC4::Datatype* >& datatypes, std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ) { //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){ @@ -594,7 +594,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin std::stringstream ss; ss << fun << "_" << types[i]; std::string dname = ss.str(); - datatypes.push_back(Datatype(dname)); + datatypes.push_back(new Datatype(dname)); ops.push_back(std::vector<Expr>()); //make unresolved type Type unres_t = mkUnresolvedType(dname); @@ -683,7 +683,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin } } Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; - datatypes[i].setSygus( types[i], bvl, true, true ); + datatypes[i]->setSygus( types[i], bvl, true, true ); mkSygusDatatype( datatypes[i], ops[i], cnames, cargs, unresolved_gterm_sym, sygus_to_builtin ); sorts.push_back( types[i] ); //set start index if applicable @@ -694,12 +694,12 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin //make Boolean type Type btype = getExprManager()->booleanType(); - datatypes.push_back(Datatype(dbname)); + datatypes.push_back(new Datatype(dbname)); ops.push_back(std::vector<Expr>()); std::vector<std::string> cnames; std::vector<std::vector<CVC4::Type> > cargs; std::vector<std::string> unresolved_gterm_sym; - Debug("parser-sygus") << "Make grammar for " << btype << " " << datatypes.back() << std::endl; + Debug("parser-sygus") << "Make grammar for " << btype << " " << *(datatypes.back()) << std::endl; //add variables for( unsigned i=0; i<sygus_vars.size(); i++ ){ if( sygus_vars[i].getType().isBoolean() ){ @@ -776,8 +776,8 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin if( range==btype ){ startIndex = sorts.size(); } - Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; - datatypes.back().setSygus( btype, bvl, true, true ); + Debug("parser-sygus") << "...make datatype " << *(datatypes.back()) << std::endl; + datatypes.back()->setSygus( btype, bvl, true, true ); mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin ); sorts.push_back( btype ); @@ -804,7 +804,7 @@ void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& o // This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1) // This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms. void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, - std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, @@ -848,7 +848,7 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, cargs[index].push_back( std::vector< CVC4::Type >() ); for( unsigned i=0; i<sgt.d_children.size(); i++ ){ std::stringstream ss; - ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i; + ss << datatypes[index]->getName() << "_" << ops[index].size() << "_arg_" << i; std::string sub_dname = ss.str(); //add datatype for child Type null_type; @@ -921,7 +921,7 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, } bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname, - std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, @@ -929,7 +929,7 @@ bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname, std::vector< bool >& allow_const, std::vector< std::vector< std::string > >& unresolved_gterm_sym ){ sorts.push_back(t); - datatypes.push_back(Datatype(dname)); + datatypes.push_back(new Datatype(dname)); ops.push_back(std::vector<Expr>()); cnames.push_back(std::vector<std::string>()); cargs.push_back(std::vector<std::vector<CVC4::Type> >()); @@ -938,7 +938,7 @@ bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname, return true; } -bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes, +bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, @@ -955,7 +955,7 @@ bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes, return true; } -Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes, +Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, @@ -1024,7 +1024,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st sygus_to_builtin[t] = curr_t; }else{ Debug("parser-sygus") << "simple argument " << t << std::endl; - Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl; + Debug("parser-sygus") << "...removing " << datatypes.back()->getName() << std::endl; //otherwise, datatype was unecessary //pop argument datatype definition popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); @@ -1034,7 +1034,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index, - std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, @@ -1045,7 +1045,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, std::vector< CVC4::Expr > let_define_args; Expr let_body; int dindex = cargs[index].size()-1; - Debug("parser-sygus") << "Process let constructor for datatype " << datatypes[index].getName() << ", #subtypes = " << cargs[index][dindex].size() << std::endl; + Debug("parser-sygus") << "Process let constructor for datatype " << datatypes[index]->getName() << ", #subtypes = " << cargs[index][dindex].size() << std::endl; for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){ Debug("parser-sygus") << " " << i << " : " << cargs[index][dindex][i] << std::endl; if( i+1==cargs[index][dindex].size() ){ @@ -1054,7 +1054,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, let_body = it->second; }else{ std::stringstream ss; - ss << datatypes[index].getName() << "_body"; + ss << datatypes[index]->getName() << "_body"; let_body = mkBoundVar(ss.str(), sygus_to_builtin[cargs[index][dindex][i]]); d_sygus_bound_var_type[let_body] = cargs[index][dindex][i]; } @@ -1094,7 +1094,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType()); std::stringstream ss; - ss << datatypes[index].getName() << "_let"; + ss << datatypes[index]->getName() << "_let"; Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); d_sygus_defined_funs.push_back( let_func ); preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) ); @@ -1130,11 +1130,11 @@ void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusAr } void Smt2::setSygusStartIndex( std::string& fun, int startIndex, - std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops ) { if( startIndex>0 ){ - CVC4::Datatype tmp_dt = datatypes[0]; + CVC4::Datatype* tmp_dt = datatypes[0]; Type tmp_sort = sorts[0]; std::vector< Expr > tmp_ops; tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() ); @@ -1218,11 +1218,11 @@ void Smt2::defineSygusFuns() { } } -void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, +void Smt2::mkSygusDatatype( CVC4::Datatype* dt, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs, std::vector<std::string>& unresolved_gterm_sym, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) { - Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl; + Debug("parser-sygus") << "Making sygus datatype " << dt->getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; for( int i=0; i<(int)cnames.size(); i++ ){ bool is_dup = false; @@ -1260,7 +1260,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, for( unsigned j=0; j<cargs[i].size(); j++ ){ Type bt = sygus_to_builtin[cargs[i][j]]; std::stringstream ss; - ss << dt.getName() << "_x_" << i << "_" << j; + ss << dt->getName() << "_x_" << i << "_" << j; Expr v = mkBoundVar(ss.str(), bt); let_args.push_back( v ); fsorts.push_back( bt ); @@ -1280,7 +1280,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType()); Debug("parser-sygus") << ": function type is " << ft << std::endl; std::stringstream ss; - ss << dt.getName() << "_df_" << i; + ss << dt->getName() << "_df_" << i; //replace operator and name ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); cnames[i] = ss.str(); @@ -1309,7 +1309,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, if( std::find( types.begin(), types.end(), t )==types.end() ){ types.push_back( t ); //identity element - Type bt = dt.getSygusType(); + Type bt = dt->getSygusType(); Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl; std::stringstream ss; ss << t << "_x_id"; @@ -1338,19 +1338,19 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, } -void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, +void Smt2::addSygusDatatypeConstructor( CVC4::Datatype* dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) { - Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt.getName() << std::endl; + Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt->getName() << std::endl; if( !let_body.isNull() ){ Debug("parser-sygus") << " let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl; //TODO : remove arguments not occurring in body //if this is a self identity function, ignore if( let_args.size()==0 && let_args[0]==let_body ){ - Debug("parser-sygus") << " identity function " << cargs[0] << " to " << dt.getName() << std::endl; + Debug("parser-sygus") << " identity function " << cargs[0] << " to " << dt->getName() << std::endl; //TODO } } - std::string name = dt.getName() + "_" + cname; + std::string name = dt->getName() + "_" + cname; std::string testerId("is-"); testerId.append(name); checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); @@ -1363,7 +1363,7 @@ void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std:: sname << name << "_" << j; c.addArg(sname.str(), cargs[j]); } - dt.addConstructor(c); + dt->addConstructor(c); } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index b99e142ba..ac4be9bee 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -173,13 +173,13 @@ public: Expr mkSygusVar(const std::string& name, const Type& type, bool isPrimed = false); - void mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes, + void mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector< CVC4::Datatype* >& datatypes, std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ); void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ); void processSygusGTerm( CVC4::SygusGTerm& sgt, int index, - std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, @@ -191,7 +191,7 @@ public: CVC4::Type& ret, bool isNested = false ); static bool pushSygusDatatypeDef( Type t, std::string& dname, - std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, @@ -199,7 +199,7 @@ public: std::vector< bool >& allow_const, std::vector< std::vector< std::string > >& unresolved_gterm_sym ); - static bool popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes, + static bool popSygusDatatypeDef( std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, @@ -208,7 +208,7 @@ public: std::vector< std::vector< std::string > >& unresolved_gterm_sym ); void setSygusStartIndex( std::string& fun, int startIndex, - std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops ); @@ -218,7 +218,7 @@ public: void defineSygusFuns(); - void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, + void mkSygusDatatype( CVC4::Datatype* dt, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs, std::vector<std::string>& unresolved_gterm_sym, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ); @@ -314,10 +314,10 @@ private: void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ); - void addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, + void addSygusDatatypeConstructor( CVC4::Datatype* dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ); - Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes, + Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, @@ -328,7 +328,7 @@ private: std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ); void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index, - std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Datatype* >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, |