diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-01 13:33:38 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-01 13:33:38 -0500 |
| commit | f4c783f97201753bf63c70c5c16b7861a236d57c (patch) | |
| tree | 8e4a9e85d7485200bdfb52b5afc5032993938488 /src/parser/smt2/smt2.h | |
| parent | 8e0fce94790249ff7aff84ff4500bb96e2ebb9e9 (diff) | |
Revert change to datatypes API for passing pointers, instead make deep copy during call to mkMutualDatatypes.
Diffstat (limited to 'src/parser/smt2/smt2.h')
| -rw-r--r-- | src/parser/smt2/smt2.h | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index ac4be9bee..b99e142ba 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, |