mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

update goal2sat interface to use explicit initialization

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-28 15:04:12 +07:00
parent 500626e814
commit 82d9e4a4fc
5 changed files with 29 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/simplifiers/dependent_expr.h
View file

@ -18,6 +18,7 @@ Author:
#pragma once #pragma once
#include "ast/ast.h" #include "ast/ast.h"
#include "ast/ast_translation.h"
class dependent_expr { class dependent_expr {
ast_manager& m; ast_manager& m;
@ -32,6 +33,15 @@ public:
m.inc_ref(fml); m.inc_ref(fml);
m.inc_ref(d); m.inc_ref(d);
} }
dependent_expr(ast_translation& tr, dependent_expr const& src) :
m(tr.to()) {
m_fml = tr(src.fml());
m.inc_ref(m_fml);
expr_dependency_translation dtr(tr);
m_dep = dtr(src.dep());
m.inc_ref(m_dep);
}
dependent_expr& operator=(dependent_expr const& other) { dependent_expr& operator=(dependent_expr const& other) {
SASSERT(&m == &other.m); SASSERT(&m == &other.m);

6
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -721,7 +721,8 @@ private:
if (m_solver.inconsistent()) if (m_solver.inconsistent())
return l_false; return l_false;
m_pc.reset(); m_pc.reset();
m_goal2sat(m, sz, fmls, m_params, m_solver, m_map, m_dep2asm, is_incremental()); m_goal2sat.init(m, m_params, m_solver, m_map, m_dep2asm, is_incremental());
m_goal2sat(sz, fmls);
if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m); if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m);
m_sat_mc->flush_smc(m_solver, m_map); m_sat_mc->flush_smc(m_solver, m_map);
return check_uninterpreted(); return check_uninterpreted();
@ -798,7 +799,8 @@ private:
fmls.append(sz, asms); fmls.append(sz, asms);
for (unsigned i = 0; i < get_num_assumptions(); ++i) for (unsigned i = 0; i < get_num_assumptions(); ++i)
fmls.push_back(get_assumption(i)); fmls.push_back(get_assumption(i));
m_goal2sat.assumptions(m, fmls.size(), fmls.data(), m_params, m_solver, m_map, m_dep2asm, is_incremental()); m_goal2sat.init(m, m_params, m_solver, m_map, m_dep2asm, is_incremental());
m_goal2sat.assumptions(fmls.size(), fmls.data());
extract_assumptions(fmls.size(), fmls.data()); extract_assumptions(fmls.size(), fmls.data());
return l_true; return l_true;
} }

5
src/sat/sat_solver/sat_smt_preprocess.cpp
View file

@ -15,8 +15,7 @@ Author:
--*/ --*/
#include "sat/sat_params.hpp"
#include "sat/sat_solver/sat_smt_preprocess.h"
#include "ast/simplifiers/bit_blaster.h" #include "ast/simplifiers/bit_blaster.h"
#include "ast/simplifiers/max_bv_sharing.h" #include "ast/simplifiers/max_bv_sharing.h"
#include "ast/simplifiers/card2bv.h" #include "ast/simplifiers/card2bv.h"
@ -24,6 +23,8 @@ Author:
#include "ast/simplifiers/rewriter_simplifier.h" #include "ast/simplifiers/rewriter_simplifier.h"
#include "ast/simplifiers/solve_eqs.h" #include "ast/simplifiers/solve_eqs.h"
#include "ast/simplifiers/eliminate_predicates.h" #include "ast/simplifiers/eliminate_predicates.h"
#include "sat/sat_params.hpp"
#include "sat/sat_solver/sat_smt_preprocess.h"
void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) { void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) {
params_ref simp1_p = p; params_ref simp1_p = p;

13
src/sat/tactic/goal2sat.cpp
View file

@ -1060,16 +1060,21 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core
(*m_imp)(g); (*m_imp)(g);
} }
void goal2sat::operator()(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external) { void goal2sat::operator()(unsigned n, expr* const* fmls) {
init(m, p, t, map, dep2asm, default_external); SASSERT(m_imp);
(*m_imp)(n, fmls); (*m_imp)(n, fmls);
} }
void goal2sat::assumptions(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external) { void goal2sat::assumptions(unsigned n, expr* const* fmls) {
init(m, p, t, map, dep2asm, default_external); SASSERT(m_imp);
m_imp->assumptions(n, fmls); m_imp->assumptions(n, fmls);
} }
sat::literal goal2sat::internalize(expr* a) {
SASSERT(m_imp);
return m_imp->internalize(a);
}
void goal2sat::get_interpreted_funs(func_decl_ref_vector& funs) { void goal2sat::get_interpreted_funs(func_decl_ref_vector& funs) {
if (m_imp) if (m_imp)

5
src/sat/tactic/goal2sat.h
View file

@ -67,12 +67,13 @@ public:
*/ */
void operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false); void operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
void operator()(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external = false); void operator()(unsigned n, expr* const* fmls);
void init(ast_manager& m, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external); void init(ast_manager& m, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external);
void assumptions(unsigned n, expr* const* fmls);
void assumptions(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external = false); sat::literal internalize(expr* a);
void get_interpreted_funs(func_decl_ref_vector& funs); void get_interpreted_funs(func_decl_ref_vector& funs);