From 090ca2e46c73aa4db2e3c3aa345298261c330e9a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 20 Oct 2012 10:47:30 -0700
Subject: [PATCH] refined difference logic check, consolidate scoped modes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 lib/dl_util.h    | 23 ++++++++++++++++++-----
 lib/pdr_util.cpp | 20 +++++---------------
 2 files changed, 23 insertions(+), 20 deletions(-)

diff --git a/lib/dl_util.h b/lib/dl_util.h
index 3e01fb8d2..1969da1a9 100644
--- a/lib/dl_util.h
+++ b/lib/dl_util.h
@@ -171,19 +171,32 @@ namespace datalog {
     */
     void display_fact(context & ctx, app * f, std::ostream & out);
 
-    class scoped_coarse_proof {
-        ast_manager& m;
+    class scoped_proof_mode {
+        ast_manager&   m;
         proof_gen_mode m_mode;
     public:
-        scoped_coarse_proof(ast_manager& m): m(m) {
+        scoped_proof_mode(ast_manager& m, proof_gen_mode mode): m(m) {
             m_mode = m.proof_mode();
-            m.toggle_proof_mode(PGM_COARSE);
+            m.toggle_proof_mode(mode);
         }
-        ~scoped_coarse_proof() {
+        ~scoped_proof_mode() {
             m.toggle_proof_mode(m_mode);            
         }
+
     };
 
+    class scoped_coarse_proof : public scoped_proof_mode {
+    public:
+        scoped_coarse_proof(ast_manager& m): scoped_proof_mode(m, PGM_COARSE) {}
+    };
+
+    class scoped_no_proof : public scoped_proof_mode {
+    public:
+        scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {}
+    };
+
+    
+
     class variable_intersection
     {
         bool values_match(const expr * v1, const expr * v2);
diff --git a/lib/pdr_util.cpp b/lib/pdr_util.cpp
index c09f1a246..1ec358fe1 100644
--- a/lib/pdr_util.cpp
+++ b/lib/pdr_util.cpp
@@ -911,22 +911,9 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
     template class rewriter_tpl<ite_hoister_cfg>;
 
 
-    class scoped_no_proof {
-        ast_manager& m;
-        proof_gen_mode m_mode;
-    public:
-        scoped_no_proof(ast_manager& m): m(m) {
-            m_mode = m.proof_mode();
-            m.toggle_proof_mode(PGM_DISABLED);
-        }
-        ~scoped_no_proof() {
-            m.toggle_proof_mode(m_mode);            
-        }
-    };
-
     void hoist_non_bool_if(expr_ref& fml) {
         ast_manager& m = fml.get_manager();
-        scoped_no_proof _sp(m);
+        datalog::scoped_no_proof _sp(m);
         params_ref p;
         ite_hoister_star ite_rw(m, p);
         expr_ref tmp(m);
@@ -951,7 +938,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
         }
 
         bool test_ineq(expr* e) const {
-            SASSERT(a.is_le(e) || a.is_ge(e));
+            SASSERT(a.is_le(e) || a.is_ge(e) || m.is_eq(e));
             SASSERT(to_app(e)->get_num_args() == 2);
             expr * lhs = to_app(e)->get_arg(0);
             expr * rhs = to_app(e)->get_arg(1);
@@ -985,6 +972,9 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
             if (!a.is_int_real(lhs)) {
                 return true;
             }
+            if (a.is_numeral(lhs) || a.is_numeral(rhs)) {
+                return test_ineq(e);
+            }
             return test_term(lhs) && test_term(rhs);
         }