mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

fix minor version numbering

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-23 01:57:03 -07:00
parent 3eac4a4aa1
commit 0b06a9b5d8
3 changed files with 25 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
CMakeLists.txt
View file

@ -11,7 +11,7 @@ if (POLICY CMP0042)
endif() endif()
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
project(Z3 VERSION 4.8.9.7 LANGUAGES CXX) project(Z3 VERSION 4.8.9.0 LANGUAGES CXX)
################################################################################ ################################################################################
# Project version # Project version

4
src/nlsat/nlsat_explain.cpp
View file

@ -1354,9 +1354,9 @@ namespace nlsat {
var max = max_var(num, ls); var max = max_var(num, ls);
SASSERT(max != null_var); SASSERT(max != null_var);
normalize(m_core2, max); normalize(m_core2, max);
TRACE("nlsat_explain", tout << "core after normalization\n"; display(tout, m_core2) << "\n";); TRACE("nlsat_explain", display(tout << "core after normalization\n", m_core2) << "\n";);
simplify(m_core2, max); simplify(m_core2, max);
TRACE("nlsat_explain", tout << "core after simplify\n"; display(tout, m_core2) << "\n";); TRACE("nlsat_explain", display(tout << "core after simplify\n", m_core2) << "\n";);
main(m_core2.size(), m_core2.c_ptr()); main(m_core2.size(), m_core2.c_ptr());
m_core2.reset(); m_core2.reset();
} }

28
src/nlsat/nlsat_solver.cpp
View file

@ -186,6 +186,7 @@ namespace nlsat {
bool m_inline_vars; bool m_inline_vars;
bool m_log_lemmas; bool m_log_lemmas;
unsigned m_max_conflicts; unsigned m_max_conflicts;
unsigned m_lemma_count;
// statistics // statistics
unsigned m_conflicts; unsigned m_conflicts;
@ -218,6 +219,7 @@ namespace nlsat {
updt_params(p); updt_params(p);
reset_statistics(); reset_statistics();
mk_true_bvar(); mk_true_bvar();
m_lemma_count = 0;
} }
~imp() { ~imp() {
@ -738,7 +740,7 @@ namespace nlsat {
display_smt2(out); display_smt2(out);
out << "(assert (not "; out << "(assert (not ";
display_smt2(out, cls) << "))\n"; display_smt2(out, cls) << "))\n";
display(out << "(echo \"", cls) << "\")\n"; display(out << "(echo \"#" << m_lemma_count << " ", cls) << "\")\n";
out << "(check-sat)\n(reset)\n"; out << "(check-sat)\n(reset)\n";
} }
@ -750,9 +752,10 @@ namespace nlsat {
for (unsigned i = 0; i < num_lits; i++) for (unsigned i = 0; i < num_lits; i++)
inc_ref(lits[i]); inc_ref(lits[i]);
inc_ref(a); inc_ref(a);
TRACE("nlsat_sort", tout << "mk_clause:\n"; display(tout, *cls); tout << "\n";); ++m_lemma_count;
TRACE("nlsat_sort", display(tout << "mk_clause:\n", *cls) << "\n";);
std::sort(cls->begin(), cls->end(), lit_lt(*this)); std::sort(cls->begin(), cls->end(), lit_lt(*this));
TRACE("nlsat_sort", tout << "after sort:\n"; display(tout, *cls); tout << "\n";); TRACE("nlsat_sort", display(tout << "#" << m_lemma_count << " after sort:\n", *cls) << "\n";);
if (learned && m_log_lemmas) { if (learned && m_log_lemmas) {
log_lemma(std::cout, *cls); log_lemma(std::cout, *cls);
} }
@ -1599,7 +1602,7 @@ namespace nlsat {
} }
void resolve_lazy_justification(bool_var b, lazy_justification const & jst) { void resolve_lazy_justification(bool_var b, lazy_justification const & jst) {
TRACE("nlsat_resolve", tout << "resolving lazy_justification for b: " << b << "\n";); TRACE("nlsat_resolve", tout << "resolving lazy_justification for b" << b << "\n";);
unsigned sz = jst.num_lits(); unsigned sz = jst.num_lits();
// Dump lemma as Mathematica formula that must be true, // Dump lemma as Mathematica formula that must be true,
@ -1785,7 +1788,7 @@ namespace nlsat {
if (t.m_kind == trail::BVAR_ASSIGNMENT) { if (t.m_kind == trail::BVAR_ASSIGNMENT) {
bool_var b = t.m_b; bool_var b = t.m_b;
if (is_marked(b)) { if (is_marked(b)) {
TRACE("nlsat_resolve", tout << "found marked bool_var: " << b << "\n"; display_atom(tout, b) << "\n";); TRACE("nlsat_resolve", tout << "found marked: b" << b << "\n"; display_atom(tout, b) << "\n";);
m_num_marks--; m_num_marks--;
reset_mark(b); reset_mark(b);
justification jst = m_justifications[b]; justification jst = m_justifications[b];
@ -2737,7 +2740,7 @@ namespace nlsat {
break; break;
case justification::LAZY: { case justification::LAZY: {
lazy_justification const& lz = *j.get_lazy(); lazy_justification const& lz = *j.get_lazy();
display(out, lz.num_lits(), lz.lits()) << "\n"; display_not(out, lz.num_lits(), lz.lits()) << "\n";
for (unsigned i = 0; i < lz.num_clauses(); ++i) { for (unsigned i = 0; i < lz.num_clauses(); ++i) {
display(out, lz.clause(i)) << "\n"; display(out, lz.clause(i)) << "\n";
} }
@ -3015,6 +3018,19 @@ namespace nlsat {
std::ostream& display(std::ostream & out, unsigned num, literal const * ls) const { std::ostream& display(std::ostream & out, unsigned num, literal const * ls) const {
return display(out, num, ls, m_display_var); return display(out, num, ls, m_display_var);
} }
std::ostream& display_not(std::ostream & out, unsigned num, literal const * ls, display_var_proc const & proc) const {
for (unsigned i = 0; i < num; i++) {
if (i > 0)
out << " or ";
display(out, ~ls[i], proc);
}
return out;
}
std::ostream& display_not(std::ostream & out, unsigned num, literal const * ls) const {
return display_not(out, num, ls, m_display_var);
}
std::ostream& display(std::ostream & out, scoped_literal_vector const & cs) { std::ostream& display(std::ostream & out, scoped_literal_vector const & cs) {
return display(out, cs.size(), cs.c_ptr(), m_display_var); return display(out, cs.size(), cs.c_ptr(), m_display_var);