mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

handle more intblast cases

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-11 15:00:06 -08:00
parent 586f0f2333
commit e93ee9fe9d
1 changed files with 0 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/intblast_solver.cpp
View file

@ -23,10 +23,7 @@ Author:
namespace intblast { namespace intblast {
solver::solver(euf::solver& ctx) : solver::solver(euf::solver& ctx) :
<<<<<<< HEAD
th_euf_solver(ctx, symbol("intblast"), ctx.get_manager().get_family_id("bv")), th_euf_solver(ctx, symbol("intblast"), ctx.get_manager().get_family_id("bv")),
=======
>>>>>>> 17c480f83 (adding band)
ctx(ctx), ctx(ctx),
s(ctx.s()), s(ctx.s()),
m(ctx.get_manager()), m(ctx.get_manager()),
@ -37,7 +34,6 @@ namespace intblast {
m_pinned(m) m_pinned(m)
{} {}
<<<<<<< HEAD
euf::theory_var solver::mk_var(euf::enode* n) { euf::theory_var solver::mk_var(euf::enode* n) {
auto r = euf::th_euf_solver::mk_var(n); auto r = euf::th_euf_solver::mk_var(n);
ctx.attach_th_var(n, this, r); ctx.attach_th_var(n, this, r);
@ -188,9 +184,6 @@ namespace intblast {
} }
lbool solver::check_solver_state() { lbool solver::check_solver_state() {
=======
lbool solver::check() {
>>>>>>> 17c480f83 (adding band)
sat::literal_vector literals; sat::literal_vector literals;
uint_set selected; uint_set selected;
for (auto const& clause : s.clauses()) { for (auto const& clause : s.clauses()) {