summaryrefslogtreecommitdiff
path: root/src/parser/cvc
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-06-07 16:16:48 +0000
committerMorgan Deters <mdeters@gmail.com>2012-06-07 16:16:48 +0000
commit0a7dc7687a4989641d8c101ba3b2d4737eaea24f (patch)
treee802b4522419f9480ba04c2c5f2e2d9b1f88426e /src/parser/cvc
parentb3d6d0ccc76e92304fe612b23dc76a7d78061567 (diff)
Adding EchoCommand and associated printer and parser rules:
* SMT-LIBv2 parser now supports (echo...). * Dump() gestures can now dump EchoCommands in CVC and SMT-LIB formats. This can make it much easier to interpret output.
Diffstat (limited to 'src/parser/cvc')
-rw-r--r--src/parser/cvc/Cvc.g7
1 files changed, 5 insertions, 2 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 2da9f0f63..1f0e6b890 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -706,8 +706,11 @@ mainCommand[CVC4::Command*& cmd]
| ECHO_TOK
( simpleSymbolicExpr[sexpr]
- { Message() << sexpr << std::endl; }
- | { Message() << std::endl; }
+ { std::stringstream ss;
+ ss << sexpr;
+ cmd = new EchoCommand(ss.str());
+ }
+ | { cmd = new EchoCommand(); }
)
| EXIT_TOK
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback