From 21b0a4fcbbe1a77eb6c54203114aee761b710cbe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2013 11:53:10 -0700 Subject: [PATCH] testing utvpi Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_context.cpp | 17 +++- src/muz_qe/pdr_context.h | 2 +- src/muz_qe/pdr_farkas_learner.cpp | 3 + src/muz_qe/pdr_prop_solver.cpp | 44 +++++----- src/smt/theory_utvpi.cpp | 1 + src/smt/theory_utvpi.h | 10 ++- src/smt/theory_utvpi_def.h | 132 +++++++++++++++++++++++++++--- 7 files changed, 176 insertions(+), 33 deletions(-) diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 62b119538..df95b1f26 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -597,7 +597,7 @@ namespace pdr { expr_ref fml = pm.mk_and(conj); th_rewriter rw(m); rw(fml); - if (ctx.is_dl()) { + if (ctx.is_dl() || ctx.is_utvpi()) { hoist_non_bool_if(fml); } TRACE("pdr", tout << mk_pp(fml, m) << "\n";); @@ -1359,9 +1359,10 @@ namespace pdr { bool m_is_bool_arith; bool m_has_arith; bool m_is_dl; + bool m_is_utvpi; public: classifier_proc(ast_manager& m, datalog::rule_set& rules): - m(m), a(m), m_is_bool(true), m_is_bool_arith(true), m_has_arith(false), m_is_dl(false) { + m(m), a(m), m_is_bool(true), m_is_bool_arith(true), m_has_arith(false), m_is_dl(false), m_is_utvpi(false) { classify(rules); } void operator()(expr* e) { @@ -1407,6 +1408,7 @@ namespace pdr { bool is_dl() const { return m_is_dl; } + bool is_utvpi() const { return m_is_utvpi; } private: @@ -1427,6 +1429,7 @@ namespace pdr { mark.reset(); m_is_dl = false; + m_is_utvpi = false; if (m_has_arith) { ptr_vector forms; for (it = rules.begin(); it != end; ++it) { @@ -1438,6 +1441,11 @@ namespace pdr { } } m_is_dl = is_difference_logic(m, forms.size(), forms.c_ptr()); +#if 0 + if (!m_is_dl) { + m_is_utvpi = is_utvpi_logic(m, forms.size(), forms.c_ptr()); + } +#endif } } @@ -1561,6 +1569,11 @@ namespace pdr { m_fparams.m_arith_mode = AS_DIFF_LOGIC; m_fparams.m_arith_expand_eqs = true; } + else if (classify.is_utvpi()) { + IF_VERBOSE(1, verbose_stream() << "UTVPI\n";); + m_fparams.m_arith_mode = AS_UTVPI; + m_fparams.m_arith_expand_eqs = true; + } } if (!use_mc && m_params.use_inductive_generalizer()) { m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0)); diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index b5652d1b6..1785991c6 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -367,7 +367,7 @@ namespace pdr { expr_ref get_answer(); bool is_dl() const { return m_fparams.m_arith_mode == AS_DIFF_LOGIC; } - + bool is_utvpi() const { return m_fparams.m_arith_mode == AS_UTVPI; } void collect_statistics(statistics& st) const; void reset_statistics(); diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp index 393090299..71404ab12 100644 --- a/src/muz_qe/pdr_farkas_learner.cpp +++ b/src/muz_qe/pdr_farkas_learner.cpp @@ -216,6 +216,9 @@ namespace pdr { } res = m.mk_not(res); th_rewriter rw(m); + params_ref params; + params.set_bool("gcd_rounding", true); + rw.updt_params(params); proof_ref pr(m); expr_ref tmp(m); rw(res, tmp, pr); diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp index 863e5c03e..f69af93e9 100644 --- a/src/muz_qe/pdr_prop_solver.cpp +++ b/src/muz_qe/pdr_prop_solver.cpp @@ -383,26 +383,32 @@ namespace pdr { fl.get_lemmas(pr, bs, lemmas); safe.elim_proxies(lemmas); fl.simplify_lemmas(lemmas); // redundant? - if (m_fparams.m_arith_mode == AS_DIFF_LOGIC && - !is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) { - IF_VERBOSE(1, - verbose_stream() << "not diff\n"; - for (unsigned i = 0; i < lemmas.size(); ++i) { - verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n"; - }); - extract_subset_core(safe); - return; + + bool outside_of_logic = + (m_fparams.m_arith_mode == AS_DIFF_LOGIC && + !is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) || + (m_fparams.m_arith_mode == AS_UTVPI && + !is_utvpi_logic(m, lemmas.size(), lemmas.c_ptr())); + + if (outside_of_logic) { + IF_VERBOSE(1, + verbose_stream() << "not diff\n"; + for (unsigned i = 0; i < lemmas.size(); ++i) { + verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n"; + }); + extract_subset_core(safe); + } + else { + + IF_VERBOSE(2, + verbose_stream() << "Lemmas\n"; + for (unsigned i = 0; i < lemmas.size(); ++i) { + verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n"; + }); + + m_core->reset(); + m_core->append(lemmas); } - - - IF_VERBOSE(2, - verbose_stream() << "Lemmas\n"; - for (unsigned i = 0; i < lemmas.size(); ++i) { - verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n"; - }); - - m_core->reset(); - m_core->append(lemmas); } lbool prop_solver::check_assumptions(const expr_ref_vector & atoms) { diff --git a/src/smt/theory_utvpi.cpp b/src/smt/theory_utvpi.cpp index e811257a6..c45cfe74a 100644 --- a/src/smt/theory_utvpi.cpp +++ b/src/smt/theory_utvpi.cpp @@ -70,6 +70,7 @@ namespace smt { } vector > const& utvpi_tester::get_linearization() const { + SASSERT(m_terms.size() <= 2); return m_terms; } diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h index 044fa11a0..40a837136 100644 --- a/src/smt/theory_utvpi.h +++ b/src/smt/theory_utvpi.h @@ -196,7 +196,7 @@ namespace smt { virtual bool internalize_term(app * term); - virtual void internalize_eq_eh(app * atom, bool_var v) {} + virtual void internalize_eq_eh(app * atom, bool_var v); virtual void assign_eh(bool_var v, bool is_true); @@ -258,6 +258,14 @@ namespace smt { private: + rational mk_value(theory_var v); + + void validate_model(); + + bool eval(expr* e); + + rational eval_num(expr* e); + bool check_z_consistency(); virtual void new_eq_eh(th_var v1, th_var v2, justification& j) { diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index c369d6826..97e00c54f 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -228,7 +228,10 @@ namespace smt { template void theory_utvpi::found_non_utvpi_expr(expr* n) { if (!m_non_utvpi_exprs) { - TRACE("utvpi", tout << "found non horn logic expression:\n" << mk_pp(n, get_manager()) << "\n";); + std::stringstream msg; + msg << "found non utvpi logic expression:\n" << mk_pp(n, get_manager()) << "\n"; + TRACE("utvpi", tout << msg.str();); + warning_msg(msg.str().c_str()); get_context().push_trail(value_trail(m_non_utvpi_exprs)); m_non_utvpi_exprs = true; } @@ -277,6 +280,24 @@ namespace smt { } } + template + void theory_utvpi::internalize_eq_eh(app * atom, bool_var v) { + context & ctx = get_context(); + app * lhs = to_app(atom->get_arg(0)); + app * rhs = to_app(atom->get_arg(1)); + if (a.is_numeral(rhs)) { + std::swap(rhs, lhs); + } + if (!a.is_numeral(rhs)) { + return; + } + if (a.is_add(lhs) || a.is_sub(lhs)) { + // force axioms for (= (+ x y) k) + // this is necessary because (+ x y) is not expressible as a utvpi term. + m_arith_eq_adapter.mk_axioms(ctx.get_enode(lhs), ctx.get_enode(rhs)); + } + } + template bool theory_utvpi::internalize_atom(app * n, bool) { context & ctx = get_context(); @@ -291,7 +312,7 @@ namespace smt { } bool is_strict = a.is_gt(n) || a.is_lt(n); - bool cl = m_test.linearize(e1, e2); + bool cl = m_test.linearize(e1, e2); if (!cl) { found_non_utvpi_expr(n); return false; @@ -324,8 +345,6 @@ namespace smt { bool theory_utvpi::internalize_term(app * term) { bool result = null_theory_var != mk_term(term); CTRACE("utvpi", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";); - TRACE("utvpi", tout << "Terms may not be internalized " << mk_pp(term, get_manager()) << "\n";); - found_non_utvpi_expr(term); return result; } @@ -478,6 +497,7 @@ namespace smt { template theory_var theory_utvpi::mk_term(app* n) { + TRACE("utvpi", tout << mk_pp(n, get_manager()) << "\n";); context& ctx = get_context(); bool cl = m_test.linearize(n); @@ -485,7 +505,7 @@ namespace smt { found_non_utvpi_expr(n); return null_theory_var; } - + coeffs coeffs; rational w; mk_coeffs(m_test.get_linearization(), coeffs, w); @@ -495,7 +515,14 @@ namespace smt { if (coeffs.size() == 1 && coeffs[0].second.is_one()) { return coeffs[0].first; } - th_var target = mk_var(ctx.mk_enode(n, false, false, true)); + if (coeffs.size() == 2) { + // do not create an alias. + return null_theory_var; + } + for (unsigned i = 0; i < n->get_num_args(); ++i) { + mk_term(to_app(n->get_arg(i))); + } + th_var target = mk_var(ctx.mk_enode(n, false, false, true)); coeffs.push_back(std::make_pair(target, rational(-1))); VERIFY(enable_edge(add_ineq(coeffs, numeral(w), null_literal))); @@ -520,7 +547,7 @@ namespace smt { v = mk_var(ctx.mk_enode(n, false, false, true)); // v = k: v <= k k <= v coeffs coeffs; - coeffs.push_back(std::make_pair(v, rational(1))); + coeffs.push_back(std::make_pair(v, rational(-1))); VERIFY(enable_edge(add_ineq(coeffs, numeral(r), null_literal))); coeffs.back().second.neg(); VERIFY(enable_edge(add_ineq(coeffs, numeral(-r), null_literal))); @@ -633,17 +660,102 @@ namespace smt { m.register_factory(m_factory); // TBD: enforce strong or tight coherence? compute_delta(); + DEBUG_CODE(validate_model();); } - + template - model_value_proc * theory_utvpi::mk_value(enode * n, model_generator & mg) { - theory_var v = n->get_th_var(get_id()); + void theory_utvpi::validate_model() { + context& ctx = get_context(); + unsigned sz = m_atoms.size(); + for (unsigned i = 0; i < sz; ++i) { + bool_var b = m_atoms[i].get_bool_var(); + bool ok = true; + expr* e = ctx.bool_var2expr(b); + switch(ctx.get_assignment(b)) { + case l_true: + ok = eval(e); + break; + case l_false: + ok = !eval(e); + break; + default: + break; + } + CTRACE("utvpi", !ok, tout << "validation failed: " << mk_pp(e, get_manager()) << "\n";); + } + } + + template + bool theory_utvpi::eval(expr* e) { + expr* e1, *e2; + if (a.is_le(e, e1, e2) || a.is_ge(e, e2, e1)) { + return eval_num(e1) <= eval_num(e2); + } + if (a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) { + return eval_num(e1) < eval_num(e2); + } + if (get_manager().is_eq(e, e1, e2)) { + return eval_num(e1) == eval_num(e2); + } + TRACE("utvpi", tout << "expression not handled: " << mk_pp(e, get_manager()) << "\n";); + return false; + } + + template + rational theory_utvpi::eval_num(expr* e) { + rational r; + expr* e1, *e2; + if (a.is_numeral(e, r)) { + return r; + } + if (a.is_sub(e, e1, e2)) { + return eval_num(e1) - eval_num(e2); + } + if (a.is_add(e)) { + r.reset(); + for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { + r += eval_num(to_app(e)->get_arg(i)); + } + return r; + } + if (a.is_mul(e)) { + r = rational(1); + for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { + r *= eval_num(to_app(e)->get_arg(i)); + } + return r; + } + if (a.is_uminus(e, e1)) { + return -eval_num(e1); + } + if (a.is_to_real(e, e1)) { + return eval_num(e1); + } + if (is_uninterp_const(e)) { + return mk_value(mk_var(e)); + } + TRACE("utvpi", tout << "expression not handled: " << mk_pp(e, get_manager()) << "\n";); + UNREACHABLE(); + return rational(0); + } + + + template + rational theory_utvpi::mk_value(th_var v) { SASSERT(v != null_theory_var); numeral val1 = m_graph.get_assignment(to_var(v)); numeral val2 = m_graph.get_assignment(neg(to_var(v))); numeral val = val1 - val2; rational num = val.get_rational() + (m_delta * val.get_infinitesimal().to_rational()); num = num/rational(2); + return num; + } + + template + model_value_proc * theory_utvpi::mk_value(enode * n, model_generator & mg) { + theory_var v = n->get_th_var(get_id()); + rational num = mk_value(v); + num = ceil(num); TRACE("utvpi", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";); return alloc(expr_wrapper_proc, m_factory->mk_value(num, a.is_int(n->get_owner()))); }