From 2679806e54a0b265fae26eb9cf76a5f6a618e963 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 11 May 2015 11:41:48 +0200 Subject: Support for arbitrary constants/variables in Sygus grammars. --- src/parser/smt2/Smt2.g | 108 ++++++++++++++++++++++++++++++++++++----------- src/parser/smt2/smt2.cpp | 17 +++++++- src/parser/smt2/smt2.h | 2 + 3 files changed, 101 insertions(+), 26 deletions(-) (limited to 'src/parser') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c7c82b2d8..57ef44df0 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -488,6 +488,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] Type t, range; std::vector terms; std::vector sorts; + std::vector sygus_vars; std::vector > sortedVarNames; SExpr sexpr; CommandSequence* seq; @@ -495,6 +496,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::vector< std::vector > ops; std::vector< std::vector< std::string > > cnames; std::vector< std::vector< std::vector< CVC4::Type > > > cargs; + bool allow_const; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] @@ -584,7 +586,9 @@ sygusCommand returns [CVC4::Command* cmd = NULL] sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { - terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); + Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); + terms.push_back( v ); + sygus_vars.push_back( v ); } Expr bvl; if( !terms.empty() ){ @@ -603,7 +607,6 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::string dname = ss.str(); sorts.push_back(t); datatypes.push_back(Datatype(dname)); - datatypes.back().setSygus( t, terms[0] ); ops.push_back(std::vector()); cnames.push_back(std::vector()); cargs.push_back(std::vector >()); @@ -611,12 +614,14 @@ sygusCommand returns [CVC4::Command* cmd = NULL] // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); } + allow_const = false; } // Note the official spec for NTDef is missing the ( parens ) // but they are necessary to parse SyGuS examples - LPAREN_TOK sygusGTerm[fun, ops.back(), cnames.back(), cargs.back()]+ RPAREN_TOK + LPAREN_TOK sygusGTerm[fun, ops.back(), cnames.back(), cargs.back(), sygus_vars, allow_const]+ RPAREN_TOK RPAREN_TOK - { PARSER_STATE->mkSygusDatatype( datatypes.back(), ops.back(), cnames.back(), cargs.back() ); + { datatypes.back().setSygus( t, terms[0], allow_const ); + PARSER_STATE->mkSygusDatatype( datatypes.back(), ops.back(), cnames.back(), cargs.back() ); PARSER_STATE->popScope(); } )+ RPAREN_TOK @@ -705,7 +710,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL] // SyGuS grammar term // fun is the name of the synth-fun this grammar term is for -sygusGTerm[std::string& fun, std::vector& ops, std::vector& cnames, std::vector< std::vector< CVC4::Type > >& cargs] +// this adds N operators to ops, N names to cnames and N type argument vectors to cargs (where typically N=1) +sygusGTerm[std::string& fun, std::vector& ops, std::vector& cnames, + std::vector< std::vector< CVC4::Type > >& cargs, std::vector& sygus_vars, + bool& allow_const] @declarations { std::string name; Kind k; @@ -713,6 +721,8 @@ sygusGTerm[std::string& fun, std::vector& ops, std::vector& ops, std::vectorisOperatorEnabled(name); - if(isBuiltinOperator) { - Kind k = PARSER_STATE->getOperatorKind(name); - if( k==CVC4::kind::BITVECTOR_UDIV ){ - k = CVC4::kind::BITVECTOR_UDIV_TOTAL; - } - ops.push_back(EXPR_MANAGER->operatorOf(k)); - name = kind::kindToString(k); + if(name=="Constant"){ + gtermType = 1; + Debug("parser-sygus") << "Sygus grammar constant." << std::endl; + }else if(name=="Variable"){ + gtermType = 2; + allow_const = true; + Debug("parser-sygus") << "Sygus grammar variable." << std::endl; }else{ - // what is this sygus term trying to accomplish here, if the - // symbol isn't yet declared?! probably the following line will - // 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) ){ - PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); + bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name); + if(isBuiltinOperator) { + Kind k = PARSER_STATE->getOperatorKind(name); + if( k==CVC4::kind::BITVECTOR_UDIV ){ + k = CVC4::kind::BITVECTOR_UDIV_TOTAL; + } + ops.push_back(EXPR_MANAGER->operatorOf(k)); + name = kind::kindToString(k); + }else{ + // what is this sygus term trying to accomplish here, if the + // symbol isn't yet declared?! probably the following line will + // 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) ){ + PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); + } + ops.push_back( PARSER_STATE->getVariable(name) ); } - ops.push_back( PARSER_STATE->getVariable(name) ); } } ) - { cnames.push_back( name ); + { if( gtermType==0 ){ + cnames.push_back( name ); + } cargs.push_back( std::vector< CVC4::Type >() ); } ( //sortSymbol[t,CHECK_NONE] symbol[sname,CHECK_NONE,SYM_VARIABLE] - { std::stringstream ss; - ss << fun << "_" << sname; - sname = ss.str(); + { + if( gtermType==0 ){ + std::stringstream ss; + ss << fun << "_" << sname; + sname = ss.str(); + } if( PARSER_STATE->isDeclared(sname, SYM_SORT) ) { t = PARSER_STATE->getSort(sname); } else { @@ -761,6 +785,40 @@ sygusGTerm[std::string& fun, std::vector& ops, std::vectorparseError(std::string("Must provide single sort for constant/variable Sygus constructor.")); + } + Type t = cargs.back()[0]; + cargs.pop_back(); + Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << std::endl; + if( gtermType==1 ){ + //PARSER_STATE->parseError(std::string("Constant/Variable in sygus not supported.")); + std::vector< Expr > consts; + PARSER_STATE->mkSygusConstantsForType( t, consts ); + for( unsigned i=0; i() ); + } + }else if( gtermType==2 ){ + for( unsigned i=0; i() ); + } + } + } + } + } | INTEGER_LITERAL { Debug("parser-sygus") << "Sygus grammar " << fun << " : integer literal " << AntlrInput::tokenText($INTEGER_LITERAL) << std::endl; ops.push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL)))); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index bf0e57eca..10e742d45 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -21,6 +21,8 @@ #include "parser/smt2/smt2.h" #include "parser/antlr_input.h" +#include "util/bitvector.h" + // ANTLR defines these, which is really bad! #undef true #undef false @@ -495,8 +497,21 @@ void Smt2::includeFile(const std::string& filename) { } +void Smt2::mkSygusConstantsForType( const Type& type, std::vector& ops ) { + if( type.isInteger() ){ + ops.push_back(getExprManager()->mkConst(Rational(0))); + ops.push_back(getExprManager()->mkConst(Rational(1))); + }else if( type.isBitVector() ){ + unsigned sz = ((BitVectorType)type).getSize(); + BitVector bval0(sz, (unsigned int)0); + ops.push_back( getExprManager()->mkConst(bval0) ); + BitVector bval1(sz, (unsigned int)1); + ops.push_back( getExprManager()->mkConst(bval1) ); + } + //TODO : others? +} - void Smt2::defineSygusFuns() { +void Smt2::defineSygusFuns() { // only define each one once while(d_nextSygusFun < d_sygusFuns.size()) { std::pair p = d_sygusFuns[d_nextSygusFun]; diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index ed6a5128b..67c019d50 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -178,6 +178,8 @@ public: return e; } + void mkSygusConstantsForType( const Type& type, std::vector& ops ); + void addSygusFun(const std::string& fun, Expr eval) { d_sygusFuns.push_back(std::make_pair(fun, eval)); } -- cgit v1.2.3