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

disable model compression for regressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-03 12:40:59 -08:00
parent 3ee5c0e7d9
commit 7399f78dfd
4 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/parsers/smt2/smt2parser.cpp
View file

@ -2677,7 +2677,7 @@ namespace smt2 {
m_ctx.regular_stream() << "(";
expr ** expr_it = expr_stack().c_ptr() + spos;
expr ** expr_end = expr_it + m_cached_strings.size();
md->compress();
// md->compress();
for (unsigned i = 0; expr_it < expr_end; expr_it++, i++) {
model::scoped_model_completion _scm(md, true);
expr_ref v = (*md)(*expr_it);

1
src/qe/qe_lite.cpp
View file

@ -2430,7 +2430,6 @@ class qe_lite_tactic : public tactic {
tactic_report report("qe-lite", *g);
proof_ref new_pr(m);
expr_ref new_f(m);
bool produce_proofs = g->proofs_enabled();
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {

2
src/sat/sat_solver.cpp
View file

@ -42,8 +42,8 @@ namespace sat {
m_checkpoint_enabled(true),
m_config(p),
m_par(nullptr),
m_cls_allocator_idx(false),
m_drat(*this),
m_cls_allocator_idx(false),
m_cleaner(*this),
m_simplifier(*this, p),
m_scc(*this, p),

4
src/util/lp/int_solver.cpp
View file

@ -282,6 +282,7 @@ void int_solver::find_feasible_solution() {
lia_move int_solver::run_gcd_test() {
if (settings().m_int_run_gcd_test) {
settings().st().m_gcd_calls++;
TRACE("int_solver", tout << "gcd-test " << settings().st().m_gcd_calls << "\n";);
if (!gcd_test()) {
settings().st().m_gcd_conflicts++;
return lia_move::conflict;
@ -291,6 +292,7 @@ lia_move int_solver::run_gcd_test() {
}
lia_move int_solver::gomory_cut() {
TRACE("int_solver", tout << "gomory " << m_number_of_calls << "\n";);
if ((m_number_of_calls) % settings().m_int_gomory_cut_period != 0)
return lia_move::undef;
@ -1052,7 +1054,7 @@ lia_move int_solver::create_branch_on_column(int j) {
m_k = m_upper? floor(get_value(j)) : ceil(get_value(j));
}
TRACE("arith_int", tout << "branching v" << j << " = " << get_value(j) << "\n";
TRACE("int_solver", tout << "branching v" << j << " = " << get_value(j) << "\n";
display_column(tout, j);
tout << "k = " << m_k << std::endl;
);