diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-11 16:05:55 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-11 16:05:55 +0200 |
commit | 711c63d026ce7d98724fe945eaf30077f0dad28d (patch) | |
tree | 385efd6d138f51cef5340952f85bc1279ddd379f /src/parser | |
parent | f1f79835adeac5c22fb744c38a83fef01d0002ad (diff) |
Handle duplicate operators in sygus grammars. Parse sygus quoted literals. Add regression.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 21 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 71 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 3 |
3 files changed, 69 insertions, 26 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 0f020c36e..ffa2994fc 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -509,13 +509,14 @@ sygusCommand returns [CVC4::Command* cmd = NULL] { PARSER_STATE->setLogic(name); $cmd = new SetBenchmarkLogicCommand("ALL_SUPPORTED"); } | /* set-options */ - SET_OPTIONS_TOK LPAREN_TOK { seq = new CommandSequence(); } - ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] symbolicExpr[sexpr] RPAREN_TOK - { PARSER_STATE->setOption(name.c_str(), sexpr); - seq->addCommand(new SetOptionCommand(name.c_str() + 1, sexpr)); + SET_OPTIONS_TOK LPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] SYGUS_QUOTED_LITERAL RPAREN_TOK + { //TODO? + //PARSER_STATE->setOption(name.c_str(), sexpr); + //seq->addCommand(new SetOptionCommand(name.c_str() + 1, sexpr)); } )+ RPAREN_TOK - { $cmd = seq; } + { $cmd = new EmptyCommand(); } | /* sort definition */ DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_SORT] @@ -644,7 +645,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] 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 ); - PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i] ); + PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i], sygus_to_builtin ); } } PARSER_STATE->popScope(); @@ -2801,6 +2802,14 @@ STRING_LITERAL_2_5 ; /** + * Matches sygus quoted literal + */ +SYGUS_QUOTED_LITERAL + : { PARSER_STATE->sygus() }?=> + '"' (ALPHA|DIGIT)* '"' + ; + +/** * Matches the comments and ignores them */ COMMENT diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ceab0a779..17bedf115 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -500,6 +500,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars ) { Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl; + std::map< CVC4::Type, CVC4::Type > sygus_to_builtin; std::stringstream ssb; ssb << fun << "_Bool"; @@ -562,7 +563,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin } Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; datatypes.back().setSygus( range, bvl, true, true ); - mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym ); + mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin ); sorts.push_back( range ); //Boolean type @@ -598,7 +599,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; Type btype = getExprManager()->booleanType(); datatypes.back().setSygus( btype, bvl, true, true ); - mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym ); + mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin ); sorts.push_back( btype ); Debug("parser-sygus") << "...finished make default grammar for " << fun << " " << range << std::endl; @@ -882,29 +883,32 @@ void Smt2::defineSygusFuns() { 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::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") << " add constructors..." << std::endl; for( int i=0; i<(int)cnames.size(); i++ ){ bool is_dup = false; - //FIXME : should allow multiple operators with different sygus type arguments - // for now, just ignore them (introduces incompleteness). + bool is_dup_op = false; + Expr let_body; + std::vector< Expr > let_args; + unsigned let_num_input_args = 0; for( int j=0; j<i; j++ ){ if( ops[i]==ops[j] ){ - is_dup = true; - break; - } - /* - if( ops[i]==ops[j] && cargs[i].size()==cargs[j].size() ){ - is_dup = true; - for( unsigned k=0; k<cargs[i].size(); k++ ){ - if( cargs[i][k]!=cargs[j][k] ){ - is_dup = false; - break; + is_dup_op = true; + if( cargs[i].size()==cargs[j].size() ){ + is_dup = true; + for( unsigned k=0; k<cargs[i].size(); k++ ){ + if( cargs[i][k]!=cargs[j][k] ){ + is_dup = false; + break; + } } } + if( is_dup ){ + break; + } } - */ } if( is_dup ){ Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << " at " << i << std::endl; @@ -912,10 +916,39 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 ); cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 ); i--; + }else if( is_dup_op ){ + Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] << " at " << i << std::endl; + //make into define-fun + std::vector<CVC4::Type> fsorts; + 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; + Expr v = mkBoundVar(ss.str(), bt); + let_args.push_back( v ); + fsorts.push_back( bt ); + } + //make the let_body + std::vector< Expr > children; + if( ops[i].getKind() != kind::BUILTIN ){ + children.push_back( ops[i] ); + } + children.insert( children.end(), let_args.begin(), let_args.end() ); + Kind sk = ops[i].getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(ops[i]); + Debug("parser-sygus") << ": replace " << ops[i] << " " << ops[i].getKind() << " " << sk << std::endl; + let_body = getExprManager()->mkExpr( sk, children ); + Debug("parser-sygus") << ": new body of function is " << let_body << std::endl; + + 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; + //replace operator and name + ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); + cnames[i] = ss.str(); + 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{ - Expr let_body; - std::vector< Expr > let_args; - unsigned let_num_input_args = 0; std::map< CVC4::Expr, CVC4::Expr >::iterator it = d_sygus_let_func_to_body.find( ops[i] ); if( it!=d_sygus_let_func_to_body.end() ){ let_body = it->second; diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index cfd062457..275c8a83a 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -230,7 +230,8 @@ 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 // j is index is datatype |