diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-31 10:32:34 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-31 10:32:34 +0200 |
commit | bf7f7d6960f6e03e90880dd3da9ff1bf00943cf3 (patch) | |
tree | 87630123b624ea6ca98bb85d8cc3e99ca75edc01 /src/parser | |
parent | f2da7296ff76920528c0e9edc35f96a715b85078 (diff) |
Sygus support for inductive datatypes.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 39 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 32 |
3 files changed, 53 insertions, 22 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 1564e6f3e..1ce7c4aff 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -606,6 +606,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); $cmd = new DefineFunctionCommand(name, func, terms, expr); } + | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] + | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] | /* synth-fun */ ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } ) { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] @@ -912,7 +914,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] // fail, but we need an operator to continue here.. Debug("parser-sygus") << "Sygus grammar " << fun; Debug("parser-sygus") << " : op (declare=" << PARSER_STATE->isDeclared(name) << ", define=" << PARSER_STATE->isDefinedFunction(name) << ") : " << name << std::endl; - if( !PARSER_STATE->isDefinedFunction(name) ){ + if( !PARSER_STATE->isDeclared(name) && !PARSER_STATE->isDefinedFunction(name) ){ PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); } sgt.d_name = name; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 9ee6d24b4..0500c9316 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -522,9 +522,13 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin for( unsigned i=0; i<sygus_vars.size(); i++ ){ Type t = sygus_vars[i].getType(); if( !t.isBoolean() && std::find( types.begin(), types.end(), t )==types.end() ){ + Debug("parser-sygus") << "...will make grammar for " << t << std::endl; types.push_back( t ); } } + if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() ){ + parseError("No default grammar for type."); + } //name of boolean sort std::stringstream ssb; @@ -993,6 +997,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, std::stringstream ss; 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) ); ops[index].pop_back(); @@ -1180,6 +1185,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, //replace operator and name ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); cnames[i] = ss.str(); + d_sygus_defined_funs.push_back( ops[i] ); preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) ); addSygusDatatypeConstructor( dt, ops[i], cnames[i], cargs[i], let_body, let_args, 0 ); }else{ @@ -1216,6 +1222,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, std::stringstream ssid; ssid << unresolved_gterm_sym[i] << "_id"; Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); + d_sygus_defined_funs.push_back( id_op ); preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) ); //make the sygus argument list std::vector< Type > id_carg; @@ -1310,15 +1317,35 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec for(size_t k = 0; k < builtApply.size(); ++k) { } Expr builtTerm; - //if( ops[i][j].getKind() == kind::BUILTIN ){ - if( !builtApply.empty() ){ - if( ops[i][j].getKind() != kind::BUILTIN ){ - builtTerm = getExprManager()->mkExpr(kind::APPLY, ops[i][j], builtApply); + Debug("parser-sygus") << "...operator is : " << ops[i][j] << ", type = " << ops[i][j].getType() << ", kind = " << ops[i][j].getKind() << ", is defined = " << isDefinedFunction( ops[i][j] ) << std::endl; + if( ops[i][j].getKind() != kind::BUILTIN ){ + Kind ok = kind::UNDEFINED_KIND; + if( isDefinedFunction( ops[i][j] ) || std::find( d_sygus_defined_funs.begin(), d_sygus_defined_funs.end(), ops[i][j] )!=d_sygus_defined_funs.end() ){ + ok = kind::APPLY; }else{ - builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); + Type t = ops[i][j].getType(); + if( t.isConstructor() ){ + ok = kind::APPLY_CONSTRUCTOR; + }else if( t.isSelector() ){ + ok = kind::APPLY_SELECTOR; + }else if( t.isTester() ){ + ok = kind::APPLY_TESTER; + }else{ + ok = getExprManager()->operatorToKind( ops[i][j] ); + } + } + Debug("parser-sygus") << "...processed operator kind : " << ok << std::endl; + if( ok!=kind::UNDEFINED_KIND ){ + builtTerm = getExprManager()->mkExpr(ok, ops[i][j], builtApply); + }else{ + builtTerm = ops[i][j]; } }else{ - builtTerm = ops[i][j]; + if( !builtApply.empty() ){ + builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); + }else{ + builtTerm = ops[i][j]; + } } Debug("parser-sygus") << "...made built term " << builtTerm << std::endl; Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index c88f7cd8f..c8b89799c 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -35,7 +35,7 @@ namespace CVC4 { class SExpr; namespace parser { - + class Smt2 : public Parser { friend class ParserBuilder; @@ -180,7 +180,7 @@ public: void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ); - void processSygusGTerm( CVC4::SygusGTerm& sgt, int index, + void processSygusGTerm( CVC4::SygusGTerm& sgt, int index, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, @@ -188,10 +188,10 @@ public: std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, std::vector< bool >& allow_const, std::vector< std::vector< std::string > >& unresolved_gterm_sym, - std::vector<CVC4::Expr>& sygus_vars, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, + std::vector<CVC4::Expr>& sygus_vars, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, CVC4::Type& ret, bool isNested = false ); - + static bool pushSygusDatatypeDef( Type t, std::string& dname, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, @@ -208,12 +208,12 @@ public: std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, std::vector< bool >& allow_const, std::vector< std::vector< std::string > >& unresolved_gterm_sym ); - - void setSygusStartIndex( std::string& fun, int startIndex, + + void setSygusStartIndex( std::string& fun, int startIndex, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops ); - + void addSygusFun(const std::string& fun, Expr eval) { d_sygusFuns.push_back(std::make_pair(fun, eval)); } @@ -222,7 +222,7 @@ public: 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::vector<std::string>& unresolved_gterm_sym, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ); // i is index in datatypes/ops @@ -230,7 +230,7 @@ public: Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops, std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms, Expr eval, const Datatype& dt, size_t i, size_t j ); - + void addSygusConstraint(Expr constraint) { @@ -311,9 +311,11 @@ private: std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars; std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body; std::map< CVC4::Expr, unsigned > d_sygus_let_func_to_num_input_vars; - + //auxiliary define-fun functions introduced for production rules + std::vector< CVC4::Expr > d_sygus_defined_funs; + 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, CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ); @@ -327,16 +329,16 @@ private: std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ); - void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index, + void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, std::vector< std::vector<std::string> >& cnames, std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector<CVC4::Expr>& sygus_vars, + std::vector<CVC4::Expr>& sygus_vars, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ); - + void addArithmeticOperators(); void addBitvectorOperators(); |