mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
87989dd93e
13 changed files with 361 additions and 76 deletions
|
|
@ -305,16 +305,23 @@ namespace qe {
|
|||
SASSERT(!contains_x(t));
|
||||
|
||||
if (s == m_var->x()) {
|
||||
expr_ref result(s, m);
|
||||
expr_ref result(t, m);
|
||||
expr_ref_vector args(m);
|
||||
sort* range = get_array_range(m.get_sort(s));
|
||||
for (unsigned i = 0; i < idxs.size(); ++i) {
|
||||
app_ref var(m);
|
||||
app_ref var(m), sel(m);
|
||||
expr_ref val(m);
|
||||
var = m.mk_fresh_const("value", range);
|
||||
vars.push_back(var);
|
||||
args.reset();
|
||||
args.push_back(result);
|
||||
|
||||
args.push_back (s);
|
||||
args.append(idxs[i].m_values.size(), idxs[i].m_vars);
|
||||
sel = a.mk_select (args.size (), args.c_ptr ());
|
||||
VERIFY (model.eval (sel, val));
|
||||
model.register_decl (var->get_decl (), val);
|
||||
|
||||
args[0] = result;
|
||||
args.push_back(var);
|
||||
result = a.mk_store(args.size(), args.c_ptr());
|
||||
}
|
||||
|
|
@ -390,15 +397,15 @@ namespace qe {
|
|||
}
|
||||
|
||||
lbool compare(expr* val1, expr* val2) {
|
||||
if (val1 == val2) {
|
||||
return l_true;
|
||||
}
|
||||
if (m.are_equal (val1, val2)) return l_true;
|
||||
if (m.are_distinct (val1, val2)) return l_false;
|
||||
|
||||
if (is_uninterp(val1) ||
|
||||
is_uninterp(val2)) {
|
||||
// TBD chase definition of nested array.
|
||||
return l_undef;
|
||||
}
|
||||
return l_true;
|
||||
return l_undef;
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -134,9 +134,7 @@ class mbp::impl {
|
|||
expr* e = lits[i].get(), *l, *r;
|
||||
if (m.is_eq(e, l, r) && reduce_eq(is_var, l, r, v, t)) {
|
||||
reduced = true;
|
||||
lits[i] = lits.back();
|
||||
lits.pop_back();
|
||||
--i;
|
||||
project_plugin::erase(lits, i);
|
||||
expr_safe_replace sub(m);
|
||||
sub.insert(v, t);
|
||||
is_rem.mark(v);
|
||||
|
|
@ -148,12 +146,16 @@ class mbp::impl {
|
|||
}
|
||||
}
|
||||
if (reduced) {
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
if (is_rem.is_marked(vars[i].get())) {
|
||||
vars[i] = vars.back();
|
||||
vars.pop_back();
|
||||
if (!is_rem.is_marked(vars[i].get())) {
|
||||
if (i != j) {
|
||||
vars[j] = vars[i].get();
|
||||
}
|
||||
++j;
|
||||
}
|
||||
}
|
||||
vars.shrink(j);
|
||||
}
|
||||
return reduced;
|
||||
}
|
||||
|
|
@ -333,9 +335,7 @@ public:
|
|||
sub(fmls[i].get(), tmp);
|
||||
rw(tmp);
|
||||
if (m.is_true(tmp)) {
|
||||
fmls[i] = fmls.back();
|
||||
fmls.pop_back();
|
||||
--i;
|
||||
project_plugin::erase(fmls, i);
|
||||
}
|
||||
else {
|
||||
fmls[i] = tmp;
|
||||
|
|
|
|||
|
|
@ -500,40 +500,40 @@ namespace qe {
|
|||
}
|
||||
}
|
||||
|
||||
class kernel {
|
||||
ast_manager& m;
|
||||
smt_params m_smtp;
|
||||
smt::kernel m_kernel;
|
||||
|
||||
public:
|
||||
kernel(ast_manager& m):
|
||||
m(m),
|
||||
m_kernel(m, m_smtp)
|
||||
{
|
||||
m_smtp.m_model = true;
|
||||
m_smtp.m_relevancy_lvl = 0;
|
||||
m_smtp.m_case_split_strategy = CS_ACTIVITY_WITH_CACHE;
|
||||
class kernel {
|
||||
ast_manager& m;
|
||||
smt_params m_smtp;
|
||||
smt::kernel m_kernel;
|
||||
|
||||
public:
|
||||
kernel(ast_manager& m):
|
||||
m(m),
|
||||
m_kernel(m, m_smtp)
|
||||
{
|
||||
m_smtp.m_model = true;
|
||||
m_smtp.m_relevancy_lvl = 0;
|
||||
m_smtp.m_case_split_strategy = CS_ACTIVITY_WITH_CACHE;
|
||||
}
|
||||
|
||||
smt::kernel& k() { return m_kernel; }
|
||||
smt::kernel const& k() const { return m_kernel; }
|
||||
|
||||
void assert_expr(expr* e) {
|
||||
m_kernel.assert_expr(e);
|
||||
}
|
||||
|
||||
void get_core(expr_ref_vector& core) {
|
||||
unsigned sz = m_kernel.get_unsat_core_size();
|
||||
core.reset();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
core.push_back(m_kernel.get_unsat_core_expr(i));
|
||||
}
|
||||
|
||||
smt::kernel& k() { return m_kernel; }
|
||||
smt::kernel const& k() const { return m_kernel; }
|
||||
|
||||
void assert_expr(expr* e) {
|
||||
m_kernel.assert_expr(e);
|
||||
}
|
||||
|
||||
void get_core(expr_ref_vector& core) {
|
||||
unsigned sz = m_kernel.get_unsat_core_size();
|
||||
core.reset();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
core.push_back(m_kernel.get_unsat_core_expr(i));
|
||||
}
|
||||
TRACE("qe", tout << "core: " << core << "\n";
|
||||
m_kernel.display(tout);
|
||||
tout << "\n";
|
||||
);
|
||||
}
|
||||
};
|
||||
TRACE("qe", tout << "core: " << core << "\n";
|
||||
m_kernel.display(tout);
|
||||
tout << "\n";
|
||||
);
|
||||
}
|
||||
};
|
||||
|
||||
class qsat : public tactic {
|
||||
|
||||
|
|
@ -1168,6 +1168,7 @@ namespace qe {
|
|||
pred_abs m_pred_abs;
|
||||
qe::mbp m_mbp;
|
||||
kernel m_kernel;
|
||||
vector<app_ref_vector> m_vars;
|
||||
|
||||
imp(ast_manager& m):
|
||||
m(m),
|
||||
|
|
@ -1180,14 +1181,36 @@ namespace qe {
|
|||
m_fmls.push_back(e);
|
||||
}
|
||||
|
||||
lbool check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t) {
|
||||
lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
|
||||
// Assume this is the only call to check.
|
||||
expr_ref_vector defs(m);
|
||||
app_ref_vector free_vars(m), vars1(m);
|
||||
expr_ref fml = mk_and(m_fmls);
|
||||
m_pred_abs.get_free_vars(fml, free_vars);
|
||||
m_pred_abs.abstract_atoms(fml, defs);
|
||||
fml = m_pred_abs.mk_abstract(fml);
|
||||
m_kernel.assert_expr(mk_and(defs));
|
||||
m_kernel.assert_expr(fml);
|
||||
obj_hashtable<app> var_set;
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
var_set.insert(vars[i]);
|
||||
}
|
||||
for (unsigned i = 0; i < free_vars.size(); ++i) {
|
||||
app* v = free_vars[i].get();
|
||||
if (!var_set.contains(v)) {
|
||||
vars1.push_back(v);
|
||||
}
|
||||
}
|
||||
bool is_m = is_max[0];
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
if (is_m != is_max[i]) {
|
||||
m_vars.push_back(vars1);
|
||||
vars1.reset();
|
||||
is_m = is_max[i];
|
||||
}
|
||||
vars1.push_back(vars[i]);
|
||||
}
|
||||
|
||||
// TBD
|
||||
|
||||
return l_undef;
|
||||
|
|
@ -1212,7 +1235,7 @@ namespace qe {
|
|||
}
|
||||
}
|
||||
|
||||
lbool min_max_opt::check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t) {
|
||||
lbool min_max_opt::check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
|
||||
return m_imp->check(is_max, vars, t);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -121,7 +121,7 @@ namespace qe {
|
|||
~min_max_opt();
|
||||
void add(expr* e);
|
||||
void add(expr_ref_vector const& fmls);
|
||||
lbool check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t);
|
||||
lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t);
|
||||
};
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -91,6 +91,25 @@ bool proto_model::is_select_of_model_value(expr* e) const {
|
|||
has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0))));
|
||||
}
|
||||
|
||||
bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
|
||||
m_eval.set_model_completion(model_completion);
|
||||
try {
|
||||
m_eval(e, result);
|
||||
#if 0
|
||||
std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n";
|
||||
#endif
|
||||
return true;
|
||||
}
|
||||
catch (model_evaluator_exception & ex) {
|
||||
(void)ex;
|
||||
TRACE("model_evaluator", tout << ex.msg() << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
/**
|
||||
\brief Evaluate the expression e in the current model, and store the result in \c result.
|
||||
It returns \c true if succeeded, and false otherwise. If the evaluation fails,
|
||||
|
|
@ -101,18 +120,7 @@ bool proto_model::is_select_of_model_value(expr* e) const {
|
|||
declaration it will build one for it. Moreover, partial functions will also be completed.
|
||||
So, if model_completion == true, the evaluator never fails if it doesn't contain quantifiers.
|
||||
*/
|
||||
bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
|
||||
m_eval.set_model_completion(model_completion);
|
||||
try {
|
||||
m_eval(e, result);
|
||||
return true;
|
||||
}
|
||||
catch (model_evaluator_exception & ex) {
|
||||
(void)ex;
|
||||
TRACE("model_evaluator", tout << ex.msg() << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Replace uninterpreted constants occurring in fi->get_else()
|
||||
|
|
@ -429,3 +437,245 @@ model * proto_model::mk_model() {
|
|||
|
||||
return m;
|
||||
}
|
||||
|
||||
|
||||
#if 0
|
||||
|
||||
#include"simplifier.h"
|
||||
#include"basic_simplifier_plugin.h"
|
||||
|
||||
// Auxiliary function for computing fi(args[0], ..., args[fi.get_arity() - 1]).
|
||||
// The result is stored in result.
|
||||
// Return true if succeeded, and false otherwise.
|
||||
// It uses the simplifier s during the computation.
|
||||
bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & result) {
|
||||
bool actuals_are_values = true;
|
||||
|
||||
if (fi.num_entries() != 0) {
|
||||
for (unsigned i = 0; actuals_are_values && i < fi.get_arity(); i++) {
|
||||
actuals_are_values = fi.m().is_value(args[i]);
|
||||
}
|
||||
}
|
||||
|
||||
func_entry * entry = fi.get_entry(args);
|
||||
if (entry != 0) {
|
||||
result = entry->get_result();
|
||||
return true;
|
||||
}
|
||||
|
||||
TRACE("func_interp", tout << "failed to find entry for: ";
|
||||
for(unsigned i = 0; i < fi.get_arity(); i++)
|
||||
tout << mk_pp(args[i], fi.m()) << " ";
|
||||
tout << "\nis partial: " << fi.is_partial() << "\n";);
|
||||
|
||||
if (!fi.eval_else(args, result)) {
|
||||
return false;
|
||||
}
|
||||
|
||||
if (actuals_are_values && fi.args_are_values()) {
|
||||
// cheap case... we are done
|
||||
return true;
|
||||
}
|
||||
|
||||
// build symbolic result... the actuals may be equal to the args of one of the entries.
|
||||
basic_simplifier_plugin * bs = static_cast<basic_simplifier_plugin*>(s.get_plugin(fi.m().get_basic_family_id()));
|
||||
for (unsigned k = 0; k < fi.num_entries(); k++) {
|
||||
func_entry const * curr = fi.get_entry(k);
|
||||
SASSERT(!curr->eq_args(fi.m(), fi.get_arity(), args));
|
||||
if (!actuals_are_values || !curr->args_are_values()) {
|
||||
expr_ref_buffer eqs(fi.m());
|
||||
unsigned i = fi.get_arity();
|
||||
while (i > 0) {
|
||||
--i;
|
||||
expr_ref new_eq(fi.m());
|
||||
bs->mk_eq(curr->get_arg(i), args[i], new_eq);
|
||||
eqs.push_back(new_eq);
|
||||
}
|
||||
SASSERT(eqs.size() == fi.get_arity());
|
||||
expr_ref new_cond(fi.m());
|
||||
bs->mk_and(eqs.size(), eqs.c_ptr(), new_cond);
|
||||
bs->mk_ite(new_cond, curr->get_result(), result, result);
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
|
||||
bool is_ok = true;
|
||||
SASSERT(is_well_sorted(m_manager, e));
|
||||
TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n";
|
||||
tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";);
|
||||
|
||||
obj_map<expr, expr*> eval_cache;
|
||||
expr_ref_vector trail(m_manager);
|
||||
sbuffer<std::pair<expr*, expr*>, 128> todo;
|
||||
ptr_buffer<expr> args;
|
||||
expr * null = static_cast<expr*>(0);
|
||||
todo.push_back(std::make_pair(e, null));
|
||||
|
||||
simplifier m_simplifier(m_manager);
|
||||
|
||||
expr * a;
|
||||
expr * expanded_a;
|
||||
while (!todo.empty()) {
|
||||
std::pair<expr *, expr *> & p = todo.back();
|
||||
a = p.first;
|
||||
expanded_a = p.second;
|
||||
if (expanded_a != 0) {
|
||||
expr * r = 0;
|
||||
eval_cache.find(expanded_a, r);
|
||||
SASSERT(r != 0);
|
||||
todo.pop_back();
|
||||
eval_cache.insert(a, r);
|
||||
TRACE("model_eval",
|
||||
tout << "orig:\n" << mk_pp(a, m_manager) << "\n";
|
||||
tout << "after beta reduction:\n" << mk_pp(expanded_a, m_manager) << "\n";
|
||||
tout << "new:\n" << mk_pp(r, m_manager) << "\n";);
|
||||
}
|
||||
else {
|
||||
switch(a->get_kind()) {
|
||||
case AST_APP: {
|
||||
app * t = to_app(a);
|
||||
bool visited = true;
|
||||
args.reset();
|
||||
unsigned num_args = t->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
expr * arg = 0;
|
||||
if (!eval_cache.find(t->get_arg(i), arg)) {
|
||||
visited = false;
|
||||
todo.push_back(std::make_pair(t->get_arg(i), null));
|
||||
}
|
||||
else {
|
||||
args.push_back(arg);
|
||||
}
|
||||
}
|
||||
if (!visited) {
|
||||
continue;
|
||||
}
|
||||
SASSERT(args.size() == t->get_num_args());
|
||||
expr_ref new_t(m_manager);
|
||||
func_decl * f = t->get_decl();
|
||||
|
||||
if (!has_interpretation(f)) {
|
||||
// the model does not assign an interpretation to f.
|
||||
SASSERT(new_t.get() == 0);
|
||||
if (f->get_family_id() == null_family_id) {
|
||||
if (model_completion) {
|
||||
// create an interpretation for f.
|
||||
new_t = mk_some_interp_for(f);
|
||||
}
|
||||
else {
|
||||
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
|
||||
is_ok = false;
|
||||
}
|
||||
}
|
||||
if (new_t.get() == 0) {
|
||||
// t is interpreted or model completion is disabled.
|
||||
m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t);
|
||||
TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";);
|
||||
trail.push_back(new_t);
|
||||
if (!is_app(new_t) || to_app(new_t)->get_decl() != f || is_select_of_model_value(new_t)) {
|
||||
// if the result is not of the form (f ...), then assume we must simplify it.
|
||||
expr * new_new_t = 0;
|
||||
if (!eval_cache.find(new_t.get(), new_new_t)) {
|
||||
todo.back().second = new_t;
|
||||
todo.push_back(std::make_pair(new_t, null));
|
||||
continue;
|
||||
}
|
||||
else {
|
||||
new_t = new_new_t;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
// the model has an interpretaion for f.
|
||||
if (num_args == 0) {
|
||||
// t is a constant
|
||||
new_t = get_const_interp(f);
|
||||
}
|
||||
else {
|
||||
// t is a function application
|
||||
SASSERT(new_t.get() == 0);
|
||||
// try to use function graph first
|
||||
func_interp * fi = get_func_interp(f);
|
||||
SASSERT(fi->get_arity() == num_args);
|
||||
expr_ref r1(m_manager);
|
||||
// fi may be partial...
|
||||
if (!::eval(*fi, m_simplifier, args.c_ptr(), r1)) {
|
||||
SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial.
|
||||
if (model_completion) {
|
||||
expr * r = get_some_value(f->get_range());
|
||||
fi->set_else(r);
|
||||
SASSERT(!fi->is_partial());
|
||||
new_t = r;
|
||||
}
|
||||
else {
|
||||
// f is an uninterpreted function, there is no need to use m_simplifier.mk_app
|
||||
new_t = m_manager.mk_app(f, num_args, args.c_ptr());
|
||||
trail.push_back(new_t);
|
||||
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
|
||||
is_ok = false;
|
||||
}
|
||||
}
|
||||
else {
|
||||
SASSERT(r1);
|
||||
trail.push_back(r1);
|
||||
TRACE("model_eval", tout << mk_pp(a, m_manager) << "\nevaluates to: " << r1 << "\n";);
|
||||
expr * r2 = 0;
|
||||
if (!eval_cache.find(r1.get(), r2)) {
|
||||
todo.back().second = r1;
|
||||
todo.push_back(std::make_pair(r1, null));
|
||||
continue;
|
||||
}
|
||||
else {
|
||||
new_t = r2;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
TRACE("model_eval",
|
||||
tout << "orig:\n" << mk_pp(t, m_manager) << "\n";
|
||||
tout << "new:\n" << mk_pp(new_t, m_manager) << "\n";);
|
||||
todo.pop_back();
|
||||
SASSERT(new_t.get() != 0);
|
||||
eval_cache.insert(t, new_t);
|
||||
break;
|
||||
}
|
||||
case AST_VAR:
|
||||
SASSERT(a != 0);
|
||||
eval_cache.insert(a, a);
|
||||
todo.pop_back();
|
||||
break;
|
||||
case AST_QUANTIFIER:
|
||||
TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";);
|
||||
is_ok = false; // evaluator does not handle quantifiers.
|
||||
SASSERT(a != 0);
|
||||
eval_cache.insert(a, a);
|
||||
todo.pop_back();
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (!eval_cache.find(e, a)) {
|
||||
TRACE("model_eval", tout << "FAILED e: " << mk_bounded_pp(e, m_manager) << "\n";);
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
||||
result = a;
|
||||
std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n";
|
||||
TRACE("model_eval",
|
||||
ast_ll_pp(tout << "original: ", m_manager, e);
|
||||
ast_ll_pp(tout << "evaluated: ", m_manager, a);
|
||||
ast_ll_pp(tout << "reduced: ", m_manager, result.get());
|
||||
tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";
|
||||
);
|
||||
SASSERT(is_well_sorted(m_manager, result.get()));
|
||||
return is_ok;
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -1308,7 +1308,7 @@ namespace smt {
|
|||
if (!gcd_test())
|
||||
return FC_CONTINUE;
|
||||
|
||||
if (m_params.m_arith_euclidean_solver)
|
||||
if (m_params.m_arith_euclidean_solver || (0 == (1 + m_branch_cut_counter) % 80))
|
||||
apply_euclidean_solver();
|
||||
|
||||
if (get_context().inconsistent())
|
||||
|
|
|
|||
|
|
@ -22,6 +22,7 @@ Revision History:
|
|||
#include"solve_eqs_tactic.h"
|
||||
#include"elim_uncnstr_tactic.h"
|
||||
#include"qe_tactic.h"
|
||||
#include"qe_lite.h"
|
||||
#include"qsat.h"
|
||||
#include"nlqsat.h"
|
||||
#include"ctx_simplify_tactic.h"
|
||||
|
|
@ -61,6 +62,7 @@ static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) {
|
|||
|
||||
tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) {
|
||||
tactic * st = and_then(mk_no_solve_eq_preprocessor(m),
|
||||
mk_qe_lite_tactic(m, p),
|
||||
mk_smt_tactic());
|
||||
st->updt_params(p);
|
||||
return st;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue