mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 19:05:51 +00:00
fix another bug uncovered by Dunlop, prepare grounds for equality solving within NNFs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
eaa80d5b02
commit
0b84c60886
13 changed files with 283 additions and 122 deletions
|
|
@ -65,7 +65,7 @@ public:
|
|||
for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, g.form(i));
|
||||
}
|
||||
const double total = ackr_helper::calculate_lemma_bound(p.m_fun2terms);
|
||||
TRACE("ackr_bound_probe", tout << "total=" << total << std::endl;);
|
||||
TRACE("ackermannize", tout << "total=" << total << std::endl;);
|
||||
return result(total);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -84,7 +84,7 @@ void ackr_model_converter::convert(model * source, model * destination) {
|
|||
}
|
||||
|
||||
void ackr_model_converter::convert_constants(model * source, model * destination) {
|
||||
TRACE("ackr_model", tout << "converting constants\n";);
|
||||
TRACE("ackermannize", tout << "converting constants\n";);
|
||||
obj_map<func_decl, func_interp*> interpretations;
|
||||
model_evaluator evaluator(*source);
|
||||
evaluator.set_model_completion(true);
|
||||
|
|
@ -113,7 +113,7 @@ void ackr_model_converter::convert_constants(model * source, model * destination
|
|||
void ackr_model_converter::add_entry(model_evaluator & evaluator,
|
||||
app* term, expr* value,
|
||||
obj_map<func_decl, func_interp*>& interpretations) {
|
||||
TRACE("ackr_model", tout << "add_entry"
|
||||
TRACE("ackermannize", tout << "add_entry"
|
||||
<< mk_ismt2_pp(term, m, 2)
|
||||
<< "->"
|
||||
<< mk_ismt2_pp(value, m, 2) << "\n";
|
||||
|
|
@ -137,7 +137,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
|
|||
args.push_back(std::move(arg_value));
|
||||
}
|
||||
if (fi->get_entry(args.c_ptr()) == nullptr) {
|
||||
TRACE("ackr_model",
|
||||
TRACE("ackermannize",
|
||||
tout << mk_ismt2_pp(declaration, m) << " args: " << std::endl;
|
||||
for (unsigned i = 0; i < args.size(); i++)
|
||||
tout << mk_ismt2_pp(args.get(i), m) << std::endl;
|
||||
|
|
@ -145,7 +145,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
|
|||
fi->insert_new_entry(args.c_ptr(), value);
|
||||
}
|
||||
else {
|
||||
TRACE("ackr_model", tout << "entry already present\n";);
|
||||
TRACE("ackermannize", tout << "entry already present\n";);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -56,7 +56,7 @@ lbool lackr::operator() () {
|
|||
if (!init()) return l_undef;
|
||||
const lbool rv = m_eager ? eager() : lazy();
|
||||
if (rv == l_true) m_sat->get_model(m_model);
|
||||
CTRACE("lackr", rv == l_true,
|
||||
CTRACE("ackermannize", rv == l_true,
|
||||
model_smt2_pp(tout << "abstr_model(\n", m_m, *(m_model.get()), 2); tout << ")\n"; );
|
||||
return rv;
|
||||
}
|
||||
|
|
@ -89,7 +89,7 @@ bool lackr::init() {
|
|||
// Introduce ackermann lemma for the two given terms.
|
||||
//
|
||||
bool lackr::ackr(app * const t1, app * const t2) {
|
||||
TRACE("lackr", tout << "ackr "
|
||||
TRACE("ackermannize", tout << "ackr "
|
||||
<< mk_ismt2_pp(t1, m_m, 2) << " , " << mk_ismt2_pp(t2, m_m, 2) << "\n";);
|
||||
const unsigned sz = t1->get_num_args();
|
||||
SASSERT(t2->get_num_args() == sz);
|
||||
|
|
@ -99,7 +99,7 @@ bool lackr::ackr(app * const t1, app * const t2) {
|
|||
expr * const arg2 = t2->get_arg(i);
|
||||
if (m_m.are_equal(arg1, arg2)) continue; // quickly skip syntactically equal
|
||||
if (m_m.are_distinct(arg1, arg2)){ // quickly abort if there are two distinct (e.g. numerals)
|
||||
TRACE("lackr", tout << "never eq\n";);
|
||||
TRACE("ackermannize", tout << "never eq\n";);
|
||||
return false;
|
||||
}
|
||||
eqs.push_back(m_m.mk_eq(arg1, arg2));
|
||||
|
|
@ -107,19 +107,19 @@ bool lackr::ackr(app * const t1, app * const t2) {
|
|||
app * const a1 = m_info->get_abstr(t1);
|
||||
app * const a2 = m_info->get_abstr(t2);
|
||||
SASSERT(a1 && a2);
|
||||
TRACE("lackr", tout << "abstr1 " << mk_ismt2_pp(a1, m_m, 2) << "\n";);
|
||||
TRACE("lackr", tout << "abstr2 " << mk_ismt2_pp(a2, m_m, 2) << "\n";);
|
||||
TRACE("ackermannize", tout << "abstr1 " << mk_ismt2_pp(a1, m_m, 2) << "\n";);
|
||||
TRACE("ackermannize", tout << "abstr2 " << mk_ismt2_pp(a2, m_m, 2) << "\n";);
|
||||
expr_ref lhs(m_m);
|
||||
lhs = (eqs.size() == 1) ? eqs.get(0) : m_m.mk_and(eqs.size(), eqs.c_ptr());
|
||||
TRACE("lackr", tout << "ackr constr lhs" << mk_ismt2_pp(lhs, m_m, 2) << "\n";);
|
||||
TRACE("ackermannize", tout << "ackr constr lhs" << mk_ismt2_pp(lhs, m_m, 2) << "\n";);
|
||||
expr_ref rhs(m_m.mk_eq(a1, a2),m_m);
|
||||
TRACE("lackr", tout << "ackr constr rhs" << mk_ismt2_pp(rhs, m_m, 2) << "\n";);
|
||||
TRACE("ackermannize", tout << "ackr constr rhs" << mk_ismt2_pp(rhs, m_m, 2) << "\n";);
|
||||
expr_ref cg(m_m.mk_implies(lhs, rhs), m_m);
|
||||
TRACE("lackr", tout << "ackr constr" << mk_ismt2_pp(cg, m_m, 2) << "\n";);
|
||||
TRACE("ackermannize", tout << "ackr constr" << mk_ismt2_pp(cg, m_m, 2) << "\n";);
|
||||
expr_ref cga(m_m);
|
||||
m_info->abstract(cg, cga); // constraint needs abstraction due to nested applications
|
||||
m_simp(cga);
|
||||
TRACE("lackr", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";);
|
||||
TRACE("ackermannize", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";);
|
||||
if (m_m.is_true(cga)) return false;
|
||||
m_st.m_ackrs_sz++;
|
||||
m_ackrs.push_back(cga);
|
||||
|
|
@ -130,11 +130,10 @@ bool lackr::ackr(app * const t1, app * const t2) {
|
|||
// Introduce the ackermann lemma for each pair of terms.
|
||||
//
|
||||
void lackr::eager_enc() {
|
||||
TRACE("lackr", tout << "#funs: " << m_fun2terms.size() << std::endl;);
|
||||
const fun2terms_map::iterator e = m_fun2terms.end();
|
||||
for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
|
||||
TRACE("ackermannize", tout << "#funs: " << m_fun2terms.size() << std::endl;);
|
||||
for (auto const& kv : m_fun2terms) {
|
||||
checkpoint();
|
||||
app_set * const ts = i->get_value();
|
||||
app_set * const ts = kv.get_value();
|
||||
const app_set::iterator r = ts->end();
|
||||
for (app_set::iterator j = ts->begin(); j != r; ++j) {
|
||||
app_set::iterator k = j;
|
||||
|
|
@ -142,10 +141,11 @@ void lackr::eager_enc() {
|
|||
for (; k != r; ++k) {
|
||||
app * const t1 = *j;
|
||||
app * const t2 = *k;
|
||||
SASSERT(t1->get_decl() == i->m_key);
|
||||
SASSERT(t2->get_decl() == i->m_key);
|
||||
if (t1 == t2) continue;
|
||||
ackr(t1,t2);
|
||||
SASSERT(t1->get_decl() == kv.m_key);
|
||||
SASSERT(t2->get_decl() == kv.m_key);
|
||||
if (t1 != t2) {
|
||||
ackr(t1,t2);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -153,18 +153,15 @@ void lackr::eager_enc() {
|
|||
|
||||
|
||||
void lackr::abstract() {
|
||||
const fun2terms_map::iterator e = m_fun2terms.end();
|
||||
for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
|
||||
func_decl* const fd = i->m_key;
|
||||
app_set * const ts = i->get_value();
|
||||
for (auto const& kv : m_fun2terms) {
|
||||
func_decl* const fd = kv.m_key;
|
||||
app_set * const ts = kv.get_value();
|
||||
sort* const s = fd->get_range();
|
||||
const app_set::iterator r = ts->end();
|
||||
for (app_set::iterator j = ts->begin(); j != r; ++j) {
|
||||
for (app * t : (*ts)) {
|
||||
app * const fc = m_m.mk_fresh_const(fd->get_name().str().c_str(), s);
|
||||
app * const t = *j;
|
||||
SASSERT(t->get_decl() == fd);
|
||||
m_info->set_abstr(t, fc);
|
||||
TRACE("lackr", tout << "abstr term "
|
||||
TRACE("ackermannize", tout << "abstr term "
|
||||
<< mk_ismt2_pp(t, m_m, 2)
|
||||
<< " -> "
|
||||
<< mk_ismt2_pp(fc, m_m, 2)
|
||||
|
|
@ -189,7 +186,7 @@ void lackr::add_term(app* a) {
|
|||
ts = alloc(app_set);
|
||||
m_fun2terms.insert(fd, ts);
|
||||
}
|
||||
TRACE("lackr", tout << "term(" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
|
||||
TRACE("ackermannize", tout << "term(" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
|
||||
ts->insert(a);
|
||||
}
|
||||
|
||||
|
|
@ -203,7 +200,7 @@ void lackr::push_abstraction() {
|
|||
lbool lackr::eager() {
|
||||
SASSERT(m_is_init);
|
||||
push_abstraction();
|
||||
TRACE("lackr", tout << "run sat 0\n"; );
|
||||
TRACE("ackermannize", tout << "run sat 0\n"; );
|
||||
const lbool rv0 = m_sat->check_sat(0, nullptr);
|
||||
if (rv0 == l_false) return l_false;
|
||||
eager_enc();
|
||||
|
|
@ -211,7 +208,7 @@ lbool lackr::eager() {
|
|||
all = m_m.mk_and(m_ackrs.size(), m_ackrs.c_ptr());
|
||||
m_simp(all);
|
||||
m_sat->assert_expr(all);
|
||||
TRACE("lackr", tout << "run sat all\n"; );
|
||||
TRACE("ackermannize", tout << "run sat all\n"; );
|
||||
return m_sat->check_sat(0, nullptr);
|
||||
}
|
||||
|
||||
|
|
@ -223,7 +220,7 @@ lbool lackr::lazy() {
|
|||
while (true) {
|
||||
m_st.m_it++;
|
||||
checkpoint();
|
||||
TRACE("lackr", tout << "lazy check: " << m_st.m_it << "\n";);
|
||||
TRACE("ackermannize", tout << "lazy check: " << m_st.m_it << "\n";);
|
||||
const lbool r = m_sat->check_sat(0, nullptr);
|
||||
if (r == l_undef) return l_undef; // give up
|
||||
if (r == l_false) return l_false; // abstraction unsat
|
||||
|
|
@ -264,16 +261,15 @@ bool lackr::collect_terms() {
|
|||
visited.mark(curr, true);
|
||||
stack.pop_back();
|
||||
break;
|
||||
case AST_APP:
|
||||
{
|
||||
case AST_APP: {
|
||||
app * const a = to_app(curr);
|
||||
if (for_each_expr_args(stack, visited, a->get_num_args(), a->get_args())) {
|
||||
visited.mark(curr, true);
|
||||
stack.pop_back();
|
||||
add_term(a);
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
case AST_QUANTIFIER:
|
||||
return false; // quantifiers not supported
|
||||
default:
|
||||
|
|
|
|||
|
|
@ -237,10 +237,12 @@ struct check_logic::imp {
|
|||
return;
|
||||
}
|
||||
else if (m_bv_arrays) {
|
||||
if (get_array_arity(s) != 1)
|
||||
fail("logic supports only unidimensional arrays");
|
||||
if (!m_bv_util.is_bv_sort(get_array_range(s)) || !m_bv_util.is_bv_sort(get_array_domain(s, 0)))
|
||||
fail("logic supports only arrays from bitvectors to bitvectors");
|
||||
unsigned sz = get_array_arity(s);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (!m_bv_util.is_bv_sort(get_array_domain(s, i)))
|
||||
fail("logic supports only arrays from bitvectors to bitvectors");
|
||||
}
|
||||
check_sort(get_array_range(s));
|
||||
}
|
||||
else {
|
||||
fail("logic does not support arrays");
|
||||
|
|
|
|||
|
|
@ -383,6 +383,7 @@ public:
|
|||
}
|
||||
if (core.empty()) {
|
||||
IF_VERBOSE(100, verbose_stream() << "(opt.maxres core is empty)\n";);
|
||||
TRACE("opt", tout << "empty core\n";);
|
||||
cores.reset();
|
||||
m_lower = m_upper;
|
||||
return l_true;
|
||||
|
|
@ -517,6 +518,10 @@ public:
|
|||
max_resolve(core, w);
|
||||
fml = mk_not(m, mk_and(m, core.size(), core.c_ptr()));
|
||||
add(fml);
|
||||
// save small cores such that lex-combinations of maxres can reuse these cores.
|
||||
if (core.size() <= 2) {
|
||||
m_defs.push_back(fml);
|
||||
}
|
||||
m_lower += w;
|
||||
if (m_st == s_primal_dual) {
|
||||
m_lower = std::min(m_lower, m_upper);
|
||||
|
|
@ -847,7 +852,10 @@ public:
|
|||
_solver->assert_expr(s().get_assertions());
|
||||
_solver->assert_expr(core);
|
||||
lbool is_sat = _solver->check_sat(0, nullptr);
|
||||
IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << "\n");
|
||||
IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << " core size " << core.size() << "\n");
|
||||
CTRACE("opt", is_sat != l_false,
|
||||
for (expr* c : core) tout << "core: " << mk_pp(c, m) << "\n";
|
||||
_solver->display(tout););
|
||||
VERIFY(is_sat == l_false);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -383,7 +383,7 @@ namespace opt {
|
|||
lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
|
||||
if (scoped) get_solver().push();
|
||||
lbool result = m_optsmt.lex(index, is_max);
|
||||
if (result == l_true) m_optsmt.get_model(m_model, m_labels);
|
||||
if (result == l_true) { m_optsmt.get_model(m_model, m_labels); SASSERT(m_model); }
|
||||
if (scoped) get_solver().pop(1);
|
||||
if (result == l_true && committed) m_optsmt.commit_assignment(index);
|
||||
if (result == l_true && m_optsmt.is_unbounded(index, is_max) && contains_quantifiers()) {
|
||||
|
|
@ -1604,6 +1604,7 @@ namespace opt {
|
|||
void context::validate_lex() {
|
||||
rational r1;
|
||||
expr_ref val(m);
|
||||
SASSERT(m_model);
|
||||
for (unsigned i = 0; i < m_objectives.size(); ++i) {
|
||||
objective const& obj = m_objectives[i];
|
||||
switch(obj.m_type) {
|
||||
|
|
|
|||
|
|
@ -171,6 +171,7 @@ namespace opt {
|
|||
}
|
||||
|
||||
lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize) {
|
||||
TRACE("opt", tout << "index: " << obj_index << " is-max: " << is_maximize << "\n";);
|
||||
arith_util arith(m);
|
||||
bool is_int = arith.is_int(m_objs[obj_index].get());
|
||||
lbool is_sat = l_true;
|
||||
|
|
@ -189,9 +190,11 @@ namespace opt {
|
|||
SASSERT(delta_per_step.is_int());
|
||||
SASSERT(delta_per_step.is_pos());
|
||||
is_sat = m_s->check_sat(0, nullptr);
|
||||
TRACE("opt", tout << "check " << is_sat << "\n";);
|
||||
if (is_sat == l_true) {
|
||||
m_s->maximize_objective(obj_index, bound);
|
||||
m_s->get_model(m_model);
|
||||
SASSERT(m_model);
|
||||
m_s->get_labels(m_labels);
|
||||
inf_eps obj = m_s->saved_objective_value(obj_index);
|
||||
update_lower_lex(obj_index, obj, is_maximize);
|
||||
|
|
@ -220,13 +223,17 @@ namespace opt {
|
|||
delta_per_step = rational::one();
|
||||
SASSERT(num_scopes > 0);
|
||||
--num_scopes;
|
||||
m_s->pop(1);
|
||||
m_s->pop(1);
|
||||
}
|
||||
else {
|
||||
break;
|
||||
}
|
||||
}
|
||||
m_s->pop(num_scopes);
|
||||
|
||||
if (is_sat == l_false && !m_model) {
|
||||
return l_false;
|
||||
}
|
||||
|
||||
if (m.canceled() || is_sat == l_undef) {
|
||||
return l_undef;
|
||||
|
|
@ -574,7 +581,7 @@ namespace opt {
|
|||
return m_upper[i];
|
||||
}
|
||||
|
||||
void optsmt::get_model(model_ref& mdl, svector<symbol> & labels) {
|
||||
void optsmt::get_model(model_ref& mdl, svector<symbol> & labels) {
|
||||
mdl = m_model.get();
|
||||
labels = m_labels;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -567,12 +567,9 @@ namespace smt {
|
|||
case b_justification::AXIOM:
|
||||
out << "axiom";
|
||||
break;
|
||||
case b_justification::BIN_CLAUSE: {
|
||||
literal l2 = j.get_literal();
|
||||
out << "bin-clause ";
|
||||
display_literal(out, l2);
|
||||
case b_justification::BIN_CLAUSE:
|
||||
out << "bin " << j.get_literal();
|
||||
break;
|
||||
}
|
||||
case b_justification::CLAUSE: {
|
||||
clause * cls = j.get_clause();
|
||||
out << "clause ";
|
||||
|
|
@ -580,10 +577,9 @@ namespace smt {
|
|||
break;
|
||||
}
|
||||
case b_justification::JUSTIFICATION: {
|
||||
out << "justification " << j.get_justification()->get_from_theory() << ": ";
|
||||
literal_vector lits;
|
||||
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
|
||||
display_literals(out, lits);
|
||||
out << "justification " << j.get_justification()->get_from_theory() << ": " << lits;
|
||||
break;
|
||||
}
|
||||
default:
|
||||
|
|
|
|||
|
|
@ -1836,8 +1836,6 @@ namespace smt {
|
|||
return false;
|
||||
}
|
||||
|
||||
// std::cout << c.lit() << "\n";
|
||||
|
||||
reset_coeffs();
|
||||
m_num_marks = 0;
|
||||
m_bound = c.k();
|
||||
|
|
@ -1936,7 +1934,10 @@ namespace smt {
|
|||
}
|
||||
if (pbj == nullptr) {
|
||||
TRACE("pb", tout << "skip justification for " << conseq << "\n";);
|
||||
inc_coeff(conseq, offset);
|
||||
// this is possible when conseq is an assumption.
|
||||
// The justification of conseq is itself,
|
||||
// don't increment the cofficient here because it assumes
|
||||
// conseq is justified further. it isnt'. conseq becomes part of the lemma.
|
||||
}
|
||||
else {
|
||||
card& c2 = pbj->get_card();
|
||||
|
|
@ -1944,7 +1945,6 @@ namespace smt {
|
|||
bound = c2.k();
|
||||
}
|
||||
|
||||
// std::cout << " offset: " << offset << " bound: " << bound << "\n";
|
||||
break;
|
||||
}
|
||||
default:
|
||||
|
|
@ -2020,6 +2020,7 @@ namespace smt {
|
|||
SASSERT(slack < 0);
|
||||
|
||||
SASSERT(validate_antecedents(m_antecedents));
|
||||
TRACE("pb", tout << "antecedents " << m_antecedents << "\n";);
|
||||
ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, nullptr)));
|
||||
|
||||
DEBUG_CODE(
|
||||
|
|
@ -2127,7 +2128,7 @@ namespace smt {
|
|||
break;
|
||||
}
|
||||
}
|
||||
TRACE("pb", display(tout << "validate: ", c, true);
|
||||
TRACE("pb_verbose", display(tout << "validate: ", c, true);
|
||||
tout << "sum: " << sum << " " << maxsum << " ";
|
||||
tout << ctx.get_assignment(c.lit()) << "\n";);
|
||||
|
||||
|
|
@ -2215,15 +2216,11 @@ namespace smt {
|
|||
|
||||
void theory_pb::display_resolved_lemma(std::ostream& out) const {
|
||||
context& ctx = get_context();
|
||||
bool_var v;
|
||||
unsigned lvl;
|
||||
out << "num marks: " << m_num_marks << "\n";
|
||||
out << "conflict level: " << m_conflict_lvl << "\n";
|
||||
for (unsigned i = 0; i < m_resolved.size(); ++i) {
|
||||
v = m_resolved[i].var();
|
||||
lvl = ctx.get_assign_level(v);
|
||||
out << lvl << ": " << m_resolved[i] << " ";
|
||||
ctx.display(out, ctx.get_justification(v));
|
||||
for (literal r : m_resolved) {
|
||||
out << ctx.get_assign_level(r) << ": " << r << " ";
|
||||
ctx.display(out, ctx.get_justification(r.var()));
|
||||
}
|
||||
|
||||
if (!m_antecedents.empty()) {
|
||||
|
|
|
|||
|
|
@ -23,7 +23,6 @@ Revision History:
|
|||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/expr_substitution.h"
|
||||
#include "tactic/goal_shared_occs.h"
|
||||
#include "ast/pb_decl_plugin.h"
|
||||
|
||||
namespace {
|
||||
class propagate_values_tactic : public tactic {
|
||||
|
|
@ -117,23 +116,10 @@ class propagate_values_tactic : public tactic {
|
|||
TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n";);
|
||||
if (new_curr != curr) {
|
||||
m_modified = true;
|
||||
//if (has_pb(curr))
|
||||
// IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n");
|
||||
}
|
||||
push_result(new_curr, new_pr);
|
||||
}
|
||||
|
||||
bool has_pb(expr* e) {
|
||||
pb_util pb(m);
|
||||
if (pb.is_ge(e)) return true;
|
||||
if (m.is_or(e)) {
|
||||
for (expr* a : *to_app(e)) {
|
||||
if (pb.is_ge(a)) return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void run(goal_ref const & g, goal_ref_buffer & result) {
|
||||
SASSERT(g->is_well_sorted());
|
||||
tactic_report report("propagate-values", *g);
|
||||
|
|
|
|||
|
|
@ -16,14 +16,15 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#include "tactic/tactical.h"
|
||||
#include "ast/rewriter/expr_replacer.h"
|
||||
#include "tactic/generic_model_converter.h"
|
||||
#include "ast/occurs.h"
|
||||
#include "util/cooperate.h"
|
||||
#include "tactic/goal_shared_occs.h"
|
||||
#include "ast/occurs.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/pb_decl_plugin.h"
|
||||
#include "tactic/goal_shared_occs.h"
|
||||
#include "tactic/tactical.h"
|
||||
#include "tactic/generic_model_converter.h"
|
||||
|
||||
class solve_eqs_tactic : public tactic {
|
||||
struct imp {
|
||||
|
|
@ -384,6 +385,20 @@ class solve_eqs_tactic : public tactic {
|
|||
|
||||
return false;
|
||||
}
|
||||
|
||||
void insert_solution(goal const& g, unsigned idx, expr* f, app* var, expr* def, proof* pr) {
|
||||
m_vars.push_back(var);
|
||||
m_candidates.push_back(f);
|
||||
m_candidate_set.mark(f);
|
||||
m_candidate_vars.mark(var);
|
||||
if (m_produce_proofs) {
|
||||
if (!pr)
|
||||
pr = g.pr(idx);
|
||||
else
|
||||
pr = m().mk_modus_ponens(g.pr(idx), pr);
|
||||
}
|
||||
m_subst->insert(var, def, pr, g.dep(idx));
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Start collecting candidates
|
||||
|
|
@ -408,17 +423,7 @@ class solve_eqs_tactic : public tactic {
|
|||
checkpoint();
|
||||
expr * f = g.form(idx);
|
||||
if (solve(f, var, def, pr)) {
|
||||
m_vars.push_back(var);
|
||||
m_candidates.push_back(f);
|
||||
m_candidate_set.mark(f);
|
||||
m_candidate_vars.mark(var);
|
||||
if (m_produce_proofs) {
|
||||
if (pr == 0)
|
||||
pr = g.pr(idx);
|
||||
else
|
||||
pr = m().mk_modus_ponens(g.pr(idx), pr);
|
||||
}
|
||||
m_subst->insert(var, def, pr, g.dep(idx));
|
||||
insert_solution(g, idx, f, var, def, pr);
|
||||
}
|
||||
m_num_steps++;
|
||||
}
|
||||
|
|
@ -430,6 +435,163 @@ class solve_eqs_tactic : public tactic {
|
|||
}
|
||||
tout << "\n";);
|
||||
}
|
||||
|
||||
struct nnf_context {
|
||||
bool m_is_and;
|
||||
expr_ref_vector m_args;
|
||||
unsigned m_index;
|
||||
nnf_context(bool is_and, expr_ref_vector const& args, unsigned idx):
|
||||
m_is_and(is_and),
|
||||
m_args(args),
|
||||
m_index(idx)
|
||||
{}
|
||||
};
|
||||
|
||||
bool is_compatible(goal const& g, unsigned idx, vector<nnf_context> const & path, expr* v, expr* eq) {
|
||||
return is_goal_compatible(g, idx, v, eq) && is_path_compatible(path, v, eq);
|
||||
}
|
||||
|
||||
bool is_goal_compatible(goal const& g, unsigned idx, expr* v, expr* eq) {
|
||||
bool all_e = false;
|
||||
for (unsigned j = 0; j < g.size(); ++j) {
|
||||
if (j != idx && !check_eq_compat(g.form(j), v, eq, all_e)) {
|
||||
TRACE("solve_eqs", tout << "occurs goal " << mk_pp(eq, m()) << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
//
|
||||
// all_e := all disjunctions contain eq
|
||||
//
|
||||
// or, all_e -> skip if all disjunctions contain eq
|
||||
// or, all_e -> fail if some disjunction contains v but not eq
|
||||
// or, all_e -> all_e := false if some disjunction does not contain v
|
||||
// and, all_e -> all_e
|
||||
//
|
||||
|
||||
bool is_path_compatible(vector<nnf_context> const & path, expr* v, expr* eq) {
|
||||
bool all_e = true;
|
||||
for (unsigned i = path.size(); i-- > 0; ) {
|
||||
auto const& p = path[i];
|
||||
auto const& args = p.m_args;
|
||||
if (p.m_is_and && !all_e) {
|
||||
for (unsigned j = 0; j < args.size(); ++j) {
|
||||
if (j != p.m_index && occurs(v, args[j])) {
|
||||
TRACE("solve_eqs", tout << "occurs and " << mk_pp(eq, m()) << " " << mk_pp(args[j], m()) << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (!p.m_is_and) {
|
||||
for (unsigned j = 0; j < args.size(); ++j) {
|
||||
if (j != p.m_index) {
|
||||
if (occurs(v, args[j])) {
|
||||
if (!check_eq_compat(args[j], v, eq, all_e)) {
|
||||
TRACE("solve_eqs", tout << "occurs or " << mk_pp(eq, m()) << " " << mk_pp(args[j], m()) << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
else {
|
||||
all_e = false;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool check_eq_compat(expr* f, expr* v, expr* eq, bool& all) {
|
||||
expr_ref_vector args(m());
|
||||
expr* f1 = nullptr;
|
||||
if (!occurs(v, f)) {
|
||||
all = false;
|
||||
return true;
|
||||
}
|
||||
if (m().is_not(f, f1) && m().is_or(f1)) {
|
||||
flatten_and(f, args);
|
||||
for (expr* arg : args) {
|
||||
if (arg == eq) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (m().is_or(f)) {
|
||||
flatten_or(f, args);
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
|
||||
for (expr* arg : args) {
|
||||
if (!check_eq_compat(arg, v, eq, all)) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void hoist_nnf(goal const& g, expr* f, vector<nnf_context> & path, unsigned idx, unsigned depth) {
|
||||
if (depth > 4) {
|
||||
return;
|
||||
}
|
||||
app_ref var(m());
|
||||
expr_ref def(m());
|
||||
proof_ref pr(m());
|
||||
expr_ref_vector args(m());
|
||||
expr* f1 = nullptr;
|
||||
|
||||
if (m().is_not(f, f1) && m().is_or(f1)) {
|
||||
flatten_and(f, args);
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
expr* arg = args.get(i), *lhs = nullptr, *rhs = nullptr;
|
||||
if (m().is_eq(arg, lhs, rhs)) {
|
||||
if (trivial_solve1(lhs, rhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) {
|
||||
insert_solution(g, idx, arg, var, def, pr);
|
||||
}
|
||||
else if (trivial_solve1(rhs, lhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) {
|
||||
insert_solution(g, idx, arg, var, def, pr);
|
||||
}
|
||||
else {
|
||||
IF_VERBOSE(0,
|
||||
verbose_stream() << "eq not solved " << mk_pp(arg, m()) << "\n";
|
||||
verbose_stream() << is_uninterp_const(lhs) << " " << !m_candidate_vars.is_marked(lhs) << " "
|
||||
<< !occurs(lhs, rhs) << " " << check_occs(lhs) << "\n";);
|
||||
}
|
||||
}
|
||||
else {
|
||||
path.push_back(nnf_context(true, args, i));
|
||||
hoist_nnf(g, arg, path, idx, depth + 1);
|
||||
path.pop_back();
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (m().is_or(f)) {
|
||||
flatten_or(f, args);
|
||||
//std::cout << "hoist or " << args.size() << "\n";
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
path.push_back(nnf_context(false, args, i));
|
||||
hoist_nnf(g, args.get(i), path, idx, depth + 1);
|
||||
path.pop_back();
|
||||
}
|
||||
}
|
||||
else {
|
||||
// std::cout << "no hoist " << mk_pp(f, m()) << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
bool collect_hoist(goal const& g) {
|
||||
bool change = false;
|
||||
unsigned size = g.size();
|
||||
vector<nnf_context> path;
|
||||
for (unsigned idx = 0; idx < size; idx++) {
|
||||
checkpoint();
|
||||
hoist_nnf(g, g.form(idx), path, idx, 0);
|
||||
}
|
||||
return change;
|
||||
}
|
||||
|
||||
void sort_vars() {
|
||||
SASSERT(m_candidates.size() == m_vars.size());
|
||||
|
|
@ -564,6 +726,10 @@ class solve_eqs_tactic : public tactic {
|
|||
++idx;
|
||||
}
|
||||
|
||||
IF_VERBOSE(10,
|
||||
verbose_stream() << "ordered vars: ";
|
||||
for (app* v : m_ordered_vars) verbose_stream() << mk_pp(v, m()) << " ";
|
||||
verbose_stream() << "\n";);
|
||||
TRACE("solve_eqs",
|
||||
tout << "ordered vars:\n";
|
||||
for (app* v : m_ordered_vars) {
|
||||
|
|
@ -756,6 +922,8 @@ class solve_eqs_tactic : public tactic {
|
|||
while (true) {
|
||||
collect_num_occs(*g);
|
||||
collect(*g);
|
||||
// TBD Disabled until tested more:
|
||||
// collect_hoist(*g);
|
||||
if (m_subst->empty())
|
||||
break;
|
||||
sort_vars();
|
||||
|
|
@ -773,6 +941,7 @@ class solve_eqs_tactic : public tactic {
|
|||
g->inc_depth();
|
||||
g->add(mc.get());
|
||||
result.push_back(g.get());
|
||||
//IF_VERBOSE(0, g->display(verbose_stream()));
|
||||
TRACE("solve_eqs", g->display(tout););
|
||||
SASSERT(g->is_well_sorted());
|
||||
}
|
||||
|
|
|
|||
|
|
@ -24,13 +24,10 @@ Notes:
|
|||
#include "tactic/bv/max_bv_sharing_tactic.h"
|
||||
#include "tactic/bv/bv_size_reduction_tactic.h"
|
||||
#include "tactic/core/ctx_simplify_tactic.h"
|
||||
#include "sat/tactic/sat_tactic.h"
|
||||
#include "ackermannization/ackermannize_bv_tactic.h"
|
||||
#include "smt/tactic/smt_tactic.h"
|
||||
|
||||
tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref main_p;
|
||||
main_p.set_bool("elim_and", true);
|
||||
main_p.set_bool("sort_store", true);
|
||||
static tactic * mk_qfaufbv_preamble(ast_manager & m, params_ref const & p) {
|
||||
|
||||
params_ref simp2_p = p;
|
||||
simp2_p.set_bool("som", true);
|
||||
|
|
@ -39,26 +36,27 @@ tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
|
|||
simp2_p.set_bool("local_ctx", true);
|
||||
simp2_p.set_uint("local_ctx_limit", 10000000);
|
||||
|
||||
params_ref ctx_simp_p;
|
||||
ctx_simp_p.set_uint("max_depth", 32);
|
||||
ctx_simp_p.set_uint("max_steps", 5000000);
|
||||
|
||||
params_ref solver_p;
|
||||
solver_p.set_bool("array.simplify", false); // disable array simplifications at old_simplify module
|
||||
return and_then(mk_simplify_tactic(m),
|
||||
mk_propagate_values_tactic(m),
|
||||
mk_solve_eqs_tactic(m),
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
// sound to use? if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
|
||||
if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
|
||||
using_params(mk_simplify_tactic(m), simp2_p),
|
||||
mk_max_bv_sharing_tactic(m),
|
||||
if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m, p)))
|
||||
);
|
||||
}
|
||||
|
||||
tactic * preamble_st = and_then(mk_simplify_tactic(m),
|
||||
mk_propagate_values_tactic(m),
|
||||
// using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
|
||||
mk_solve_eqs_tactic(m),
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
|
||||
using_params(mk_simplify_tactic(m), simp2_p),
|
||||
mk_max_bv_sharing_tactic(m)
|
||||
);
|
||||
tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref main_p;
|
||||
main_p.set_bool("elim_and", true);
|
||||
main_p.set_bool("sort_store", true);
|
||||
|
||||
tactic * st = using_params(and_then(preamble_st,
|
||||
using_params(mk_smt_tactic(m), solver_p)),
|
||||
main_p);
|
||||
tactic * preamble_st = mk_qfaufbv_preamble(m, p);
|
||||
|
||||
tactic * st = using_params(and_then(preamble_st, mk_smt_tactic(m)), main_p);
|
||||
|
||||
st->updt_params(p);
|
||||
return st;
|
||||
|
|
|
|||
|
|
@ -39,13 +39,14 @@ struct tactic_report::imp {
|
|||
~imp() {
|
||||
m_watch.stop();
|
||||
double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
|
||||
verbose_stream() << "(" << m_id
|
||||
<< " :num-exprs " << m_goal.num_exprs()
|
||||
<< " :num-asts " << m_goal.m().get_num_asts()
|
||||
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds()
|
||||
<< " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory
|
||||
<< " :after-memory " << std::fixed << std::setprecision(2) << end_memory
|
||||
<< ")" << std::endl;
|
||||
IF_VERBOSE(0,
|
||||
verbose_stream() << "(" << m_id
|
||||
<< " :num-exprs " << m_goal.num_exprs()
|
||||
<< " :num-asts " << m_goal.m().get_num_asts()
|
||||
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds()
|
||||
<< " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory
|
||||
<< " :after-memory " << std::fixed << std::setprecision(2) << end_memory
|
||||
<< ")" << std::endl);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue