From 2ca14b49fe45a09aa39c36b1856e32f5ac8843ea Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 16 May 2014 09:45:32 -0700
Subject: [PATCH] fix AV in debug assertion, address warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/cmd_context/pdecl.cpp | 2 +-
src/duality/duality.h | 2 +-
src/duality/duality_solver.cpp | 2 +-
src/muz/transforms/dl_mk_coi_filter.cpp | 18 +++++++++++++++++-
4 files changed, 20 insertions(+), 4 deletions(-)
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 4a51e4943..08a29e381 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -189,7 +189,7 @@ class psort_app : public psort {
m.inc_ref(d);
m.inc_ref(num_args, args);
SASSERT(num_args == m_decl->get_num_params() || m_decl->has_var_params());
- DEBUG_CODE(for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this););
+ DEBUG_CODE(if (num_args == num_params) { for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this); });
}
virtual void finalize(pdecl_manager & m) {
diff --git a/src/duality/duality.h b/src/duality/duality.h
index fc70ffa70..4005adc1a 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -29,7 +29,7 @@ using namespace stl_ext;
namespace Duality {
- class implicant_solver;
+ struct implicant_solver;
/* Generic operations on Z3 formulas */
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index ff3bc190b..79055b43a 100755
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -2201,7 +2201,7 @@ namespace Duality {
#endif
int expand_max = 1;
if(0&&duality->BatchExpand){
- int thing = stack.size() * 0.1;
+ int thing = stack.size() / 10; // * 0.1;
expand_max = std::max(1,thing);
if(expand_max > 1)
std::cout << "foo!\n";
diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp
index 31af7a53f..c7a8d5aa0 100644
--- a/src/muz/transforms/dl_mk_coi_filter.cpp
+++ b/src/muz/transforms/dl_mk_coi_filter.cpp
@@ -200,7 +200,23 @@ namespace datalog {
func_decl_set::iterator it = pruned_preds.begin();
extension_model_converter* mc0 = alloc(extension_model_converter, m);
for (; it != end; ++it) {
- mc0->insert(*it, m.mk_true());
+ const rule_vector& rules = source.get_predicate_rules(*it);
+ expr_ref_vector fmls(m);
+ for (unsigned i = 0; i < rules.size(); ++i) {
+ app* head = rules[i]->get_head();
+ expr_ref_vector conj(m);
+ unsigned n = head->get_num_args()-1;
+ for (unsigned j = 0; j < head->get_num_args(); ++j) {
+ expr* arg = head->get_arg(j);
+ if (!is_var(arg)) {
+ conj.push_back(m.mk_eq(m.mk_var(j, m.get_sort(arg)), arg));
+ }
+ }
+ fmls.push_back(m.mk_and(conj.size(), conj.c_ptr()));
+ }
+ expr_ref fml(m);
+ fml = m.mk_or(fmls.size(), fmls.c_ptr());
+ mc0->insert(*it, fml);
}
m_context.add_model_converter(mc0);
}