3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00

add accessors for implied values to API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-28 19:46:39 -07:00
parent 4628cb8e79
commit 59d8895d15
23 changed files with 347 additions and 2 deletions

View file

@ -554,6 +554,39 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
Z3_ast Z3_API Z3_solver_get_implied_value(Z3_context c, Z3_solver s, Z3_ast e) {
Z3_TRY;
LOG_Z3_solver_get_implied_value(c, s, e);
RESET_ERROR_CODE();
init_solver(c, s);
expr_ref v = to_solver_ref(s)->get_implied_value(to_expr(e));
mk_c(c)->save_ast_trail(v);
RETURN_Z3(of_ast(v));
Z3_CATCH_RETURN(nullptr);
}
Z3_ast Z3_API Z3_solver_get_implied_lower(Z3_context c, Z3_solver s, Z3_ast e) {
Z3_TRY;
LOG_Z3_solver_get_implied_lower(c, s, e);
RESET_ERROR_CODE();
init_solver(c, s);
expr_ref v = to_solver_ref(s)->get_implied_lower_bound(to_expr(e));
mk_c(c)->save_ast_trail(v);
RETURN_Z3(of_ast(v));
Z3_CATCH_RETURN(nullptr);
}
Z3_ast Z3_API Z3_solver_get_implied_upper(Z3_context c, Z3_solver s, Z3_ast e) {
Z3_TRY;
LOG_Z3_solver_get_implied_upper(c, s, e);
RESET_ERROR_CODE();
init_solver(c, s);
expr_ref v = to_solver_ref(s)->get_implied_upper_bound(to_expr(e));
mk_c(c)->save_ast_trail(v);
RETURN_Z3(of_ast(v));
Z3_CATCH_RETURN(nullptr);
}
static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) {
for (unsigned i = 0; i < num_assumptions; i++) {
if (!is_expr(to_ast(assumptions[i]))) {

View file

@ -2379,12 +2379,25 @@ namespace z3 {
}
void add(expr const & e, char const * p) {
add(e, ctx().bool_const(p));
}
void add(expr_vector const& v) {
check_context(*this, v);
for (unsigned i = 0; i < v.size(); ++i)
add(v[i]);
}
// fails for some compilers:
// void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
expr lower(expr const& e) {
Z3_ast r = Z3_solver_get_implied_lower(ctx(), m_solver, e); check_error(); return expr(ctx(), r);
}
expr upper(expr const& e) {
Z3_ast r = Z3_solver_get_implied_upper(ctx(), m_solver, e); check_error(); return expr(ctx(), r);
}
expr value(expr const& e) {
Z3_ast r = Z3_solver_get_implied_value(ctx(), m_solver, e); check_error(); return expr(ctx(), r);
}
check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
check_result check(unsigned n, expr * const assumptions) {
array<Z3_ast> _assumptions(n);

View file

@ -6857,6 +6857,21 @@ class Solver(Z3PPObject):
"""
return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
def value(self, e):
"""Return value of term in solver, if any is given.
"""
return _to_expr_ref(Z3_solver_get_implied_value(self.ctx.ref(), self.solver, e.as_ast()), self.ctx)
def lower(self, e):
"""Return lower bound known to solver based on the last call.
"""
return _to_expr_ref(Z3_solver_get_implied_lower(self.ctx.ref(), self.solver, e.as_ast()), self.ctx)
def upper(self, e):
"""Return upper bound known to solver based on the last call.
"""
return _to_expr_ref(Z3_solver_get_implied_upper(self.ctx.ref(), self.solver, e.as_ast()), self.ctx)
def statistics(self):
"""Return statistics for the last `check()`.

View file

@ -6486,6 +6486,34 @@ extern "C" {
*/
void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[]);
/**
\brief retrieve implied value for expression, if any is implied by solver at search level.
The method works for expressions that are known to the solver state, such as Boolean and
arithmetical variables.
def_API('Z3_solver_get_implied_value', AST, (_in(CONTEXT), _in(SOLVER), _in(AST)))
*/
Z3_ast Z3_API Z3_solver_get_implied_value(Z3_context c, Z3_solver s, Z3_ast e);
/**
\brief retrieve implied lower bound value for arithmetic expression.
If a lower bound is implied at search level, the arithmetic expression returned
is a constant representing the bound.
def_API('Z3_solver_get_implied_lower', AST, (_in(CONTEXT), _in(SOLVER), _in(AST)))
*/
Z3_ast Z3_API Z3_solver_get_implied_lower(Z3_context c, Z3_solver s, Z3_ast e);
/**
\brief retrieve implied upper bound value for arithmetic expression.
If an upper bound is implied at search level, the arithmetic expression returned
is a constant representing the bound.
def_API('Z3_solver_get_implied_upper', AST, (_in(CONTEXT), _in(SOLVER), _in(AST)))
*/
Z3_ast Z3_API Z3_solver_get_implied_upper(Z3_context c, Z3_solver s, Z3_ast e);
/**
\brief Check whether the assertions in a given solver are consistent or not.

View file

@ -123,6 +123,9 @@ public:
expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override { m_solver.get_levels(vars, depth); }
expr_ref_vector get_trail() override { return m_solver.get_trail(); }
expr_ref get_implied_value(expr* e) override { return m_solver.get_implied_value(e); }
expr_ref get_implied_lower_bound(expr* e) override { return m_solver.get_implied_lower_bound(e); }
expr_ref get_implied_upper_bound(expr* e) override { return m_solver.get_implied_upper_bound(e); }
void push() override;
void pop(unsigned n) override;

View file

@ -111,6 +111,9 @@ namespace opt {
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override;
expr_ref_vector get_trail() override { return m_context.get_trail(); }
expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
expr_ref get_implied_value(expr* e) override { return m_context.get_implied_value(e); }
expr_ref get_implied_lower_bound(expr* e) override { return m_context.get_implied_lower_bound(e); }
expr_ref get_implied_upper_bound(expr* e) override { return m_context.get_implied_upper_bound(e); }
void set_logic(symbol const& logic);

View file

@ -363,6 +363,19 @@ public:
return nullptr;
}
// TODO
expr_ref get_implied_value(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_lower_bound(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_upper_bound(expr* e) override {
return expr_ref(e, m);
}
expr_ref_vector last_cube(bool is_sat) {
expr_ref_vector result(m);
result.push_back(is_sat ? m.mk_true() : m.mk_false());

View file

@ -125,9 +125,37 @@ namespace smt {
return false;
}
expr_ref arith_value::get_lo(expr* e) const {
rational lo;
bool s = false;
if (a.is_int_real(e) && get_lo(e, lo, s) && !s) {
return expr_ref(a.mk_numeral(lo, m.get_sort(e)), m);
}
return expr_ref(e, m);
}
expr_ref arith_value::get_up(expr* e) const {
rational up;
bool s = false;
if (a.is_int_real(e) && get_up(e, up, s) && !s) {
return expr_ref(a.mk_numeral(up, m.get_sort(e)), m);
}
return expr_ref(e, m);
}
expr_ref arith_value::get_fixed(expr* e) const {
rational lo, up;
bool s = false;
if (a.is_int_real(e) && get_lo(e, lo, s) && !s && get_up(e, up, s) && !s && lo == up) {
return expr_ref(a.mk_numeral(lo, m.get_sort(e)), m);
}
return expr_ref(e, m);
}
final_check_status arith_value::final_check() {
family_id afid = a.get_family_id();
theory * th = m_ctx->get_theory(afid);
return th->final_check_eh();
}
};

View file

@ -42,6 +42,9 @@ namespace smt {
bool get_lo(expr* e, rational& lo, bool& strict) const;
bool get_up(expr* e, rational& up, bool& strict) const;
bool get_value(expr* e, rational& value) const;
expr_ref get_lo(expr* e) const;
expr_ref get_up(expr* e) const;
expr_ref get_fixed(expr* e) const;
final_check_status final_check();
};
};

View file

@ -39,6 +39,7 @@ Revision History:
#include "smt/smt_model_checker.h"
#include "smt/smt_model_finder.h"
#include "smt/smt_parallel.h"
#include "smt/smt_arith_value.h"
namespace smt {
@ -4555,6 +4556,48 @@ namespace smt {
TRACE("model", tout << *m_model << "\n";);
}
expr_ref context::get_implied_value(expr* e) {
pop_to_search_lvl();
if (m.is_bool(e)) {
if (b_internalized(e)) {
bool_var v = get_bool_var(e);
switch (get_assignment(get_bool_var(e))) {
case l_true: e = m.mk_true(); break;
case l_false: e = m.mk_false(); break;
default: break;
}
}
return expr_ref(e, m);
}
if (e_internalized(e)) {
enode* n = get_enode(e);
for (enode* r : *n) {
if (m.is_value(r->get_owner())) {
return expr_ref(r->get_owner(), m);
}
}
}
arith_value av(m);
av.init(this);
return av.get_fixed(e);
}
expr_ref context::get_implied_lower_bound(expr* e) {
pop_to_search_lvl();
arith_value av(m);
av.init(this);
return av.get_lo(e);
}
expr_ref context::get_implied_upper_bound(expr* e) {
pop_to_search_lvl();
arith_value av(m);
av.init(this);
return av.get_up(e);
}
};

View file

@ -580,6 +580,13 @@ namespace smt {
return get_bdata(v).get_theory();
}
expr_ref get_implied_value(expr* e);
expr_ref get_implied_lower_bound(expr* e);
expr_ref get_implied_upper_bound(expr* e);
friend class set_var_theory_trail;
void set_var_theory(bool_var v, theory_id tid);

View file

@ -131,6 +131,18 @@ namespace smt {
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
return m_kernel.find_mutexes(vars, mutexes);
}
expr_ref get_implied_value(expr* e) {
return m_kernel.get_implied_value(e);
}
expr_ref get_implied_lower_bound(expr* e) {
return m_kernel.get_implied_lower_bound(e);
}
expr_ref get_implied_upper_bound(expr* e) {
return m_kernel.get_implied_upper_bound(e);
}
void get_model(model_ref & m) {
m_kernel.get_model(m);
@ -412,5 +424,18 @@ namespace smt {
return m_imp->get_trail();
}
expr_ref kernel::get_implied_value(expr* e) {
return m_imp->get_implied_value(e);
}
expr_ref kernel::get_implied_lower_bound(expr* e) {
return m_imp->get_implied_lower_bound(e);
}
expr_ref kernel::get_implied_upper_bound(expr* e) {
return m_imp->get_implied_upper_bound(e);
}
};

View file

@ -218,6 +218,17 @@ namespace smt {
*/
expr_ref next_cube();
/**
\brief retrieve upper/lower bound for arithmetic term, if it is implied.
retrieve implied values if terms are fixed to a value.
*/
expr_ref get_implied_value(expr* e);
expr_ref get_implied_lower_bound(expr* e);
expr_ref get_implied_upper_bound(expr* e);
/**
\brief retrieve depth of variables from decision stack.
*/

View file

@ -361,6 +361,18 @@ namespace {
}
}
expr_ref get_implied_value(expr* e) override {
return m_context.get_implied_value(e);
}
expr_ref get_implied_lower_bound(expr* e) override {
return m_context.get_implied_lower_bound(e);
}
expr_ref get_implied_upper_bound(expr* e) override {
return m_context.get_implied_upper_bound(e);
}
bool fds_intersect(func_decl_set & pattern_fds, func_decl_set & assrtn_fds) {
for (func_decl * fd : pattern_fds) {
if (assrtn_fds.contains(fd))

View file

@ -1724,6 +1724,7 @@ public:
is_sat = make_feasible();
}
final_check_status st = FC_DONE;
switch (is_sat) {
case l_true:
TRACE("arith", /*display(tout);*/

View file

@ -184,6 +184,28 @@ public:
return m_solver1->get_scope_level();
}
expr_ref get_implied_value(expr* e) override {
if (m_use_solver1_results)
return m_solver1->get_implied_value(e);
else
return m_solver2->get_implied_value(e);
}
expr_ref get_implied_lower_bound(expr* e) override {
if (m_use_solver1_results)
return m_solver1->get_implied_lower_bound(e);
else
return m_solver2->get_implied_lower_bound(e);
}
expr_ref get_implied_upper_bound(expr* e) override {
if (m_use_solver1_results)
return m_solver1->get_implied_upper_bound(e);
else
return m_solver2->get_implied_upper_bound(e);
}
lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override {
switch_inc_mode();
m_use_solver1_results = false;

View file

@ -226,6 +226,19 @@ public:
virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) = 0;
/**
\brief retrieve fixed value assignment in current solver state, if it is implied.
*/
virtual expr_ref get_implied_value(expr* e) = 0;
/**
\brief retrieve upper/lower bound for arithmetic term, if it is implied.
*/
virtual expr_ref get_implied_lower_bound(expr* e) = 0;
virtual expr_ref get_implied_upper_bound(expr* e) = 0;
/**
\brief Display the content of this solver.
*/

View file

@ -127,6 +127,18 @@ public:
return m_base->get_trail();
}
expr_ref get_implied_value(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_lower_bound(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_upper_bound(expr* e) override {
return expr_ref(e, m);
}
lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
SASSERT(!m_pushed || get_scope_level() > 0);
m_proof.reset();

View file

@ -97,6 +97,17 @@ public:
throw default_exception("cannot retrieve trail from solvers created using tactcis");
}
expr_ref get_implied_value(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_lower_bound(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_upper_bound(expr* e) override {
return expr_ref(e, m);
}
};

View file

@ -361,6 +361,18 @@ private:
}
}
expr_ref get_implied_value(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_lower_bound(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_upper_bound(expr* e) override {
return expr_ref(e, m);
}
};
solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s) {

View file

@ -194,6 +194,18 @@ public:
return m_solver->get_assertion(idx);
}
expr_ref get_implied_value(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_lower_bound(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_upper_bound(expr* e) override {
return expr_ref(e, m);
}
};
solver * mk_enum2bv_solver(ast_manager & m, params_ref const & p, solver* s) {

View file

@ -147,6 +147,18 @@ public:
return m_solver->get_assertion(idx);
}
expr_ref get_implied_value(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_lower_bound(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_upper_bound(expr* e) override {
return expr_ref(e, m);
}
private:
void flush_assertions() const {

View file

@ -2103,6 +2103,19 @@ namespace smtfd {
expr * get_assertion(unsigned idx) const override {
return m_assertions.get(idx);
}
expr_ref get_implied_value(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_lower_bound(expr* e) override {
return expr_ref(e, m);
}
expr_ref get_implied_upper_bound(expr* e) override {
return expr_ref(e, m);
}
};
}