mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
This commit is contained in:
parent
1b5f7cd9e5
commit
bc9c6ad93d
|
@ -18,6 +18,7 @@ Author:
|
|||
|
||||
#include "sat/smt/pb_solver.h"
|
||||
#include "ast/pb_decl_plugin.h"
|
||||
#include "sat/smt/euf_solver.h"
|
||||
|
||||
namespace pb {
|
||||
|
||||
|
@ -27,8 +28,12 @@ namespace pb {
|
|||
|
||||
literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
|
||||
flet<bool> _redundant(m_is_redundant, redundant);
|
||||
if (m_pb.is_pb(e))
|
||||
return internalize_pb(e, sign, root);
|
||||
if (m_pb.is_pb(e)) {
|
||||
sat::literal lit = internalize_pb(e, sign, root);
|
||||
if (m_ctx && !root && lit != sat::null_literal)
|
||||
m_ctx->attach_lit(lit, e);
|
||||
return lit;
|
||||
}
|
||||
UNREACHABLE();
|
||||
return sat::null_literal;
|
||||
}
|
||||
|
|
|
@ -1338,7 +1338,9 @@ namespace pb {
|
|||
}
|
||||
|
||||
solver::solver(euf::solver& ctx, euf::theory_id id) :
|
||||
solver(ctx.get_manager(), ctx.get_si(), id) {}
|
||||
solver(ctx.get_manager(), ctx.get_si(), id) {
|
||||
m_ctx = &ctx;
|
||||
}
|
||||
|
||||
solver::solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id)
|
||||
: euf::th_solver(m, symbol("ba"), id),
|
||||
|
|
|
@ -80,7 +80,8 @@ namespace pb {
|
|||
sat::sat_internalizer& si;
|
||||
pb_util m_pb;
|
||||
|
||||
sat::lookahead* m_lookahead{ nullptr };
|
||||
sat::lookahead* m_lookahead = nullptr;
|
||||
euf::solver* m_ctx = nullptr;
|
||||
stats m_stats;
|
||||
small_object_allocator m_allocator;
|
||||
|
||||
|
|
Loading…
Reference in a new issue