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

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-06 15:59:55 -07:00
parent a954ab7d8d
commit 21738d9750
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

@ -1174,7 +1174,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
@ -1199,8 +1200,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()) {
@ -1617,13 +1618,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;
}