Integrating Nikolaj's Saturday changes (at unstable branch)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

ml/compile_mlapi.cmd

@@ -22,7 +22,7 @@ if %STATIC% == true (
     set Z3DBGLIB=z3lib.lib
 ) else (
     set Z3LIB=z3.lib
-    set Z3DBGLIB=z3_dbg.lib
+    set Z3DBGLIB=z3.lib
 )
 
 REM ocaml 3.11 and later calls the linker through flexlink

src/api_headers/z3_api.h

@@ -1159,7 +1159,7 @@ typedef enum
 
 #endif
 
-/*
+/**
   Definitions for update_api.py
   
   def_Type('CONFIG',           'Z3_config',           'Config')
@@ -3970,12 +3970,12 @@ END_MLAPI_EXCLUDE
     */
     Z3_ast_kind Z3_API Z3_get_ast_kind(__in Z3_context c, __in Z3_ast a);
 
-    /*
+    /**
       def_API('Z3_is_app', BOOL, (_in(CONTEXT), _in(AST)))      
     */
     Z3_bool Z3_API Z3_is_app(__in Z3_context c, __in Z3_ast a);
 
-    /*
+    /**
       def_API('Z3_is_numeral_ast', BOOL, (_in(CONTEXT), _in(AST)))
     */
     Z3_bool Z3_API Z3_is_numeral_ast(__in Z3_context c, __in Z3_ast a);
@@ -4757,17 +4757,17 @@ END_MLAPI_EXCLUDE
     */
     Z3_string Z3_API Z3_ast_to_string(__in Z3_context c, __in Z3_ast a);
 
-    /*
+    /**
       def_API('Z3_pattern_to_string', STRING, (_in(CONTEXT), _in(PATTERN)))
     */
     Z3_string Z3_API Z3_pattern_to_string(__in Z3_context c, __in Z3_pattern p);
 
-    /*
+    /**
       def_API('Z3_sort_to_string', STRING, (_in(CONTEXT), _in(SORT)))
     */
     Z3_string Z3_API Z3_sort_to_string(__in Z3_context c, __in Z3_sort s);
     
-    /*
+    /**
       def_API('Z3_func_decl_to_string', STRING, (_in(CONTEXT), _in(FUNC_DECL)))
     */
     Z3_string Z3_API Z3_func_decl_to_string(__in Z3_context c, __in Z3_func_decl d);

src/muz_qe/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);

src/muz_qe/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: 

src/muz_qe/pdr_farkas_learner.cpp

@@ -29,6 +29,7 @@ Revision History:
 #include "pdr_util.h"
 #include "pdr_farkas_learner.h"
 #include "th_rewriter.h"
+#include "smtparser.h"
 #include "pdr_interpolant_provider.h"
 #include "ast_ll_pp.h"
 #include "arith_bounds_tactic.h"
@@ -857,7 +858,6 @@ namespace pdr {
 
 
     void farkas_learner::test(char const* filename)  {
-#if 0
         if (!filename) {
             test();
             return;
@@ -886,7 +886,6 @@ namespace pdr {
         expr_ref_vector lemmas(m);
         bool res = fl.get_lemma_guesses(A, B, lemmas);        
         std::cout << "lemmas: " << pp_cube(lemmas, m) << "\n";
-#endif
     }
 };
 

src/muz_qe/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);
         }