mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

mico-tuning

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-10-08 09:10:02 -07:00
parent 24d7b05c0d
commit c6cd25c822
2 changed files with 8 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/normal_forms/nnf.cpp
View file

@ -69,6 +69,7 @@ class skolemizer {
typedef act_cache cache; typedef act_cache cache;
ast_manager & m; ast_manager & m;
var_subst m_subst;
symbol m_sk_hack; symbol m_sk_hack;
bool m_sk_hack_enabled; bool m_sk_hack_enabled;
cache m_cache; cache m_cache;
@ -128,7 +129,6 @@ class skolemizer {
// //
// (VAR 0) should be in the last position of substitution. // (VAR 0) should be in the last position of substitution.
// //
var_subst s(m);
SASSERT(is_well_sorted(m, q->get_expr())); SASSERT(is_well_sorted(m, q->get_expr()));
expr_ref tmp(m); expr_ref tmp(m);
expr * body = q->get_expr(); expr * body = q->get_expr();
@ -146,7 +146,7 @@ class skolemizer {
} }
} }
} }
r = s(body, substitution); r = m_subst(body, substitution);
p = nullptr; p = nullptr;
if (m_proofs_enabled) { if (m_proofs_enabled) {
if (q->get_kind() == forall_k) if (q->get_kind() == forall_k)
@ -159,6 +159,7 @@ class skolemizer {
public: public:
skolemizer(ast_manager & m): skolemizer(ast_manager & m):
m(m), m(m),
m_subst(m),
m_sk_hack("sk_hack"), m_sk_hack("sk_hack"),
m_sk_hack_enabled(false), m_sk_hack_enabled(false),
m_cache(m), m_cache(m),

16
src/ast/recfun_decl_plugin.cpp
View file

@ -240,23 +240,18 @@ namespace recfun {
{ {
VERIFY(m_cases.empty() && "cases cannot already be computed"); VERIFY(m_cases.empty() && "cases cannot already be computed");
SASSERT(n_vars == m_domain.size()); SASSERT(n_vars == m_domain.size());
TRACEFN("compute cases " << mk_pp(rhs, m)); TRACEFN("compute cases " << mk_pp(rhs, m));
unsigned case_idx = 0;
std::string name("case-");
name.append(m_name.str());
m_vars.append(n_vars, vars);
m_rhs = rhs;
if (!is_macro) if (!is_macro)
for (expr* e : subterms::all(m_rhs)) for (expr* e : subterms::all(m_rhs))
if (is_lambda(e)) if (is_lambda(e))
throw default_exception("recursive definitions with lambdas are not supported"); throw default_exception("recursive definitions with lambdas are not supported");
unsigned case_idx = 0;
expr_ref_vector conditions(m); expr_ref_vector conditions(m);
m_vars.append(n_vars, vars);
m_rhs = rhs;
// is the function a macro (unconditional body)? // is the function a macro (unconditional body)?
if (is_macro || n_vars == 0 || !contains_ite(u, rhs)) { if (is_macro || n_vars == 0 || !contains_ite(u, rhs)) {
@ -265,7 +260,6 @@ namespace recfun {
return; return;
} }
// analyze control flow of `rhs`, accumulating guards and // analyze control flow of `rhs`, accumulating guards and
// rebuilding a `ite`-free RHS on the fly for each path in `rhs`. // rebuilding a `ite`-free RHS on the fly for each path in `rhs`.