mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
updated sat state
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1e143971c3
commit
dfeb4b5235
|
@ -192,8 +192,6 @@ namespace sat {
|
|||
return;
|
||||
if (!m_subsumption && !bce_enabled() && !bca_enabled() && !elim_vars_enabled())
|
||||
return;
|
||||
|
||||
// solver::scoped_disable_checkpoint _scoped_disable_checkpoint(s);
|
||||
|
||||
initialize();
|
||||
|
||||
|
@ -257,7 +255,6 @@ namespace sat {
|
|||
TRACE("sat_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
|
||||
|
||||
finalize();
|
||||
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
@ -530,7 +530,6 @@ namespace sat {
|
|||
}
|
||||
|
||||
void solver::defrag_clauses() {
|
||||
return;
|
||||
if (memory_pressure()) return;
|
||||
pop(scope_lvl());
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-defrag)\n");
|
||||
|
@ -802,9 +801,9 @@ namespace sat {
|
|||
|
||||
if (m_config.m_propagate_prefetch) {
|
||||
#if defined(__GLUC__) || defined(__clang__)
|
||||
__builtin_prefetch((const char*)(&*(m_watches[l.index()].c_ptr())));
|
||||
__builtin_prefetch((const char*)((m_watches[l.index()].c_ptr())));
|
||||
#else
|
||||
_mm_prefetch((const char*)(&*(m_watches[l.index()].c_ptr())), _MM_HINT_T1);
|
||||
_mm_prefetch((const char*)((m_watches[l.index()].c_ptr())), _MM_HINT_T1);
|
||||
#endif
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue