mico-tuning

src/ast/normal_forms/nnf.cpp

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

src/ast/recfun_decl_plugin.cpp

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