Merge branch 'master' of https://github.com/Z3Prover/z3

src/api/api_context.h

@@ -245,7 +245,7 @@ inline api::context * mk_c(Z3_context c) { return reinterpret_cast<api::context*
 #define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } }
 #define CHECK_SEARCHING(c) mk_c(c)->check_searching();
 inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); }
-#define CHECK_IS_EXPR(_p_, _ret_) { if (!is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } }
+#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == 0 || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } }
 inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); }
 #define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } }
 inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); }

src/api/api_solver.cpp

@@ -443,7 +443,24 @@ extern "C" {
             }
             _variables.push_back(to_expr(__variables[i]));
         }
-        lbool result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences);
+        lbool result = l_undef;
+        unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
+        unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
+        bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);
+        cancel_eh<reslimit> eh(mk_c(c)->m().limit());
+        api::context::set_interruptable si(*(mk_c(c)), eh);
+        {
+            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_timer timer(timeout, &eh);
+            scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
+            try {
+                result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences);
+            }
+            catch (z3_exception & ex) {
+                mk_c(c)->handle_exception(ex);
+                return Z3_L_UNDEF;
+            }
+        }
         for (unsigned i = 0; i < _consequences.size(); ++i) {
             to_ast_vector_ref(consequences).push_back(_consequences[i].get());
         }

src/api/dotnet/Context.cs

@@ -1055,6 +1055,19 @@ namespace Microsoft.Z3
             return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
+        /// <summary>
+        /// Create an expression representing <c>t[0] * t[1] * ...</c>.
+        /// </summary>
+        public ArithExpr MkMul(IEnumerable<ArithExpr> t)
+        {
+            Contract.Requires(t != null);
+            Contract.Requires(Contract.ForAll(t, a => a != null));
+            Contract.Ensures(Contract.Result<ArithExpr>() != null);
+
+            CheckContextMatch(t);
+            return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
+        }
+
         /// <summary>
         /// Create an expression representing <c>t[0] - t[1] - ...</c>.
         /// </summary>

src/ast/macros/macro_util.cpp

@@ -482,12 +482,13 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
     }
     if (changed) {
         // REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution.
-        var_subst subst(m_manager); 
+        var_subst subst(m_manager, true); 
         TRACE("macro_util_bug",
               tout << "head: " << mk_pp(head, m_manager) << "\n";
-              tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitituion:\n";
+              tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n";
               for (unsigned i = 0; i < var_mapping.size(); i++) {
-                  tout << "#" << i << " -> " << mk_pp(var_mapping[i], m_manager) << "\n";
+                  if (var_mapping[i] != 0)
+                    tout << "#" << i << " -> " << mk_pp(var_mapping[i], m_manager) << "\n";
               });
         subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t);
     }

src/ast/rewriter/rewriter_def.h

@@ -39,7 +39,7 @@ void rewriter_tpl<Config>::process_var(var * v) {
         unsigned idx = v->get_idx();
         if (idx < m_bindings.size()) {
             unsigned index = m_bindings.size() - idx - 1;
-            expr * r = m_bindings[index];
+            var * r = (var*)(m_bindings[index]);
             if (r != 0) {
                 SASSERT(v->get_sort() == m().get_sort(r));
                 if (!is_ground(r) && m_shifts[index] != m_bindings.size()) {

src/cmd_context/cmd_context.cpp

@@ -580,7 +580,7 @@ bool cmd_context::logic_has_bv() const {
 }
 
 bool cmd_context::logic_has_seq_core(symbol const& s) const {
-    return s == "QF_BVRE" || s == "QF_S";
+    return s == "QF_BVRE" || s == "QF_S" || s == "ALL";
 }
 
 bool cmd_context::logic_has_seq() const {
@@ -588,7 +588,7 @@ bool cmd_context::logic_has_seq() const {
 }
 
 bool cmd_context::logic_has_fpa_core(symbol const& s) const {
-    return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP";
+    return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "ALL";
 }
 
 bool cmd_context::logic_has_fpa() const {
@@ -705,7 +705,7 @@ void cmd_context::init_external_manager() {
 }
 
 bool cmd_context::supported_logic(symbol const & s) const {
-    return s == "QF_UF" || s == "UF" || 
+    return s == "QF_UF" || s == "UF" || s == "ALL" ||
         logic_has_arith_core(s) || logic_has_bv_core(s) ||
         logic_has_array_core(s) || logic_has_seq_core(s) ||
         logic_has_horn(s) || logic_has_fpa_core(s);

src/parsers/smt2/smt2scanner.cpp

@@ -92,7 +92,7 @@ namespace smt2 {
     }
 
     scanner::token scanner::read_symbol_core() {
-        while (true) {
+        while (!m_at_eof) {
             char c = curr();
             signed char n = m_normalized[static_cast<unsigned char>(c)];
             if (n == 'a' || n == '0' || n == '-') {
@@ -106,6 +106,7 @@ namespace smt2 {
                 return SYMBOL_TOKEN;
             }
         }
+        return EOF_TOKEN;
     }
 
     scanner::token scanner::read_symbol() {

src/smt/tactic/smt_tactic.cpp

@@ -199,6 +199,7 @@ public:
                   tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n";
                   tout << "params_ref: " << m_params_ref << "\n";
                   tout << "nnf: " << fparams().m_nnf_cnf << "\n";);
+            TRACE("smt_tactic_params", m_params.display(tout););
             TRACE("smt_tactic_detail", in->display(tout););
             TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);
             scoped_init_ctx  init(*this, m);

src/solver/solver_na2as.cpp

@@ -62,6 +62,7 @@ struct append_assumptions {
 
 lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) {
     append_assumptions app(m_assumptions, num_assumptions, assumptions);
+    TRACE("solver_na2as", display(tout););
     return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr());
 }
 

src/tactic/arith/purify_arith_tactic.cpp

@@ -410,14 +410,12 @@ struct purify_arith_proc {
             expr * x = args[0];
             expr * zero = u().mk_numeral(rational(0), is_int);
             expr * one  = u().mk_numeral(rational(1), is_int);
-            if (y.is_zero() && complete()) {
+            if (y.is_zero()) {
                 // (^ x 0) --> k  |  x != 0 implies k = 1,   x = 0 implies k = 0^0 
                 push_cnstr(OR(EQ(x, zero), EQ(k, one)));
                 push_cnstr_pr(result_pr);
-                if (complete()) {
+                push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real())));
-                    push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real())));
+                push_cnstr_pr(result_pr);
-                    push_cnstr_pr(result_pr);
-                }
             }
             else if (!is_int) {
                 SASSERT(!y.is_int());