diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-20 14:52:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-20 14:52:31 -0500 |
| commit | 78373c7f5fe93b7e8bbea10e3924f24d25a618ac (patch) | |
| tree | b3bd84e3d2154a4835679c71c028e87dbe1e2665 /src/parser/smt2/Smt2.g | |
| parent | fc0a5dcc002b12f075681d53e87cca1ddfbd479d (diff) | |
Make Sygus conjectures higher-order (#1244)
* Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks.
* Minor fix
* Fix bug in Node::hasBoundVar for non-ground operators.
* Add regression.
* Address review.
* Apply clang format.
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 05faf040e..4d39c7635 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -626,6 +626,7 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] 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 + // TODO (as part of #1170) : make this a standard command. seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type)); PARSER_STATE->pushScope(true); for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = |