From b5e4b809d1913c9cfc5cf95c04e9fc34c1ca42f3 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 21 Sep 2012 20:34:19 +0000 Subject: 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.) --- src/parser/smt2/Smt2.g | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/parser/smt2/Smt2.g') 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); -- cgit v1.2.3