diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-21 14:30:32 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-21 16:25:13 -0400 |
commit | ed40bbae19622ff29e1ca6eb873d20262ed21926 (patch) | |
tree | a3f1954f8311cf96a5a30eadf59786e80b8693c4 /src/parser | |
parent | 332772cb9ec225587d2107881d3b6f119e332b84 (diff) |
Add the ability to "mute" commands, needed for SMT-LIB compliance.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 4 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a390cf452..387a24fe1 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -952,6 +952,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] std::string attr_name = attr; attr_name.erase( attr_name.begin() ); Command* c = new SetUserAttributeCommand( attr_name, expr ); + c->setMuted(true); PARSER_STATE->preemptCommand(c); } else { PARSER_STATE->attributeNotSupported(attr); @@ -979,6 +980,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] // bind name to expr with define-fun Command* c = new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr); + c->setMuted(true); PARSER_STATE->preemptCommand(c); } ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e1f977890..5d104531f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -290,7 +290,9 @@ void Smt2::checkThatLogicIsSet() { setLogic("ALL_SUPPORTED"); - preemptCommand(new SetBenchmarkLogicCommand("ALL_SUPPORTED")); + Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED"); + c->setMuted(true); + preemptCommand(c); } } } |