From 2ff51e9a6084c88450f1cff7a9c8379fcf23ed0f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Nov 2013 21:33:35 +0100 Subject: [PATCH] move model_evaluator from pdr to model, call it model_implicant Signed-off-by: Nikolaj Bjorner --- src/model/model_implicant.cpp | 917 +++++++++++++++++++++++++++ src/model/model_implicant.h | 118 ++++ src/muz/pdr/pdr_context.cpp | 3 +- src/muz/pdr/pdr_util.cpp | 873 ------------------------- src/muz/pdr/pdr_util.h | 80 --- src/opt/fu_malik.cpp | 2 +- src/opt/opt_solver.cpp | 19 +- src/opt/opt_solver.h | 5 +- src/smt/theory_pb.cpp | 260 ++++---- src/smt/theory_pb.h | 9 +- src/tactic/arith/lia2card_tactic.cpp | 569 +++++++++-------- 11 files changed, 1514 insertions(+), 1341 deletions(-) create mode 100644 src/model/model_implicant.cpp create mode 100644 src/model/model_implicant.h diff --git a/src/model/model_implicant.cpp b/src/model/model_implicant.cpp new file mode 100644 index 000000000..44c70036c --- /dev/null +++ b/src/model/model_implicant.cpp @@ -0,0 +1,917 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + model_implicant.cpp + +Abstract: + + Facility to extract prime implicant from model. + +Author: + + Krystof Hoder (t-khoder) 2011-8-19. + +Revision History: + + +Notes: + + +--*/ + +#include +#include "array_decl_plugin.h" +#include "ast_pp.h" +#include "bool_rewriter.h" +#include "for_each_expr.h" +#include "model.h" +#include "ref_vector.h" +#include "rewriter.h" +#include "rewriter_def.h" +#include "util.h" +#include "model_implicant.h" +#include "arith_decl_plugin.h" +#include "expr_replacer.h" +#include "model_smt2_pp.h" +#include "poly_rewriter.h" +#include "poly_rewriter_def.h" +#include "arith_rewriter.h" +#include "scoped_proof.h" + + + +///////////////////////// +// model_implicant +// + + +void model_implicant::assign_value(expr* e, expr* val) { + rational r; + if (m.is_true(val)) { + set_true(e); + } + else if (m.is_false(val)) { + set_false(e); + } + else if (m_arith.is_numeral(val, r)) { + set_number(e, r); + } + else if (m.is_value(val)) { + set_value(e, val); + } + else { + IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";); + TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";); + set_x(e); + } +} + +void model_implicant::setup_model(model_ref& model) { + m_numbers.reset(); + m_values.reset(); + m_model = model; + rational r; + unsigned sz = model->get_num_constants(); + for (unsigned i = 0; i < sz; i++) { + func_decl * d = model->get_constant(i); + expr* val = model->get_const_interp(d); + expr* e = m.mk_const(d); + m_refs.push_back(e); + assign_value(e, val); + } +} + +void model_implicant::reset() { + m1.reset(); + m2.reset(); + m_values.reset(); + m_visited.reset(); + m_numbers.reset(); + m_refs.reset(); + m_model = 0; +} + +expr_ref_vector model_implicant::minimize_model(ptr_vector const & formulas, model_ref& mdl) { + setup_model(mdl); + + TRACE("pdr_verbose", + tout << "formulas:\n"; + for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; + ); + + expr_ref_vector model = prune_by_cone_of_influence(formulas); + TRACE("pdr_verbose", + tout << "pruned model:\n"; + for (unsigned i = 0; i < model.size(); ++i) tout << mk_pp(model[i].get(), m) << "\n";); + + reset(); + + DEBUG_CODE( + setup_model(mdl); + VERIFY(check_model(formulas)); + reset();); + + return model; +} + +expr_ref_vector model_implicant::minimize_literals(ptr_vector const& formulas, model_ref& mdl) { + + TRACE("pdr", + tout << "formulas:\n"; + for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; + ); + + expr_ref_vector result(m); + expr_ref tmp(m); + ptr_vector tocollect; + + setup_model(mdl); + collect(formulas, tocollect); + for (unsigned i = 0; i < tocollect.size(); ++i) { + expr* e = tocollect[i]; + expr* e1, *e2; + SASSERT(m.is_bool(e)); + SASSERT(is_true(e) || is_false(e)); + if (is_true(e)) { + result.push_back(e); + } + // hack to break disequalities for arithmetic variables. + else if (m.is_eq(e, e1, e2) && m_arith.is_int_real(e1)) { + if (get_number(e1) < get_number(e2)) { + result.push_back(m_arith.mk_lt(e1,e2)); + } + else { + result.push_back(m_arith.mk_lt(e2,e1)); + } + } + else { + result.push_back(m.mk_not(e)); + } + } + reset(); + TRACE("pdr", + tout << "minimized model:\n"; + for (unsigned i = 0; i < result.size(); ++i) tout << mk_pp(result[i].get(), m) << "\n"; + ); + + return result; +} + +void model_implicant::process_formula(app* e, ptr_vector& todo, ptr_vector& tocollect) { + SASSERT(m.is_bool(e)); + SASSERT(is_true(e) || is_false(e)); + unsigned v = is_true(e); + unsigned sz = e->get_num_args(); + expr* const* args = e->get_args(); + if (e->get_family_id() == m.get_basic_family_id()) { + switch(e->get_decl_kind()) { + case OP_TRUE: + break; + case OP_FALSE: + break; + case OP_EQ: + case OP_IFF: + if (args[0] == args[1]) { + SASSERT(v); + // no-op + } + else if (m.is_bool(args[0])) { + todo.append(sz, args); + } + else { + tocollect.push_back(e); + } + break; + case OP_DISTINCT: + tocollect.push_back(e); + break; + case OP_ITE: + if (args[1] == args[2]) { + tocollect.push_back(args[1]); + } + else if (is_true(args[1]) && is_true(args[2])) { + todo.append(2, args+1); + } + else if (is_false(args[1]) && is_false(args[2])) { + todo.append(2, args+1); + } + else if (is_true(args[0])) { + todo.append(2, args); + } + else { + SASSERT(is_false(args[0])); + todo.push_back(args[0]); + todo.push_back(args[2]); + } + break; + case OP_AND: + if (v) { + todo.append(sz, args); + } + else { + unsigned i = 0; + for (; !is_false(args[i]) && i < sz; ++i); + if (i == sz) { + fatal_error(1); + } + VERIFY(i < sz); + todo.push_back(args[i]); + } + break; + case OP_OR: + if (v) { + unsigned i = 0; + for (; !is_true(args[i]) && i < sz; ++i); + if (i == sz) { + fatal_error(1); + } + VERIFY(i < sz); + todo.push_back(args[i]); + } + else { + todo.append(sz, args); + } + break; + case OP_XOR: + case OP_NOT: + todo.append(sz, args); + break; + case OP_IMPLIES: + if (v) { + if (is_true(args[1])) { + todo.push_back(args[1]); + } + else if (is_false(args[0])) { + todo.push_back(args[0]); + } + else { + IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); + UNREACHABLE(); + } + } + else { + todo.append(sz, args); + } + break; + default: + IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); + UNREACHABLE(); + } + } + else { + tocollect.push_back(e); + } +} + +void model_implicant::collect(ptr_vector const& formulas, ptr_vector& tocollect) { + ptr_vector todo; + todo.append(formulas); + m_visited.reset(); + + VERIFY(check_model(formulas)); + + while (!todo.empty()) { + app* e = to_app(todo.back()); + todo.pop_back(); + if (!m_visited.is_marked(e)) { + process_formula(e, todo, tocollect); + m_visited.mark(e, true); + } + } + m_visited.reset(); +} + +expr_ref_vector model_implicant::prune_by_cone_of_influence(ptr_vector const & formulas) { + ptr_vector tocollect; + collect(formulas, tocollect); + m1.reset(); + m2.reset(); + for (unsigned i = 0; i < tocollect.size(); ++i) { + TRACE("pdr_verbose", tout << "collect: " << mk_pp(tocollect[i], m) << "\n";); + for_each_expr(*this, m_visited, tocollect[i]); + } + unsigned sz = m_model->get_num_constants(); + expr_ref e(m), eq(m), val(m); + expr_ref_vector model(m); + for (unsigned i = 0; i < sz; i++) { + e = m.mk_const(m_model->get_constant(i)); + if (m_visited.is_marked(e)) { + val = eval(m_model, e); + eq = m.mk_eq(e, val); + model.push_back(eq); + } + } + m_visited.reset(); + TRACE("pdr", tout << sz << " ==> " << model.size() << "\n";); + return model; + +} + +void model_implicant::eval_arith(app* e) { + rational r, r2; + +#define ARG1 e->get_arg(0) +#define ARG2 e->get_arg(1) + + unsigned arity = e->get_num_args(); + for (unsigned i = 0; i < arity; ++i) { + expr* arg = e->get_arg(i); + if (is_x(arg)) { + set_x(e); + return; + } + SASSERT(!is_unknown(arg)); + } + switch(e->get_decl_kind()) { + case OP_NUM: + VERIFY(m_arith.is_numeral(e, r)); + set_number(e, r); + break; + case OP_IRRATIONAL_ALGEBRAIC_NUM: + set_x(e); + break; + case OP_LE: + set_bool(e, get_number(ARG1) <= get_number(ARG2)); + break; + case OP_GE: + set_bool(e, get_number(ARG1) >= get_number(ARG2)); + break; + case OP_LT: + set_bool(e, get_number(ARG1) < get_number(ARG2)); + break; + case OP_GT: + set_bool(e, get_number(ARG1) > get_number(ARG2)); + break; + case OP_ADD: + r = rational::zero(); + for (unsigned i = 0; i < arity; ++i) { + r += get_number(e->get_arg(i)); + } + set_number(e, r); + break; + case OP_SUB: + r = get_number(e->get_arg(0)); + for (unsigned i = 1; i < arity; ++i) { + r -= get_number(e->get_arg(i)); + } + set_number(e, r); + break; + case OP_UMINUS: + SASSERT(arity == 1); + set_number(e, get_number(e->get_arg(0))); + break; + case OP_MUL: + r = rational::one(); + for (unsigned i = 0; i < arity; ++i) { + r *= get_number(e->get_arg(i)); + } + set_number(e, r); + break; + case OP_DIV: + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); + } + else { + set_number(e, get_number(ARG1) / r); + } + break; + case OP_IDIV: + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); + } + else { + set_number(e, div(get_number(ARG1), r)); + } + break; + case OP_REM: + // rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2) + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); + } + else { + r2 = mod(get_number(ARG1), r); + if (r.is_neg()) r2.neg(); + set_number(e, r2); + } + break; + case OP_MOD: + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); + } + else { + set_number(e, mod(get_number(ARG1), r)); + } + break; + case OP_TO_REAL: + SASSERT(arity == 1); + set_number(e, get_number(ARG1)); + break; + case OP_TO_INT: + SASSERT(arity == 1); + set_number(e, floor(get_number(ARG1))); + break; + case OP_IS_INT: + SASSERT(arity == 1); + set_bool(e, get_number(ARG1).is_int()); + break; + case OP_POWER: + set_x(e); + break; + default: + IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); + UNREACHABLE(); + break; + } +} + +void model_implicant::inherit_value(expr* e, expr* v) { + expr* w; + SASSERT(!is_unknown(v)); + SASSERT(m.get_sort(e) == m.get_sort(v)); + if (is_x(v)) { + set_x(e); + } + else if (m.is_bool(e)) { + SASSERT(m.is_bool(v)); + if (is_true(v)) set_true(e); + else if (is_false(v)) set_false(e); + else { + TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";); + set_x(e); + } + } + else if (m_arith.is_int_real(e)) { + set_number(e, get_number(v)); + } + else if (m.is_value(v)) { + set_value(e, v); + } + else if (m_values.find(v, w)) { + set_value(e, w); + } + else { + TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";); + set_x(e); + } +} + +void model_implicant::eval_exprs(expr_ref_vector& es) { + model_ref mr(m_model); + for (unsigned j = 0; j < es.size(); ++j) { + if (m_array.is_as_array(es[j].get())) { + es[j] = eval(mr, es[j].get()); + } + } +} + +bool model_implicant::extract_array_func_interp(expr* a, vector& stores, expr_ref& else_case) { + SASSERT(m_array.is_array(a)); + + TRACE("pdr", tout << mk_pp(a, m) << "\n";); + while (m_array.is_store(a)) { + expr_ref_vector store(m); + store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1); + eval_exprs(store); + stores.push_back(store); + a = to_app(a)->get_arg(0); + } + + if (m_array.is_const(a)) { + else_case = to_app(a)->get_arg(0); + return true; + } + + while (m_array.is_as_array(a)) { + func_decl* f = m_array.get_as_array_func_decl(to_app(a)); + func_interp* g = m_model->get_func_interp(f); + unsigned sz = g->num_entries(); + unsigned arity = f->get_arity(); + for (unsigned i = 0; i < sz; ++i) { + expr_ref_vector store(m); + func_entry const* fe = g->get_entry(i); + store.append(arity, fe->get_args()); + store.push_back(fe->get_result()); + for (unsigned j = 0; j < store.size(); ++j) { + if (!is_ground(store[j].get())) { + TRACE("pdr", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";); + return false; + } + } + eval_exprs(store); + stores.push_back(store); + } + else_case = g->get_else(); + if (!else_case) { + TRACE("pdr", tout << "no else case " << mk_pp(a, m) << "\n";); + return false; + } + if (!is_ground(else_case)) { + TRACE("pdr", tout << "non-ground else case " << mk_pp(a, m) << "\n" << mk_pp(else_case, m) << "\n";); + return false; + } + if (m_array.is_as_array(else_case)) { + model_ref mr(m_model); + else_case = eval(mr, else_case); + } + TRACE("pdr", tout << "else case: " << mk_pp(else_case, m) << "\n";); + return true; + } + TRACE("pdr", tout << "no translation: " << mk_pp(a, m) << "\n";); + + return false; +} + +/** + best effort evaluator of extensional array equality. +*/ +void model_implicant::eval_array_eq(app* e, expr* arg1, expr* arg2) { + TRACE("pdr", tout << "array equality: " << mk_pp(e, m) << "\n";); + expr_ref v1(m), v2(m); + m_model->eval(arg1, v1); + m_model->eval(arg2, v2); + if (v1 == v2) { + set_true(e); + return; + } + sort* s = m.get_sort(arg1); + sort* r = get_array_range(s); + // give up evaluating finite domain/range arrays + if (!r->is_infinite() && !r->is_very_big() && !s->is_infinite() && !s->is_very_big()) { + TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); + set_x(e); + return; + } + vector store; + expr_ref else1(m), else2(m); + if (!extract_array_func_interp(v1, store, else1) || + !extract_array_func_interp(v2, store, else2)) { + TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); + set_x(e); + return; + } + + if (else1 != else2) { + if (m.is_value(else1) && m.is_value(else2)) { + TRACE("pdr", tout + << "defaults are different: " << mk_pp(e, m) << " " + << mk_pp(else1, m) << " " << mk_pp(else2, m) << "\n";); + set_false(e); + } + else if (m_array.is_array(else1)) { + eval_array_eq(e, else1, else2); + } + else { + TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); + set_x(e); + } + return; + } + + expr_ref s1(m), s2(m), w1(m), w2(m); + expr_ref_vector args1(m), args2(m); + args1.push_back(v1); + args2.push_back(v2); + for (unsigned i = 0; i < store.size(); ++i) { + args1.resize(1); + args2.resize(1); + args1.append(store[i].size()-1, store[i].c_ptr()); + args2.append(store[i].size()-1, store[i].c_ptr()); + s1 = m_array.mk_select(args1.size(), args1.c_ptr()); + s2 = m_array.mk_select(args2.size(), args2.c_ptr()); + m_model->eval(s1, w1); + m_model->eval(s2, w2); + if (w1 == w2) { + continue; + } + if (m.is_value(w1) && m.is_value(w2)) { + TRACE("pdr", tout << "Equality evaluation: " << mk_pp(e, m) << "\n"; + tout << mk_pp(s1, m) << " |-> " << mk_pp(w1, m) << "\n"; + tout << mk_pp(s2, m) << " |-> " << mk_pp(w2, m) << "\n";); + set_false(e); + } + else if (m_array.is_array(w1)) { + eval_array_eq(e, w1, w2); + if (is_true(e)) { + continue; + } + } + else { + TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); + set_x(e); + } + return; + } + set_true(e); +} + +void model_implicant::eval_eq(app* e, expr* arg1, expr* arg2) { + if (arg1 == arg2) { + set_true(e); + } + else if (m_array.is_array(arg1)) { + eval_array_eq(e, arg1, arg2); + } + else if (is_x(arg1) || is_x(arg2)) { + expr_ref eq(m), vl(m); + eq = m.mk_eq(arg1, arg2); + m_model->eval(eq, vl); + if (m.is_true(vl)) { + set_bool(e, true); + } + else if (m.is_false(vl)) { + set_bool(e, false); + } + else { + TRACE("pdr", tout << "cannot evaluate: " << mk_pp(vl, m) << "\n";); + set_x(e); + } + } + else if (m.is_bool(arg1)) { + bool val = is_true(arg1) == is_true(arg2); + SASSERT(val == (is_false(arg1) == is_false(arg2))); + if (val) { + set_true(e); + } + else { + set_false(e); + } + } + else if (m_arith.is_int_real(arg1)) { + set_bool(e, get_number(arg1) == get_number(arg2)); + } + else { + expr* e1 = get_value(arg1); + expr* e2 = get_value(arg2); + if (m.is_value(e1) && m.is_value(e2)) { + set_bool(e, e1 == e2); + } + else if (e1 == e2) { + set_bool(e, true); + } + else { + TRACE("pdr", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";); + set_x(e); + } + } +} + +void model_implicant::eval_basic(app* e) { + expr* arg1, *arg2; + expr *argCond, *argThen, *argElse, *arg; + bool has_x = false; + unsigned arity = e->get_num_args(); + switch(e->get_decl_kind()) { + case OP_AND: + for (unsigned j = 0; j < arity; ++j) { + expr * arg = e->get_arg(j); + if (is_false(arg)) { + set_false(e); + return; + } + else if (is_x(arg)) { + has_x = true; + } + else { + SASSERT(is_true(arg)); + } + } + if (has_x) { + set_x(e); + } + else { + set_true(e); + } + break; + case OP_OR: + for (unsigned j = 0; j < arity; ++j) { + expr * arg = e->get_arg(j); + if (is_true(arg)) { + set_true(e); + return; + } + else if (is_x(arg)) { + has_x = true; + } + else { + SASSERT(is_false(arg)); + } + } + if (has_x) { + set_x(e); + } + else { + set_false(e); + } + break; + case OP_NOT: + VERIFY(m.is_not(e, arg)); + if (is_true(arg)) { + set_false(e); + } + else if (is_false(arg)) { + set_true(e); + } + else { + SASSERT(is_x(arg)); + set_x(e); + } + break; + case OP_IMPLIES: + VERIFY(m.is_implies(e, arg1, arg2)); + if (is_false(arg1) || is_true(arg2)) { + set_true(e); + } + else if (arg1 == arg2) { + set_true(e); + } + else if (is_true(arg1) && is_false(arg2)) { + set_false(e); + } + else { + SASSERT(is_x(arg1) || is_x(arg2)); + set_x(e); + } + break; + case OP_IFF: + VERIFY(m.is_iff(e, arg1, arg2)); + eval_eq(e, arg1, arg2); + break; + case OP_ITE: + VERIFY(m.is_ite(e, argCond, argThen, argElse)); + if (is_true(argCond)) { + inherit_value(e, argThen); + } + else if (is_false(argCond)) { + inherit_value(e, argElse); + } + else if (argThen == argElse) { + inherit_value(e, argThen); + } + else if (m.is_bool(e)) { + SASSERT(is_x(argCond)); + if (is_x(argThen) || is_x(argElse)) { + set_x(e); + } + else if (is_true(argThen) == is_true(argElse)) { + inherit_value(e, argThen); + } + else { + set_x(e); + } + } + else { + set_x(e); + } + break; + case OP_TRUE: + set_true(e); + break; + case OP_FALSE: + set_false(e); + break; + case OP_EQ: + VERIFY(m.is_eq(e, arg1, arg2)); + eval_eq(e, arg1, arg2); + break; + case OP_DISTINCT: { + vector values; + for (unsigned i = 0; i < arity; ++i) { + expr* arg = e->get_arg(i); + if (is_x(arg)) { + set_x(e); + return; + } + values.push_back(get_number(arg)); + } + std::sort(values.begin(), values.end()); + for (unsigned i = 0; i + 1 < values.size(); ++i) { + if (values[i] == values[i+1]) { + set_false(e); + return; + } + } + set_true(e); + break; + } + default: + IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); + UNREACHABLE(); + } +} + +bool model_implicant::check_model(ptr_vector const& formulas) { + ptr_vector todo(formulas); + + while (!todo.empty()) { + expr * curr_e = todo.back(); + + if (!is_app(curr_e)) { + todo.pop_back(); + continue; + } + app * curr = to_app(curr_e); + + if (!is_unknown(curr)) { + todo.pop_back(); + continue; + } + unsigned arity = curr->get_num_args(); + for (unsigned i = 0; i < arity; ++i) { + if (is_unknown(curr->get_arg(i))) { + todo.push_back(curr->get_arg(i)); + } + } + if (todo.back() != curr) { + continue; + } + todo.pop_back(); + if (curr->get_family_id() == m_arith.get_family_id()) { + eval_arith(curr); + } + else if (curr->get_family_id() == m.get_basic_family_id()) { + eval_basic(curr); + } + else { + expr_ref vl(m); + m_model->eval(curr, vl); + assign_value(curr, vl); + } + + IF_VERBOSE(35,verbose_stream() << "assigned "<get_arity() == 0); + expr_ref result(m); + if (m_array.is_array(d->get_range())) { + expr_ref e(m); + e = m.mk_const(d); + result = eval(model, e); + } + else { + result = model->get_const_interp(d); + } + return result; +} + +expr_ref model_implicant::eval(model_ref& model, expr* e) { + expr_ref result(m); + m_model = model; + VERIFY(m_model->eval(e, result, true)); + if (m_array.is_array(e)) { + vector stores; + expr_ref_vector args(m); + expr_ref else_case(m); + if (extract_array_func_interp(result, stores, else_case)) { + result = m_array.mk_const_array(m.get_sort(e), else_case); + while (!stores.empty() && stores.back().back() == else_case) { + stores.pop_back(); + } + for (unsigned i = stores.size(); i > 0; ) { + --i; + args.resize(1); + args[0] = result; + args.append(stores[i]); + result = m_array.mk_store(args.size(), args.c_ptr()); + } + return result; + } + } + return result; +} + + + + diff --git a/src/model/model_implicant.h b/src/model/model_implicant.h new file mode 100644 index 000000000..55b466ca3 --- /dev/null +++ b/src/model/model_implicant.h @@ -0,0 +1,118 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + model_implicant.h + +Abstract: + + Facility to extract prime implicant from model. + +Author: + + Krystof Hoder (t-khoder) 2011-8-19. + +Revision History: + +--*/ + +#ifndef _MODEL_IMPLICANT_H_ +#define _MODEL_IMPLICANT_H_ + +#include "ast.h" +#include "ast_pp.h" +#include "obj_hashtable.h" +#include "ref_vector.h" +#include "trace.h" +#include "vector.h" +#include "arith_decl_plugin.h" +#include "array_decl_plugin.h" + +class model; +class model_core; + +class model_implicant { + ast_manager& m; + arith_util m_arith; + array_util m_array; + obj_map m_numbers; + expr_ref_vector m_refs; + obj_map m_values; + model_ref m_model; + + //00 -- non-visited + //01 -- X + //10 -- false + //11 -- true + expr_mark m1; + expr_mark m2; + expr_mark m_visited; + + + void reset(); + void setup_model(model_ref& model); + void assign_value(expr* e, expr* v); + void collect(ptr_vector const& formulas, ptr_vector& tocollect); + void process_formula(app* e, ptr_vector& todo, ptr_vector& tocollect); + expr_ref_vector prune_by_cone_of_influence(ptr_vector const & formulas); + void eval_arith(app* e); + void eval_basic(app* e); + void eval_eq(app* e, expr* arg1, expr* arg2); + void eval_array_eq(app* e, expr* arg1, expr* arg2); + void inherit_value(expr* e, expr* v); + + inline bool is_unknown(expr* x) { return !m1.is_marked(x) && !m2.is_marked(x); } + inline void set_unknown(expr* x) { m1.mark(x, false); m2.mark(x, false); } + inline bool is_x(expr* x) { return !m1.is_marked(x) && m2.is_marked(x); } + inline bool is_false(expr* x) { return m1.is_marked(x) && !m2.is_marked(x); } + inline bool is_true(expr* x) { return m1.is_marked(x) && m2.is_marked(x); } + inline void set_x(expr* x) { SASSERT(is_unknown(x)); m2.mark(x); } + inline void set_v(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); } + inline void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); } + inline void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); } + inline void set_bool(expr* x, bool v) { if (v) { set_true(x); } else { set_false(x); } } + inline rational const& get_number(expr* x) const { return m_numbers.find(x); } + inline void set_number(expr* x, rational const& v) { + set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_numbers.insert(x,v); + } + inline expr* get_value(expr* x) { return m_values.find(x); } + inline void set_value(expr* x, expr* v) { set_v(x); m_refs.push_back(v); m_values.insert(x, v); } + + bool check_model(ptr_vector const & formulas); + + bool extract_array_func_interp(expr* a, vector& stores, expr_ref& else_case); + + void eval_exprs(expr_ref_vector& es); + +public: + model_implicant(ast_manager& m) : + m(m), m_arith(m), m_array(m), m_refs(m) {} + + /** + \brief extract equalities from model that suffice to satisfy formula. + + \pre model satisfies formulas + */ + + expr_ref_vector minimize_model(ptr_vector const & formulas, model_ref& mdl); + + /** + \brief extract literals from formulas that satisfy formulas. + + \pre model satisfies formulas + */ + expr_ref_vector minimize_literals(ptr_vector const & formulas, model_ref& mdl); + + /** + for_each_expr visitor. + */ + void operator()(expr* e) {} + + expr_ref eval(model_ref& mdl, expr* e); + + expr_ref eval(model_ref& mdl, func_decl* d); +}; + + +#endif diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index d2ac29689..f530dd7f9 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -48,6 +48,7 @@ Notes: #include "qe_util.h" #include "scoped_proof.h" #include "blast_term_ite_tactic.h" +#include "model_implicant.h" namespace pdr { @@ -1978,7 +1979,7 @@ namespace pdr { tout << "Transition:\n" << mk_pp(T, m) << "\n"; tout << "Phi:\n" << mk_pp(phi, m) << "\n";); - model_evaluator mev(m); + model_implicant mev(m); expr_ref_vector mdl(m), forms(m), Phi(m); forms.push_back(T); forms.push_back(phi); diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp index 33c98fae4..18e5b680d 100644 --- a/src/muz/pdr/pdr_util.cpp +++ b/src/muz/pdr/pdr_util.cpp @@ -90,879 +90,6 @@ namespace pdr { return res.str(); } - - - ///////////////////////// - // model_evaluator - // - - - void model_evaluator::assign_value(expr* e, expr* val) { - rational r; - if (m.is_true(val)) { - set_true(e); - } - else if (m.is_false(val)) { - set_false(e); - } - else if (m_arith.is_numeral(val, r)) { - set_number(e, r); - } - else if (m.is_value(val)) { - set_value(e, val); - } - else { - IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";); - TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";); - set_x(e); - } - } - - void model_evaluator::setup_model(model_ref& model) { - m_numbers.reset(); - m_values.reset(); - m_model = model; - rational r; - unsigned sz = model->get_num_constants(); - for (unsigned i = 0; i < sz; i++) { - func_decl * d = model->get_constant(i); - expr* val = model->get_const_interp(d); - expr* e = m.mk_const(d); - m_refs.push_back(e); - assign_value(e, val); - } - } - - void model_evaluator::reset() { - m1.reset(); - m2.reset(); - m_values.reset(); - m_visited.reset(); - m_numbers.reset(); - m_refs.reset(); - m_model = 0; - } - - expr_ref_vector model_evaluator::minimize_model(ptr_vector const & formulas, model_ref& mdl) { - setup_model(mdl); - - TRACE("pdr_verbose", - tout << "formulas:\n"; - for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; - ); - - expr_ref_vector model = prune_by_cone_of_influence(formulas); - TRACE("pdr_verbose", - tout << "pruned model:\n"; - for (unsigned i = 0; i < model.size(); ++i) tout << mk_pp(model[i].get(), m) << "\n";); - - reset(); - - DEBUG_CODE( - setup_model(mdl); - VERIFY(check_model(formulas)); - reset();); - - return model; - } - - expr_ref_vector model_evaluator::minimize_literals(ptr_vector const& formulas, model_ref& mdl) { - - TRACE("pdr", - tout << "formulas:\n"; - for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; - ); - - expr_ref_vector result(m); - expr_ref tmp(m); - ptr_vector tocollect; - - setup_model(mdl); - collect(formulas, tocollect); - for (unsigned i = 0; i < tocollect.size(); ++i) { - expr* e = tocollect[i]; - expr* e1, *e2; - SASSERT(m.is_bool(e)); - SASSERT(is_true(e) || is_false(e)); - if (is_true(e)) { - result.push_back(e); - } - // hack to break disequalities for arithmetic variables. - else if (m.is_eq(e, e1, e2) && m_arith.is_int_real(e1)) { - if (get_number(e1) < get_number(e2)) { - result.push_back(m_arith.mk_lt(e1,e2)); - } - else { - result.push_back(m_arith.mk_lt(e2,e1)); - } - } - else { - result.push_back(m.mk_not(e)); - } - } - reset(); - TRACE("pdr", - tout << "minimized model:\n"; - for (unsigned i = 0; i < result.size(); ++i) tout << mk_pp(result[i].get(), m) << "\n"; - ); - - return result; - } - - void model_evaluator::process_formula(app* e, ptr_vector& todo, ptr_vector& tocollect) { - SASSERT(m.is_bool(e)); - SASSERT(is_true(e) || is_false(e)); - unsigned v = is_true(e); - unsigned sz = e->get_num_args(); - expr* const* args = e->get_args(); - if (e->get_family_id() == m.get_basic_family_id()) { - switch(e->get_decl_kind()) { - case OP_TRUE: - break; - case OP_FALSE: - break; - case OP_EQ: - case OP_IFF: - if (args[0] == args[1]) { - SASSERT(v); - // no-op - } - else if (m.is_bool(args[0])) { - todo.append(sz, args); - } - else { - tocollect.push_back(e); - } - break; - case OP_DISTINCT: - tocollect.push_back(e); - break; - case OP_ITE: - if (args[1] == args[2]) { - tocollect.push_back(args[1]); - } - else if (is_true(args[1]) && is_true(args[2])) { - todo.append(2, args+1); - } - else if (is_false(args[1]) && is_false(args[2])) { - todo.append(2, args+1); - } - else if (is_true(args[0])) { - todo.append(2, args); - } - else { - SASSERT(is_false(args[0])); - todo.push_back(args[0]); - todo.push_back(args[2]); - } - break; - case OP_AND: - if (v) { - todo.append(sz, args); - } - else { - unsigned i = 0; - for (; !is_false(args[i]) && i < sz; ++i); - if (i == sz) { - fatal_error(1); - } - VERIFY(i < sz); - todo.push_back(args[i]); - } - break; - case OP_OR: - if (v) { - unsigned i = 0; - for (; !is_true(args[i]) && i < sz; ++i); - if (i == sz) { - fatal_error(1); - } - VERIFY(i < sz); - todo.push_back(args[i]); - } - else { - todo.append(sz, args); - } - break; - case OP_XOR: - case OP_NOT: - todo.append(sz, args); - break; - case OP_IMPLIES: - if (v) { - if (is_true(args[1])) { - todo.push_back(args[1]); - } - else if (is_false(args[0])) { - todo.push_back(args[0]); - } - else { - IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); - UNREACHABLE(); - } - } - else { - todo.append(sz, args); - } - break; - default: - IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); - UNREACHABLE(); - } - } - else { - tocollect.push_back(e); - } - } - - void model_evaluator::collect(ptr_vector const& formulas, ptr_vector& tocollect) { - ptr_vector todo; - todo.append(formulas); - m_visited.reset(); - - VERIFY(check_model(formulas)); - - while (!todo.empty()) { - app* e = to_app(todo.back()); - todo.pop_back(); - if (!m_visited.is_marked(e)) { - process_formula(e, todo, tocollect); - m_visited.mark(e, true); - } - } - m_visited.reset(); - } - - expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector const & formulas) { - ptr_vector tocollect; - collect(formulas, tocollect); - m1.reset(); - m2.reset(); - for (unsigned i = 0; i < tocollect.size(); ++i) { - TRACE("pdr_verbose", tout << "collect: " << mk_pp(tocollect[i], m) << "\n";); - for_each_expr(*this, m_visited, tocollect[i]); - } - unsigned sz = m_model->get_num_constants(); - expr_ref e(m), eq(m), val(m); - expr_ref_vector model(m); - for (unsigned i = 0; i < sz; i++) { - e = m.mk_const(m_model->get_constant(i)); - if (m_visited.is_marked(e)) { - val = eval(m_model, e); - eq = m.mk_eq(e, val); - model.push_back(eq); - } - } - m_visited.reset(); - TRACE("pdr", tout << sz << " ==> " << model.size() << "\n";); - return model; - - } - - void model_evaluator::eval_arith(app* e) { - rational r, r2; - -#define ARG1 e->get_arg(0) -#define ARG2 e->get_arg(1) - - unsigned arity = e->get_num_args(); - for (unsigned i = 0; i < arity; ++i) { - expr* arg = e->get_arg(i); - if (is_x(arg)) { - set_x(e); - return; - } - SASSERT(!is_unknown(arg)); - } - switch(e->get_decl_kind()) { - case OP_NUM: - VERIFY(m_arith.is_numeral(e, r)); - set_number(e, r); - break; - case OP_IRRATIONAL_ALGEBRAIC_NUM: - set_x(e); - break; - case OP_LE: - set_bool(e, get_number(ARG1) <= get_number(ARG2)); - break; - case OP_GE: - set_bool(e, get_number(ARG1) >= get_number(ARG2)); - break; - case OP_LT: - set_bool(e, get_number(ARG1) < get_number(ARG2)); - break; - case OP_GT: - set_bool(e, get_number(ARG1) > get_number(ARG2)); - break; - case OP_ADD: - r = rational::zero(); - for (unsigned i = 0; i < arity; ++i) { - r += get_number(e->get_arg(i)); - } - set_number(e, r); - break; - case OP_SUB: - r = get_number(e->get_arg(0)); - for (unsigned i = 1; i < arity; ++i) { - r -= get_number(e->get_arg(i)); - } - set_number(e, r); - break; - case OP_UMINUS: - SASSERT(arity == 1); - set_number(e, get_number(e->get_arg(0))); - break; - case OP_MUL: - r = rational::one(); - for (unsigned i = 0; i < arity; ++i) { - r *= get_number(e->get_arg(i)); - } - set_number(e, r); - break; - case OP_DIV: - SASSERT(arity == 2); - r = get_number(ARG2); - if (r.is_zero()) { - set_x(e); - } - else { - set_number(e, get_number(ARG1) / r); - } - break; - case OP_IDIV: - SASSERT(arity == 2); - r = get_number(ARG2); - if (r.is_zero()) { - set_x(e); - } - else { - set_number(e, div(get_number(ARG1), r)); - } - break; - case OP_REM: - // rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2) - SASSERT(arity == 2); - r = get_number(ARG2); - if (r.is_zero()) { - set_x(e); - } - else { - r2 = mod(get_number(ARG1), r); - if (r.is_neg()) r2.neg(); - set_number(e, r2); - } - break; - case OP_MOD: - SASSERT(arity == 2); - r = get_number(ARG2); - if (r.is_zero()) { - set_x(e); - } - else { - set_number(e, mod(get_number(ARG1), r)); - } - break; - case OP_TO_REAL: - SASSERT(arity == 1); - set_number(e, get_number(ARG1)); - break; - case OP_TO_INT: - SASSERT(arity == 1); - set_number(e, floor(get_number(ARG1))); - break; - case OP_IS_INT: - SASSERT(arity == 1); - set_bool(e, get_number(ARG1).is_int()); - break; - case OP_POWER: - set_x(e); - break; - default: - IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); - UNREACHABLE(); - break; - } - } - - void model_evaluator::inherit_value(expr* e, expr* v) { - expr* w; - SASSERT(!is_unknown(v)); - SASSERT(m.get_sort(e) == m.get_sort(v)); - if (is_x(v)) { - set_x(e); - } - else if (m.is_bool(e)) { - SASSERT(m.is_bool(v)); - if (is_true(v)) set_true(e); - else if (is_false(v)) set_false(e); - else { - TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";); - set_x(e); - } - } - else if (m_arith.is_int_real(e)) { - set_number(e, get_number(v)); - } - else if (m.is_value(v)) { - set_value(e, v); - } - else if (m_values.find(v, w)) { - set_value(e, w); - } - else { - TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";); - set_x(e); - } - } - - void model_evaluator::eval_exprs(expr_ref_vector& es) { - model_ref mr(m_model); - for (unsigned j = 0; j < es.size(); ++j) { - if (m_array.is_as_array(es[j].get())) { - es[j] = eval(mr, es[j].get()); - } - } - } - - bool model_evaluator::extract_array_func_interp(expr* a, vector& stores, expr_ref& else_case) { - SASSERT(m_array.is_array(a)); - - TRACE("pdr", tout << mk_pp(a, m) << "\n";); - while (m_array.is_store(a)) { - expr_ref_vector store(m); - store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1); - eval_exprs(store); - stores.push_back(store); - a = to_app(a)->get_arg(0); - } - - if (m_array.is_const(a)) { - else_case = to_app(a)->get_arg(0); - return true; - } - - while (m_array.is_as_array(a)) { - func_decl* f = m_array.get_as_array_func_decl(to_app(a)); - func_interp* g = m_model->get_func_interp(f); - unsigned sz = g->num_entries(); - unsigned arity = f->get_arity(); - for (unsigned i = 0; i < sz; ++i) { - expr_ref_vector store(m); - func_entry const* fe = g->get_entry(i); - store.append(arity, fe->get_args()); - store.push_back(fe->get_result()); - for (unsigned j = 0; j < store.size(); ++j) { - if (!is_ground(store[j].get())) { - TRACE("pdr", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";); - return false; - } - } - eval_exprs(store); - stores.push_back(store); - } - else_case = g->get_else(); - if (!else_case) { - TRACE("pdr", tout << "no else case " << mk_pp(a, m) << "\n";); - return false; - } - if (!is_ground(else_case)) { - TRACE("pdr", tout << "non-ground else case " << mk_pp(a, m) << "\n" << mk_pp(else_case, m) << "\n";); - return false; - } - if (m_array.is_as_array(else_case)) { - model_ref mr(m_model); - else_case = eval(mr, else_case); - } - TRACE("pdr", tout << "else case: " << mk_pp(else_case, m) << "\n";); - return true; - } - TRACE("pdr", tout << "no translation: " << mk_pp(a, m) << "\n";); - - return false; - } - - /** - best effort evaluator of extensional array equality. - */ - void model_evaluator::eval_array_eq(app* e, expr* arg1, expr* arg2) { - TRACE("pdr", tout << "array equality: " << mk_pp(e, m) << "\n";); - expr_ref v1(m), v2(m); - m_model->eval(arg1, v1); - m_model->eval(arg2, v2); - if (v1 == v2) { - set_true(e); - return; - } - sort* s = m.get_sort(arg1); - sort* r = get_array_range(s); - // give up evaluating finite domain/range arrays - if (!r->is_infinite() && !r->is_very_big() && !s->is_infinite() && !s->is_very_big()) { - TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); - set_x(e); - return; - } - vector store; - expr_ref else1(m), else2(m); - if (!extract_array_func_interp(v1, store, else1) || - !extract_array_func_interp(v2, store, else2)) { - TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); - set_x(e); - return; - } - - if (else1 != else2) { - if (m.is_value(else1) && m.is_value(else2)) { - TRACE("pdr", tout - << "defaults are different: " << mk_pp(e, m) << " " - << mk_pp(else1, m) << " " << mk_pp(else2, m) << "\n";); - set_false(e); - } - else if (m_array.is_array(else1)) { - eval_array_eq(e, else1, else2); - } - else { - TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); - set_x(e); - } - return; - } - - expr_ref s1(m), s2(m), w1(m), w2(m); - expr_ref_vector args1(m), args2(m); - args1.push_back(v1); - args2.push_back(v2); - for (unsigned i = 0; i < store.size(); ++i) { - args1.resize(1); - args2.resize(1); - args1.append(store[i].size()-1, store[i].c_ptr()); - args2.append(store[i].size()-1, store[i].c_ptr()); - s1 = m_array.mk_select(args1.size(), args1.c_ptr()); - s2 = m_array.mk_select(args2.size(), args2.c_ptr()); - m_model->eval(s1, w1); - m_model->eval(s2, w2); - if (w1 == w2) { - continue; - } - if (m.is_value(w1) && m.is_value(w2)) { - TRACE("pdr", tout << "Equality evaluation: " << mk_pp(e, m) << "\n"; - tout << mk_pp(s1, m) << " |-> " << mk_pp(w1, m) << "\n"; - tout << mk_pp(s2, m) << " |-> " << mk_pp(w2, m) << "\n";); - set_false(e); - } - else if (m_array.is_array(w1)) { - eval_array_eq(e, w1, w2); - if (is_true(e)) { - continue; - } - } - else { - TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); - set_x(e); - } - return; - } - set_true(e); - } - - void model_evaluator::eval_eq(app* e, expr* arg1, expr* arg2) { - if (arg1 == arg2) { - set_true(e); - } - else if (m_array.is_array(arg1)) { - eval_array_eq(e, arg1, arg2); - } - else if (is_x(arg1) || is_x(arg2)) { - expr_ref eq(m), vl(m); - eq = m.mk_eq(arg1, arg2); - m_model->eval(eq, vl); - if (m.is_true(vl)) { - set_bool(e, true); - } - else if (m.is_false(vl)) { - set_bool(e, false); - } - else { - TRACE("pdr", tout << "cannot evaluate: " << mk_pp(vl, m) << "\n";); - set_x(e); - } - } - else if (m.is_bool(arg1)) { - bool val = is_true(arg1) == is_true(arg2); - SASSERT(val == (is_false(arg1) == is_false(arg2))); - if (val) { - set_true(e); - } - else { - set_false(e); - } - } - else if (m_arith.is_int_real(arg1)) { - set_bool(e, get_number(arg1) == get_number(arg2)); - } - else { - expr* e1 = get_value(arg1); - expr* e2 = get_value(arg2); - if (m.is_value(e1) && m.is_value(e2)) { - set_bool(e, e1 == e2); - } - else if (e1 == e2) { - set_bool(e, true); - } - else { - TRACE("pdr", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";); - set_x(e); - } - } - } - - void model_evaluator::eval_basic(app* e) { - expr* arg1, *arg2; - expr *argCond, *argThen, *argElse, *arg; - bool has_x = false; - unsigned arity = e->get_num_args(); - switch(e->get_decl_kind()) { - case OP_AND: - for (unsigned j = 0; j < arity; ++j) { - expr * arg = e->get_arg(j); - if (is_false(arg)) { - set_false(e); - return; - } - else if (is_x(arg)) { - has_x = true; - } - else { - SASSERT(is_true(arg)); - } - } - if (has_x) { - set_x(e); - } - else { - set_true(e); - } - break; - case OP_OR: - for (unsigned j = 0; j < arity; ++j) { - expr * arg = e->get_arg(j); - if (is_true(arg)) { - set_true(e); - return; - } - else if (is_x(arg)) { - has_x = true; - } - else { - SASSERT(is_false(arg)); - } - } - if (has_x) { - set_x(e); - } - else { - set_false(e); - } - break; - case OP_NOT: - VERIFY(m.is_not(e, arg)); - if (is_true(arg)) { - set_false(e); - } - else if (is_false(arg)) { - set_true(e); - } - else { - SASSERT(is_x(arg)); - set_x(e); - } - break; - case OP_IMPLIES: - VERIFY(m.is_implies(e, arg1, arg2)); - if (is_false(arg1) || is_true(arg2)) { - set_true(e); - } - else if (arg1 == arg2) { - set_true(e); - } - else if (is_true(arg1) && is_false(arg2)) { - set_false(e); - } - else { - SASSERT(is_x(arg1) || is_x(arg2)); - set_x(e); - } - break; - case OP_IFF: - VERIFY(m.is_iff(e, arg1, arg2)); - eval_eq(e, arg1, arg2); - break; - case OP_ITE: - VERIFY(m.is_ite(e, argCond, argThen, argElse)); - if (is_true(argCond)) { - inherit_value(e, argThen); - } - else if (is_false(argCond)) { - inherit_value(e, argElse); - } - else if (argThen == argElse) { - inherit_value(e, argThen); - } - else if (m.is_bool(e)) { - SASSERT(is_x(argCond)); - if (is_x(argThen) || is_x(argElse)) { - set_x(e); - } - else if (is_true(argThen) == is_true(argElse)) { - inherit_value(e, argThen); - } - else { - set_x(e); - } - } - else { - set_x(e); - } - break; - case OP_TRUE: - set_true(e); - break; - case OP_FALSE: - set_false(e); - break; - case OP_EQ: - VERIFY(m.is_eq(e, arg1, arg2)); - eval_eq(e, arg1, arg2); - break; - case OP_DISTINCT: { - vector values; - for (unsigned i = 0; i < arity; ++i) { - expr* arg = e->get_arg(i); - if (is_x(arg)) { - set_x(e); - return; - } - values.push_back(get_number(arg)); - } - std::sort(values.begin(), values.end()); - for (unsigned i = 0; i + 1 < values.size(); ++i) { - if (values[i] == values[i+1]) { - set_false(e); - return; - } - } - set_true(e); - break; - } - default: - IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); - UNREACHABLE(); - } - } - - bool model_evaluator::check_model(ptr_vector const& formulas) { - ptr_vector todo(formulas); - - while (!todo.empty()) { - expr * curr_e = todo.back(); - - if (!is_app(curr_e)) { - todo.pop_back(); - continue; - } - app * curr = to_app(curr_e); - - if (!is_unknown(curr)) { - todo.pop_back(); - continue; - } - unsigned arity = curr->get_num_args(); - for (unsigned i = 0; i < arity; ++i) { - if (is_unknown(curr->get_arg(i))) { - todo.push_back(curr->get_arg(i)); - } - } - if (todo.back() != curr) { - continue; - } - todo.pop_back(); - if (curr->get_family_id() == m_arith.get_family_id()) { - eval_arith(curr); - } - else if (curr->get_family_id() == m.get_basic_family_id()) { - eval_basic(curr); - } - else { - expr_ref vl(m); - m_model->eval(curr, vl); - assign_value(curr, vl); - } - - IF_VERBOSE(35,verbose_stream() << "assigned "<get_arity() == 0); - expr_ref result(m); - if (m_array.is_array(d->get_range())) { - expr_ref e(m); - e = m.mk_const(d); - result = eval(model, e); - } - else { - result = model->get_const_interp(d); - } - return result; - } - - expr_ref model_evaluator::eval(model_ref& model, expr* e) { - expr_ref result(m); - m_model = model; - VERIFY(m_model->eval(e, result, true)); - if (m_array.is_array(e)) { - vector stores; - expr_ref_vector args(m); - expr_ref else_case(m); - if (extract_array_func_interp(result, stores, else_case)) { - result = m_array.mk_const_array(m.get_sort(e), else_case); - while (!stores.empty() && stores.back().back() == else_case) { - stores.pop_back(); - } - for (unsigned i = stores.size(); i > 0; ) { - --i; - args.resize(1); - args[0] = result; - args.append(stores[i]); - result = m_array.mk_store(args.size(), args.c_ptr()); - } - return result; - } - } - return result; - } - - void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) { ast_manager& m = fml.get_manager(); expr_ref_vector conjs(m); diff --git a/src/muz/pdr/pdr_util.h b/src/muz/pdr/pdr_util.h index 150cf2bb5..29b640d74 100644 --- a/src/muz/pdr/pdr_util.h +++ b/src/muz/pdr/pdr_util.h @@ -54,86 +54,6 @@ namespace pdr { std::string pp_cube(unsigned sz, app * const * lits, ast_manager& manager); std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& manager); - class model_evaluator { - ast_manager& m; - arith_util m_arith; - array_util m_array; - obj_map m_numbers; - expr_ref_vector m_refs; - obj_map m_values; - model_ref m_model; - - //00 -- non-visited - //01 -- X - //10 -- false - //11 -- true - expr_mark m1; - expr_mark m2; - expr_mark m_visited; - - - void reset(); - void setup_model(model_ref& model); - void assign_value(expr* e, expr* v); - void collect(ptr_vector const& formulas, ptr_vector& tocollect); - void process_formula(app* e, ptr_vector& todo, ptr_vector& tocollect); - expr_ref_vector prune_by_cone_of_influence(ptr_vector const & formulas); - void eval_arith(app* e); - void eval_basic(app* e); - void eval_eq(app* e, expr* arg1, expr* arg2); - void eval_array_eq(app* e, expr* arg1, expr* arg2); - void inherit_value(expr* e, expr* v); - - inline bool is_unknown(expr* x) { return !m1.is_marked(x) && !m2.is_marked(x); } - inline void set_unknown(expr* x) { m1.mark(x, false); m2.mark(x, false); } - inline bool is_x(expr* x) { return !m1.is_marked(x) && m2.is_marked(x); } - inline bool is_false(expr* x) { return m1.is_marked(x) && !m2.is_marked(x); } - inline bool is_true(expr* x) { return m1.is_marked(x) && m2.is_marked(x); } - inline void set_x(expr* x) { SASSERT(is_unknown(x)); m2.mark(x); } - inline void set_v(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); } - inline void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); } - inline void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); } - inline void set_bool(expr* x, bool v) { if (v) { set_true(x); } else { set_false(x); } } - inline rational const& get_number(expr* x) const { return m_numbers.find(x); } - inline void set_number(expr* x, rational const& v) { - set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_numbers.insert(x,v); - } - inline expr* get_value(expr* x) { return m_values.find(x); } - inline void set_value(expr* x, expr* v) { set_v(x); m_refs.push_back(v); m_values.insert(x, v); } - - bool check_model(ptr_vector const & formulas); - - bool extract_array_func_interp(expr* a, vector& stores, expr_ref& else_case); - - void eval_exprs(expr_ref_vector& es); - - public: - model_evaluator(ast_manager& m) : m(m), m_arith(m), m_array(m), m_refs(m) {} - - /** - \brief extract equalities from model that suffice to satisfy formula. - - \pre model satisfies formulas - */ - - expr_ref_vector minimize_model(ptr_vector const & formulas, model_ref& mdl); - - /** - \brief extract literals from formulas that satisfy formulas. - - \pre model satisfies formulas - */ - expr_ref_vector minimize_literals(ptr_vector const & formulas, model_ref& mdl); - - /** - for_each_expr visitor. - */ - void operator()(expr* e) {} - - expr_ref eval(model_ref& mdl, expr* e); - - expr_ref eval(model_ref& mdl, func_decl* d); - }; /** \brief replace variables that are used in many disequalities by diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index a0395ab84..90420ad72 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -243,7 +243,7 @@ namespace opt { void set_solver() { opt_solver & opt_s = opt_solver::to_opt(m_original_solver); - if (opt_s.is_dumping_benchmark()) + if (opt_s.dump_benchmarks()) return; solver& current_solver = s(); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 88d1cab1f..754c32d31 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -35,7 +35,8 @@ namespace opt { m_context(mgr, m_params), m(mgr), m_objective_enabled(false), - m_is_dump(false) { + m_dump_benchmarks(false), + m_dump_count(0) { m_logic = l; if (m_logic != symbol::null) m_context.set_logic(m_logic); @@ -45,7 +46,7 @@ namespace opt { } void opt_solver::updt_params(params_ref const & p) { - m_is_dump = p.get_bool("dump_benchmarks", false); + m_dump_benchmarks = p.get_bool("dump_benchmarks", false); m_params.updt_params(p); m_context.updt_params(p); } @@ -105,22 +106,22 @@ namespace opt { static unsigned g_checksat_count = 0; - bool opt_solver::is_dumping_benchmark() { - return m_is_dump; + bool opt_solver::dump_benchmarks() { + return m_dump_benchmarks; } lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { - TRACE("opt_solver_na2as", { - tout << "opt_opt_solver::check_sat_core: " << m_context.size() << "\n"; + TRACE("opt", { + tout << "context size: " << m_context.size() << "\n"; for (unsigned i = 0; i < m_context.size(); ++i) { - tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n"; + tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n"; } }); lbool r = m_context.check(num_assumptions, assumptions); - if (m_is_dump) { + if (dump_benchmarks()) { std::stringstream file_name; - file_name << "opt_solver" << ++g_checksat_count << ".smt2"; + file_name << "opt_solver" << ++m_dump_count << ".smt2"; std::ofstream buffer(file_name.str().c_str()); to_smt2_benchmark(buffer, "opt_solver", "QF_BV"); buffer.close(); diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index e946d2131..3be11f4bc 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -46,7 +46,8 @@ namespace opt { bool m_objective_enabled; svector m_objective_vars; vector m_objective_values; - bool m_is_dump; + bool m_dump_benchmarks; + unsigned m_dump_count; statistics m_stats; public: opt_solver(ast_manager & m, params_ref const & p, symbol const & l); @@ -79,7 +80,7 @@ namespace opt { static opt_solver& to_opt(solver& s); void set_interim_stats(statistics & st); - bool is_dumping_benchmark(); + bool dump_benchmarks(); class toggle_objective { opt_solver& s; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index b46ad7e0d..46a8eb443 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -26,8 +26,6 @@ Notes: namespace smt { - bool theory_pb::s_debug_conflict = true; // false; // true; // - void theory_pb::ineq::negate() { m_lit.neg(); numeral sum(0); @@ -205,10 +203,54 @@ namespace smt { } k = k_new; } + // + // normalize coefficients that fall within a range + // k/n <= ... < k/(n-1) for some n = 1,2,... + // + // e.g, k/n <= min <= max < k/(n-1) + // k/min <= n, n-1 < k/max + // . floor(k/max) = ceil(k/min) - 1 + // . floor(k/max) < k/max + // + // example: k = 5, min = 3, max = 4: 5/3 -> 2 5/4 -> 1, n = 2 + // replace all coefficients by 1, and k by 2. + // + if (!k.is_one()) { + numeral min = coeff(0), max = coeff(0); + for (unsigned i = 1; i < size(); ++i) { + if (coeff(i) < min) min = coeff(i); + if (coeff(i) > max) max = coeff(i); + } + numeral n0 = k/max; + numeral n1 = floor(n0); + numeral n2 = ceil(k/min) - numeral::one(); + if (n1 == n2 && !n0.is_int()) { + for (unsigned i = 0; i < size(); ++i) { + args[i].second = numeral::one(); + } + k = n1 + numeral::one(); + } + } + SASSERT(well_formed()); return l_undef; } + app_ref theory_pb::ineq::to_expr(context& ctx, ast_manager& m) { + expr_ref tmp(m); + app_ref result(m); + svector coeffs; + expr_ref_vector args(m); + for (unsigned i = 0; i < size(); ++i) { + ctx.literal2expr(lit(i), tmp); + args.push_back(tmp); + coeffs.push_back(coeff(i)); + } + pb_util pb(m); + result = pb.mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), k()); + return result; + } + bool theory_pb::ineq::well_formed() const { SASSERT(k().is_pos()); uint_set vars; @@ -406,12 +448,20 @@ namespace smt { } --c.m_watch_sz; c.m_max_sum -= coeff; + if (c.max_coeff() == coeff) { + coeff = c.coeff(0); + for (unsigned i = 1; coeff != c.max_coeff() && i < c.m_watch_sz; ++i) { + if (coeff < c.coeff(i)) coeff = c.coeff(i); + } + c.set_max_coeff(coeff); + } // current index of unwatched literal is c.watch_size(). } void theory_pb::add_watch(ineq& c, unsigned i) { - bool_var v = c.lit(i).var(); + literal lit = c.lit(i); + bool_var v = lit.var(); c.m_max_sum += c.coeff(i); SASSERT(i >= c.watch_size()); if (i > c.watch_size()) { @@ -419,9 +469,9 @@ namespace smt { } ++c.m_watch_sz; ptr_vector* ineqs; - if (!m_watch.find(v, ineqs)) { + if (!m_watch.find(lit.index(), ineqs)) { ineqs = alloc(ptr_vector); - m_watch.insert(v, ineqs); + m_watch.insert(lit.index(), ineqs); } ineqs->push_back(&c); } @@ -500,8 +550,8 @@ namespace smt { void theory_pb::assign_eh(bool_var v, bool is_true) { context& ctx = get_context(); ptr_vector* ineqs = 0; - - if (m_watch.find(v, ineqs)) { + literal lit(v, !is_true); + if (m_watch.find(lit.index(), ineqs)) { for (unsigned i = 0; i < ineqs->size(); ++i) { if (assign_watch(v, is_true, *ineqs, i)) { // i was removed from watch list. @@ -572,7 +622,7 @@ namespace smt { if (maxsum < c.k()) { literal_vector& lits = get_unhelpful_literals(c, false); lits.push_back(~c.lit()); - add_clause(c, ~lits[0], lits); + add_clause(c, lits); } else { c.m_max_sum = numeral::zero(); @@ -601,68 +651,63 @@ namespace smt { unsigned w = c.find_lit(v, 0, c.watch_size()); SASSERT(ctx.get_assignment(c.lit()) == l_true); + SASSERT(is_true == c.lit(w).sign()); - if (is_true == c.lit(w).sign()) { - // - // max_sum is decreased. - // Adjust set of watched literals. - // - - numeral k = c.k(); - numeral coeff = c.coeff(w); - - for (unsigned i = c.watch_size(); c.max_sum() - coeff < k + c.max_coeff() && i < c.size(); ++i) { - if (ctx.get_assignment(c.lit(i)) != l_false) { - add_watch(c, i); - } - } - + // + // max_sum is decreased. + // Adjust set of watched literals. + // - if (c.max_sum() - coeff < k) { - // - // L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0, x2 <- 0 - // create clause x1 or x2 or ~L - // - literal_vector& lits = get_unhelpful_literals(c, false); - lits.push_back(~c.lit()); - add_clause(c, literal(v, !is_true), lits); + numeral k = c.k(); + numeral coeff = c.coeff(w); + + for (unsigned i = c.watch_size(); c.max_sum() - coeff < k + c.max_coeff() && i < c.size(); ++i) { + if (ctx.get_assignment(c.lit(i)) != l_false) { + add_watch(c, i); } - else { - del_watch(watch, watch_index, c, w); - removed = true; - if (c.max_sum() - coeff < k + c.max_coeff()) { - - // - // opportunities for unit propagation for unassigned - // literals whose coefficients satisfy - // c.max_sum() - coeff < k - // - // L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0 - // Create clauses x1 or ~L or x2 - // x1 or ~L or x4 - // - - literal_vector& lits = get_unhelpful_literals(c, true); - lits.push_back(c.lit()); - for (unsigned i = 0; i < c.size(); ++i) { - if (c.max_sum() - c.coeff(i) < k && ctx.get_assignment(c.lit(i)) == l_undef) { - add_assign(c, lits, c.lit(i)); - } + } + + if (c.max_sum() - coeff < k) { + // + // L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0, x2 <- 0 + // create clause x1 or x2 or ~L + // + literal_vector& lits = get_unhelpful_literals(c, false); + lits.push_back(~c.lit()); + add_clause(c, lits); + } + else { + del_watch(watch, watch_index, c, w); + removed = true; + if (c.max_sum() - coeff < k + c.max_coeff()) { + + // + // opportunities for unit propagation for unassigned + // literals whose coefficients satisfy + // c.max_sum() - coeff < k + // + // L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0 + // Create clauses x1 or ~L or x2 + // x1 or ~L or x4 + // + + literal_vector& lits = get_unhelpful_literals(c, true); + lits.push_back(c.lit()); + for (unsigned i = 0; i < c.size(); ++i) { + if (c.max_sum() - c.coeff(i) < k && ctx.get_assignment(c.lit(i)) == l_undef) { + add_assign(c, lits, c.lit(i)); } } - // - // else: c.max_sum() >= k + c.max_coeff() - // we might miss opportunities for unit propagation if - // max_coeff is not the maximal coefficient - // of the current unassigned literal, but we can - // rely on eventually learning this from propagations. - // } + // + // else: c.max_sum() >= k + c.max_coeff() + // we might miss opportunities for unit propagation if + // max_coeff is not the maximal coefficient + // of the current unassigned literal, but we can + // rely on eventually learning this from propagations. + // } - // - // else: the current set of watch remain a potentially feasible assignment. - // TRACE("pb", tout << "assign: " << literal(v) << " <- " << is_true << "\n"; display(tout, c); ); @@ -872,9 +917,9 @@ namespace smt { while (m_assign_ineqs_trail.size() > sz) { ineq* c = m_assign_ineqs_trail.back(); for (unsigned i = 0; i < c->watch_size(); ++i) { - bool_var w = c->lit(i).var(); + literal w = c->lit(i); ptr_vector* ineqs = 0; - VERIFY(m_watch.find(w, ineqs)); + VERIFY(m_watch.find(w.index(), ineqs)); for (unsigned j = 0; j < ineqs->size(); ++j) { if ((*ineqs)[j] == c) { std::swap((*ineqs)[j],(*ineqs)[ineqs->size()-1]); @@ -904,7 +949,7 @@ namespace smt { void theory_pb::display(std::ostream& out) const { u_map*>::iterator it = m_watch.begin(), end = m_watch.end(); for (; it != end; ++it) { - out << "watch: " << literal(it->m_key) << " |-> "; + out << "watch: " << to_literal(it->m_key) << " |-> "; watch_list const& wl = *it->m_value; for (unsigned i = 0; i < wl.size(); ++i) { out << wl[i]->lit() << " "; @@ -988,7 +1033,7 @@ namespace smt { - void theory_pb::add_clause(ineq& c, literal conseq, literal_vector const& lits) { + void theory_pb::add_clause(ineq& c, literal_vector const& lits) { inc_propagations(c); m_stats.m_num_conflicts++; context& ctx = get_context(); @@ -999,21 +1044,16 @@ namespace smt { tout << "\n"; display(tout, c, true);); -#if 0 - DEBUG_CODE( - if (s_debug_conflict) { - resolve_conflict(conseq, c); - }); -#else - resolve_conflict(conseq, c); -#endif + resolve_conflict(c); + +#if 1 justification* js = 0; ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(), lits.size(), lits.c_ptr()); verbose_stream() << "\n";); // ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); - +#endif } void theory_pb::set_mark(bool_var v, unsigned idx) { @@ -1022,9 +1062,7 @@ namespace smt { m_conseq_index.resize(v+1, null_index); } SASSERT(!is_marked(v) || m_conseq_index[v] == idx); - if (m_conseq_index[v] == null_index) { - m_conseq_index[v] = idx; - } + m_conseq_index[v] = idx; } bool theory_pb::is_marked(bool_var v) const { @@ -1115,11 +1153,12 @@ namespace smt { // // modeled after sat_solver/smt_context // - void theory_pb::resolve_conflict(literal conseq, ineq& c) { + bool theory_pb::resolve_conflict(ineq& c) { - TRACE("pb", tout << "RESOLVE: " << conseq << "\n"; display(tout, c, true);); + TRACE("pb", display(tout, c, true);); bool_var v; + literal conseq; context& ctx = get_context(); unsigned& lvl = m_conflict_lvl = 0; for (unsigned i = 0; i < c.size(); ++i) { @@ -1127,12 +1166,8 @@ namespace smt { lvl = std::max(lvl, ctx.get_assign_level(c.lit(i))); } } - - SASSERT(lvl >= ctx.get_assign_level(c.lit())); - SASSERT(ctx.get_assignment(conseq) == l_true); - - if (lvl == ctx.get_base_level()) { - return; + if (lvl < ctx.get_assign_level(c.lit()) || lvl == ctx.get_base_level()) { + return false; } m_num_marks = 0; @@ -1229,52 +1264,37 @@ namespace smt { default: UNREACHABLE(); } - m_lemma.normalize(); } + for (unsigned i = 0; i < m_lemma.size(); ++i) { unset_mark(m_lemma.lit(i)); } TRACE("pb", display(tout << "lemma: ", m_lemma);); - - // TBD: - // create clause m_ineq_literals => m_lemma; - // -#if 1 hoist_maximal_values(); - IF_VERBOSE(1, display(verbose_stream() << "lemma: ", m_lemma);); - ast_manager& m = get_manager(); - svector coeffs; - expr_ref_vector args(m); - expr_ref tmp(m); - for (unsigned i = 0; i < m_lemma.size(); ++i) { - ctx.literal2expr(m_lemma.lit(i), tmp); - args.push_back(tmp); - coeffs.push_back(m_lemma.coeff(i)); + lbool is_true = m_lemma.normalize(); + + IF_VERBOSE(1, display(verbose_stream() << "lemma: ", m_lemma);); + switch(is_true) { + case l_true: + UNREACHABLE(); + return false; + case l_false: + add_assign(c, m_ineq_literals, false_literal); + break; + default: { + app_ref tmp = m_lemma.to_expr(ctx, get_manager()); + internalize_atom(tmp, false); + ctx.mark_as_relevant(tmp); + literal l(ctx.get_bool_var(tmp)); + add_assign(c, m_ineq_literals, l); + break; } - numeral k = m_lemma.k(); - tmp = m_util.mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), k); - internalize_atom(to_app(tmp), false); - //m_ineq_literals.push_back(literal(ctx.get_bool_var(tmp))); - ctx.mark_as_relevant(tmp); - //justification* mjs = 0; - //ctx.mk_clause(m_ineq_literals.size(), m_ineq_literals.c_ptr(), mjs, CLS_AUX_LEMMA, 0); - literal l(ctx.get_bool_var(tmp)); - ineq* cc = 0; - if (m_ineqs.find(l.var(), cc)) { - add_assign(*cc, m_ineq_literals, l); } - else { - ctx.assign(l, ctx.mk_justification( - theory_propagation_justification( - get_id(), ctx.get_region(), - m_ineq_literals.size(), m_ineq_literals.c_ptr(), l))); -// IF_VERBOSE(0, verbose_stream() << "Did not compile " << tmp << "\n";); - } -#endif + return true; } void theory_pb::hoist_maximal_values() { diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index dd0fd41dc..17d35c1dd 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -71,6 +71,7 @@ namespace smt { numeral const& max_sum() const { return m_max_sum; } numeral const& max_coeff() const { return m_max_coeff; } + void set_max_coeff(numeral const& n) { m_max_coeff = n; } unsigned watch_size() const { return m_watch_sz; } @@ -91,8 +92,7 @@ namespace smt { bool well_formed() const; - //static numeral gcd(numeral a, numeral b); - //static numeral lcm(numeral a, numeral b); + app_ref to_expr(context& ctx, ast_manager& m); }; @@ -119,7 +119,7 @@ namespace smt { std::ostream& display(std::ostream& out, ineq& c, bool values = false) const; virtual void display(std::ostream& out) const; - void add_clause(ineq& c, literal conseq, literal_vector const& lits); + void add_clause(ineq& c, literal_vector const& lits); void add_assign(ineq& c, literal_vector const& lits, literal l); literal_vector& get_lits(); @@ -149,7 +149,7 @@ namespace smt { void set_mark(bool_var v, unsigned idx); void unset_mark(literal l); - void resolve_conflict(literal conseq, ineq& c); + bool resolve_conflict(ineq& c); void process_antecedent(literal l, numeral coeff); void process_ineq(ineq& c, literal conseq, numeral coeff); @@ -179,6 +179,5 @@ namespace smt { virtual void restart_eh(); virtual void collect_statistics(::statistics & st) const; - static bool s_debug_conflict; }; }; diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index ec2368ba8..c5db50427 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -21,7 +21,6 @@ Notes: #include"bound_manager.h" #include"ast_pp.h" #include"expr_safe_replace.h" // NB: should use proof-producing expr_substitute in polished version. - #include"pb_decl_plugin.h" #include"arith_decl_plugin.h" @@ -31,10 +30,10 @@ class lia2card_tactic : public tactic { typedef obj_hashtable expr_set; ast_manager & m; arith_util a; - pb_util m_pb; - obj_map > m_uses; - obj_map m_converted; + pb_util m_pb; + mutable ptr_vector m_todo; expr_set m_01s; + imp(ast_manager & _m, params_ref const & p): m(_m), @@ -56,8 +55,6 @@ class lia2card_tactic : public tactic { SASSERT(g->is_well_sorted()); mc = 0; pc = 0; core = 0; m_01s.reset(); - m_uses.reset(); - m_converted.reset(); tactic_report report("cardinality-intro", *g); @@ -76,36 +73,9 @@ class lia2card_tactic : public tactic { TRACE("pb", tout << "add bound " << mk_pp(x, m) << "\n";); } } - if (m_01s.empty()) { - result.push_back(g.get()); - return; - } - expr_set::iterator it = m_01s.begin(), end = m_01s.end(); - for (; it != end; ++it) { - m_uses.insert(*it, ptr_vector()); - } - for (unsigned j = 0; j < g->size(); ++j) { - ast_mark mark; - collect_uses(mark, g->form(j)); - } - - it = m_01s.begin(), end = m_01s.end(); - for (; it != end; ++it) { - if (!validate_uses(m_uses.find(*it))) { - std::cout << "did not validate: " << mk_pp(*it, m) << "\n"; - m_uses.remove(*it); - m_01s.remove(*it); - it = m_01s.begin(); - end = m_01s.end(); - } - } - if (m_01s.empty()) { - result.push_back(g.get()); - return; - } expr_safe_replace sub(m); - extract_substitution(sub); + extract_pb_substitution(g, sub); expr_ref new_curr(m); proof_ref new_pr(m); @@ -124,248 +94,110 @@ class lia2card_tactic : public tactic { // TBD: support proof conversion (or not..) } - void extract_substitution(expr_safe_replace& sub) { - expr_set::iterator it = m_01s.begin(), end = m_01s.end(); - for (; it != end; ++it) { - extract_substitution(sub, *it); + void extract_pb_substitution(goal_ref const& g, expr_safe_replace& sub) { + ast_mark mark; + for (unsigned i = 0; i < g->size(); i++) { + extract_pb_substitution(mark, g->form(i), sub); } } - void extract_substitution(expr_safe_replace& sub, expr* x) { - ptr_vector const& use_list = m_uses.find(x); - for (unsigned i = 0; i < use_list.size(); ++i) { - expr* u = use_list[i]; - convert_01(sub, u); + void extract_pb_substitution(ast_mark& mark, expr* fml, expr_safe_replace& sub) { + expr_ref tmp(m); + m_todo.reset(); + m_todo.push_back(fml); + while (!m_todo.empty()) { + expr* e = m_todo.back(); + m_todo.pop_back(); + if (mark.is_marked(e) || !is_app(e)) { + continue; + } + mark.mark(e, true); + if (get_pb_relation(sub, e, tmp)) { + sub.insert(e, tmp); + continue; + } + app* ap = to_app(e); + m_todo.append(ap->get_num_args(), ap->get_args()); } } - expr_ref mk_le(expr* x, rational const& bound) { - if (bound.is_pos()) { - return expr_ref(m.mk_true(), m); - } - else if (bound.is_zero()) { - return expr_ref(m.mk_not(mk_01(x)), m); - } - else { - return expr_ref(m.mk_false(), m); - } - } - - expr_ref mk_ge(expr* x, rational const& bound) { - if (bound.is_one()) { - return expr_ref(mk_01(x), m); - } - else if (bound.is_pos()) { - return expr_ref(m.mk_false(), m); - } - else { - return expr_ref(m.mk_true(), m); - } - } bool is_01var(expr* x) const { return m_01s.contains(x); } - void convert_01(expr_safe_replace& sub, expr* fml) { - rational n; - unsigned k; - expr_ref_vector args(m); - expr_ref result(m); - expr* x, *y; - if (a.is_le(fml, x, y) || a.is_ge(fml, y, x)) { - if (is_01var(x) && a.is_numeral(y, n)) { - sub.insert(fml, mk_le(x, n)); - } - else if (is_01var(y) && a.is_numeral(x, n)) { - sub.insert(fml, mk_ge(y, n)); - } - else if (is_add(x, args) && is_unsigned(y, k)) { // x <= k - sub.insert(fml, m_pb.mk_at_most_k(args.size(), args.c_ptr(), k)); - } - else if (is_add(y, args) && is_unsigned(x, k)) { // k <= y <=> not (y <= k-1) - if (k == 0) - sub.insert(fml, m.mk_true()); - else - sub.insert(fml, m.mk_not(m_pb.mk_at_most_k(args.size(), args.c_ptr(), k-1))); - } - else { - UNREACHABLE(); - } - } - else if (a.is_lt(fml, x, y) || a.is_gt(fml, y, x)) { - if (is_01var(x) && a.is_numeral(y, n)) { - sub.insert(fml, mk_le(x, n-rational(1))); - } - else if (is_01var(y) && a.is_numeral(x, n)) { - sub.insert(fml, mk_ge(y, n+rational(1))); - } - else if (is_add(x, args) && is_unsigned(y, k)) { // x < k - if (k == 0) - sub.insert(fml, m.mk_false()); - else - sub.insert(fml, m_pb.mk_at_most_k(args.size(), args.c_ptr(), k-1)); - } - else if (is_add(y, args) && is_unsigned(x, k)) { // k < y <=> not (y <= k) - sub.insert(fml, m.mk_not(m_pb.mk_at_most_k(args.size(), args.c_ptr(), k))); - } - else { - UNREACHABLE(); - } - } - else if (m.is_eq(fml, x, y)) { - if (!is_01var(x)) { - std::swap(x, y); - } - else if (is_01var(x) && a.is_numeral(y, n)) { - if (n.is_one()) { - sub.insert(fml, mk_01(x)); - } - else if (n.is_zero()) { - sub.insert(fml, m.mk_not(mk_01(x))); - } - else { - sub.insert(fml, m.mk_false()); - } - } - else { - UNREACHABLE(); - } - } - else if (is_sum(fml)) { - SASSERT(m_uses.contains(fml)); - ptr_vector const& u = m_uses.find(fml); - for (unsigned i = 0; i < u.size(); ++i) { - convert_01(sub, u[i]); - } - } - else { - UNREACHABLE(); - } - } - expr_ref mk_01(expr* x) { - expr* r; - SASSERT(is_01var(x)); - if (!m_converted.find(x, r)) { - symbol name = to_app(x)->get_decl()->get_name(); - r = m.mk_fresh_const(name.str().c_str(), m.mk_bool_sort()); - m_converted.insert(x, r); - } + expr* r = m.mk_eq(x, a.mk_numeral(rational(1), m.get_sort(x))); return expr_ref(r, m); - } + } - - bool is_add(expr* x, expr_ref_vector& args) { - if (a.is_add(x)) { - app* ap = to_app(x); - for (unsigned i = 0; i < ap->get_num_args(); ++i) { - args.push_back(mk_01(ap->get_arg(i))); - } - return true; - } - else { - return false; - } - } - - bool validate_uses(ptr_vector const& use_list) { - for (unsigned i = 0; i < use_list.size(); ++i) { - if (!validate_use(use_list[i])) { - return false; - } - } - return true; - } - - bool validate_use(expr* fml) { + bool get_pb_relation(expr_safe_replace& sub, expr* fml, expr_ref& result) { expr* x, *y; - if (a.is_le(fml, x, y) || - a.is_ge(fml, x, y) || - a.is_lt(fml, x, y) || - a.is_gt(fml, x, y) || - m.is_eq(fml, x, y)) { - if (a.is_numeral(x)) { - std::swap(x,y); - } - if ((is_one(y) || a.is_zero(y)) && is_01var(x)) - return true; - if (a.is_numeral(y) && is_sum(x) && !m.is_eq(fml)) { - return true; - } - } - if (is_sum(fml)) { - SASSERT(m_uses.contains(fml)); - ptr_vector const& u = m_uses.find(fml); - for (unsigned i = 0; i < u.size(); ++i) { - if (!validate_use(u[i])) { - return false; - } - } + expr_ref_vector args(m); + vector coeffs; + rational coeff; + if ((a.is_le(fml, x, y) || a.is_ge(fml, y, x)) && + get_pb_sum(x, rational::one(), args, coeffs, coeff) && + get_pb_sum(y, -rational::one(), args, coeffs, coeff)) { + result = m_pb.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff); return true; } - TRACE("pb", tout << "Use not validated: " << mk_pp(fml, m) << "\n";); - + else if ((a.is_lt(fml, y, x) || a.is_gt(fml, x, y)) && + get_pb_sum(x, rational::one(), args, coeffs, coeff) && + get_pb_sum(y, -rational::one(), args, coeffs, coeff)) { + result = m.mk_not(m_pb.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff)); + return true; + } + else if (m.is_eq(fml, x, y) && + get_pb_sum(x, rational::one(), args, coeffs, coeff) && + get_pb_sum(y, -rational::one(), args, coeffs, coeff)) { + result = m.mk_and(m_pb.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff), + m_pb.mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff)); + return true; + } return false; } - bool is_sum(expr* x) const { + bool get_pb_sum(expr* x, rational const& mul, expr_ref_vector& args, vector& coeffs, rational& coeff) { + expr *y, *z, *u; + rational r, q; + app* f = to_app(x); + bool ok = true; if (a.is_add(x)) { - app* ap = to_app(x); - for (unsigned i = 0; i < ap->get_num_args(); ++i) { - if (!is_01var(ap->get_arg(i))) { - return false; - } + for (unsigned i = 0; ok && i < f->get_num_args(); ++i) { + ok = get_pb_sum(f->get_arg(i), mul, args, coeffs, coeff); } - return true; } - return false; - } - - bool is_unsigned(expr* x, unsigned& k) { - rational r; - if (a.is_numeral(x, r) && r.is_unsigned()) { - k = r.get_unsigned(); - SASSERT(rational(k) == r); - return true; + else if (a.is_sub(x, y, z)) { + ok = get_pb_sum(y, mul, args, coeffs, coeff); + ok = ok && get_pb_sum(z, -mul, args, coeffs, coeff); + } + else if (a.is_uminus(x, y)) { + ok = get_pb_sum(y, -mul, args, coeffs, coeff); + } + else if (a.is_mul(x, y, z) && a.is_numeral(y, r)) { + ok = get_pb_sum(z, r*mul, args, coeffs, coeff); + } + else if (a.is_mul(x, z, y) && a.is_numeral(y, r)) { + ok = get_pb_sum(z, r*mul, args, coeffs, coeff); + } + else if (m.is_ite(x, y, z, u) && a.is_numeral(z, r) && a.is_numeral(u, q)) { + args.push_back(y); + coeffs.push_back(r*mul); + args.push_back(m.mk_not(y)); + coeffs.push_back(q*mul); + } + else if (is_01var(x)) { + args.push_back(mk_01(x)); + coeffs.push_back(mul); + } + else if (a.is_numeral(x, r)) { + coeff += mul*r; } else { - return false; - } - } - - bool is_one(expr* x) { - rational r; - return a.is_numeral(x, r) && r.is_one(); - } - - void collect_uses(ast_mark& mark, expr* f) { - ptr_vector todo; - todo.push_back(f); - while (!todo.empty()) { - f = todo.back(); - todo.pop_back(); - if (mark.is_marked(f)) { - continue; - } - mark.mark(f, true); - if (is_var(f)) { - continue; - } - if (is_quantifier(f)) { - todo.push_back(to_quantifier(f)->get_expr()); - continue; - } - app* a = to_app(f); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr* arg = a->get_arg(i); - if (!m_uses.contains(arg)) { - m_uses.insert(arg, ptr_vector()); - } - m_uses.find(arg).push_back(a); - todo.push_back(arg); - } + ok = false; } + return ok; } }; @@ -426,3 +258,240 @@ tactic * mk_lia2card_tactic(ast_manager & m, params_ref const & p) { return clean(alloc(lia2card_tactic, m, p)); } + +#if 0 + void extract_substitution(expr_safe_replace& sub) { + expr_set::iterator it = m_01s.begin(), end = m_01s.end(); + for (; it != end; ++it) { + extract_substitution(sub, *it); + } + } + + void extract_substitution(expr_safe_replace& sub, expr* x) { + ptr_vector const& use_list = m_uses.find(x); + for (unsigned i = 0; i < use_list.size(); ++i) { + expr* u = use_list[i]; + convert_01(sub, u); + } + } + + expr_ref mk_le(expr* x, rational const& bound) { + if (bound.is_pos()) { + return expr_ref(m.mk_true(), m); + } + else if (bound.is_zero()) { + return expr_ref(m.mk_not(mk_01(x)), m); + } + else { + return expr_ref(m.mk_false(), m); + } + } + + expr_ref mk_ge(expr* x, rational const& bound) { + if (bound.is_one()) { + return expr_ref(mk_01(x), m); + } + else if (bound.is_pos()) { + return expr_ref(m.mk_false(), m); + } + else { + return expr_ref(m.mk_true(), m); + } + } + + void convert_01(expr_safe_replace& sub, expr* fml) { + rational n; + unsigned k; + expr_ref_vector args(m); + expr_ref result(m); + expr* x, *y; + if (a.is_le(fml, x, y) || a.is_ge(fml, y, x)) { + if (is_01var(x) && a.is_numeral(y, n)) { + sub.insert(fml, mk_le(x, n)); + } + else if (is_01var(y) && a.is_numeral(x, n)) { + sub.insert(fml, mk_ge(y, n)); + } + else if (is_01_add(x, args) && is_unsigned(y, k)) { // x <= k + sub.insert(fml, m_pb.mk_at_most_k(args.size(), args.c_ptr(), k)); + } + else if (is_01_add(y, args) && is_unsigned(x, k)) { // k <= y <=> not (y <= k-1) + if (k == 0) + sub.insert(fml, m.mk_true()); + else + sub.insert(fml, m.mk_not(m_pb.mk_at_most_k(args.size(), args.c_ptr(), k-1))); + } + else { + UNREACHABLE(); + } + } + else if (a.is_lt(fml, x, y) || a.is_gt(fml, y, x)) { + if (is_01var(x) && a.is_numeral(y, n)) { + sub.insert(fml, mk_le(x, n-rational(1))); + } + else if (is_01var(y) && a.is_numeral(x, n)) { + sub.insert(fml, mk_ge(y, n+rational(1))); + } + else if (is_01_add(x, args) && is_unsigned(y, k)) { // x < k + if (k == 0) + sub.insert(fml, m.mk_false()); + else + sub.insert(fml, m_pb.mk_at_most_k(args.size(), args.c_ptr(), k-1)); + } + else if (is_01_add(y, args) && is_unsigned(x, k)) { // k < y <=> not (y <= k) + sub.insert(fml, m.mk_not(m_pb.mk_at_most_k(args.size(), args.c_ptr(), k))); + } + else { + UNREACHABLE(); + } + } + else if (m.is_eq(fml, x, y)) { + if (!is_01var(x)) { + std::swap(x, y); + } + if (is_01var(x) && a.is_numeral(y, n)) { + if (n.is_one()) { + sub.insert(fml, mk_01(x)); + } + else if (n.is_zero()) { + sub.insert(fml, m.mk_not(mk_01(x))); + } + else { + sub.insert(fml, m.mk_false()); + } + } + else { + UNREACHABLE(); + } + } + else if (is_01_sum(fml)) { + SASSERT(m_uses.contains(fml)); + ptr_vector const& u = m_uses.find(fml); + for (unsigned i = 0; i < u.size(); ++i) { + convert_01(sub, u[i]); + } + } + else { + UNREACHABLE(); + } + } + + bool is_01_add(expr* x, expr_ref_vector& args) { + if (a.is_add(x)) { + app* ap = to_app(x); + for (unsigned i = 0; i < ap->get_num_args(); ++i) { + if (!is_01var(ap->get_arg(i))) { + return false; + } + args.push_back(mk_01(ap->get_arg(i))); + } + return true; + } + else { + return false; + } + } + + bool validate_uses(ptr_vector const& use_list) { + for (unsigned i = 0; i < use_list.size(); ++i) { + if (!validate_use(use_list[i])) { + return false; + } + } + return true; + } + + bool validate_use(expr* fml) { + expr* x, *y; + if (a.is_le(fml, x, y) || + a.is_ge(fml, x, y) || + a.is_lt(fml, x, y) || + a.is_gt(fml, x, y) || + m.is_eq(fml, x, y)) { + if (a.is_numeral(x)) { + std::swap(x,y); + } + if ((is_one(y) || a.is_zero(y)) && is_01var(x)) + return true; + if (a.is_numeral(y) && is_01_sum(x) && !m.is_eq(fml)) { + return true; + } + } + if (is_01_sum(fml)) { + SASSERT(m_uses.contains(fml)); + ptr_vector const& u = m_uses.find(fml); + for (unsigned i = 0; i < u.size(); ++i) { + if (!validate_use(u[i])) { + return false; + } + } + return true; + } + TRACE("pb", tout << "Use not validated: " << mk_pp(fml, m) << "\n";); + + return false; + } + + bool is_01_sum(expr* x) const { + if (a.is_add(x)) { + app* ap = to_app(x); + for (unsigned i = 0; i < ap->get_num_args(); ++i) { + if (!is_01var(ap->get_arg(i))) { + return false; + } + } + return true; + } + return false; + } + + + void collect_uses(ast_mark& mark, expr* f) { + m_todo.reset(); + m_todo.push_back(f); + while (!m_todo.empty()) { + f = m_todo.back(); + m_todo.pop_back(); + if (mark.is_marked(f)) { + continue; + } + mark.mark(f, true); + if (is_var(f)) { + continue; + } + if (is_quantifier(f)) { + m_todo.push_back(to_quantifier(f)->get_expr()); + continue; + } + app* a = to_app(f); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr* arg = a->get_arg(i); + if (!m_uses.contains(arg)) { + m_uses.insert(arg, ptr_vector()); + } + m_uses.find(arg).push_back(a); + m_todo.push_back(arg); + } + } + } + + bool is_unsigned(expr* x, unsigned& k) { + rational r; + if (a.is_numeral(x, r) && r.is_unsigned()) { + k = r.get_unsigned(); + SASSERT(rational(k) == r); + return true; + } + else { + return false; + } + } + + bool is_one(expr* x) { + rational r; + return a.is_numeral(x, r) && r.is_one(); + } + + }; + +#endif