From 730801e2f01a71cc184008506789d8444eca5b8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Dec 2012 21:21:02 -0800 Subject: [PATCH 1/2] fix unintialized variable Signed-off-by: Nikolaj Bjorner --- src/muz_qe/qe_lite.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index 3e15818e4..cced1ed50 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -578,7 +578,7 @@ namespace eq { } public: - der(ast_manager & m): m(m), a(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m) {} + der(ast_manager & m): m(m), a(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m), m_cancel(false) {} void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} From b6459a8a92a347ec326e07052e5220406fb8a2f2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Dec 2012 10:53:21 -0800 Subject: [PATCH 2/2] add solver object to get_implied_equalities Signed-off-by: Nikolaj Bjorner --- src/api/api_solver_old.cpp | 7 +++++-- src/api/z3_api.h | 7 ++++--- src/smt/smt_implied_equalities.cpp | 32 ++++++++++++++---------------- src/smt/smt_implied_equalities.h | 7 +++++-- 4 files changed, 29 insertions(+), 24 deletions(-) diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index cd4b797e3..d43e103c2 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -24,6 +24,7 @@ Revision History: #include"api_model.h" #include"smt_implied_equalities.h" #include"cancel_eh.h" +#include"api_solver.h" extern "C" { @@ -113,14 +114,16 @@ extern "C" { } Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c, + Z3_solver s, unsigned num_terms, Z3_ast const terms[], unsigned class_ids[]) { Z3_TRY; - LOG_Z3_get_implied_equalities(c, num_terms, terms, class_ids); + LOG_Z3_get_implied_equalities(c, s, num_terms, terms, class_ids); + ast_manager& m = mk_c(c)->m(); RESET_ERROR_CODE(); CHECK_SEARCHING(c); - lbool result = smt::implied_equalities(mk_c(c)->get_smt_kernel(), num_terms, to_exprs(terms), class_ids); + lbool result = smt::implied_equalities(m, *to_solver_ref(s), num_terms, to_exprs(terms), class_ids); return static_cast(result); Z3_CATCH_RETURN(Z3_L_UNDEF); } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 49d59e125..e12ce3591 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -7123,18 +7123,19 @@ END_MLAPI_EXCLUDE This means that two terms map to the same class identifier if and only if the current context implies that they are equal. - A side-effect of the function is a satisfiability check. + A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in. The function return Z3_L_FALSE if the current assertions are not satisfiable. \sa Z3_check_and_get_model \sa Z3_check - \deprecated Subsumed by Z3_solver API + \deprecated To be moved outside of API. - def_API('Z3_get_implied_equalities', UINT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _out_array(1, UINT))) + def_API('Z3_get_implied_equalities', UINT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT))) */ Z3_lbool Z3_API Z3_get_implied_equalities( __in Z3_context c, + __in Z3_solver s, __in unsigned num_terms, __in_ecount(num_terms) Z3_ast const terms[], __out_ecount(num_terms) unsigned class_ids[] diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp index c6f28d4b2..70229ccab 100644 --- a/src/smt/smt_implied_equalities.cpp +++ b/src/smt/smt_implied_equalities.cpp @@ -21,23 +21,21 @@ Revision History: #include "smt_implied_equalities.h" #include "union_find.h" -#include "cmd_context.h" -#include "parametric_cmd.h" #include "ast_pp.h" -#include "arith_decl_plugin.h" -#include "datatype_decl_plugin.h" #include "array_decl_plugin.h" #include "uint_set.h" -#include "model_v2_pp.h" #include "smt_value_sort.h" - +#include "model_smt2_pp.h" +#include "stopwatch.h" +#include "model.h" +#include "solver.h" namespace smt { class get_implied_equalities_impl { ast_manager& m; - smt::kernel& m_solver; + solver& m_solver; union_find_default_ctx m_df; union_find m_uf; array_util m_array_util; @@ -98,7 +96,7 @@ namespace smt { ++m_stats_calls; m_solver.push(); m_solver.assert_expr(m.mk_not(m.mk_eq(s, t))); - bool is_eq = l_false == m_solver.check(); + bool is_eq = l_false == m_solver.check_sat(0,0); m_solver.pop(1); TRACE("get_implied_equalities", tout << mk_pp(t, m) << " = " << mk_pp(s, m) << " " << (is_eq?"eq":"unrelated") << "\n";); if (is_eq) { @@ -125,7 +123,7 @@ namespace smt { m_stats_timer.start(); m_solver.push(); m_solver.assert_expr(m.mk_not(m.mk_eq(s, t))); - bool is_eq = l_false == m_solver.check(); + bool is_eq = l_false == m_solver.check_sat(0,0); m_solver.pop(1); m_stats_timer.stop(); TRACE("get_implied_equalities", tout << mk_pp(t, m) << " = " << mk_pp(s, m) << " " << (is_eq?"eq":"unrelated") << "\n";); @@ -168,7 +166,7 @@ namespace smt { terms[i].term = m.mk_app(m_array_util.get_family_id(), OP_SELECT, 0, 0, args.size(), args.c_ptr()); } assert_relevant(terms); - lbool is_sat = m_solver.check(); + lbool is_sat = m_solver.check_sat(0,0); model_ref model1; m_solver.get_model(model1); SASSERT(model1.get()); @@ -218,7 +216,7 @@ namespace smt { expr* s = terms[vec[j]].term; m_solver.push(); m_solver.assert_expr(m.mk_not(m.mk_eq(t, s))); - lbool is_sat = m_solver.check(); + lbool is_sat = m_solver.check_sat(0,0); m_solver.pop(1); TRACE("get_implied_equalities", tout << mk_pp(t, m) << " = " << mk_pp(s, m) << " " << is_sat << "\n";); if (is_sat == l_false) { @@ -237,7 +235,7 @@ namespace smt { if (!non_values.empty()) { - TRACE("get_implied_equalities", model_v2_pp(tout, *model, true);); + TRACE("get_implied_equalities", model_smt2_pp(tout, m, *model, 0);); get_implied_equalities_filter_basic(non_values, terms); //get_implied_equalities_basic(terms); } @@ -321,7 +319,7 @@ namespace smt { public: - get_implied_equalities_impl(smt::kernel& s) : m(s.m()), m_solver(s), m_uf(m_df), m_array_util(m), m_stats_calls(0) {} + get_implied_equalities_impl(ast_manager& m, solver& s) : m(m), m_solver(s), m_uf(m_df), m_array_util(m), m_stats_calls(0) {} lbool operator()(unsigned num_terms, expr* const* terms, unsigned* class_ids) { params_ref p; @@ -338,7 +336,7 @@ namespace smt { m_solver.push(); assert_relevant(num_terms, terms); - lbool is_sat = m_solver.check(); + lbool is_sat = m_solver.check_sat(0,0); if (is_sat != l_false) { model_ref model; @@ -374,8 +372,8 @@ namespace smt { stopwatch get_implied_equalities_impl::s_timer; stopwatch get_implied_equalities_impl::s_stats_val_eq_timer; - lbool implied_equalities(smt::kernel& solver, unsigned num_terms, expr* const* terms, unsigned* class_ids) { - get_implied_equalities_impl gi(solver); + lbool implied_equalities(ast_manager& m, solver& solver, unsigned num_terms, expr* const* terms, unsigned* class_ids) { + get_implied_equalities_impl gi(m, solver); return gi(num_terms, terms, class_ids); } }; @@ -552,7 +550,7 @@ namespace smt { m_solver.assert_expr(m.mk_implies(eq_lit, eq)); } m_solver.assert_expr(m.mk_not(m.mk_and(eqs.size(), eqs.c_ptr()))); - lbool is_sat = m_solver.check(); + lbool is_sat = m_solver.check_sat(0,0); switch(is_sat) { case l_false: for (unsigned i = 0; i + 1 < terms.size(); ++i) { diff --git a/src/smt/smt_implied_equalities.h b/src/smt/smt_implied_equalities.h index 6fc002ff1..ec9b4bd21 100644 --- a/src/smt/smt_implied_equalities.h +++ b/src/smt/smt_implied_equalities.h @@ -23,13 +23,16 @@ Revision History: #ifndef __SMT_IMPLIED_EQUALITIES_H__ #define __SMT_IMPLIED_EQUALITIES_H__ -#include"smt_kernel.h" +#include"smt_solver.h" +#include"lbool.h" +#include"ast.h" namespace smt { lbool implied_equalities( - kernel & solver, + ast_manager & m, + solver & solver, unsigned num_terms, expr* const* terms, unsigned* class_ids);