+setOptionInternal[CVC4::Command*& cmd]
+@init {
+ std::string name;
+ SExpr sexpr;
+}
+ : keyword[name] symbolicExpr[sexpr]
+ { PARSER_STATE->setOption(name.c_str() + 1, sexpr);
+ cmd = new SetOptionCommand(name.c_str() + 1, sexpr);
+ // Ugly that this changes the state of the parser; but
+ // global-declarations affects parsing, so we can't hold off
+ // on this until some SmtEngine eventually (if ever) executes it.
+ if(name == ":global-declarations") {
+ PARSER_STATE->setGlobalDeclarations(sexpr.getValue() == "true");
+ }
+ }
+ ;
+