mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-04-08 15:46:41 -07:00
parent f2dfc0dc24 21738d9750
commit 00685ff04f
2 changed files with 6 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_model_converter.cpp
View file

@ -75,7 +75,7 @@ namespace sat {
void model_converter::operator()(model & m) const {
vector<entry>::const_iterator begin = m_entries.begin();
vector<entry>::const_iterator it = m_entries.end();
bool first = true; // false; // true; // false; // true;
bool first = false; // true; // false; // // true;
//SASSERT(!m_solver || m_solver->check_clauses(m));
while (it != begin) {
--it;
@ -101,6 +101,7 @@ namespace sat {
if (!sat && it->get_kind() != ATE && v0 != null_bool_var) {
VERIFY(legal_to_flip(v0));
m[v0] = var_sign ? l_false : l_true;
//IF_VERBOSE(0, verbose_stream() << "assign " << v0 << " "<< m[v0] << "\n");
}
elim_stack* st = it->m_elim_stack[index];
if (st) {

14
src/sat/sat_simplifier.cpp
View file

@ -1186,7 +1186,8 @@ namespace sat {
This routine removes literals that were not relevant to establishing it was blocked.
It has a bug: literals that are used to prune tautologies during resolution intersection should be included
in the dependencies.
in the dependencies. They may get used in some RI prunings and then they have to be included to avoid flipping
RI literals.
*/
void minimize_covered_clause(unsigned idx) {
// IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause
@ -1211,8 +1212,8 @@ namespace sat {
}
for (unsigned i = idx; i > 0; --i) {
literal lit = m_covered_clause[i];
//s.mark_visited(lit);
//continue;
s.mark_visited(lit);
continue;
if (!s.is_marked(lit)) continue;
clause_ante const& ante = m_covered_antecedent[i];
if (ante.cls()) {
@ -1630,13 +1631,6 @@ namespace sat {
for (literal l2 : m_intersection) {
watched* w = find_binary_watch(s.get_wlist(~l), ~l2);
if (!w) {
#if 0
IF_VERBOSE(0, verbose_stream() << "bca " << l << " " << ~l2 << "\n");
if (l.var() == 10219 && l2.var() == 10202) {
IF_VERBOSE(0, s.s.display(verbose_stream()));
exit(0);
}
#endif
s.s.mk_bin_clause(l, ~l2, true);
++s.m_num_bca;
}