fix #6355

conversion from AIG to expressions should always use the optimized conversion function.

the aig-tactic should throttle regarding output bloat from AIG.
If the expression after AIG simpification, for whatever reason, is bloated the rewrite does not take place.

src/tactic/aig/aig.cpp

@@ -18,7 +18,8 @@ Notes:
 --*/
 #include "tactic/aig/aig.h"
 #include "tactic/goal.h"
-#include "ast/ast_smt2_pp.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/ast_util.h"
 
 #define USE_TWO_LEVEL_RULES
 #define FIRST_NODE_ID (UINT_MAX/2)
@@ -431,13 +432,8 @@ struct aig_manager::imp {
         expr2aig(imp & _m):m(_m) {}
         
         ~expr2aig() {
-            obj_map<expr, aig_lit>::iterator it  = m_cache.begin();
+            for (auto& [k,v] : m_cache) 
-            obj_map<expr, aig_lit>::iterator end = m_cache.end();
+                m.dec_ref(v);
-            for (; it != end; ++it) {
-                TRACE("expr2aig", tout << "dec-ref: "; m.display_ref(tout, it->m_value); 
-                      tout << " ref-count: " << ref_count(it->m_value) << "\n";);
-                m.dec_ref(it->m_value);
-            }
             restore_result_stack(0);
         }
         
@@ -447,7 +443,7 @@ struct aig_manager::imp {
         }
 
         void cache_result(expr * t, aig_lit const & r) {
-            TRACE("expr2aig", tout << "caching:\n" << mk_ismt2_pp(t, m.m()) << "\n---> "; m.display_ref(tout, r); tout << "\n";); 
+            TRACE("expr2aig", tout << "caching:\n" << mk_bounded_pp(t, m.m()) << "\n---> "; m.display_ref(tout, r); tout << "\n";); 
             SASSERT(!m_cache.contains(t));
             m.inc_ref(r);
             m_cache.insert(t, r);
@@ -1009,33 +1005,34 @@ struct aig_manager::imp {
                 r = invert(r);
         }
 
-        void operator()(aig_lit const & l, expr_ref & r) {
+        void not_naive(aig_lit const& l, expr_ref & r) {
-            naive(l, r);
-        }
-
-        void operator()(aig_lit const & l, goal & g) {
-            g.reset();
             sbuffer<aig_lit> roots;
+            expr_ref_vector rs(r.m());
             roots.push_back(l);
             while (!roots.empty()) {
                 aig_lit n = roots.back();
                 roots.pop_back();
                 if (n.is_inverted()) {
-                    g.assert_expr(invert(process_root(n.ptr())), nullptr, nullptr);
+                    rs.push_back(invert(process_root(n.ptr())));
                     continue;
                 }
                 aig * p = n.ptr();
                 if (m.is_ite(p)) {
-                    g.assert_expr(process_root(p), nullptr, nullptr);
+                    rs.push_back(process_root(p));
                     continue;
                 }
                 if (is_var(p)) {
-                    g.assert_expr(m.var2expr(p), nullptr, nullptr);
+                    rs.push_back(m.var2expr(p));
                     continue;
                 }
                 roots.push_back(left(p));
                 roots.push_back(right(p));
             }
+            r = ::mk_and(rs);
+        }
+
+        void operator()(aig_lit const & l, expr_ref & r) {            
+            not_naive(l, r);
         }
 
     };
@@ -1534,18 +1531,14 @@ public:
             }
             SASSERT(ref_count(r) >= 1);
         }
-    catch (const aig_exception & ex) {
+        catch (const aig_exception & ex) {
-        dec_ref(r);
+            dec_ref(r);
-        throw ex;
+            throw ex;
-    }
+        }
         dec_ref_result(r);
         return r;
     }
 
