diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-09 21:56:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-09 21:56:40 -0500 |
commit | 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 (patch) | |
tree | 427223e34ce9bd100ef4443c80b95a9526169363 /src/parser/smt2 | |
parent | 3b0ce95e7b7d1cbc351df9a7d2acbf3b6e13f9e7 (diff) |
Split term database (#1206)
* Move equality query to own file, move equality inference to quantifiers engine.
* Move quantifiers attributes out of TermDb and into QuantAttribute.
* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.
* Split term database into term util.
* Partial fix for #1205 that eliminates need for dependency in node.cpp.
* Add more references to github issues.
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 1 |
2 files changed, 3 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 29f507238..1b3d7b23f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -624,8 +624,8 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] }else{ synth_fun_type = range; } - // allow overloading for synth fun - synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type, ExprManager::VAR_FLAG_NONE, true); + // we do not allow overloading for synth fun + synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type); // we add a declare function command here // this is the single unmuted command in the sequence generated by this smt2 command seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type)); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index acfd886ce..a6830d95d 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1090,6 +1090,7 @@ const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) { } const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){ + //FIXME #1205 : we should not create a proxy, instead quantify on synth_fun and set Type t as an attribute Expr sym = mkBoundVar("sfproxy", t); d_sygusFunSymbols.push_back(sym); |