From 3dbc307ecd11d20137ab9027f5117515830a5663 Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Wed, 16 Dec 2015 20:10:14 +0000 Subject: [PATCH] Setting up the lackr branch. --- src/ackr/ackr_info.h | 2 +- src/ackr/lackr.cpp | 22 +++++++++++++++------- src/ackr/lackr.h | 6 +++++- src/ackr/lackr_model_constructor.cpp | 8 ++++---- src/muz/README | 2 +- src/tactic/bv/bvarray2uf_tactic.h | 2 +- src/tactic/fpa/fpa2bv_model_converter.h | 2 +- 7 files changed, 28 insertions(+), 16 deletions(-) diff --git a/src/ackr/ackr_info.h b/src/ackr/ackr_info.h index 6d2b596fe..3c92f0ab3 100644 --- a/src/ackr/ackr_info.h +++ b/src/ackr/ackr_info.h @@ -98,8 +98,8 @@ class ackr_info { scoped_ptr m_er; expr_substitution m_subst; - bool m_sealed; // debugging unsigned m_ref_count; // reference counting + bool m_sealed; // debugging }; typedef ref ackr_info_ref; diff --git a/src/ackr/lackr.cpp b/src/ackr/lackr.cpp index 4fa154c34..6081633c1 100644 --- a/src/ackr/lackr.cpp +++ b/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: diff --git a/src/ackr/lackr.h b/src/ackr/lackr.h index f1e3de884..38f810d04 100644 --- a/src/ackr/lackr.h +++ b/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"); } diff --git a/src/ackr/lackr_model_constructor.cpp b/src/ackr/lackr_model_constructor.cpp index 5f0060ad5..3f727cd92 100644 --- a/src/ackr/lackr_model_constructor.cpp +++ b/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>& 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>& m_conflicts; + conflict_list& m_conflicts; bool_rewriter m_b_rw; bv_rewriter m_bv_rw; scoped_ptr 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; -} \ No newline at end of file +} diff --git a/src/muz/README b/src/muz/README index c7d5a9665..3cebe98f6 100644 --- a/src/muz/README +++ b/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 \ No newline at end of file +- fp - main exported routines diff --git a/src/tactic/bv/bvarray2uf_tactic.h b/src/tactic/bv/bvarray2uf_tactic.h index 608a831e0..336911bf7 100644 --- a/src/tactic/bv/bvarray2uf_tactic.h +++ b/src/tactic/bv/bvarray2uf_tactic.h @@ -30,4 +30,4 @@ tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref */ -#endif \ No newline at end of file +#endif diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 534fb6e1c..854543f24 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/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 \ No newline at end of file +#endif