From 37a13b1d09f0a63548525d4389f805a629b432b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Nov 2012 14:15:24 +0200 Subject: [PATCH] update slicing to fix unbound variables. test datatype realizer Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_slice.cpp | 10 +++++-- src/muz_qe/qe_datatype_plugin.cpp | 47 ++++++++++++++++++------------- src/test/quant_solve.cpp | 36 +++++++++++++++-------- 3 files changed, 59 insertions(+), 34 deletions(-) diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp index 0b9115e57..1f1d12340 100644 --- a/src/muz_qe/dl_mk_slice.cpp +++ b/src/muz_qe/dl_mk_slice.cpp @@ -732,7 +732,7 @@ namespace datalog { void mk_slice::update_rule(rule& r, rule_set& dst) { - rule* new_rule; + rule_ref new_rule(rm); if (rule_updated(r)) { init_vars(r); app_ref_vector tail(m); @@ -794,16 +794,20 @@ namespace datalog { } + new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0); + + rm.fix_unbound_vars(new_rule, false); + TRACE("dl", r.display(m_ctx, tout << "replacing:\n"); new_rule->display(m_ctx, tout << "by:\n");); } else { new_rule = &r; } - dst.add_rule(new_rule); + dst.add_rule(new_rule.get()); if (m_pc) { - m_pc->insert(&r, new_rule, 0, 0); + m_pc->insert(&r, new_rule.get(), 0, 0); } } diff --git a/src/muz_qe/qe_datatype_plugin.cpp b/src/muz_qe/qe_datatype_plugin.cpp index c280df964..3978a9ba4 100644 --- a/src/muz_qe/qe_datatype_plugin.cpp +++ b/src/muz_qe/qe_datatype_plugin.cpp @@ -133,7 +133,7 @@ namespace qe { func_decl* f = a->get_decl(); if (m_util.is_recognizer(f) && a->get_arg(0) == x) { m_recognizers.push_back(a); - TRACE("quant_elim", tout << "add recognizer:" << mk_pp(a, m) << "\n";); + TRACE("qe", tout << "add recognizer:" << mk_pp(a, m) << "\n";); return true; } if (!m.is_eq(a)) { @@ -161,6 +161,10 @@ namespace qe { unsigned num_neqs() { return m_neq_atoms.size(); } app* neq_atom(unsigned i) { return m_neq_atoms[i].get(); } + unsigned num_neq_terms() const { return m_neqs.size(); } + expr* neq_term(unsigned i) const { return m_neqs[i]; } + expr* const* neq_terms() const { return m_neqs.c_ptr(); } + unsigned num_recognizers() { return m_recognizers.size(); } app* recognizer(unsigned i) { return m_recognizers[i].get(); } @@ -212,7 +216,7 @@ namespace qe { } void add_atom(app* a, bool is_pos) { - TRACE("quant_elim", tout << "add atom:" << mk_pp(a, m) << " " << (is_pos?"pos":"neg") << "\n";); + TRACE("qe", tout << "add atom:" << mk_pp(a, m) << " " << (is_pos?"pos":"neg") << "\n";); if (is_pos) { m_eq_atoms.push_back(a); } @@ -326,7 +330,7 @@ namespace qe { for_each_expr(*this, fml.get()); if (m_change) { fml = get_expr(fml.get()); - TRACE("quant_elim", tout << "lift:\n" << mk_pp(fml.get(), m) << "\n";); + TRACE("qe", tout << "lift:\n" << mk_pp(fml.get(), m) << "\n";); } return m_change; } @@ -380,7 +384,7 @@ namespace qe { } expr* e = m.mk_and(conj.size(), conj.c_ptr()); m_map.insert(a, e, 0); - TRACE("quant_elim", tout << "replace: " << mk_pp(a, m) << " ==> \n" << mk_pp(e, m) << "\n";); + TRACE("qe", tout << "replace: " << mk_pp(a, m) << " ==> \n" << mk_pp(e, m) << "\n";); return true; } @@ -456,7 +460,7 @@ namespace qe { virtual void assign(contains_app& x, expr* fml, rational const& vl) { sort* s = x.x()->get_decl()->get_range(); SASSERT(m_datatype_util.is_datatype(s)); - TRACE("quant_elim", tout << mk_pp(x.x(), m) << " " << vl << "\n";); + TRACE("qe", tout << mk_pp(x.x(), m) << " " << vl << "\n";); if (m_datatype_util.is_recursive(s)) { assign_rec(x, fml, vl); } @@ -468,16 +472,13 @@ namespace qe { virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) { sort* s = x.x()->get_decl()->get_range(); SASSERT(m_datatype_util.is_datatype(s)); - TRACE("quant_elim", tout << mk_pp(x.x(), m) << " " << vl << "\n";); + TRACE("qe", tout << mk_pp(x.x(), m) << " " << vl << "\n";); if (m_datatype_util.is_recursive(s)) { subst_rec(x, vl, fml, def); } else { subst_nonrec(x, vl, fml, def); } - if (def) { - *def = 0; // TBD - } } virtual unsigned get_weight( contains_app& x, expr* fml) { @@ -605,7 +606,7 @@ namespace qe { num_branches = rational(eqs.num_eqs() + 1); return true; } - TRACE("quant_elim", tout << "could not get number of branches " << mk_pp(x.x(), m) << "\n";); + TRACE("qe", tout << "could not get number of branches " << mk_pp(x.x(), m) << "\n";); return false; } @@ -660,6 +661,7 @@ namespace qe { SASSERT(m_datatype_util.is_datatype(s)); func_decl* c = 0, *r = 0; + TRACE("qe", tout << mk_pp(x, m) << " " << vl << " " << mk_pp(fml, m) << " " << (def != 0) << "\n";); // // Add recognizer to formula. // Introduce auxiliary variable to eliminate. @@ -673,13 +675,13 @@ namespace qe { m_ctx.add_var(fresh_x); m_replace->apply_substitution(x, fresh_x, 0, fml); add_def(fresh_x, def); - TRACE("quant_elim", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";); + TRACE("qe", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";); return; } if (has_selector(contains_x, fml, c)) { - TRACE("quant_elim", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";); + TRACE("qe", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";); subst_constructor(contains_x, c, fml, def); return; } @@ -721,14 +723,19 @@ namespace qe { } for (unsigned i = 0; i < eqs.num_neqs(); ++i) { - m_replace->apply_substitution(eqs.neq_atom(i), m.mk_true(), fml); + m_replace->apply_substitution(eqs.neq_atom(i), m.mk_false(), fml); } if (def) { - NOT_IMPLEMENTED_YET(); - // you need to create a diagonal term + sort* s = m.get_sort(x); + ptr_vector sorts; + sorts.resize(eqs.num_neq_terms(), s); + func_decl* diag = m.mk_func_decl(symbol("diag"), sorts.size(), sorts.c_ptr(), s); + expr_ref t(m); + t = m.mk_app(diag, eqs.num_neq_terms(), eqs.neq_terms()); + add_def(t, def); } } - TRACE("quant_elim", tout << "reduced " << mk_pp(fml.get(), m) << "\n";); + TRACE("qe", tout << "reduced " << mk_pp(fml.get(), m) << "\n";); } bool get_num_branches_nonrec( contains_app& x, expr* fml, rational& num_branches) { @@ -738,10 +745,10 @@ namespace qe { func_decl* c = 0, *r = 0; if (sz != 1 && has_recognizer(x.x(), fml, r, c)) { - TRACE("quant_elim", tout << mk_pp(x.x(), m) << " has a recognizer\n";); + TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";); num_branches = rational(1); } - TRACE("quant_elim", tout << mk_pp(x.x(), m) << " branches: " << sz << "\n";); + TRACE("qe", tout << mk_pp(x.x(), m) << " branches: " << sz << "\n";); return true; } @@ -757,7 +764,7 @@ namespace qe { } func_decl* c = 0, *r = 0; if (has_recognizer(x, fml, r, c)) { - TRACE("quant_elim", tout << mk_pp(x, m) << " has a recognizer\n";); + TRACE("qe", tout << mk_pp(x, m) << " has a recognizer\n";); return; } @@ -776,7 +783,7 @@ namespace qe { SASSERT(!m_datatype_util.is_recursive(s)); func_decl* c = 0, *r = 0; if (has_recognizer(x.x(), fml, r, c)) { - TRACE("quant_elim", tout << mk_pp(x.x(), m) << " has a recognizer\n";); + TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";); } else { unsigned sz = m_datatype_util.get_datatype_num_constructors(s); diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp index af6861af0..bae63f129 100644 --- a/src/test/quant_solve.cpp +++ b/src/test/quant_solve.cpp @@ -77,7 +77,7 @@ static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards) #endif -static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml) { +static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml, bool validate) { front_end_params params; qe::expr_quant_elim qe(m, params); qe::guarded_defs defs(m); @@ -86,7 +86,8 @@ static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* std::cout << mk_pp(fml, m) << "\n"; if (success) { defs.display(std::cout); - for (unsigned i = 0; i < defs.size(); ++i) { + + for (unsigned i = 0; validate && i < defs.size(); ++i) { validate_quant_solution(m, fml, defs.guard(i), defs.defs(i)); } } @@ -106,6 +107,10 @@ static expr_ref parse_fml(ast_manager& m, char const* str) { << "(declare-const z Int)\n" << "(declare-const a Int)\n" << "(declare-const b Int)\n" + << "(declare-const P Bool)\n" + << "(declare-const Q Bool)\n" + << "(declare-const r1 Real)\n" + << "(declare-const r2 Real)\n" << "(declare-datatypes () ((IList (nil) (cons (car Int) (cdr IList)))))\n" << "(declare-const l1 IList)\n" << "(declare-const l2 IList)\n" @@ -140,21 +145,21 @@ static void parse_fml(char const* str, app_ref_vector& vars, expr_ref& fml) { } } -static void test_quant_solver(ast_manager& m, app* x, char const* str) { +static void test_quant_solver(ast_manager& m, app* x, char const* str, bool validate = true) { expr_ref fml = parse_fml(m, str); - test_quant_solver(m, 1, &x, fml); + test_quant_solver(m, 1, &x, fml, validate); } -static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, char const* str) { +static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, char const* str, bool validate = true) { expr_ref fml = parse_fml(m, str); - test_quant_solver(m, sz, xs, fml); + test_quant_solver(m, sz, xs, fml, validate); } -static void test_quant_solver(ast_manager& m, char const* str) { +static void test_quant_solver(ast_manager& m, char const* str, bool validate = true) { expr_ref fml(m); app_ref_vector vars(m); parse_fml(str, vars, fml); - test_quant_solver(m, vars.size(), vars.c_ptr(), fml); + test_quant_solver(m, vars.size(), vars.c_ptr(), fml, validate); } @@ -222,9 +227,18 @@ static void test_quant_solve1() { test_quant_solver(m, "(exists ((c Cell)) (= c null))"); test_quant_solver(m, "(exists ((c Cell)) (= c (cell null c1)))"); - //TBD: - //test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))"); - //test_quant_solver(m, "(exists ((c Cell)) (not (= c null)))"); + + test_quant_solver(m, "(exists ((c Cell)) (not (= c null)))", false); + test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))", false); + test_quant_solver(m, "(exists ((c Cell)) (= (cell c (cdr c1)) c1))", false); + + test_quant_solver(m, "(exists ((t Tuple)) (= (tuple a P r1) t))"); + test_quant_solver(m, "(exists ((t Tuple)) (= a (first t)))"); + test_quant_solver(m, "(exists ((t Tuple)) (= P (second t)))"); + test_quant_solver(m, "(exists ((t Tuple)) (= r2 (third t)))"); + test_quant_solver(m, "(exists ((t Tuple)) (not (= a (first t))))"); + test_quant_solver(m, "(exists ((t Tuple)) (not (= P (second t))))"); + test_quant_solver(m, "(exists ((t Tuple)) (not (= r2 (third t))))"); }