Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

lib/dl_util.h

@@ -171,19 +171,32 @@ namespace datalog {
     */
     void display_fact(context & ctx, app * f, std::ostream & out);
 
-    class scoped_coarse_proof {
+    class scoped_proof_mode {
-        ast_manager& m;
+        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);

lib/pdr_context.cpp

@@ -1618,24 +1618,16 @@ namespace pdr {
 
        - T(x0,x1,x)   for transition
        - phi(x)       for n.state()
-       - psi(x0,x1,x) for psi
        - M(x0,x1,x)   for n.model()
 
        Assumptions:
-         M => psi
+         M => phi & T
-         psi => phi & T
-         psi & M  agree on which rules are taken.
 
        In other words, 
-       1. psi is a weakening of M
+       1. phi & T is implied by M
-       2. phi & T is implied by psi
        
        Goal is to find phi0(x0), phi1(x1) such that:
 
-         phi(x) & phi0(x0) & phi1(x1) => psi(x0, x1, x)
-
-       or at least (ignoring psi alltogether):
-
          phi(x) & phi0(x0) & phi1(x1) => T(x0, x1, x)       
 
        Strategy: 

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);
         }