From 6c3e2e67643757811b7123e87d7dad04902689be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 Mar 2013 21:03:08 -0800 Subject: [PATCH] add default simplifications as tactic Signed-off-by: Nikolaj Bjorner --- src/muz_qe/hilbert_basis.cpp | 7 +-- src/muz_qe/horn_tactic.cpp | 85 ++++++++++++++++++++++++++++++++---- src/muz_qe/horn_tactic.h | 5 +++ 3 files changed, 86 insertions(+), 11 deletions(-) diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index c1d941c1c..e7c7928a3 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -23,8 +23,6 @@ Revision History: #include "heap_trie.h" #include "stopwatch.h" -template -class rational_map : public map {}; typedef int_hashtable > int_table; @@ -264,7 +262,10 @@ class hilbert_basis::index { void reset() { memset(this, 0, sizeof(*this)); } }; - typedef rational_map value_map; + template + class numeral_map : public map {}; + + typedef numeral_map value_map; hilbert_basis& hb; value_map m_neg; value_index m_pos; diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index 0637148d6..a8ace78aa 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -21,15 +21,18 @@ Revision History: #include"proof_converter.h" #include"horn_tactic.h" #include"dl_context.h" +#include"expr_replacer.h" class horn_tactic : public tactic { struct imp { ast_manager& m; + bool m_is_simplify; datalog::context m_ctx; smt_params m_fparams; - imp(ast_manager & m, params_ref const & p): + imp(bool is_simplify, ast_manager & m, params_ref const & p): m(m), + m_is_simplify(is_simplify), m_ctx(m, m_fparams) { updt_params(p); } @@ -180,6 +183,9 @@ class horn_tactic : public tactic { expr_ref_vector queries(m); std::stringstream msg; + m_ctx.reset(); + m_ctx.ensure_opened(); + for (unsigned i = 0; i < sz; i++) { f = g->form(i); formula_kind k = get_formula_kind(f); @@ -196,7 +202,7 @@ class horn_tactic : public tactic { } } - if (queries.size() != 1) { + if (queries.size() != 1 || m_is_simplify) { q = m.mk_fresh_const("query", m.mk_bool_sort()); register_predicate(q); for (unsigned i = 0; i < queries.size(); ++i) { @@ -208,8 +214,26 @@ class horn_tactic : public tactic { } SASSERT(queries.size() == 1); q = queries[0].get(); + if (m_is_simplify) { + simplify(q, g, result, mc, pc); + } + else { + verify(q, g, result, mc, pc); + } + } + + void verify(expr* q, + goal_ref const& g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc) { + lbool is_reachable = m_ctx.query(q); g->inc_depth(); + + bool produce_models = g->models_enabled(); + bool produce_proofs = g->proofs_enabled(); + result.push_back(g.get()); switch (is_reachable) { case l_true: { @@ -237,19 +261,60 @@ class horn_tactic : public tactic { TRACE("horn", g->display(tout);); SASSERT(g->is_well_sorted()); } + + void simplify(expr* q, + goal_ref const& g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc) { + + expr_ref fml(m); + bool produce_models = g->models_enabled(); + bool produce_proofs = g->proofs_enabled(); + + if (produce_models) { + mc = datalog::mk_skip_model_converter(); + } + if (produce_proofs) { + pc = datalog::mk_skip_proof_converter(); + } + + func_decl* query_pred = to_app(q)->get_decl(); + m_ctx.set_output_predicate(query_pred); + m_ctx.get_rules(); // flush adding rules. + m_ctx.apply_default_transformation(mc, pc); + + expr_substitution sub(m); + sub.insert(q, m.mk_false()); + scoped_ptr rep = mk_default_expr_replacer(m); + g->inc_depth(); + g->reset(); + result.push_back(g.get()); + datalog::rule_set const& rules = m_ctx.get_rules(); + datalog::rule_set::iterator it = rules.begin(), end = rules.end(); + for (; it != end; ++it) { + datalog::rule* r = *it; + r->to_formula(fml); + (*rep)(fml); + g->assert_expr(fml); + } + } + }; - + + bool m_is_simplify; params_ref m_params; statistics m_stats; imp * m_imp; public: - horn_tactic(ast_manager & m, params_ref const & p): + horn_tactic(bool is_simplify, ast_manager & m, params_ref const & p): + m_is_simplify(is_simplify), m_params(p) { - m_imp = alloc(imp, m, p); + m_imp = alloc(imp, is_simplify, m, p); } virtual tactic * translate(ast_manager & m) { - return alloc(horn_tactic, m, m_params); + return alloc(horn_tactic, m_is_simplify, m, m_params); } virtual ~horn_tactic() { @@ -293,7 +358,7 @@ public: m_imp = 0; } dealloc(d); - d = alloc(imp, m, m_params); + d = alloc(imp, m_is_simplify, m, m_params); #pragma omp critical (tactic_cancel) { m_imp = d; @@ -308,6 +373,10 @@ protected: }; tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(horn_tactic, m, p)); + return clean(alloc(horn_tactic, false, m, p)); +} + +tactic * mk_horn_simplify_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(horn_tactic, true, m, p)); } diff --git a/src/muz_qe/horn_tactic.h b/src/muz_qe/horn_tactic.h index 7f56a77ba..f041321ea 100644 --- a/src/muz_qe/horn_tactic.h +++ b/src/muz_qe/horn_tactic.h @@ -27,4 +27,9 @@ tactic * mk_horn_tactic(ast_manager & m, params_ref const & p = params_ref()); /* ADD_TACTIC("horn", "apply tactic for horn clauses.", "mk_horn_tactic(m, p)") */ + +tactic * mk_horn_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("horn-simplify", "simplify horn clauses.", "mk_horn_simplify_tactic(m, p)") +*/ #endif