-    void to_formula(aig_lit const & r, goal & g) {
-        aig2expr proc(*this);
-        proc(r, g);
-    }
     
     void to_formula(aig_lit const & r, expr_ref & result) {
         aig2expr proc(*this);
@@ -1581,7 +1574,7 @@ public:
             qhead++;
             display_ref(out, n); out << ": ";
             if (is_var(n)) {
-                out << mk_ismt2_pp(m_var2exprs[n->m_id], m()) << "\n";
+                out << mk_bounded_pp(m_var2exprs[n->m_id], m()) << "\n";
             }
             else {
                 display_ref(out, n->m_children[0]);
@@ -1607,7 +1600,7 @@ public:
         if (r.is_inverted())
             out << "(not ";
         if (is_var(r)) {
-            out << mk_ismt2_pp(var2expr(r.ptr()), m());
+            out << mk_bounded_pp(var2expr(r.ptr()), m());
         }
         else {
             out << "aig" << to_idx(r.ptr());
@@ -1738,11 +1731,6 @@ void aig_manager::max_sharing(aig_ref & r) {
     r = aig_ref(*this, m_imp->max_sharing(aig_lit(r)));
 }
 
-void aig_manager::to_formula(aig_ref const & r, goal & g) {
-    SASSERT(!g.proofs_enabled());
-    SASSERT(!g.unsat_core_enabled());
-    return m_imp->to_formula(aig_lit(r), g);
-}
 
 void aig_manager::to_formula(aig_ref const & r, expr_ref & res) {
     return m_imp->to_formula(aig_lit(r), res);

src/tactic/aig/aig_tactic.cpp

@@ -16,6 +16,9 @@ Author:
 Notes:
 
 --*/
+#include "ast/ast_util.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/for_each_expr.h"
 #include "tactic/tactical.h"
 #include "tactic/aig/aig.h"
 
@@ -24,7 +27,6 @@ class aig_manager;
 class aig_tactic : public tactic {
     unsigned long long m_max_memory;
     bool               m_aig_gate_encoding;
-    bool               m_aig_per_assertion;
     aig_manager *      m_aig_manager;
 
     struct mk_aig_manager {
@@ -52,40 +54,54 @@ public:
         aig_tactic * t = alloc(aig_tactic);
         t->m_max_memory = m_max_memory;
         t->m_aig_gate_encoding = m_aig_gate_encoding;
-        t->m_aig_per_assertion = m_aig_per_assertion;
         return t;
     }
 
     void updt_params(params_ref const & p) override {
         m_max_memory        = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
         m_aig_gate_encoding = p.get_bool("aig_default_gate_encoding", true);
-        m_aig_per_assertion = p.get_bool("aig_per_assertion", true); 
     }
 
     void collect_param_descrs(param_descrs & r) override {
         insert_max_memory(r);
-        r.insert("aig_per_assertion", CPK_BOOL, "(default: true) process one assertion at a time.");
     }
 
     void operator()(goal_ref const & g) {
+        ast_manager& m = g->m();
+        mk_aig_manager mk(*this, m);
 
-        mk_aig_manager mk(*this, g->m());
+        expr_ref_vector nodeps(m);
-        if (m_aig_per_assertion) {
+        
-            for (unsigned i = 0; i < g->size(); i++) {
+        for (unsigned i = 0; i < g->size(); i++) {
+            expr_dependency * ed = g->dep(i);
+            if (!ed) {
+                nodeps.push_back(g->form(i));
+                g->update(i, m.mk_true());
+            }
+            else {
                 aig_ref r = m_aig_manager->mk_aig(g->form(i));
                 m_aig_manager->max_sharing(r);
-                expr_ref new_f(g->m());
+                expr_ref new_f(m);
                 m_aig_manager->to_formula(r, new_f);
-                expr_dependency * ed = g->dep(i);
+                unsigned old_sz = get_num_exprs(g->form(i));
-                g->update(i, new_f, nullptr, ed);
+                unsigned new_sz = get_num_exprs(new_f);
+                if (new_sz <= 1.2*old_sz)
+                    g->update(i, new_f, nullptr, ed);
             }
         }
-        else {
+
-            fail_if_unsat_core_generation("aig", g);
+        if (!nodeps.empty()) {
-            aig_ref r = m_aig_manager->mk_aig(*(g.get()));
+            expr_ref conj(::mk_and(nodeps));
-            g->reset(); // save memory
+            aig_ref r = m_aig_manager->mk_aig(conj);
             m_aig_manager->max_sharing(r);
-            m_aig_manager->to_formula(r, *(g.get()));
+            expr_ref new_f(m);
+            m_aig_manager->to_formula(r, new_f);
+            unsigned old_sz = get_num_exprs(conj);
+            unsigned new_sz = get_num_exprs(new_f);
+            
+            if (new_sz > 1.2*old_sz)
+                new_f = conj;
+            g->assert_expr(new_f);                       
         }
     }
     

src/tactic/smtlogics/qfbv_tactic.cpp

@@ -90,9 +90,6 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
     params_ref solver_p;
     solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.
 
-    params_ref big_aig_p;
-    big_aig_p.set_bool("aig_per_assertion", false);
-
     tactic* preamble_st = mk_qfbv_preamble(m, p);
     tactic * st = main_p(and_then(preamble_st,
                                   // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function
@@ -107,10 +104,7 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
                                                           and_then(using_params(and_then(mk_simplify_tactic(m),
                                                                                          mk_solve_eqs_tactic(m)),
                                                                                 local_ctx_p),
-                                                                   if_no_proofs(cond(mk_produce_unsat_cores_probe(),
+                                                                   if_no_proofs(mk_aig_tactic()))),
-                                                                                     mk_aig_tactic(),
-                                                                                     using_params(mk_aig_tactic(),
-                                                                                                  big_aig_p))))),
                                                      sat),
                                             smt))));