From a0af3383db03d07a0ce337c5009c38616ebfba54 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 14 Jun 2018 16:49:04 -0700
Subject: [PATCH] fixes to bdd

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qe_mbi.cpp     |  8 ++++----
 src/sat/ba_solver.cpp |  2 +-
 src/sat/sat_bdd.cpp   | 10 +++++-----
 src/sat/sat_bdd.h     |  2 ++
 4 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index 3af377371..6b777aa02 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -259,7 +259,7 @@ namespace qe {
         app_ref_vector& m_vars;
         arith_util      arith;
         obj_hashtable<func_decl> m_exclude;
-        is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared):
+        is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared): 
             m(vars.m()), m_vars(vars), arith(m) {
             for (func_decl* f : shared) m_exclude.insert(f);
         }
@@ -317,8 +317,8 @@ namespace qe {
     app_ref_vector euf_arith_mbi_plugin::get_arith_vars(expr_ref_vector const& lits) {
                 arith_util a(m);
                 app_ref_vector avars(m);
-                is_arith_var_proc _proc(avars, m_shared);
-        for_each_expr(_proc, lits);
+                is_arith_var_proc _proc(avars, m_shared);        
+        for_each_expr(_proc, lits);                
         return avars;
     }
 
@@ -484,7 +484,7 @@ namespace qe {
                         return l_true, mbp of local, mdl of local & blocked
                   else if !is_sat(local & lits) then
                       return l_false, mbp of local, nullptr
-                  else if is_sat(local & lits) && !is_sat(local & lits & blocked)
+                  else // is_sat(local & lits) && !is_sat(local & lits & blocked)
                       MISSING CASE
                       MUST PRODUCE AN IMPLICANT OF LOCAL that is inconsistent with lits & blocked
                       in this case !is_sat(local & lits & mdl) and is_sat(mdl, blocked)
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index d7cdea132..930617301 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -556,7 +556,7 @@ namespace sat {
             bool is_false = false;
             for (unsigned k = 0; k < sz; ++k) {
                 SASSERT(!is_false || value(p[k].second) == l_false);
-                SASSERT(k < j == (value(p[k].second) != l_false));
+                SASSERT((k < j) == (value(p[k].second) != l_false));
                 is_false = value(p[k].second) == l_false;
             });
 
diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp
index 74af4bf5e..bd1745765 100644
--- a/src/sat/sat_bdd.cpp
+++ b/src/sat/sat_bdd.cpp
@@ -108,7 +108,7 @@ namespace sat {
 
     bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) {
         if (e1 != e2) {
-            SASSERT(e2->m_result != -1);
+            SASSERT(e2->m_result != null_bdd);
             push_entry(e1);
             e1 = nullptr;
             return true;            
@@ -117,7 +117,7 @@ namespace sat {
             e1->m_bdd1 = a;
             e1->m_bdd2 = b;
             e1->m_op = c;
-            SASSERT(e1->m_result == -1);
+            SASSERT(e1->m_result == null_bdd);
             return false;        
         }
     }
@@ -203,7 +203,7 @@ namespace sat {
             void * mem = m_alloc.allocate(sizeof(op_entry));
             result = new (mem) op_entry(l, r, op);
         }
-        result->m_result = -1;
+        result->m_result = null_bdd;
         return result;
     }
 
@@ -667,7 +667,7 @@ namespace sat {
                 r = e2->m_result;
             }
             else {
-                SASSERT(e1->m_result == -1);
+                SASSERT(e1->m_result == null_bdd);
                 push(mk_quant_rec(l, lo(b), op));
                 push(mk_quant_rec(l, hi(b), op));
                 r = make_node(lvl, read(2), read(1));
@@ -782,7 +782,7 @@ namespace sat {
 
         ptr_vector<op_entry> to_delete, to_keep;
         for (auto* e : m_op_cache) {            
-            if (e->m_result != -1) {
+            if (e->m_result != null_bdd) {
                 to_delete.push_back(e);
             }
             else {
diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h
index 41d1115b9..70f6960fe 100644
--- a/src/sat/sat_bdd.h
+++ b/src/sat/sat_bdd.h
@@ -32,6 +32,8 @@ namespace sat {
 
         typedef unsigned BDD;
 
+        const BDD null_bdd = UINT_MAX;
+
         enum bdd_op {
             bdd_and_op = 2,
             bdd_or_op = 3,