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
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;
}
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;
}
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));
}