From 711c63d026ce7d98724fe945eaf30077f0dad28d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 11 Jun 2015 16:05:55 +0200 Subject: [PATCH] Handle duplicate operators in sygus grammars. Parse sygus quoted literals. Add regression. --- src/parser/smt2/Smt2.g | 21 +++++--- src/parser/smt2/smt2.cpp | 71 ++++++++++++++++++------- src/parser/smt2/smt2.h | 3 +- test/regress/regress0/sygus/Makefile.am | 3 +- 4 files changed, 71 insertions(+), 27 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(); @@ -2800,6 +2801,14 @@ STRING_LITERAL_2_5 '"' (~('"') | '""')* '"' ; +/** + * Matches sygus quoted literal + */ +SYGUS_QUOTED_LITERAL + : { PARSER_STATE->sygus() }?=> + '"' (ALPHA|DIGIT)* '"' + ; + /** * Matches the comments and ignores them */ 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& sorts, std::vector< std::vector >& ops, std::vector 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& ops, std::vector& cnames, std::vector< std::vector< CVC4::Type > >& cargs, - std::vector& unresolved_gterm_sym ) { + std::vector& 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 Duplicate gterm : " << ops[i] << " at " << i << std::endl; @@ -912,10 +916,39 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& 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 fsorts; + for( unsigned j=0; j 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& ops, std::vector& cnames, std::vector< std::vector< CVC4::Type > >& cargs, - std::vector& unresolved_gterm_sym ); + std::vector& unresolved_gterm_sym, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ); // i is index in datatypes/ops // j is index is datatype diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index abf51d992..50f755fef 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -36,7 +36,8 @@ TESTS = commutative.sy \ twolets2-orig.sy \ let-ringer.sy \ let-simp.sy \ - tl-type.sy + tl-type.sy \ + dup-op.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ -- 2.30.2