From 04678d96282e7ef62346b5b0877201b3708115a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Aug 2013 17:56:07 -0700 Subject: [PATCH 1/4] improve error message when sorts are non-numeric Signed-off-by: Nikolaj Bjorner --- src/ast/dl_decl_plugin.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 4f0c9a75d..6d0823a24 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -657,7 +657,9 @@ namespace datalog { SASSERT(value == 1); return m.mk_true(); } - m.raise_exception("unrecognized sort"); + std::stringstream strm; + strm << "sort '" << mk_pp(s, m) << "' is not recognized as a sort that contains numeric values.\nUse Bool, BitVec, Int, Real, or a Finite domain sort"; + m.raise_exception(strm.str().c_str()); return 0; } From 01d59d2c9164d1070d895c9db7f9c78f576e169f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Aug 2013 18:36:27 -0700 Subject: [PATCH 2/4] fix bugs reported by Arie Gurfinkel Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_context.cpp | 5 +++++ src/muz_qe/pdr_generalizers.cpp | 11 ++++++----- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index fd86a4402..ff40be4f3 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1881,6 +1881,11 @@ namespace pdr { // predicate transformer (or some unfolding of it). // lbool context::expand_state(model_node& n, expr_ref_vector& result, bool& uses_level) { + TRACE("pdr", + tout << "expand_state: " << n.pt().head()->get_name(); + tout << " level: " << n.level() << "\n"; + tout << mk_pp(n.state(), m) << "\n";); + return n.pt().is_reachable(n, &result, uses_level); } diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index bf1693ce3..28226dffa 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -195,13 +195,14 @@ namespace pdr { } conv1.append(eqs); if (m_is_closure) { - conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real()))); - conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real()))); - } - else { conv1.push_back(a.mk_ge(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real()))); conv1.push_back(a.mk_ge(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real()))); } + else { + // is interior: + conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real()))); + conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real()))); + } conv1.push_back(m.mk_eq(a.mk_numeral(rational(1), a.mk_real()), a.mk_add(m_sigma[0].get(), m_sigma[1].get()))); expr_ref fml = n.pt().get_formulas(n.level(), false); expr_ref_vector fmls(m); @@ -235,7 +236,7 @@ namespace pdr { verbose_stream() << "Generalized to:\n" << mk_pp(state1, m) << "\n";); } } - if (!m_is_closure || new_cores.empty()) { + if (!m_is_closure || new_cores.size() == orig_size) { new_cores.push_back(std::make_pair(core, uses_level)); } From 7bbabcdf6dadcc133044f7b36e0647583ec63796 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 Aug 2013 14:47:48 -0700 Subject: [PATCH 3/4] updated documentation for finite domain sizes Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 8 ++++++++ src/api/z3_api.h | 2 ++ 2 files changed, 10 insertions(+) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 68cca046e..ae8b233d1 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -303,6 +303,9 @@ namespace Microsoft.Z3 /// /// Create a new finite domain sort. + /// The name used to identify the sort + /// The size of the sort + /// The result is a sort /// public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size) { @@ -315,6 +318,11 @@ namespace Microsoft.Z3 /// /// Create a new finite domain sort. + /// The name used to identify the sort + /// The size of the sort + /// The result is a sort + /// Elements of the sort are created using , + /// and the elements range from 0 to size-1. /// public FiniteDomainSort MkFiniteDomainSort(string name, ulong size) { diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 458e2f53f..2b8c74e65 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1721,6 +1721,8 @@ extern "C" { To create constants that belong to the finite domain, use the APIs for creating numerals and pass a numeric constant together with the sort returned by this call. + The numeric constant should be between 0 and the less + than the size of the domain. \sa Z3_get_finite_domain_sort_size From e43383b6a8fa70afde7a205e3cd6ec27c71ecf13 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Aug 2013 21:11:14 -0700 Subject: [PATCH 4/4] filter query predicates from models Signed-off-by: Nikolaj Bjorner --- src/muz_qe/clp_context.cpp | 10 +++++++--- src/muz_qe/dl_mk_array_blast.cpp | 2 +- src/muz_qe/dl_rule.cpp | 9 ++++++++- src/muz_qe/horn_tactic.cpp | 12 +++++++++++- 4 files changed, 27 insertions(+), 6 deletions(-) diff --git a/src/muz_qe/clp_context.cpp b/src/muz_qe/clp_context.cpp index 3a3908f59..01299a2b7 100644 --- a/src/muz_qe/clp_context.cpp +++ b/src/muz_qe/clp_context.cpp @@ -68,9 +68,13 @@ namespace datalog { m_goals.reset(); rm.mk_query(query, m_ctx.get_rules()); m_ctx.apply_default_transformation(); - func_decl *head_decl = m_ctx.get_rules().get_output_predicate(); - - expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m); + func_decl* head_decl = m_ctx.get_rules().get_output_predicate(); + rule_set& rules = m_ctx.get_rules(); + rule_vector const& rv = rules.get_predicate_rules(head_decl); + if (rv.empty()) { + return l_false; + } + expr_ref head(rv[0]->get_head(), m); ground(head); m_goals.push_back(to_app(head)); return search(20, 0); diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp index 9f057a148..2bfb6807a 100644 --- a/src/muz_qe/dl_mk_array_blast.cpp +++ b/src/muz_qe/dl_mk_array_blast.cpp @@ -250,11 +250,11 @@ namespace datalog { rule_set new_rules(m_ctx); rm.mk_rule(fml2, p, new_rules, r.name()); - TRACE("dl", new_rules.last()->display(m_ctx, tout << "new rule\n");); rule_ref new_rule(rm); if (m_simplifier.transform_rule(new_rules.last(), new_rule)) { rules.add_rule(new_rule.get()); rm.mk_rule_rewrite_proof(r, *new_rule.get()); + TRACE("dl", new_rule->display(m_ctx, tout << "new rule\n");); } return true; } diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index ac683eca9..70da4ed4b 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -41,6 +41,7 @@ Revision History: #include"expr_replacer.h" #include"bool_rewriter.h" #include"expr_safe_replace.h" +#include"filter_model_converter.h" namespace datalog { @@ -335,8 +336,14 @@ namespace datalog { vars.reverse(); names.reverse(); func_decl* qpred = m_ctx.mk_fresh_head_predicate(symbol("query"), symbol(), vars.size(), vars.c_ptr(), body_pred); - m_ctx.register_predicate(qpred, false); + m_ctx.register_predicate(qpred, false); rules.set_output_predicate(qpred); + + if (m_ctx.get_model_converter()) { + filter_model_converter* mc = alloc(filter_model_converter, m); + mc->insert(qpred); + m_ctx.add_model_converter(mc); + } expr_ref_vector qhead_args(m); for (unsigned i = 0; i < vars.size(); i++) { diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index 9d331cbfa..1916839f4 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -24,6 +24,7 @@ Revision History: #include"expr_replacer.h" #include"dl_rule_transformer.h" #include"dl_mk_slice.h" +#include"filter_model_converter.h" class horn_tactic : public tactic { struct imp { @@ -226,6 +227,9 @@ class horn_tactic : public tactic { } queries.reset(); queries.push_back(q); + filter_model_converter* mc1 = alloc(filter_model_converter, m); + mc1->insert(to_app(q)->get_decl()); + mc = mc1; } SASSERT(queries.size() == 1); q = queries[0].get(); @@ -276,7 +280,13 @@ class horn_tactic : public tactic { g->reset(); if (produce_models) { model_ref md = m_ctx.get_model(); - mc = model2model_converter(&*md); + model_converter_ref mc2 = model2model_converter(&*md); + if (mc) { + mc = concat(mc.get(), mc2.get()); + } + else { + mc = mc2; + } } break; }