From f44631ce73e9e1d1f97416ca08dbb3618fc930cb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Oct 2012 16:13:27 -0700 Subject: [PATCH] fix bugs encountered by regression tests Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 8 +++- src/muz_qe/dl_util.cpp | 11 ++++- src/muz_qe/pdr_context.cpp | 9 +++- src/muz_qe/pdr_util.cpp | 68 ++++++++++++++++++++++--------- src/muz_qe/pdr_util.h | 8 ++-- src/muz_qe/qe_datatype_plugin.cpp | 5 ++- src/smt/theory_diff_logic_def.h | 1 + 7 files changed, 79 insertions(+), 31 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 856060a52..64df1d830 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2883,9 +2883,9 @@ proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premis ptr_vector fmls; SASSERT(positions.size() + 1 == substs.size()); for (unsigned i = 0; i < num_premises; ++i) { - TRACE("dl", tout << mk_pp(premises[i], *this) << "\n";); + TRACE("hyper_res", tout << mk_pp(premises[i], *this) << "\n";); fmls.push_back(get_fact(premises[i])); - } + } SASSERT(is_bool(concl)); vector params; for (unsigned i = 0; i < substs.size(); ++i) { @@ -2898,6 +2898,10 @@ proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premis params.push_back(parameter(positions[i].second)); } } + TRACE("hyper_res", + for (unsigned i = 0; i < params.size(); ++i) { + params[i].display(tout); tout << "\n"; + }); ptr_vector sorts; ptr_vector args; for (unsigned i = 0; i < num_premises; ++i) { diff --git a/src/muz_qe/dl_util.cpp b/src/muz_qe/dl_util.cpp index 52080ba73..4b48a1687 100644 --- a/src/muz_qe/dl_util.cpp +++ b/src/muz_qe/dl_util.cpp @@ -638,7 +638,16 @@ namespace datalog { TRACE("dl", tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n"; - tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";); + for (unsigned i = 0; i < s1.size(); ++i) { + tout << mk_pp(s1[i], m) << " "; + } + tout << "\n"; + tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n"; + for (unsigned i = 0; i < s2.size(); ++i) { + tout << mk_pp(s2[i], m) << " "; + } + tout << "\n"; + ); pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs); pc->insert(pr); diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 629ebaaae..b89e7852f 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -42,6 +42,7 @@ Notes: #include "dl_mk_rule_inliner.h" #include "ast_smt2_pp.h" #include "qe_lite.h" +#include "ast_ll_pp.h" namespace pdr { @@ -398,6 +399,9 @@ namespace pdr { lbool is_sat = m_solver.check_conjunction_as_assumptions(n.state()); if (is_sat == l_true && core) { core->reset(); + TRACE("pdr", tout << "updating model\n"; + model_smt2_pp(tout, m, *model, 0); + tout << mk_pp(n.state(), m) << "\n";); n.set_model(model); } return is_sat; @@ -758,7 +762,7 @@ namespace pdr { } r0 = const_cast(&pt().find_rule(*m_model.get())); app_ref_vector& inst = pt().get_inst(r0); - TRACE("pdr", tout << mk_pp(state(), m) << "\n";); + TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";); for (unsigned i = 0; i < inst.size(); ++i) { expr* v; if (model.find(inst[i].get(), v)) { @@ -1421,6 +1425,7 @@ namespace pdr { proof_ref proof(m); SASSERT(m_last_result == l_true); proof = m_search.get_proof_trace(*this); + TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";); apply(m, m_pc.get(), proof); return proof; } @@ -1844,7 +1849,7 @@ namespace pdr { break; } case l_true: { - strm << mk_ismt2_pp(mk_sat_answer(), m); + strm << mk_pp(mk_sat_answer(), m); break; } case l_undef: { diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index 3e1ebac46..c4a897503 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -126,9 +126,6 @@ void model_evaluator::setup_model(model_ref& model) { m_refs.push_back(e); assign_value(e, val); } - - m_level1 = m1.get_level(); - m_level2 = m2.get_level(); } void model_evaluator::reset() { @@ -170,11 +167,11 @@ expr_ref_vector model_evaluator::minimize_literals(ptr_vector const& formu tout << "formulas:\n"; for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; ); - - setup_model(mdl); + expr_ref_vector result(m); ptr_vector tocollect; - + + setup_model(mdl); collect(formulas, tocollect); for (unsigned i = 0; i < tocollect.size(); ++i) { expr* e = tocollect[i]; @@ -301,8 +298,6 @@ void model_evaluator::collect(ptr_vector const& formulas, ptr_vector ptr_vector todo; todo.append(formulas); m_visited.reset(); - m1.set_level(m_level1); - m2.set_level(m_level2); VERIFY(check_model(formulas)); @@ -923,13 +918,32 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { arith_util a; bool m_is_dl; - // NB. ite terms are non-arihmetical but their then/else branches can be. - // this gets ignored (also in static_features) + bool is_numeric(expr* e) const { + if (a.is_numeral(e)) { + return true; + } + expr* cond, *th, *el; + if (m.is_ite(e, cond, th, el)) { + return is_numeric(th) && is_numeric(el); + } + return false; + } bool is_arith_expr(expr *e) const { return is_app(e) && a.get_family_id() == to_app(e)->get_family_id(); } + bool is_var_or_numeric(expr* e) const { + if (a.is_numeral(e)) { + return true; + } + expr* cond, *th, *el; + if (m.is_ite(e, cond, th, el)) { + return is_var_or_numeric(th) && is_var_or_numeric(el); + } + return !is_arith_expr(e); + } + bool is_minus_one(expr const * e) const { rational r; return a.is_numeral(e, r) && r.is_minus_one(); } @@ -939,14 +953,14 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { SASSERT(to_app(e)->get_num_args() == 2); expr * lhs = to_app(e)->get_arg(0); expr * rhs = to_app(e)->get_arg(1); - if (!is_arith_expr(lhs) && !is_arith_expr(rhs)) + if (is_var_or_numeric(lhs) && is_var_or_numeric(rhs)) return true; - if (!a.is_numeral(rhs)) + if (!is_numeric(rhs)) std::swap(lhs, rhs); - if (!a.is_numeral(rhs)) + if (!is_numeric(rhs)) return false; // lhs can be 'x' or '(+ x (* -1 y))' - if (!is_arith_expr(lhs)) + if (is_var_or_numeric(lhs)) return true; expr* arg1, *arg2; if (!a.is_add(lhs, arg1, arg2)) @@ -960,7 +974,7 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { expr* m1, *m2; if (!a.is_mul(arg2, m1, m2)) return false; - return is_minus_one(m1) && !is_arith_expr(m2); + return is_minus_one(m1) && is_var_or_numeric(m2); } bool test_eq(expr* e) const { @@ -976,21 +990,21 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { } bool test_term(expr* e) const { - if (!is_arith_expr(e)) { - return true; - } if (m.is_bool(e)) { return true; } if (a.is_numeral(e)) { return true; } + if (is_var_or_numeric(e)) { + return true; + } expr* lhs, *rhs; if (a.is_add(e, lhs, rhs)) { if (!a.is_numeral(lhs)) { std::swap(lhs, rhs); } - return a.is_numeral(lhs) && !is_arith_expr(rhs); + return a.is_numeral(lhs) && is_var_or_numeric(rhs); } if (a.is_mul(e, lhs, rhs)) { return is_minus_one(lhs) || is_minus_one(rhs); @@ -998,6 +1012,17 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { return false; } + bool is_non_arith_or_basic(expr* e) { + if (!is_app(e)) { + return false; + } + family_id fid = to_app(e)->get_family_id(); + return + fid != m.get_basic_family_id() && + fid != null_family_id && + fid != a.get_family_id(); + } + public: test_diff_logic(ast_manager& m): m(m), a(m), m_is_dl(true) {} @@ -1011,8 +1036,11 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { else if (m.is_eq(e)) { m_is_dl = test_eq(e); } + else if (is_non_arith_or_basic(e)) { + m_is_dl = false; + } else if (is_app(e)) { - app* a = to_app(e); + app* a = to_app(e); for (unsigned i = 0; m_is_dl && i < a->get_num_args(); ++i) { m_is_dl = test_term(a->get_arg(i)); } diff --git a/src/muz_qe/pdr_util.h b/src/muz_qe/pdr_util.h index 810831592..1d1e86262 100644 --- a/src/muz_qe/pdr_util.h +++ b/src/muz_qe/pdr_util.h @@ -65,10 +65,8 @@ namespace pdr { //01 -- X //10 -- false //11 -- true - ast_fast_mark1 m1; - ast_fast_mark2 m2; - unsigned m_level1; - unsigned m_level2; + expr_mark m1; + expr_mark m2; expr_mark m_visited; @@ -84,7 +82,7 @@ namespace pdr { 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.reset_mark(x); m2.reset_mark(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); } diff --git a/src/muz_qe/qe_datatype_plugin.cpp b/src/muz_qe/qe_datatype_plugin.cpp index f200262be..c280df964 100644 --- a/src/muz_qe/qe_datatype_plugin.cpp +++ b/src/muz_qe/qe_datatype_plugin.cpp @@ -107,6 +107,7 @@ namespace qe { ast_manager& m; app_ref_vector m_recognizers; expr_ref_vector m_eqs; + expr_ref_vector m_neqs; app_ref_vector m_eq_atoms; app_ref_vector m_neq_atoms; app_ref_vector m_unsat_atoms; @@ -117,7 +118,8 @@ namespace qe { datatype_atoms(ast_manager& m) : m(m), m_recognizers(m), - m_eqs(m), + m_eqs(m), + m_neqs(m), m_eq_atoms(m), m_neq_atoms(m), m_unsat_atoms(m), m_eq_conds(m), m_util(m) {} @@ -291,6 +293,7 @@ namespace qe { } app* a = to_app(a0); if (a == x) { + m_neqs.push_back(b); return true; } if (!m_util.is_constructor(a)) { diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 779960361..f7d75be8c 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -972,6 +972,7 @@ model_value_proc * theory_diff_logic::mk_value(enode * n, model_generator & SASSERT(v != null_theory_var); numeral val = m_graph.get_assignment(v); rational num = val.get_rational().to_rational() + m_delta * val.get_infinitesimal().to_rational(); + TRACE("arith", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";); return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(n->get_owner()))); }