mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-07 16:31:55 +00:00
Code Activity

internalize assertions during simplify

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-11 17:40:41 -07:00
parent dcd947f5ef
commit ea4bec9d03
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/smt_parallel2.cpp
View file

@ -255,6 +255,8 @@ namespace smt {
void parallel2::worker::simplify() { void parallel2::worker::simplify() {
if (!m.inc())
return;
// first attempt: one-shot simplification of the context. // first attempt: one-shot simplification of the context.
// a precise schedule of repeated simplification is TBD. // a precise schedule of repeated simplification is TBD.
// also, the in-processing simplifier should be applied to // also, the in-processing simplifier should be applied to
@ -309,6 +311,14 @@ namespace smt {
} }
ctx = new_ctx.detach(); ctx = new_ctx.detach();
ctx->internalize_assertions();
auto old_atoms = m_num_initial_atoms;
m_num_shared_units = ctx->assigned_literals().size();
m_num_initial_atoms = ctx->get_num_bool_vars();
LOG_WORKER(1, " inprocess " << old_atoms << " -> " << m_num_initial_atoms << "\n");
// TODO: copy user-propagators similar to context::copy. // TODO: copy user-propagators similar to context::copy.
} }