diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-20 10:23:08 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-20 10:23:14 +0100 |
commit | 9e5b1fd1083c1c82d5bbc61a4a316211db629c43 (patch) | |
tree | 98c4b9d7cbe3eb52400021e17edb3bd4c97eef93 /src/parser/smt2 | |
parent | 66daf10d1bf4cb2f1846f599fe11e27312ac2069 (diff) |
Handle miniscoping of conjunctions in synthesis properties. Refactor construction of sygus datatypes. Expand define-fun in evaluators.
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 86 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 34 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 9 |
3 files changed, 66 insertions, 63 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 920803c28..d2f38cc82 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -493,6 +493,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] CommandSequence* seq; std::vector<CVC4::Datatype> datatypes; std::vector< std::vector<Expr> > ops; + std::vector< std::vector< std::string > > cnames; + std::vector< std::vector< std::vector< CVC4::Type > > > cargs; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] @@ -599,6 +601,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] sorts.push_back(t); datatypes.push_back(Datatype(dname)); ops.push_back(std::vector<Expr>()); + cnames.push_back(std::vector<std::string>()); + cargs.push_back(std::vector<std::vector<CVC4::Type> >()); if(!PARSER_STATE->isUnresolvedType(dname)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); @@ -606,9 +610,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL] } // Note the official spec for NTDef is missing the ( parens ) // but they are necessary to parse SyGuS examples - LPAREN_TOK sygusGTerm[fun, datatypes.back(), ops.back()]+ RPAREN_TOK + LPAREN_TOK sygusGTerm[fun, ops.back(), cnames.back(), cargs.back()]+ RPAREN_TOK RPAREN_TOK - { PARSER_STATE->popScope(); } + { PARSER_STATE->mkSygusDatatype( datatypes.back(), ops.back(), cnames.back(), cargs.back() ); + PARSER_STATE->popScope(); } )+ RPAREN_TOK { PARSER_STATE->popScope(); @@ -691,7 +696,7 @@ 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, CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops] +sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs] @declarations { std::string name; Kind k; @@ -702,24 +707,24 @@ sygusGTerm[std::string& fun, CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops] } : LPAREN_TOK ( builtinOp[k] - { ops.push_back(EXPR_MANAGER->operatorOf(k)); + { Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl; + ops.push_back(EXPR_MANAGER->operatorOf(k)); name = kind::kindToString(k); - Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl; } | symbol[name,CHECK_NONE,SYM_VARIABLE] { // 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.. - Expr bv = PARSER_STATE->getVariable(name); - ops.push_back(bv); - Debug("parser-sygus") << "Sygus grammar " << fun << " : op : " << name << std::endl; + 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) ); } ) - { name = dt.getName() + "_" + name; - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - ctor = new CVC4::DatatypeConstructor(name, testerId); + { cnames.push_back( name ); + cargs.push_back( std::vector< CVC4::Type >() ); } ( //sortSymbol[t,CHECK_NONE] symbol[sname,CHECK_NONE,SYM_VARIABLE] @@ -727,75 +732,46 @@ sygusGTerm[std::string& fun, CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops] ss << fun << "_" << sname; sname = ss.str(); if( PARSER_STATE->isDeclared(sname, SYM_SORT) ) { - t = PARSER_STATE->getSort(sname); + t = PARSER_STATE->getSort(sname); } else { - t = PARSER_STATE->mkUnresolvedType(sname); + t = PARSER_STATE->mkUnresolvedType(sname); } - std::stringstream cname; - cname << fun << "_" << name << "_" << ++count; - ctor->addArg(cname.str(), t); + cargs.back().push_back(t); } )+ RPAREN_TOK - { dt.addConstructor(*ctor); - delete ctor; } | 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)))); - name = dt.getName() + "_" + AntlrInput::tokenText($INTEGER_LITERAL); - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); - dt.addConstructor(c); + cnames.push_back( AntlrInput::tokenText($INTEGER_LITERAL) ); + cargs.push_back( std::vector< CVC4::Type >() ); } | HEX_LITERAL { Debug("parser-sygus") << "Sygus grammar " << fun << " : hex literal " << AntlrInput::tokenText($HEX_LITERAL) << std::endl; assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); ops.push_back(MK_CONST( BitVector(hexString, 16) )); - name = dt.getName() + "_" + AntlrInput::tokenText($HEX_LITERAL); - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); - dt.addConstructor(c); + cnames.push_back( AntlrInput::tokenText($HEX_LITERAL) ); + cargs.push_back( std::vector< CVC4::Type >() ); } | BINARY_LITERAL { Debug("parser-sygus") << "Sygus grammar " << fun << " : binary literal " << AntlrInput::tokenText($BINARY_LITERAL) << std::endl; assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); ops.push_back(MK_CONST( BitVector(binString, 2) )); - name = dt.getName() + "_" + AntlrInput::tokenText($BINARY_LITERAL); - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); - dt.addConstructor(c); + cnames.push_back( AntlrInput::tokenText($BINARY_LITERAL) ); + cargs.push_back( std::vector< CVC4::Type >() ); } | symbol[name,CHECK_NONE,SYM_VARIABLE] { if( name[0] == '-' ){ //hack for unary minus Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl; ops.push_back(MK_CONST(Rational(name))); - name = dt.getName() + "_" + name; - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); - dt.addConstructor(c); + cnames.push_back( name ); + cargs.push_back( std::vector< CVC4::Type >() ); }else{ Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl; Expr bv = PARSER_STATE->getVariable(name); ops.push_back(bv); - name = dt.getName() + "_" + name; - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); - dt.addConstructor(c); + cnames.push_back( name ); + cargs.push_back( std::vector< CVC4::Type >() ); } } ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index d20d48b13..077f385b0 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -504,7 +504,7 @@ void Smt2::includeFile(const std::string& filename) { //Type t = getExprManager()->mkFunctionType(types, rangeType); //Debug("parser-sygus") << "...function type : " << t << std::endl; - + Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED); Debug("parser-sygus") << "...made function : " << lambda << std::endl; std::vector<Expr> applyv; @@ -524,10 +524,30 @@ void Smt2::includeFile(const std::string& filename) { } } +void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, + std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ) { + //minimize grammar goes here + + for( unsigned i=0; i<cnames.size(); i++ ){ + std::string name = dt.getName() + "_" + cnames[i]; + std::string testerId("is-"); + testerId.append(name); + checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + CVC4::DatatypeConstructor c(name, testerId); + for( unsigned j=0; j<cargs[i].size(); j++ ){ + std::stringstream sname; + sname << name << "_" << j; + c.addArg(sname.str(), cargs[i][j]); + } + dt.addConstructor(c); + } +} + // i is index in datatypes/ops // j is index is datatype -Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops, - std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms, +Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops, + std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms, Expr eval, const Datatype& dt, size_t i, size_t j ) { const DatatypeConstructor& ctor = dt[j]; Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl; @@ -567,7 +587,11 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec Expr builtTerm; //if( ops[i][j].getKind() == kind::BUILTIN ){ if( !builtApply.empty() ){ - builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); + if( ops[i][j].getKind() != kind::BUILTIN ){ + builtTerm = getExprManager()->mkExpr(kind::APPLY, ops[i][j], builtApply); + }else{ + builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); + } }else{ builtTerm = ops[i][j]; } @@ -577,7 +601,7 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern); assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern); Debug("parser-sygus") << "...made assertion " << assertion << std::endl; - + //linearize multiplication if possible if( builtTerm.getKind()==kind::MULT ){ for(size_t k = 0; k < ctor.getNumArgs(); ++k) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index ca1602f36..ed6a5128b 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -183,11 +183,14 @@ public: } void defineSygusFuns(); - + + void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, + std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ); + // i is index in datatypes/ops // j is index is datatype - Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops, - std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms, + Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops, + std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms, Expr eval, const Datatype& dt, size_t i, size_t j ); void addSygusConstraint(Expr constraint) { |