From: Morgan Deters Date: Wed, 20 Apr 2011 11:19:50 +0000 (+0000) Subject: numerous bugfixes X-Git-Tag: cvc5-1.0.0~8583 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2499bd64a5ac688573ebbcd6114983f64a8094eb;p=cvc5.git numerous bugfixes --- diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index cfcc62335..8dd329b83 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -72,6 +72,10 @@ bool DeclarationScope::isBoundDefinedFunction(const std::string& name) const thr return found != d_exprMap->end() && d_functions->contains((*found).second); } +bool DeclarationScope::isBoundDefinedFunction(Expr func) const throw() { + return d_functions->contains(func); +} + Expr DeclarationScope::lookup(const std::string& name) const throw(AssertionException) { return (*d_exprMap->find(name)).second; } diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 6d89f5f4e..699dca6fa 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -133,6 +133,12 @@ public: */ bool isBoundDefinedFunction(const std::string& name) const throw(); + /** + * Check whether an Expr was bound to a function (i.e., was the + * second arg to bindDefinedFunction()). + */ + bool isBoundDefinedFunction(Expr func) const throw(); + /** * Check whether a name is bound to a type (or type constructor). * diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 794f0a670..543538f32 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -88,6 +88,7 @@ tokens { BAR = '|'; DOT = '.'; DOTDOT = '..'; + UNDERSCORE = '_'; SQHASH = '[#'; HASHSQ = '#]'; @@ -349,6 +350,14 @@ Expr createPrecedenceTree(ExprManager* em, return e; } +/** Add n NOTs to the front of e and return the result. */ +Expr addNots(ExprManager* em, size_t n, Expr e) { + while(n-- > 0) { + e = em->mkExpr(kind::NOT, e); + } + return e; +} + }/* @parser::members */ @header { @@ -480,6 +489,7 @@ command returns [CVC4::Command* cmd = 0] { PARSER_STATE->popScope(); cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } | toplevelDeclaration[cmd] + | SEMICOLON c=command { $cmd = c; } | EOF ; @@ -710,7 +720,6 @@ type[CVC4::Type& t, } else { args.push_back(t); } - Debug("parser") << "type: " << t << std::endl; } ( ARROW_TOK type[t2,check] { args.push_back(t2); } )? { if(t2.isNull()) { @@ -783,9 +792,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, t = Type(); } /* subrange types */ - | LBRACKET bound DOTDOT bound RBRACKET +/* parsing not working -- some kind of conflict betw [0..1] and 0.0 + | bounds { PARSER_STATE->unimplementedFeature("subranges not supported yet"); t = Type(); } +*/ /* tuple types / old-style function types */ | LBRACKET type[t,check] { types.push_back(t); } @@ -828,12 +839,6 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } ; -bound - : '_' - | numeral - | MINUS_TOK numeral - ; - /** * Matches a type identifier. Returns the identifier. If the type is * declared, returns the Type in the 't' parameter; otherwise a null @@ -873,6 +878,52 @@ typeLetDecl[CVC4::parser::DeclarationCheck check] formula[CVC4::Expr& f] @init { Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Expr f2; + std::vector expressions; + std::vector operators; + unsigned op; +} + : n=nots + ( prefixFormula[f] + { f = addNots(EXPR_MANAGER, n, f); } + | comparison[f] + { f = addNots(EXPR_MANAGER, n, f); + expressions.push_back(f); + } + i=morecomparisons[expressions,operators]? + { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } + ) + ; + +morecomparisons[std::vector& expressions, + std::vector& operators] returns [size_t i] +@init { + unsigned op; + Expr f; + $i = expressions.size(); +} + : booleanBinop[op] { operators.push_back(op); } + n=nots + ( prefixFormula[f] + { expressions.push_back(addNots(EXPR_MANAGER, n, f)); } + | comparison[f] + { f = addNots(EXPR_MANAGER, n, f); + expressions.push_back(f); + } + inner=morecomparisons[expressions,operators]? + ) + ; + +/** Matches 0 or more NOTs. */ +nots returns [size_t n] +@init { + $n = 0; +} + : ( NOT_TOK { ++$n; } )* + ; + +prefixFormula[CVC4::Expr& f] +@init { std::vector ids; std::vector terms; std::vector types; @@ -894,20 +945,20 @@ formula[CVC4::Expr& f] f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType()); } - /* lets: letDecl defines the variables and functionss, we just + /* lets: letDecl defines the variables and functionss, we just * manage the scopes here. NOTE that LET in the CVC language is * always sequential! */ | LET_TOK { PARSER_STATE->pushScope(); } letDecl ( COMMA letDecl )* IN_TOK formula[f] { PARSER_STATE->popScope(); } - /* lambda */ + /* lambda */ | LAMBDA { PARSER_STATE->pushScope(); } LPAREN boundVarDeclsReturn[terms,types] RPAREN COLON formula[f] { PARSER_STATE->popScope(); Type t = EXPR_MANAGER->mkFunctionType(types, f.getType()); - Expr func = PARSER_STATE->mkFunction("anonymous", t); + Expr func = PARSER_STATE->mkAnonymousFunction("lambda", t); Command* cmd = new DefineFunctionCommand(func, terms, f); PARSER_STATE->preemptCommand(cmd); f = func; @@ -920,9 +971,6 @@ formula[CVC4::Expr& f] PARSER_STATE->unimplementedFeature("array literals not supported yet"); f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType())); } - - /* everything else */ - | booleanFormula[f] ; instantiationPatterns @@ -949,36 +997,6 @@ letDecl } ; -booleanFormula[CVC4::Expr& f] -@init { - std::vector expressions; - std::vector operators; - unsigned op; - unsigned notCount = 0; -} - : ( NOT_TOK { ++notCount; } )* comparison[f] - { while(notCount > 0) { - --notCount; - f = EXPR_MANAGER->mkExpr(kind::NOT, f); - } - expressions.push_back(f); - Assert(notCount == 0); - } - ( booleanBinop[op] ( NOT_TOK { ++notCount; } )* comparison[f] - { while(notCount > 0) { - --notCount; - f = EXPR_MANAGER->mkExpr(kind::NOT, f); - } - operators.push_back(op); -# warning cannot do NOT FORALL or TRUE AND FORALL, or.. - expressions.push_back(f); - Assert(notCount == 0); - } - )* - { Assert(notCount == 0); - f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } - ; - booleanBinop[unsigned& op] @init { op = LT(1)->getType(LT(1)); @@ -1089,17 +1107,19 @@ bvNegTerm[CVC4::Expr& f] ; /** - * Parses an array select / bitvector extract / bitvector shift. - * These are all parsed the same way because they are all effectively - * post-fix operators and can continue piling onto an expression. - * Array selects and bitvector extracts even share similar syntax with - * their use of [ square brackets ], so we left-factor as much out as - * possible to make ANTLR happy. + * Parses an array select / bitvector extract / bitvector shift / + * function or constructor application. These are all parsed the same + * way because they are all effectively post-fix operators and can + * continue piling onto an expression. Array selects and bitvector + * extracts even share similar syntax with their use of [ square + * brackets ], so we left-factor as much out as possible to make ANTLR + * happy. */ selectExtractShift[CVC4::Expr& f] @init { Expr f2; bool extract, left; + std::vector args; } : bvTerm[f] ( /* array select / bitvector extract */ @@ -1115,6 +1135,8 @@ selectExtractShift[CVC4::Expr& f] f = MK_EXPR(CVC4::kind::SELECT, f, f2); } } + + /* left- or right-shift */ | ( LEFTSHIFT_TOK { left = true; } | RIGHTSHIFT_TOK { left = false; } ) k=numeral { // Defined in: @@ -1127,6 +1149,29 @@ selectExtractShift[CVC4::Expr& f] MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f)); } } + + /* function/constructor application */ + | LPAREN { args.push_back(f); } + formula[f] { args.push_back(f); } + ( COMMA formula[f] { args.push_back(f); } )* RPAREN + // TODO: check arity + { Type t = args.front().getType(); + Debug("parser") << "type is " << t << std::endl; + Debug("parser") << "expr is " << args.front() << std::endl; + if(PARSER_STATE->isDefinedFunction(args.front())) { + f = MK_EXPR(CVC4::kind::APPLY, args); + } else if(t.isFunction()) { + f = MK_EXPR(CVC4::kind::APPLY_UF, args); + } else if(t.isConstructor()) { + f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args); + } else if(t.isSelector()) { + f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args); + } else if(t.isTester()) { + f = MK_EXPR(CVC4::kind::APPLY_TESTER, args); + } else { + Unhandled(t); + } + } )* ; @@ -1135,15 +1180,15 @@ bvTerm[CVC4::Expr& f] Expr f2; } /* BV xor */ - : BVXOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN + : BVXOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_XOR, f, f2); } - | BVNAND_TOK LPAREN formula[f] COMMA formula[f] RPAREN + | BVNAND_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_NAND, f, f2); } - | BVNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN + | BVNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_NOR, f, f2); } - | BVCOMP_TOK LPAREN formula[f] COMMA formula[f] RPAREN + | BVCOMP_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_COMP, f, f2); } - | BVXNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN + | BVXNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_XNOR, f, f2); } /* BV unary minus */ @@ -1159,7 +1204,7 @@ bvTerm[CVC4::Expr& f] if(k > size) { f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); } else if(k < size) { - f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); + f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f); } } /* BV subtraction */ @@ -1172,12 +1217,12 @@ bvTerm[CVC4::Expr& f] if(k > size) { f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); } else if(k < size) { - f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); + f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f); } } /* BV multiplication */ | BVMULT_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN - { MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2); + { f = MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2); if(k == 0) { PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0"); } @@ -1185,7 +1230,7 @@ bvTerm[CVC4::Expr& f] if(k > size) { f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); } else if(k < size) { - f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); + f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f); } } /* BV unsigned division */ @@ -1271,44 +1316,8 @@ simpleTerm[CVC4::Expr& f] std::vector args; Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; } - /* function/constructor application */ - : identifier[name,CHECK_DECLARED,SYM_VARIABLE] - { Debug("parser") << " at level " << PARSER_STATE->getDeclarationLevel() << std::endl; - Debug("parser") << " isFunction " << PARSER_STATE->isFunctionLike(name) << std::endl; - Debug("parser") << " isDefinedFunction " << PARSER_STATE->isDefinedFunction(name) << std::endl; - Debug("parser") << " name " << name << std::endl; - Debug("parser") << " isDeclared " << PARSER_STATE->isDeclared(name) << std::endl; - Debug("parser") << " getType " << PARSER_STATE->getType(name) << std::endl; - PARSER_STATE->checkFunctionLike(name); - f = PARSER_STATE->getVariable(name); - args.push_back(f); - } - LPAREN formula[f] { args.push_back(f); } - ( COMMA formula[f] { args.push_back(f); } )* RPAREN - // TODO: check arity - { Type t = args.front().getType(); - Debug("parser") << "type is " << t << std::endl; - Debug("parser") << "expr is " << args.front() << std::endl; - if(PARSER_STATE->isDefinedFunction(name)) { - f = MK_EXPR(CVC4::kind::APPLY, args); - } else if(t.isFunction()) { - f = MK_EXPR(CVC4::kind::APPLY_UF, args); - } else if(t.isConstructor()) { - Debug("parser-idt") << "apply constructor: " << name.c_str() << " " << args.size() << std::endl; - f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args); - } else if(t.isSelector()) { - Debug("parser-idt") << "apply selector: " << name.c_str() << " " << args.size() << std::endl; - f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args); - } else if(t.isTester()) { - Debug("parser-idt") << "apply tester: " << name.c_str() << " " << args.size() << std::endl; - f = MK_EXPR(CVC4::kind::APPLY_TESTER, args); - } else { - Unhandled(t); - } - } - /* if-then-else */ - | iteTerm[f] + : iteTerm[f] /* parenthesized sub-formula / tuple literals */ | LPAREN formula[f] { args.push_back(f); } @@ -1345,9 +1354,11 @@ simpleTerm[CVC4::Expr& f] | identifier[name,CHECK_DECLARED,SYM_VARIABLE] { f = PARSER_STATE->getVariable(name); // datatypes: zero-ary constructors - if(PARSER_STATE->getType(name).isConstructor()) { - args.push_back(f); - f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args); + Type t = PARSER_STATE->getType(name); + if(t.isConstructor() && ConstructorType(t).getArity() == 0) { + // don't require parentheses, immediately turn it into an + // apply + f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f); } } ; @@ -1475,7 +1486,7 @@ numeral returns [unsigned k] /** * Matches a decimal literal. */ -DECIMAL_LITERAL: DIGIT+ '.' DIGIT+; +DECIMAL_LITERAL: DIGIT+ DOT DIGIT+; /** * Matches a hexadecimal constant. diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 19d1bbcb8..29ade43c1 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -45,6 +45,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par d_input(input), d_declScopeAllocated(), d_declScope(&d_declScopeAllocated), + d_anonymousFunctionCount(0), d_done(false), d_checksEnabled(true), d_strictMode(strictMode), @@ -117,6 +118,13 @@ bool Parser::isDefinedFunction(const std::string& name) { return d_declScope->isBoundDefinedFunction(name); } +/* Returns true if the Expr is a defined function. */ +bool Parser::isDefinedFunction(Expr func) { + // more permissive in type than isFunction(), because defined + // functions can be zero-ary and declared functions cannot. + return d_declScope->isBoundDefinedFunction(func); +} + /* Returns true if name is bound to a function returning boolean. */ bool Parser::isPredicate(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); @@ -138,6 +146,13 @@ Parser::mkFunction(const std::string& name, const Type& type) { return expr; } +Expr +Parser::mkAnonymousFunction(const std::string& prefix, const Type& type) { + stringstream name; + name << prefix << ':' << ++d_anonymousFunctionCount; + return mkFunction(name.str(), type); +} + std::vector Parser::mkVars(const std::vector names, const Type& type) { diff --git a/src/parser/parser.h b/src/parser/parser.h index 25fb30be6..033abb42a 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -125,8 +125,8 @@ class CVC4_PUBLIC Parser { */ DeclarationScope* d_declScope; - /** The name of the input file. */ -// std::string d_filename; + /** How many anonymous functions we've created. */ + size_t d_anonymousFunctionCount; /** Are we done */ bool d_done; @@ -322,6 +322,13 @@ public: /** Create a new CVC4 function expression of the given type. */ Expr mkFunction(const std::string& name, const Type& type); + /** + * Create a new CVC4 function expression of the given type, + * appending a unique index to its name. (That's the ONLY + * difference between mkAnonymousFunction() and mkFunction()). + */ + Expr mkAnonymousFunction(const std::string& prefix, const Type& type); + /** Create a new variable definition (e.g., from a let binding). */ void defineVar(const std::string& name, const Expr& val); @@ -394,6 +401,9 @@ public: /** Is the symbol bound to a defined function? */ bool isDefinedFunction(const std::string& name); + /** Is the Expr a defined function? */ + bool isDefinedFunction(Expr func); + /** Is the symbol bound to a predicate? */ bool isPredicate(const std::string& name); diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index e23d7c88b..b83fd42dc 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -198,12 +198,23 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, case kind::FUNCTION_TYPE: case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: - case kind::TESTER_TYPE: - if(n.getNumChildren() > 0) { - copy(n.begin(), n.end() - 1, ostream_iterator(out, " -> ")); - out << n[n.getNumChildren() - 1]; + if(n.getNumChildren() > 2) { + out << '('; + for(unsigned i = 0; i < n.getNumChildren() - 2; ++i) { + out << n[i] << ", "; + } + out << n[n.getNumChildren() - 2] + << ") -> " << n[n.getNumChildren() - 1]; + } else if(n.getNumChildren() == 2) { + out << n[0] << " -> " << n[1]; + } else { + Assert(n.getNumChildren() == 1); + out << n[0]; } break; + case kind::TESTER_TYPE: + out << n[0] << " -> BOOLEAN"; + break; case kind::ARRAY_TYPE: out << "ARRAY " << n[0] << " OF " << n[1]; @@ -265,6 +276,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, out << n.getOperator() << '(' << n[0] << ',' << n[1] << ')'; break; + // N-ary infix + case kind::BITVECTOR_CONCAT: + out << '('; + for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) { + cout << n[i] << ' ' << n.getOperator(); + } + out << n[n.getNumChildren() - 1] << ')'; + default: if(k == kind::NOT && n[0].getKind() == kind::EQUAL) { // collapse NOT-over-EQUAL diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index ec98e61d2..0d313594c 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -48,9 +48,15 @@ class ApplyTypeRule { TNode::iterator argument_it = n.begin(); TNode::iterator argument_it_end = n.end(); TypeNode::iterator argument_type_it = fType.begin(); - for(; argument_it != argument_it_end; ++argument_it) { + for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) { if((*argument_it).getType() != *argument_type_it) { - throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + std::stringstream ss; + ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)); + ss << "argument types do not match the function type:\n" + << "argument: " << *argument_it << "\n" + << "has type: " << (*argument_it).getType() << "\n" + << "not equal: " << *argument_type_it; + throw TypeCheckingExceptionPrivate(n, ss.str()); } } } else { @@ -75,6 +81,7 @@ class EqualityTypeRule { if ( lhsType != rhsType ) { std::stringstream ss; + ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)); ss << "Types do not match in equation "; ss << "[" << lhsType << "<>" << rhsType << "]"; diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 748ac3f9d..7a4bf721f 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -41,9 +41,15 @@ public: TNode::iterator argument_it = n.begin(); TNode::iterator argument_it_end = n.end(); TypeNode::iterator argument_type_it = fType.begin(); - for(; argument_it != argument_it_end; ++argument_it) { + for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) { if((*argument_it).getType() != *argument_type_it) { - throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + std::stringstream ss; + ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)) + << "argument types do not match the function type:\n" + << "argument: " << *argument_it << "\n" + << "has type: " << (*argument_it).getType() << "\n" + << "not equal: " << *argument_type_it; + throw TypeCheckingExceptionPrivate(n, ss.str()); } } } diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index abce24751..ac864d16b 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -127,6 +127,7 @@ int runTest() { runTestString("(= (f (f y)) x)"); runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4); + runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", input::LANG_CVC4); runTestString("a[x][y] = a[y][x]", input::LANG_CVC4); delete psr; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index f288f6b1a..632db2b91 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -200,6 +200,7 @@ public: void testGoodCvc4Inputs() { tryGoodInput(""); // empty string is OK + tryGoodInput(";"); // no command is OK tryGoodInput("ASSERT TRUE;"); tryGoodInput("QUERY TRUE;"); tryGoodInput("CHECKSAT FALSE;"); @@ -219,7 +220,6 @@ public: } void testBadCvc4Inputs() { - tryBadInput(";"); // no command tryBadInput("ASSERT;"); // no args tryBadInput("QUERY"); tryBadInput("CHECKSAT");