Setting up the lackr branch.

src/ackr/ackr_info.h

@@ -98,8 +98,8 @@ class ackr_info {
         scoped_ptr<expr_replacer> m_er;
         expr_substitution m_subst;
 
-        bool m_sealed; // debugging
         unsigned m_ref_count; // reference counting
+        bool m_sealed; // debugging
 };
 
 typedef ref<ackr_info> ackr_info_ref;

src/ackr/lackr.cpp

@@ -104,6 +104,7 @@ lbool lackr::operator() () {
     if (!ok) return l_undef;
     TRACE("lackr", tout << "sat goal\n"; m_sat->display(tout););
     const lbool rv = m_eager ? eager() : lazy();
+    std::cout << "res: " << rv << "\n";
     if (rv == l_true) m_sat->get_model(m_model);
     TRACE("lackr", tout << "sat:" << rv << '\n'; );
     CTRACE("lackr", rv == l_true,
@@ -234,16 +235,22 @@ void lackr::add_term(app* a) {
 lbool lackr::eager() {
     m_sat->assert_expr(m_abstr);
     TRACE("lackr", tout << "run sat 0\n"; );
-    if (m_sat->check_sat(0, 0) == l_false)
-        return l_false;
+    std::cout << "++sat call\n";
+    const lbool rv0 = m_sat->check_sat(0, 0);
+    std::cout << "--sat call\n";
+    if (rv0 == l_false) return l_false;    
     checkpoint();
     if (!eager_enc()) return l_undef;
+    checkpoint();
     expr_ref all(m_m);
     all = m_m.mk_and(m_ackrs.size(), m_ackrs.c_ptr());
     m_simp(all);
     TRACE("lackr", tout << "run sat\n"; );
     m_sat->assert_expr(all);
-    return m_sat->check_sat(0, 0);
+    std::cout << "++sat call\n";
+    const lbool rv = m_sat->check_sat(0, 0);
+    std::cout << "--sat call\n";
+    return rv;
 }
 
 
@@ -276,10 +283,10 @@ lbool lackr::lazy() {
 }
 
 void lackr::setup_sat() {
-    if (m_use_sat) {
-        //std::cout << "; qfbv sat\n";
-        tactic_ref t = mk_qfbv_tactic(m_m, m_p);
-        m_sat = mk_tactic2solver(m_m, t.get(), m_p);
+    if (m_use_sat) {        
+        //tactic_ref t = mk_qfbv_tactic(m_m, m_p);
+        //m_sat = mk_tactic2solver(m_m, t.get(), m_p);
+        m_sat = mk_inc_sat_solver(m_m, m_p);
     }
     else {
         //std::cout << "; smt sat\n";
@@ -318,6 +325,7 @@ bool lackr::collect_terms() {
                     visited.mark(curr, true);
                     stack.pop_back();
                     add_term(to_app(curr));
+                    checkpoint();
                 }
                 break;
             case AST_QUANTIFIER:

src/ackr/lackr.h

@@ -57,7 +57,11 @@ class lackr {
         //  timeout mechanisms
         //
         void checkpoint() {
-            if (m_cancel) throw tactic_exception(TACTIC_CANCELED_MSG);
+            //std::cout << "chk\n";
+            if (m_m.canceled()) {
+                std::cout << "canceled\n";
+                throw tactic_exception(TACTIC_CANCELED_MSG);
+            }
             cooperate("lackr");
         }
 

src/ackr/lackr_model_constructor.cpp

@@ -26,7 +26,7 @@ struct lackr_model_constructor::imp {
         imp(ast_manager& m,
             ackr_info_ref info,
             model_ref& abstr_model,
-            vector<std::pair<app*,app*>>& conflicts)
+            conflict_list& conflicts)
             : m_m(m)
             , m_info(info)
             , m_abstr_model(abstr_model)
@@ -45,7 +45,7 @@ struct lackr_model_constructor::imp {
                     m_m.dec_ref(i->m_value.value);
                     m_m.dec_ref(i->m_value.source_term);
                 }
-            }            
+            }
             {
                 app2val_t::iterator i = m_app2val.begin();
                 const app2val_t::iterator e = m_app2val.end();
@@ -72,7 +72,7 @@ struct lackr_model_constructor::imp {
         ast_manager&                    m_m;
         ackr_info_ref                   m_info;
         model_ref&                      m_abstr_model;
-        vector<std::pair<app*,app*>>&   m_conflicts;
+        conflict_list&                  m_conflicts;
         bool_rewriter                   m_b_rw;
         bv_rewriter                     m_bv_rw;
         scoped_ptr<model_evaluator>     m_evaluator;
@@ -310,4 +310,4 @@ bool lackr_model_constructor::check(model_ref& abstr_model) {
     const bool rv = i.check();
     state = rv ? CHECKED : CONFLICT;
     return rv;
-}
+}

src/muz/README

@@ -9,4 +9,4 @@ solving Datalog programs.
 - clp - Dart/Symbolic execution-based solver
 - tab - Tabulation based solver
 - bmc - Bounded model checking based solver
-- fp  - main exported routines
+- fp  - main exported routines

src/tactic/bv/bvarray2uf_tactic.h

@@ -30,4 +30,4 @@ tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref
 */
 
 
-#endif
+#endif

src/tactic/fpa/fpa2bv_model_converter.h

@@ -107,4 +107,4 @@ protected:
 
 model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv);
 
-#endif
+#endif