mirror of
https://github.com/Z3Prover/z3
synced 2025-04-30 20:35:51 +00:00
merged
This commit is contained in:
Leonardo de Moura
commit
bfe6678ad2
5 changed files with 30 additions and 25 deletions
|
|
@ -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<Z3_lbool>(result);
|
||||
Z3_CATCH_RETURN(Z3_L_UNDEF);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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[]
|
||||
|
|
|
|||
|
|
@ -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;}
|
||||
|
||||
|
|
|
|||
|
|
@ -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<union_find_default_ctx> 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) {
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue