Merge pull request #505 from MikolasJanota/tmp

Improvement in lazy ackermannization.

src/ackermannization/ackermannize_bv_tactic.cpp

@@ -38,6 +38,7 @@ public:
         tactic_report report("ackermannize", *g);
         fail_if_unsat_core_generation("ackermannize", g);
         fail_if_proof_generation("ackermannize", g);
+        TRACE("ackermannize", g->display(tout << "in\n"););
 
         expr_ref_vector flas(m);
         const unsigned sz = g->size();
@@ -48,6 +49,7 @@ public:
         goal_ref resg(alloc(goal, *g, true));
         const bool success = lackr.mk_ackermann(resg, m_lemma_limit);
         if (!success) { // Just pass on the input unchanged
+            TRACE("ackermannize", tout << "ackermannize not run due to limit" << std::endl;);
             result.reset();
             result.push_back(g.get());
             mc = 0;
@@ -62,7 +64,7 @@ public:
         }
 
         resg->inc_depth();
-        TRACE("ackermannize", resg->display(tout););
+        TRACE("ackermannize", resg->display(tout << "out\n"););
         SASSERT(resg->is_well_sorted());
     }
 

src/ackermannization/lackr_model_constructor.cpp

@@ -34,11 +34,13 @@ struct lackr_model_constructor::imp {
             , m_conflicts(conflicts)
             , m_b_rw(m)
             , m_bv_rw(m)
+            , m_evaluator(NULL)
             , m_empty_model(m)
             , m_ackr_helper(m)
         {}
 
         ~imp() {
+            if (m_evaluator) dealloc(m_evaluator);
             {
                 values2val_t::iterator i = m_values2val.begin();
                 const values2val_t::iterator e = m_values2val.end();
@@ -60,15 +62,17 @@ struct lackr_model_constructor::imp {
 
         //
         // Returns true iff model was successfully constructed.
+        // Conflicts are saved as a side effect.
         //
         bool check() {
+            bool retv = true;
             for (unsigned i = 0; i < m_abstr_model->get_num_constants(); i++) {
                 func_decl * const c = m_abstr_model->get_constant(i);
-                app * const term = m_info->find_term(c);
+                app * const  _term = m_info->find_term(c);
-                if (term) m_stack.push_back(term);
+                expr * const term  = _term ? _term : m_m.mk_const(c);
-                else m_stack.push_back(m_m.mk_const(c));
+                if (!check_term(term)) retv = false;
             }
-            return run();
+            return retv;
         }
 
 
@@ -134,7 +138,7 @@ struct lackr_model_constructor::imp {
         conflict_list&                  m_conflicts;
         bool_rewriter                   m_b_rw;
         bv_rewriter                     m_bv_rw;
-        scoped_ptr<model_evaluator>     m_evaluator;
+        model_evaluator *               m_evaluator;
         model                           m_empty_model;
     private:
         struct val_info { expr * value; app * source_term; };
@@ -144,6 +148,7 @@ struct lackr_model_constructor::imp {
         app2val_t        m_app2val;
         ptr_vector<expr> m_stack;
         ackr_helper      m_ackr_helper;
+        expr_mark        m_visited;
 
         static inline val_info mk_val_info(expr* value, app* source_term) {
             val_info rv;
@@ -152,17 +157,23 @@ struct lackr_model_constructor::imp {
             return rv;
         }
 
-        //
+        // Performs congruence check on a given term.
+        bool check_term(expr * term) {
+            m_stack.push_back(term);
+            const bool rv = _check_stack();
+            m_stack.reset();
+            return rv;
+        }
+
         // Performs congruence check on terms on the stack.
-        // (Currently stops upon the first failure).
+        // Stops upon the first failure.
-        // Returns true if and only if congruence check succeeded.
+        // Returns true if and only if all congruence checks succeeded.
-        bool run() {
+        bool _check_stack() {
-            m_evaluator = alloc(model_evaluator, m_empty_model);
+            if (m_evaluator == NULL) m_evaluator = alloc(model_evaluator, m_empty_model);
-            expr_mark visited;
             expr *  curr;
             while (!m_stack.empty()) {
                 curr = m_stack.back();
-                if (visited.is_marked(curr)) {
+                if (m_visited.is_marked(curr)) {
                     m_stack.pop_back();
                     continue;
                 }
@@ -173,8 +184,8 @@ struct lackr_model_constructor::imp {
                         return false;
                     case AST_APP: {
                             app * a = to_app(curr);
-                            if (for_each_expr_args(m_stack, visited, a->get_num_args(), a->get_args())) {
+                            if (for_each_expr_args(m_stack, m_visited, a->get_num_args(), a->get_args())) {
-                                visited.mark(a, true);
+                                m_visited.mark(a, true);
                                 m_stack.pop_back();
                                 if (!mk_value(a)) return false;
                             }
@@ -212,7 +223,11 @@ struct lackr_model_constructor::imp {
             for (unsigned i = 0; i < num; ++i) {
                 expr * val;
                 const bool b = eval_cached(to_app(args[i]), val); // TODO: OK conversion to_app?
-                CTRACE("model_constructor", !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2); );
+                CTRACE("model_constructor", m_conflicts.empty() && !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2) << '\n'; );
+                if (!b) {
+                    // bailing out because args eval failed previously
+                    return false;
+                }
                 TRACE("model_constructor", tout <<
                     "arg val " << i << "(\n" << mk_ismt2_pp(args[i], m_m, 2)
                     << " : " << mk_ismt2_pp(val, m_m, 2) << '\n'; );

src/tactic/smtlogics/qfufbv_tactic.cpp

@@ -47,6 +47,7 @@ public:
         : m_m(m)
         , m_p(p)
         , m_use_sat(false)
+        , m_inc_use_sat(false)
     {}
 
     virtual ~qfufbv_ackr_tactic() { }
@@ -85,6 +86,7 @@ public:
     void updt_params(params_ref const & _p) {
         qfufbv_tactic_params p(_p);
         m_use_sat = p.sat_backend();
+        m_inc_use_sat = p.inc_sat_backend();
     }
 
     virtual void collect_statistics(statistics & st) const {
@@ -105,13 +107,19 @@ private:
     params_ref                           m_p;
     lackr_stats                          m_st;
     bool                                 m_use_sat;
+    bool                                 m_inc_use_sat;
 
     solver* setup_sat() {
         solver * sat(NULL);
         if (m_use_sat) {
+            if (m_inc_use_sat) {
+                sat = mk_inc_sat_solver(m_m, m_p);
+            }
+            else {
                 tactic_ref t = mk_qfbv_tactic(m_m, m_p);
                 sat = mk_tactic2solver(m_m, t.get(), m_p);
             }
+        }
         else {
             tactic_ref t = mk_qfaufbv_tactic(m_m, m_p);
             sat = mk_tactic2solver(m_m, t.get(), m_p);

src/tactic/smtlogics/qfufbv_tactic_params.pyg

@@ -4,5 +4,6 @@ def_module_params('ackermannization',
                   export=True,
                   params=(
                           ('sat_backend', BOOL, False, 'use SAT rather than SMT in qfufbv_ackr_tactic'),
+                          ('inc_sat_backend', BOOL, False, 'use incremental SAT'),
                           ))