diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-14 10:08:11 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-14 10:08:11 +0200 |
commit | 88adf5e1416fb0c533fe3a24da5fce50aa5a2c0b (patch) | |
tree | c8963086026c80bd01c12f824411bce1461cbc9e /src | |
parent | aac70d0b7e1784f1c34be7df9e22f3fba1cb1522 (diff) |
sygusComp2018: update semantics for declare-fun in sygus. (#2102)
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/Smt2.g | 13 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 9 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 3 |
3 files changed, 18 insertions, 7 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4b8c52841..b52be77bb 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -353,8 +353,17 @@ command [std::unique_ptr<CVC4::Command>* cmd] "be declared in logic "); } // we allow overloading for function declarations - Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); - cmd->reset(new DeclareFunctionCommand(name, func, t)); + if (PARSER_STATE->sygus()) + { + // it is a higher-order universal variable + PARSER_STATE->mkSygusVar(name, t); + cmd->reset(new EmptyCommand()); + } + else + { + Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); + cmd->reset(new DeclareFunctionCommand(name, func, t)); + } } | /* function definition */ DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 33ac69c63..257ee1171 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -625,10 +625,12 @@ Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) d_sygusVars.push_back(e); d_sygusVarPrimed[e] = false; if( isPrimed ){ + d_sygusInvVars.push_back(e); std::stringstream ss; ss << name << "'"; Expr ep = mkBoundVar(ss.str(), type); d_sygusVars.push_back(ep); + d_sygusInvVars.push_back(ep); d_sygusVarPrimed[ep] = true; } return e; @@ -1228,15 +1230,14 @@ Expr Smt2::makeSygusBoundVarList(Datatype& dt, } const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) { - for( unsigned i=0; i<d_sygusVars.size(); i++ ){ - Expr v = d_sygusVars[i]; + for (unsigned i = 0, size = d_sygusInvVars.size(); i < size; i++) + { + Expr v = d_sygusInvVars[i]; std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v ); if( it!=d_sygusVarPrimed.end() ){ if( it->second==isPrimed ){ vars.push_back( v ); } - }else{ - //should never happen } } } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 85d9b112e..c9b224d39 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -64,7 +64,8 @@ private: std::unordered_map<std::string, Kind> operatorKindMap; std::pair<Expr, std::string> d_lastNamedTerm; // for sygus - std::vector<Expr> d_sygusVars, d_sygusConstraints, d_sygusFunSymbols; + std::vector<Expr> d_sygusVars, d_sygusInvVars, d_sygusConstraints, + d_sygusFunSymbols; std::map< Expr, bool > d_sygusVarPrimed; protected: |