flush cache when proof mode changes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/python/z3.py

@@ -553,6 +553,8 @@ def _to_sort_ref(s, ctx):
         return ArraySortRef(s, ctx)
     elif k == Z3_DATATYPE_SORT:
         return DatatypeSortRef(s, ctx)
+    elif k == Z3_FINITE_DOMAIN_SORT:
+	return FiniteDomainSortRef(s, ctx)
     return SortRef(s, ctx)
 
 def _sort(ctx, a):
@@ -6179,7 +6181,7 @@ class Fixedpoint(Z3PPObject):
         """
         query = _get_args(query)
         sz = len(query)
-        if sz >= 1 and isinstance(query[0], FuncDecl):            
+        if sz >= 1 and isinstance(query[0], FuncDeclRef):            
             _decls = (FuncDecl * sz)()
             i = 0
             for q in query:
@@ -6307,6 +6309,28 @@ class Fixedpoint(Z3PPObject):
             return Exists(self.vars, fml)
 
 
+#########################################
+#
+# Finite domain sorts
+#
+#########################################
+
+class FiniteDomainSortRef(SortRef):
+    """Finite domain sort."""
+
+    def size(self):
+	"""Return the size of the finite domain sort"""
+	r = (ctype.c_ulonglong * 1)()
+	if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast(), r):
+	    return r[0]
+	else:
+	    raise Z3Exception("Failed to retrieve finite domain sort size")
+
+def FiniteDomainSort(name, sz, ctx=None):
+    """Create a named finite domain sort of a given size sz"""
+    ctx = _get_ctx(ctx)
+    return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
+
 #########################################
 #
 # Optimize

src/ast/expr_map.h

@@ -44,6 +44,10 @@ public:
     void erase(expr * k);
     void reset();
     void flush();
+    void set_store_proofs(bool f) { 
+        if (m_store_proofs != f) flush();
+        m_store_proofs = f; 
+    }
 };
 
 #endif

src/ast/simplifier/base_simplifier.h

@@ -20,6 +20,7 @@ Notes:
 #define _BASE_SIMPLIFIER_H_
 
 #include"expr_map.h"
+#include"ast_pp.h"
 
 /**
    \brief Implements basic functionality used by expression simplifiers.
@@ -32,12 +33,19 @@ protected:
 
     void cache_result(expr * n, expr * r, proof * p) { 
         m_cache.insert(n, r, p); 
+        CTRACE("simplifier", !is_rewrite_proof(n, r, p),
+               tout << mk_pp(n, m) << "\n";
+               tout << mk_pp(r, m) << "\n";
+               tout << mk_pp(p, m) << "\n";);
         SASSERT(is_rewrite_proof(n, r, p));
     }
     void reset_cache() { m_cache.reset(); }
     void flush_cache() { m_cache.flush(); }
     void get_cached(expr * n, expr * & r, proof * & p) const { m_cache.get(n, r, p); }
 
+    void reinitialize() { m_cache.set_store_proofs(m.fine_grain_proofs()); }
+
+
     void visit(expr * n, bool & visited) {
         if (!is_cached(n)) {
             m_todo.push_back(n);
@@ -55,6 +63,7 @@ public:
 
     bool is_rewrite_proof(expr* n, expr* r, proof* p) {
         if (p && 
+            !m.is_undef_proof(p) && 
             !(m.has_fact(p) && 
               (m.is_eq(m.get_fact(p)) || m.is_oeq(m.get_fact(p)) || m.is_iff(m.get_fact(p))) && 
               to_app(m.get_fact(p))->get_arg(0) == n && 

src/ast/simplifier/simplifier.cpp

@@ -61,6 +61,7 @@ void simplifier::enable_ac_support(bool flag) {
 */
 void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) {
     m_need_reset = true;
+    reinitialize();
     expr  * s_orig = s;
     expr  * old_s;
     expr  * result;

src/muz/rel/rel_context.cpp

@@ -51,6 +51,7 @@ Revision History:
 #include"dl_mk_interp_tail_simplifier.h"
 #include"dl_mk_bit_blast.h"
 #include"dl_mk_separate_negated_tails.h"
+#include"ast_util.h"
 
 
 namespace datalog {
@@ -258,11 +259,21 @@ namespace datalog {
                     is_approx = true;
                 }
                 rel.to_formula(e);
+#if 0
+                // Alternative format: 
+                // List the signature of the relation as 
+                // part of the answer.
+                expr_ref_vector args(m);
+                for (unsigned j = 0; j < q->get_arity(); ++j) {
+                    args.push_back(m.mk_var(j, q->get_domain(j)));
+                }
+                e = m.mk_implies(m.mk_app(q, args.size(), args.c_ptr()), e);
+#endif
                 ans.push_back(e);
             }
             SASSERT(!m_last_result_relation);
             if (some_non_empty) {
-                m_answer = m.mk_and(ans.size(), ans.c_ptr());
+                m_answer = mk_and(m, ans.size(), ans.c_ptr());
                 if (is_approx) {
                     res = l_undef;
                     m_context.set_status(APPROX);

src/smt/theory_arith.h

@@ -883,7 +883,7 @@ namespace smt {
         max_min_t max_min(row & r, bool max, bool& has_shared);
         bool max_min(svector<theory_var> const & vars);
 
-        max_min_t max_min_new(theory_var v, bool max, bool& has_shared);
+        // max_min_t max_min_new(theory_var v, bool max, bool& has_shared);
 
         // -----------------------------------
         //