diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-18 23:24:26 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-18 23:24:26 +0000 |
commit | 9f8f4ae9ef9d9d79973b77b6c61af4c5db034841 (patch) | |
tree | c9f2159ab870534a2cd0d887944c84d00da9b2a4 /src/parser/smt | |
parent | a377bee55e41ba9ceef3380742e536545299181c (diff) |
Adding --no-checking option to disable semantic checks in parser
Diffstat (limited to 'src/parser/smt')
-rw-r--r-- | src/parser/smt/smt_parser.g | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index a9f06d92c..39cadd47f 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -16,7 +16,6 @@ header "post_include_hpp" { #include "parser/antlr_parser.h" #include "expr/command.h" -#include "util/Assert.h" } header "post_include_cpp" { @@ -123,7 +122,7 @@ annotatedFormula returns [CVC4::Expr formula] } : /* a built-in operator application */ LPAREN kind = builtinOp annotatedFormulas[args] RPAREN - { AlwaysAssert( checkArity(kind, args.size()) ); + { checkArity(kind, args.size()); formula = mkExpr(kind,args); } | /* A non-built-in function application */ @@ -213,7 +212,7 @@ functionSymbol returns [CVC4::Expr fun] string name; } : name = functionName[CHECK_DECLARED] - { AlwaysAssert( checkFunction(name) ); + { checkFunction(name); fun = getFunction(name); } ; @@ -316,6 +315,6 @@ returns [std::string id] } : x:IDENTIFIER { id = x->getText(); - AlwaysAssert( checkDeclaration(id, check,type) ); } + checkDeclaration(id, check,type); } ; |