From e9b9a29339622e94d5542a53c377f7952ae1ea33 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Jul 2017 08:44:19 -0700 Subject: [PATCH] revert first fix for #1173, replace by handling single arity chainables Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 8 ++++---- src/ast/ast.cpp | 5 ++++- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 66580a1dd..2eb0f4d90 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -414,10 +414,10 @@ inline decl_kind arith_decl_plugin::fix_kind(decl_kind k, unsigned arity) { return OP_UMINUS; } switch (k) { - case OP_LE: check_arity(arity, 2); break; - case OP_GE: check_arity(arity, 2); break; - case OP_LT: check_arity(arity, 2); break; - case OP_GT: check_arity(arity, 2); break; + case OP_LE: break; + case OP_GE: break; + case OP_LT: break; + case OP_GT: break; case OP_ADD: break; case OP_SUB: break; case OP_UMINUS: check_arity(arity, 1); break; diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 5f2de5170..1c3be5e68 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2178,7 +2178,10 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar throw ast_exception(buffer.str().c_str()); } app * r = 0; - if (num_args > 2 && !decl->is_flat_associative()) { + if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) { + r = mk_true(); + } + else if (num_args > 2 && !decl->is_flat_associative()) { if (decl->is_right_associative()) { unsigned j = num_args - 1; r = mk_app_core(decl, args[j-1], args[j]);