mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-06-23 11:34:18 -07:00
commit e3ec7e7d05
10 changed files with 19 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

5
CMakeLists.txt
View file

@ -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)

2
src/api/CMakeLists.txt
View file

@ -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()

2
src/ast/pattern/CMakeLists.txt
View file

@ -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()

2
src/muz/rel/dl_mk_similarity_compressor.cpp
View file

@ -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

2
src/muz/rel/dl_mk_simple_joins.cpp
View file

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

3
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
View file

@ -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() {

2
src/muz/transforms/dl_mk_slice.cpp
View file

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

2
src/muz/transforms/dl_mk_unbound_compressor.cpp
View file

@ -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());

9
src/opt/opt_context.cpp
View file

@ -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()) {

1
src/util/lp/dense_matrix_instances.cpp
View file

@ -11,6 +11,7 @@ template void lean::dense_matrix<double, double>::apply_from_left(vector<double>
template lean::dense_matrix<double, double>::dense_matrix(lean::matrix<double, double> const*);
template lean::dense_matrix<double, double>::dense_matrix(unsigned int, unsigned int);
template lean::dense_matrix<double, double>& lean::dense_matrix<double, double>::operator=(lean::dense_matrix<double, double> const&);
template lean::dense_matrix<lean::mpq, lean::mpq>::dense_matrix(unsigned int, unsigned int);
template lean::dense_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::dense_matrix(lean::matrix<lean::mpq, lean::numeric_pair<lean::mpq> > const*);
template void lean::dense_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::apply_from_left(vector<lean::mpq>&);
template lean::dense_matrix<lean::mpq, lean::mpq> lean::operator*<lean::mpq, lean::mpq>(lean::matrix<lean::mpq, lean::mpq>&, lean::matrix<lean::mpq, lean::mpq>&);