mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

add solver object to get_implied_equalities

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-12-11 10:53:21 -08:00
parent 01826fa8c9
commit b6459a8a92
4 changed files with 29 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/api_solver_old.cpp
View file

@ -24,6 +24,7 @@ Revision History:
#include"api_model.h" #include"api_model.h"
#include"smt_implied_equalities.h" #include"smt_implied_equalities.h"
#include"cancel_eh.h" #include"cancel_eh.h"
#include"api_solver.h"
extern "C" { extern "C" {
@ -113,14 +114,16 @@ extern "C" {
} }
Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c, Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c,
Z3_solver s,
unsigned num_terms, unsigned num_terms,
Z3_ast const terms[], Z3_ast const terms[],
unsigned class_ids[]) { unsigned class_ids[]) {
Z3_TRY; 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(); RESET_ERROR_CODE();
CHECK_SEARCHING(c); 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<Z3_lbool>(result); return static_cast<Z3_lbool>(result);
Z3_CATCH_RETURN(Z3_L_UNDEF); Z3_CATCH_RETURN(Z3_L_UNDEF);
} }

7
src/api/z3_api.h
View file

@ -7123,18 +7123,19 @@ END_MLAPI_EXCLUDE
This means that two terms map to the same class identifier if and only if This means that two terms map to the same class identifier if and only if
the current context implies that they are equal. 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. The function return Z3_L_FALSE if the current assertions are not satisfiable.
\sa Z3_check_and_get_model \sa Z3_check_and_get_model
\sa Z3_check \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( Z3_lbool Z3_API Z3_get_implied_equalities(
__in Z3_context c, __in Z3_context c,
__in Z3_solver s,
__in unsigned num_terms, __in unsigned num_terms,
__in_ecount(num_terms) Z3_ast const terms[], __in_ecount(num_terms) Z3_ast const terms[],
__out_ecount(num_terms) unsigned class_ids[] __out_ecount(num_terms) unsigned class_ids[]

32
src/smt/smt_implied_equalities.cpp
View file

@ -21,23 +21,21 @@ Revision History:
#include "smt_implied_equalities.h" #include "smt_implied_equalities.h"
#include "union_find.h" #include "union_find.h"
#include "cmd_context.h"
#include "parametric_cmd.h"
#include "ast_pp.h" #include "ast_pp.h"
#include "arith_decl_plugin.h"
#include "datatype_decl_plugin.h"
#include "array_decl_plugin.h" #include "array_decl_plugin.h"
#include "uint_set.h" #include "uint_set.h"
#include "model_v2_pp.h"
#include "smt_value_sort.h" #include "smt_value_sort.h"
#include "model_smt2_pp.h"
#include "stopwatch.h"
#include "model.h"
#include "solver.h"
namespace smt { namespace smt {
class get_implied_equalities_impl { class get_implied_equalities_impl {
ast_manager& m; ast_manager& m;
smt::kernel& m_solver; solver& m_solver;
union_find_default_ctx m_df; union_find_default_ctx m_df;
union_find<union_find_default_ctx> m_uf; union_find<union_find_default_ctx> m_uf;
array_util m_array_util; array_util m_array_util;
@ -98,7 +96,7 @@ namespace smt {
++m_stats_calls; ++m_stats_calls;
m_solver.push(); m_solver.push();
m_solver.assert_expr(m.mk_not(m.mk_eq(s, t))); 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_solver.pop(1);
TRACE("get_implied_equalities", tout << mk_pp(t, m) << " = " << mk_pp(s, m) << " " << (is_eq?"eq":"unrelated") << "\n";); TRACE("get_implied_equalities", tout << mk_pp(t, m) << " = " << mk_pp(s, m) << " " << (is_eq?"eq":"unrelated") << "\n";);
if (is_eq) { if (is_eq) {
@ -125,7 +123,7 @@ namespace smt {
m_stats_timer.start(); m_stats_timer.start();
m_solver.push(); m_solver.push();
m_solver.assert_expr(m.mk_not(m.mk_eq(s, t))); 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_solver.pop(1);
m_stats_timer.stop(); m_stats_timer.stop();
TRACE("get_implied_equalities", tout << mk_pp(t, m) << " = " << mk_pp(s, m) << " " << (is_eq?"eq":"unrelated") << "\n";); 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()); terms[i].term = m.mk_app(m_array_util.get_family_id(), OP_SELECT, 0, 0, args.size(), args.c_ptr());
} }
assert_relevant(terms); assert_relevant(terms);
lbool is_sat = m_solver.check(); lbool is_sat = m_solver.check_sat(0,0);
model_ref model1; model_ref model1;
m_solver.get_model(model1); m_solver.get_model(model1);
SASSERT(model1.get()); SASSERT(model1.get());
@ -218,7 +216,7 @@ namespace smt {
expr* s = terms[vec[j]].term; expr* s = terms[vec[j]].term;
m_solver.push(); m_solver.push();
m_solver.assert_expr(m.mk_not(m.mk_eq(t, s))); 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); m_solver.pop(1);
TRACE("get_implied_equalities", tout << mk_pp(t, m) << " = " << mk_pp(s, m) << " " << is_sat << "\n";); TRACE("get_implied_equalities", tout << mk_pp(t, m) << " = " << mk_pp(s, m) << " " << is_sat << "\n";);
if (is_sat == l_false) { if (is_sat == l_false) {
@ -237,7 +235,7 @@ namespace smt {
if (!non_values.empty()) { 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_filter_basic(non_values, terms);
//get_implied_equalities_basic(terms); //get_implied_equalities_basic(terms);
} }
@ -321,7 +319,7 @@ namespace smt {
public: 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) { lbool operator()(unsigned num_terms, expr* const* terms, unsigned* class_ids) {
params_ref p; params_ref p;
@ -338,7 +336,7 @@ namespace smt {
m_solver.push(); m_solver.push();
assert_relevant(num_terms, terms); 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) { if (is_sat != l_false) {
model_ref model; model_ref model;
@ -374,8 +372,8 @@ namespace smt {
stopwatch get_implied_equalities_impl::s_timer; stopwatch get_implied_equalities_impl::s_timer;
stopwatch get_implied_equalities_impl::s_stats_val_eq_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) { lbool implied_equalities(ast_manager& m, solver& solver, unsigned num_terms, expr* const* terms, unsigned* class_ids) {
get_implied_equalities_impl gi(solver); get_implied_equalities_impl gi(m, solver);
return gi(num_terms, terms, class_ids); 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_implies(eq_lit, eq));
} }
m_solver.assert_expr(m.mk_not(m.mk_and(eqs.size(), eqs.c_ptr()))); 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) { switch(is_sat) {
case l_false: case l_false:
for (unsigned i = 0; i + 1 < terms.size(); ++i) { for (unsigned i = 0; i + 1 < terms.size(); ++i) {

7
src/smt/smt_implied_equalities.h
View file

@ -23,13 +23,16 @@ Revision History:
#ifndef __SMT_IMPLIED_EQUALITIES_H__ #ifndef __SMT_IMPLIED_EQUALITIES_H__
#define __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 { namespace smt {
lbool implied_equalities( lbool implied_equalities(
kernel & solver, ast_manager & m,
solver & solver,
unsigned num_terms, expr* const* terms, unsigned num_terms, expr* const* terms,
unsigned* class_ids); unsigned* class_ids);