diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-09-21 20:34:19 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-09-21 20:34:19 +0000 |
| commit | b5e4b809d1913c9cfc5cf95c04e9fc34c1ca42f3 (patch) | |
| tree | 38f605f758581026af28e5c4d4ad72e12b9cb944 /src/parser/smt2/Smt2.g | |
| parent | 9c543757e459bfae5ce1254322212f72af0d37a4 (diff) | |
SMT-LIBv2 compliance updates:
* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default
Also:
* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5950f568f..03aa7acc1 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -584,6 +584,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] expr = EXPR_MANAGER->mkAssociative(kind,args); } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) { expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); + } else if( ( kind == CVC4::kind::IFF || kind == CVC4::kind::EQUAL || + kind == CVC4::kind::LT || kind == CVC4::kind::GT || + kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) && + args.size() > 2 ) { + expr = MK_EXPR(CVC4::kind::CHAIN, MK_CONST(kind), args); } else { PARSER_STATE->checkOperator(kind, args.size()); expr = MK_EXPR(kind, args); |