From 2679806e54a0b265fae26eb9cf76a5f6a618e963 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 11 May 2015 11:41:48 +0200 Subject: [PATCH] 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 + src/theory/quantifiers/term_database.cpp | 20 +++-- src/util/datatype.cpp | 7 +- src/util/datatype.h | 6 +- test/regress/regress0/sygus/Makefile.am | 3 +- 7 files changed, 125 insertions(+), 38 deletions(-) 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)); } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 6c32ccb4a..62eb78679 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1586,16 +1586,18 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn ) { const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Assert( dt.isSygus() ); Node sc; - int carg = getOpArg( tn, c ); - if( carg!=-1 ){ - sc = Node::fromExpr( dt[carg].getSygusOp() ); + // if we are not interested in reconstructing constants, or the grammar allows them, return a proxy + if( !options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst() ){ + Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" ); + SygusProxyAttribute spa; + k.setAttribute(spa,c); + sc = k; }else{ - //TODO - if( !options::cegqiSingleInvReconstructConst() ){ - Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" ); - SygusProxyAttribute spa; - k.setAttribute(spa,c); - sc = k; + int carg = getOpArg( tn, c ); + if( carg!=-1 ){ + sc = Node::fromExpr( dt[carg].getSygusOp() ); + }else{ + //TODO } } d_builtin_const_to_sygus[tn][c] = sc; diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 1e310251c..18ef25e7f 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -134,11 +134,12 @@ void Datatype::addConstructor(const DatatypeConstructor& c) { } -void Datatype::setSygus( Type st, Expr bvl ){ +void Datatype::setSygus( Type st, Expr bvl, bool allow_const ){ CheckArgument(!d_resolved, this, "cannot set sygus type to a finalized Datatype"); d_sygus_type = st; d_sygus_bvl = bvl; + d_sygus_allow_const = allow_const; } @@ -470,6 +471,10 @@ Expr Datatype::getSygusVarList() const { return d_sygus_bvl; } +bool Datatype::getSygusAllowConst() const { + return d_sygus_allow_const; +} + bool Datatype::involvesExternalType() const{ return d_involvesExt; } diff --git a/src/util/datatype.h b/src/util/datatype.h index 6e7e09fa0..79e7bf7d7 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -456,6 +456,7 @@ private: /** information for sygus */ Type d_sygus_type; Expr d_sygus_bvl; + bool d_sygus_allow_const; // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache @@ -534,8 +535,9 @@ public: /** set the sygus information of this datatype * st : the builtin type for this grammar * bvl : the list of arguments for the synth-fun + * allow_const : whether all constants are (implicitly) included in the grammar */ - void setSygus( Type st, Expr bvl ); + void setSygus( Type st, Expr bvl, bool allow_const ); /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -664,6 +666,8 @@ public: Type getSygusType() const; /** get sygus var list */ Expr getSygusVarList() const; + /** does it allow constants */ + bool getSygusAllowConst() const; /** * Get whether this datatype involves an external type. If so, diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index efa656e7b..4f9d233fd 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -28,7 +28,8 @@ TESTS = commutative.sy \ twolets1.sy \ array_search_2.sy \ hd-01-d1-prog.sy \ - icfp_28_10.sy + icfp_28_10.sy \ + const-var-test.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ -- 2.30.2