From 05b7aa3ebb6ce3bca4e849b5db150f3861e51c69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Jan 2015 14:32:18 +0530 Subject: [PATCH] flush cache when proof mode changes Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 26 +++++++++++++++++++++++++- src/ast/expr_map.h | 4 ++++ src/ast/simplifier/base_simplifier.h | 9 +++++++++ src/ast/simplifier/simplifier.cpp | 1 + src/muz/rel/rel_context.cpp | 13 ++++++++++++- src/smt/theory_arith.h | 2 +- 6 files changed, 52 insertions(+), 3 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index e803aece9..ca04c419b 100644 --- a/src/api/python/z3.py +++ b/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 diff --git a/src/ast/expr_map.h b/src/ast/expr_map.h index 5ab6545f8..3e6f71e86 100644 --- a/src/ast/expr_map.h +++ b/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 diff --git a/src/ast/simplifier/base_simplifier.h b/src/ast/simplifier/base_simplifier.h index 5ebcdc30e..26bb43838 100644 --- a/src/ast/simplifier/base_simplifier.h +++ b/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 && diff --git a/src/ast/simplifier/simplifier.cpp b/src/ast/simplifier/simplifier.cpp index fcd4e91b6..5358e01e4 100644 --- a/src/ast/simplifier/simplifier.cpp +++ b/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; diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 0d07b7c81..5054bc192 100644 --- a/src/muz/rel/rel_context.cpp +++ b/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); diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 1eb7c7de8..ffdc82f86 100644 --- a/src/smt/theory_arith.h +++ b/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 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); // ----------------------------------- //