diff --git a/src/api/api_context.h b/src/api/api_context.h index 7cba15c44..d2c0b3ad4 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -245,7 +245,7 @@ inline api::context * mk_c(Z3_context c) { return reinterpret_castcheck_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); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index cf235b4af..b37dc12d7 100644 --- a/src/api/dotnet/Context.cs +++ b/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))); } + /// + /// Create an expression representing t[0] * t[1] * .... + /// + public ArithExpr MkMul(IEnumerable t) + { + Contract.Requires(t != null); + Contract.Requires(Contract.ForAll(t, a => a != null)); + Contract.Ensures(Contract.Result() != null); + + CheckContextMatch(t); + return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t))); + } + /// /// Create an expression representing t[0] - t[1] - .... /// diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index ce8834cc7..bc2feafed 100644 --- a/src/ast/macros/macro_util.cpp +++ b/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); } diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 9c200a3e2..cd6a63acc 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -39,7 +39,7 @@ void rewriter_tpl::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()) { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index f6c3582d4..3260f02b0 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/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); diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index baaaf7bb0..f2fbcf6d9 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/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); diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 99917fff8..29ce4864f 100644 --- a/src/solver/solver_na2as.cpp +++ b/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()); } diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 6affe2fa0..463e1a9e8 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/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_pr(result_pr); - } + 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); } else if (!is_int) { SASSERT(!y.is_int());