add n-ary disjunction and conjunction

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_ast.cpp

@@ -335,7 +335,7 @@ extern "C" {
     Z3_bool Z3_API Z3_is_app(Z3_context c, Z3_ast a) {
         LOG_Z3_is_app(c, a);
         RESET_ERROR_CODE();
-        return is_app(reinterpret_cast<ast*>(a));
+        return a != 0 && is_app(reinterpret_cast<ast*>(a));
     }
 
     Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a) {

src/api/c++/z3++.h

@@ -802,6 +802,9 @@ namespace z3 {
         friend expr implies(expr const & a, bool b);
         friend expr implies(bool a, expr const & b);
 
+        friend expr or(expr_vector const& args);
+        friend expr and(expr_vector const& args);
+
         friend expr ite(expr const & c, expr const & t, expr const & e);
 
         friend expr distinct(expr_vector const& args);
@@ -947,6 +950,7 @@ namespace z3 {
     inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
     inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
 
+
     inline expr pw(expr const & a, expr const & b) {
         assert(a.is_arith() && b.is_arith());
         check_context(a, b);
@@ -1497,6 +1501,20 @@ namespace z3 {
         return expr(ctx, r);
     }
 
+    inline expr or(expr_vector const& args) { 
+        array<Z3_ast> _args(args);
+        Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
+        args.check_error();
+        return expr(args.ctx(), r);
+    }
+    inline expr and(expr_vector const& args) {
+        array<Z3_ast> _args(args);
+        Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
+        args.check_error();
+        return expr(args.ctx(), r);
+    }
+
+
     class func_entry : public object {
         Z3_func_entry m_entry;
         void init(Z3_func_entry e) {

src/smt/smt_context.cpp

@@ -2996,6 +2996,8 @@ namespace smt {
             // in a consistent context.
             if (inconsistent())
                 return; 
+            if (get_cancel_flag())
+                return;
             push_scope();
             for (unsigned i = 0; i < num_assumptions; i++) {
                 expr * curr_assumption = assumptions[i];
@@ -3337,6 +3339,7 @@ namespace smt {
                     break; 
                 }
                 if (cmr == quantifier_manager::UNKNOWN) {
+                    IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";);
                     // giving up
                     m_last_search_failure = QUANTIFIERS;
                     status                = l_undef;
@@ -3487,6 +3490,7 @@ namespace smt {
             }
 
             if (resource_limits_exceeded() && !inconsistent()) {
+                m_last_search_failure = RESOURCE_LIMIT;
                 return l_undef;
             }
         }
@@ -4109,7 +4113,7 @@ namespace smt {
               m_fingerprints.display(tout); 
               );
         failure fl = get_last_search_failure();
-        if (fl == MEMOUT || fl == CANCELED || fl == TIMEOUT || fl == NUM_CONFLICTS) {
+        if (fl == MEMOUT || fl == CANCELED || fl == TIMEOUT || fl == NUM_CONFLICTS || fl == RESOURCE_LIMIT) {
             return;
         }
 

src/smt/smt_context_pp.cpp

@@ -39,6 +39,8 @@ namespace smt {
             return out << "CANCELED";
         case NUM_CONFLICTS:
             return out << "NUM_CONFLICTS";
+        case RESOURCE_LIMIT:
+            return out << "RESOURCE_LIMIT";
         case THEORY:
             if (!m_incomplete_theories.empty()) {
                 ptr_vector<theory>::const_iterator it  = m_incomplete_theories.begin();
@@ -78,6 +80,7 @@ namespace smt {
             r += "))";
             break;
         }
+        case RESOURCE_LIMIT: r = "(resource limits reached)"; break;
         case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
         case UNKNOWN: r = m_unknown; break;
         }

src/smt/smt_failure.h

@@ -32,6 +32,7 @@ namespace smt {
         CANCELED,      //!< External cancel flag was set
         NUM_CONFLICTS, //!< Maximum number of conflicts was reached
         THEORY,        //!< Theory is incomplete
+        RESOURCE_LIMIT,
         QUANTIFIERS    //!< Logical context contains universal quantifiers.
     };
 

src/smt/smt_model_checker.cpp

@@ -112,7 +112,6 @@ namespace smt {
         if (!m_curr_model->eval(q->get_expr(), tmp, true)) {
             return;
         }
-        //std::cout << tmp << "\n";
         TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);        
         ptr_buffer<expr> subst_args;
         unsigned num_decls = q->get_num_decls();
@@ -373,7 +372,8 @@ namespace smt {
             return true;
 
         if (m_iteration_idx >= m_params.m_mbqi_max_iterations) {
-            IF_VERBOSE(10, verbose_stream() << "(smt.mbqi \"max instantiations reached \")" << m_iteration_idx << "\n";);
+            IF_VERBOSE(1, verbose_stream() << "(smt.mbqi \"max instantiations " << m_iteration_idx << " reached\")\n";);
+            m_context->set_reason_unknown("max mbqi instantiations reached");
             return false;
         }
 

src/smt/tactic/smt_tactic.cpp

@@ -293,8 +293,11 @@ public:
                 if (m_ctx->canceled()) {
                     throw tactic_exception(Z3_CANCELED_MSG);
                 }
-                if (m_fail_if_inconclusive)
+                if (m_fail_if_inconclusive) {
-                    throw tactic_exception("smt tactic failed to show goal to be sat/unsat");
+                    std::stringstream strm;
+                    strm << "smt tactic failed to show goal to be sat/unsat " << m_ctx->last_failure_as_string();
+                    throw tactic_exception(strm.str().c_str());
+                }
                 result.push_back(in.get());
                 if (m_candidate_models) {
                     switch (m_ctx->last_failure()) {