mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-22 05:36:41 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-11-13 19:48:09 -10:00
parent d0e139f2b3
commit 71cdbf7b72
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/nlsat/nlsat_solver.cpp
View file

@ -224,6 +224,7 @@ namespace nlsat {
bool m_dump_mathematica; bool m_dump_mathematica;
bool m_check_lemmas; bool m_check_lemmas;
unsigned m_max_conflicts; unsigned m_max_conflicts;
unsigned m_lemma_rlimit;
unsigned m_lemma_count; unsigned m_lemma_count;
unsigned m_variable_ordering_strategy; unsigned m_variable_ordering_strategy;
bool m_set_0_more; bool m_set_0_more;
@ -271,6 +272,7 @@ namespace nlsat {
reset_statistics(); reset_statistics();
mk_true_bvar(); mk_true_bvar();
m_lemma_count = 0; m_lemma_count = 0;
m_lemma_rlimit = 10 * 1000;
} }
~imp() { ~imp() {
@ -1139,8 +1141,9 @@ namespace nlsat {
used_vars[v] = true; used_vars[v] = true;
} }
TRACE(nlsat, display(tout << "(echo \"#" << ++ttt << " expl lemma ", n, cls) << "\")\n"); TRACE(nlsat, display(tout << "(echo \"#" << ++ttt << " expl lemma ", n, cls) << "\")\n");
display(out << "(echo \"#" << ttt << (is_valid?" learned " : " conflict ") , n, cls) << "\")\n"; display(out << "(echo \"#" << ttt << (is_valid ? " learned " : " conflict "), n, cls) << "\")\n";
out << "(set-logic ALL)\n"; out << "(set-logic ALL)\n";
out << "(set-option :rlimit " << m_lemma_rlimit << ")\n";
if (is_valid) { if (is_valid) {
display_smt2_bool_decls(out, used_bools); display_smt2_bool_decls(out, used_bools);
display_smt2_arith_decls(out, used_vars); display_smt2_arith_decls(out, used_vars);
@ -2243,8 +2246,9 @@ namespace nlsat {
for (var v : vars) for (var v : vars)
used_vars[v] = true; used_vars[v] = true;
} }
out << "(echo \"#" << ttt<< " assignment lemma\")\n"; out << "(echo \"#" << ttt << " assignment lemma\")\n";
out << "(set-logic ALL)\n"; out << "(set-logic ALL)\n";
out << "(set-option :rlimit " << m_lemma_rlimit << ")\n";
display_smt2_bool_decls(out, used_bools); display_smt2_bool_decls(out, used_bools);
display_smt2_arith_decls(out, used_vars); display_smt2_arith_decls(out, used_vars);
display_bool_assignment(out, false, &used_bools); display_bool_assignment(out, false, &used_bools);