mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

set recorded cubes outside and remember to reset

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-31 01:52:35 -07:00
parent f0d03e99c4
commit 3ae6853e6b
4 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.h
View file

@ -137,7 +137,7 @@ namespace smt {
scoped_ptr<base_dependent_expr_state> m_fmls; scoped_ptr<base_dependent_expr_state> m_fmls;
svector<double> m_lit_scores[2]; svector<double> m_lit_scores[2];
vector<expr_ref_vector> m_recorded_cubes; vector<expr_ref_vector>* m_recorded_cubes = nullptr;
// ----------------------------------- // -----------------------------------

4
src/smt/smt_internalizer.cpp
View file

@ -967,6 +967,8 @@ namespace smt {
// following the pattern of solver::persist_clause in src/sat/smt/user_solver.cpp // following the pattern of solver::persist_clause in src/sat/smt/user_solver.cpp
void context::record_cube(unsigned num_lits, literal const *lits) { void context::record_cube(unsigned num_lits, literal const *lits) {
if (!m_recorded_cubes)
return;
expr_ref_vector cube(m); expr_ref_vector cube(m);
for (unsigned i = 0; i < num_lits; ++i) { for (unsigned i = 0; i < num_lits; ++i) {
literal lit = lits[i]; literal lit = lits[i];
@ -976,7 +978,7 @@ namespace smt {
e = m.mk_not(e); // only negate positive literal e = m.mk_not(e); // only negate positive literal
cube.push_back(e); cube.push_back(e);
} }
m_recorded_cubes.push_back(cube); m_recorded_cubes->push_back(cube);
} }
void context::add_scores(unsigned n, literal const *lits) { void context::add_scores(unsigned n, literal const *lits) {

4
src/smt/smt_parallel.cpp
View file

@ -67,6 +67,8 @@ namespace smt {
lbool parallel::param_generator::run_prefix_step() { lbool parallel::param_generator::run_prefix_step() {
IF_VERBOSE(1, verbose_stream() << " Param generator running prefix step\n"); IF_VERBOSE(1, verbose_stream() << " Param generator running prefix step\n");
ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts; ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts;
m_recorded_cubes.reset();
ctx->m_recorded_cubes = &m_recorded_cubes;
lbool r = l_undef; lbool r = l_undef;
try { try {
r = ctx->check(); r = ctx->check();
@ -110,7 +112,7 @@ namespace smt {
double score = 0.0; double score = 0.0;
// replay the cube (negation of the clause) // replay the cube (negation of the clause)
for (expr_ref_vector const& cube : probe_ctx->m_recorded_cubes) { for (expr_ref_vector const& cube : m_recorded_cubes) {
lbool r = probe_ctx->check(cube.size(), cube.data()); lbool r = probe_ctx->check(cube.size(), cube.data());
unsigned conflicts = probe_ctx->m_stats.m_num_conflicts; unsigned conflicts = probe_ctx->m_stats.m_num_conflicts;
unsigned decisions = probe_ctx->m_stats.m_num_decisions; unsigned decisions = probe_ctx->m_stats.m_num_decisions;

1
src/smt/smt_parallel.h
View file

@ -128,6 +128,7 @@ namespace smt {
unsigned m_max_prefix_conflicts = 1000; unsigned m_max_prefix_conflicts = 1000;
scoped_ptr<context> m_prefix_solver; scoped_ptr<context> m_prefix_solver;
vector<expr_ref_vector> m_recorded_cubes;
params_ref m_p; params_ref m_p;
param_values m_param_state; param_values m_param_state;