From ed038c2a107854d64d292406b32b34d608818cdd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 22 Jun 2017 09:42:22 +0100 Subject: [PATCH 1/6] [CMake] Fix CMake warning about CMP0042 on macOS --- CMakeLists.txt | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 5ed7ee06a..6f39cac13 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -14,6 +14,11 @@ if (POLICY CMP0054) cmake_policy(SET CMP0054 OLD) endif() +if (POLICY CMP0042) + # Enable `MACOSX_RPATH` by default. + cmake_policy(SET CMP0042 NEW) +endif() + set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") project(Z3 CXX) From 2a5f1d6e93d032172f3ea4f505e4f192a8652c5f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 22 Jun 2017 10:32:35 -0700 Subject: [PATCH 2/6] add a template instantination Signed-off-by: Lev Nachmanson --- src/util/lp/dense_matrix_instances.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/lp/dense_matrix_instances.cpp b/src/util/lp/dense_matrix_instances.cpp index 1e931211d..95ba01801 100644 --- a/src/util/lp/dense_matrix_instances.cpp +++ b/src/util/lp/dense_matrix_instances.cpp @@ -11,6 +11,7 @@ template void lean::dense_matrix::apply_from_left(vector template lean::dense_matrix::dense_matrix(lean::matrix const*); template lean::dense_matrix::dense_matrix(unsigned int, unsigned int); template lean::dense_matrix& lean::dense_matrix::operator=(lean::dense_matrix const&); +template lean::dense_matrix::dense_matrix(unsigned int, unsigned int); template lean::dense_matrix >::dense_matrix(lean::matrix > const*); template void lean::dense_matrix >::apply_from_left(vector&); template lean::dense_matrix lean::operator*(lean::matrix&, lean::matrix&); From 7386f2e04535485c92733aab76290e26c3c45741 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Jun 2017 14:18:53 -0700 Subject: [PATCH 3/6] #1101 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 54909939f..0e1c150c0 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1313,17 +1313,18 @@ namespace opt { rational r = n.get_rational(); rational eps = n.get_infinitesimal(); expr_ref_vector args(m); + bool is_int = eps.is_zero() && r.is_int(); if (!inf.is_zero()) { - expr* oo = m.mk_const(symbol("oo"), m_arith.mk_int()); + expr* oo = m.mk_const(symbol("oo"), is_int ? m_arith.mk_int() : m_arith.mk_real()); if (inf.is_one()) { args.push_back(oo); } else { - args.push_back(m_arith.mk_mul(m_arith.mk_numeral(inf, inf.is_int()), oo)); + args.push_back(m_arith.mk_mul(m_arith.mk_numeral(inf, is_int), oo)); } } if (!r.is_zero()) { - args.push_back(m_arith.mk_numeral(r, r.is_int())); + args.push_back(m_arith.mk_numeral(r, is_int)); } if (!eps.is_zero()) { expr* ep = m.mk_const(symbol("epsilon"), m_arith.mk_real()); @@ -1331,7 +1332,7 @@ namespace opt { args.push_back(ep); } else { - args.push_back(m_arith.mk_mul(m_arith.mk_numeral(eps, eps.is_int()), ep)); + args.push_back(m_arith.mk_mul(m_arith.mk_numeral(eps, is_int), ep)); } } switch(args.size()) { From 9874db7458ddcda1375aedb9237a176f95e2c818 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Fri, 23 Jun 2017 09:36:09 -0400 Subject: [PATCH 4/6] [CMake] typos in cmake --- src/api/CMakeLists.txt | 2 +- src/ast/pattern/CMakeLists.txt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 8e796168f..79c5fc1c9 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -7,7 +7,7 @@ set(generated_files # Sanity check foreach (gen_file ${generated_files}) if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${gen_file}") - message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${gen_files}\"" + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${gen_file}\"" ${z3_polluted_tree_msg}) endif() endforeach() diff --git a/src/ast/pattern/CMakeLists.txt b/src/ast/pattern/CMakeLists.txt index 59e0545a1..6e8301afc 100644 --- a/src/ast/pattern/CMakeLists.txt +++ b/src/ast/pattern/CMakeLists.txt @@ -2,7 +2,7 @@ # for other components then we should refactor this code into # z3_add_component() if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/database.h") - message(FATAL_ERROR "The generated file \"database.h\"" + message(FATAL_ERROR "The generated file \"${CMAKE_CURRENT_SOURCE_DIR}/database.h\"" ${z3_polluted_tree_msg}) endif() From 0dead22dca50d07207e0fd816be4b3e441cdb0b1 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Fri, 23 Jun 2017 09:36:44 -0400 Subject: [PATCH 5/6] fix missing initialization --- src/muz/transforms/dl_mk_quantifier_abstraction.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index 5c0d442df..a22a67416 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -142,7 +142,8 @@ namespace datalog { m(ctx.get_manager()), m_ctx(ctx), a(m), - m_refs(m) { + m_refs(m), + m_mc(NULL){ } mk_quantifier_abstraction::~mk_quantifier_abstraction() { From c7fbab0c1160b069a2f6458e621a2f04185a7d8a Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Fri, 23 Jun 2017 09:37:19 -0400 Subject: [PATCH 6/6] propagate rule names during xform --- src/muz/rel/dl_mk_similarity_compressor.cpp | 2 +- src/muz/rel/dl_mk_simple_joins.cpp | 2 +- src/muz/transforms/dl_mk_slice.cpp | 2 +- src/muz/transforms/dl_mk_unbound_compressor.cpp | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/muz/rel/dl_mk_similarity_compressor.cpp b/src/muz/rel/dl_mk_similarity_compressor.cpp index 75caba6ae..b65ed455c 100644 --- a/src/muz/rel/dl_mk_similarity_compressor.cpp +++ b/src/muz/rel/dl_mk_similarity_compressor.cpp @@ -426,7 +426,7 @@ namespace datalog { new_negs.push_back(false); rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), - new_negs.c_ptr()); + new_negs.c_ptr(), r->name()); m_result_rules.push_back(new_rule); //TODO: allow for a rule to have multiple parent objects diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp index e428fdd2e..a8e54085d 100644 --- a/src/muz/rel/dl_mk_simple_joins.cpp +++ b/src/muz/rel/dl_mk_simple_joins.cpp @@ -726,7 +726,7 @@ namespace datalog { } rule * new_rule = m_context.get_rule_manager().mk(orig_r->get_head(), tail.size(), tail.c_ptr(), - negs.c_ptr()); + negs.c_ptr(), orig_r->name()); new_rule->set_accounting_parent_object(m_context, orig_r); m_context.get_rule_manager().mk_rule_rewrite_proof(*orig_r, *new_rule); diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index aa910002d..cefda74e8 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -789,7 +789,7 @@ namespace datalog { tail.push_back(to_app(e)); } - new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0); + new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0, r.name()); rm.fix_unbound_vars(new_rule, false); diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp index 41b181450..78133aab7 100644 --- a/src/muz/transforms/dl_mk_unbound_compressor.cpp +++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp @@ -173,7 +173,7 @@ namespace datalog { return l_false; } else { - rule_ref new_rule(m_context.get_rule_manager().mk(r, chead), m_context.get_rule_manager()); + rule_ref new_rule(m_context.get_rule_manager().mk(r, chead, r->name()), m_context.get_rule_manager()); new_rule->set_accounting_parent_object(m_context, r); m_head_occurrence_ctr.dec(m_rules.get(rule_index)->get_decl());