diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-11 20:06:21 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-11 20:06:21 +0200 |
commit | 54f1d00d5475710ec5a4c3eab82d786ba95dfdde (patch) | |
tree | 547bd29a009a3d119a26b2ddcd509a3ef2e5d061 /src/parser | |
parent | 870b29b0cce85941ed72d7e0ca75b61b0cfcf711 (diff) |
Allow sygus with no syntactic restrictions for LIA. Add regressions.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 19 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 108 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 3 |
3 files changed, 122 insertions, 8 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 57ef44df0..dc00ead8c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -496,7 +496,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::vector< std::vector<Expr> > ops; std::vector< std::vector< std::string > > cnames; std::vector< std::vector< std::vector< CVC4::Type > > > cargs; - bool allow_const; + bool allow_const = false; + bool read_syntax = false; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] @@ -598,7 +599,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] terms.push_back(bvl); } sortSymbol[range,CHECK_DECLARED] - LPAREN_TOK + ( LPAREN_TOK ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->pushScope(true); } sortSymbol[t,CHECK_DECLARED] @@ -614,18 +615,23 @@ 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(), sygus_vars, allow_const]+ RPAREN_TOK RPAREN_TOK - { datatypes.back().setSygus( t, terms[0], allow_const ); + { datatypes.back().setSygus( t, terms[0], allow_const, false ); PARSER_STATE->mkSygusDatatype( datatypes.back(), ops.back(), cnames.back(), cargs.back() ); PARSER_STATE->popScope(); } )+ - RPAREN_TOK - { PARSER_STATE->popScope(); + RPAREN_TOK { read_syntax = true; } + )? + { + if( !read_syntax ){ + //create the default grammar + PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars ); + } + PARSER_STATE->popScope(); seq = new CommandSequence(); std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes); seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes)); @@ -794,7 +800,6 @@ sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::stri 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<consts.size(); i++ ){ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 10e742d45..e837980bd 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -496,7 +496,113 @@ void Smt2::includeFile(const std::string& filename) { } } - +void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes, + 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::stringstream ssb; + ssb << fun << "_Bool"; + std::string dbname = ssb.str(); + + std::stringstream ss; + ss << fun << "_" << range; + std::string dname = ss.str(); + datatypes.push_back(Datatype(dname)); + ops.push_back(std::vector<Expr>()); + std::vector<std::string> cnames; + std::vector<std::vector<CVC4::Type> > cargs; + //variables + for( unsigned i=0; i<sygus_vars.size(); i++ ){ + if( sygus_vars[i].getType()==range ){ + std::stringstream ss; + ss << sygus_vars[i]; + Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl; + ops.back().push_back( sygus_vars[i] ); + cnames.push_back( ss.str() ); + cargs.push_back( std::vector< CVC4::Type >() ); + } + } + //constants + std::vector< Expr > consts; + mkSygusConstantsForType( range, consts ); + for( unsigned i=0; i<consts.size(); i++ ){ + std::stringstream ss; + ss << consts[i]; + Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl; + ops.back().push_back( consts[i] ); + cnames.push_back( ss.str() ); + cargs.push_back( std::vector< CVC4::Type >() ); + } + //ITE + CVC4::Kind k = kind::ITE; + Debug("parser-sygus") << "...add for " << k << std::endl; + ops.back().push_back(getExprManager()->operatorOf(k)); + cnames.push_back( kind::kindToString(k) ); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(mkUnresolvedType(ssb.str())); + cargs.back().push_back(mkUnresolvedType(ss.str())); + cargs.back().push_back(mkUnresolvedType(ss.str())); + + if( range.isInteger() ){ + for( unsigned i=0; i<2; i++ ){ + CVC4::Kind k = i==0 ? kind::PLUS : kind::MINUS; + Debug("parser-sygus") << "...add for " << k << std::endl; + ops.back().push_back(getExprManager()->operatorOf(k)); + cnames.push_back(kind::kindToString(k)); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(mkUnresolvedType(ss.str())); + cargs.back().push_back(mkUnresolvedType(ss.str())); + } + }else{ + std::stringstream sserr; + sserr << "Don't know default Sygus grammar for type " << range << std::endl; + parseError(sserr.str()); + } + Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; + datatypes.back().setSygus( range, bvl, true, true ); + mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs ); + sorts.push_back( range ); + + //Boolean type + datatypes.push_back(Datatype(dbname)); + ops.push_back(std::vector<Expr>()); + cnames.clear(); + cargs.clear(); + for( unsigned i=0; i<4; i++ ){ + CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : ( i==2 ? kind::OR : kind::EQUAL ) ); + Debug("parser-sygus") << "...add for " << k << std::endl; + ops.back().push_back(getExprManager()->operatorOf(k)); + cnames.push_back(kind::kindToString(k)); + cargs.push_back( std::vector< CVC4::Type >() ); + if( k==kind::NOT ){ + cargs.back().push_back(mkUnresolvedType(ssb.str())); + }else if( k==kind::AND || k==kind::OR ){ + cargs.back().push_back(mkUnresolvedType(ssb.str())); + cargs.back().push_back(mkUnresolvedType(ssb.str())); + }else if( k==kind::EQUAL ){ + cargs.back().push_back(mkUnresolvedType(ss.str())); + cargs.back().push_back(mkUnresolvedType(ss.str())); + } + } + if( range.isInteger() ){ + CVC4::Kind k = kind::LEQ; + Debug("parser-sygus") << "...add for " << k << std::endl; + ops.back().push_back(getExprManager()->operatorOf(k)); + cnames.push_back(kind::kindToString(k)); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(mkUnresolvedType(ss.str())); + cargs.back().push_back(mkUnresolvedType(ss.str())); + } + 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 ); + sorts.push_back( btype ); + + Debug("parser-sygus") << "...finished make default grammar for " << fun << " " << range << std::endl; +} + void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) { if( type.isInteger() ){ ops.push_back(getExprManager()->mkConst(Rational(0))); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 67c019d50..eaf9e7b47 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -178,6 +178,9 @@ public: return e; } + void mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes, + std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars ); + void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ); void addSygusFun(const std::string& fun, Expr eval) { |