From 82d9e4a4fc09e401995865487de22c905a3dbb3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Nov 2022 15:04:12 +0700 Subject: [PATCH] update goal2sat interface to use explicit initialization --- src/ast/simplifiers/dependent_expr.h | 10 ++++++++++ src/sat/sat_solver/inc_sat_solver.cpp | 6 ++++-- src/sat/sat_solver/sat_smt_preprocess.cpp | 5 +++-- src/sat/tactic/goal2sat.cpp | 13 +++++++++---- src/sat/tactic/goal2sat.h | 5 +++-- 5 files changed, 29 insertions(+), 10 deletions(-) diff --git a/src/ast/simplifiers/dependent_expr.h b/src/ast/simplifiers/dependent_expr.h index f789bf332..4d16bc2bb 100644 --- a/src/ast/simplifiers/dependent_expr.h +++ b/src/ast/simplifiers/dependent_expr.h @@ -18,6 +18,7 @@ Author: #pragma once #include "ast/ast.h" +#include "ast/ast_translation.h" class dependent_expr { ast_manager& m; @@ -32,6 +33,15 @@ public: m.inc_ref(fml); 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) { SASSERT(&m == &other.m); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 6fb936435..41b8e609c 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -721,7 +721,8 @@ private: if (m_solver.inconsistent()) return l_false; 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); m_sat_mc->flush_smc(m_solver, m_map); return check_uninterpreted(); @@ -798,7 +799,8 @@ private: fmls.append(sz, asms); for (unsigned i = 0; i < get_num_assumptions(); ++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()); return l_true; } diff --git a/src/sat/sat_solver/sat_smt_preprocess.cpp b/src/sat/sat_solver/sat_smt_preprocess.cpp index 7efe0cadc..72c7c5232 100644 --- a/src/sat/sat_solver/sat_smt_preprocess.cpp +++ b/src/sat/sat_solver/sat_smt_preprocess.cpp @@ -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/max_bv_sharing.h" #include "ast/simplifiers/card2bv.h" @@ -24,6 +23,8 @@ Author: #include "ast/simplifiers/rewriter_simplifier.h" #include "ast/simplifiers/solve_eqs.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) { params_ref simp1_p = p; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 97a766df9..0f23527dd 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -1060,16 +1060,21 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core (*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) { - init(m, p, t, map, dep2asm, default_external); +void goal2sat::operator()(unsigned n, expr* const* fmls) { + SASSERT(m_imp); (*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) { - init(m, p, t, map, dep2asm, default_external); +void goal2sat::assumptions(unsigned n, expr* const* fmls) { + SASSERT(m_imp); 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) { if (m_imp) diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 5f85d59ce..d68467868 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -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()(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 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);