diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-08 12:10:41 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-08 12:10:41 -0600 |
| commit | 346c85d145f6938ce7dce74e7e7cb855d5a6025a (patch) | |
| tree | fb9cc78736360756e2af81fc3457c4ed9929f32f /src/parser | |
| parent | b4c7be882b88c6741212ecd9c6be4e91fec76087 (diff) | |
Extend synthesis solver to handle single invocation with additional universal quantification. Refactor query/check-sat to call one internal function in SmtEngine. Make check-synth its own command. Minor work on quant ee.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 9d2392715..0526ba66d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -765,9 +765,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] Command* c = new SetUserAttributeCommand("sygus", sygusVar); c->setMuted(true); PARSER_STATE->preemptCommand(c); - c = new AssertCommand(body); - PARSER_STATE->preemptCommand(c); - $cmd = new CheckSatCommand(); + $cmd = new CheckSynthCommand(body); } | c = command { $cmd = c; } // /* error handling */ |