From 0f13ec6e42912c6380ce8fdb5f0c8ef1370e40b7 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 18 Jun 2013 12:28:20 -0700 Subject: [PATCH] adding timeout to duality --- src/duality/duality.h | 14 ++++++++++++++ src/duality/duality_solver.cpp | 4 ++++ src/duality/duality_wrapper.cpp | 1 + src/duality/duality_wrapper.h | 17 +++++++++++++++-- src/muz_qe/dl_context.cpp | 1 + src/muz_qe/duality_dl_interface.cpp | 10 +++++++++- 6 files changed, 44 insertions(+), 3 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index f7ef4eb7a..166e8ef0d 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -174,6 +174,10 @@ namespace Duality { const std::vector &assumptions, const std::vector &theory ){} + + /** Cancel, throw Canceled object if possible. */ + virtual void cancel(){ } + virtual ~LogicSolver(){} }; @@ -225,8 +229,11 @@ namespace Duality { #if 0 islvr->write_interpolation_problem(file_name,assumptions,theory); #endif + } + void cancel(){islvr->cancel();} + /** Declare a constant in the background theory. */ virtual void declare_constant(const func_decl &f){ bckg.insert(f); @@ -835,6 +842,13 @@ namespace Duality { static Solver *Create(const std::string &solver_class, RPFP *rpfp); + /** This can be called asynchrnously to cause Solve to throw a + Canceled exception at some time in the future. + */ + virtual void Cancel() = 0; + /** Object thrown on cancellation */ + struct Canceled {}; + }; } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 4519efd7a..897c88c30 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -282,6 +282,10 @@ namespace Duality { return res; } + void Cancel(){ + // TODO + } + #if 0 virtual void Restart(RPFP *_rpfp){ rpfp = _rpfp; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 67768d3c8..567c81820 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -36,6 +36,7 @@ namespace Duality { p.set_bool("unsat_core", true); scoped_ptr sf = mk_smt_solver_factory(); m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); + canceled = false; } expr context::constant(const std::string &name, const sort &ty){ diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 18fcc3e9f..1048734f7 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -773,10 +773,11 @@ namespace Duality { protected: ::solver *m_solver; model the_model; + bool canceled; public: solver(context & c); - solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; } - solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver;} + solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;} + solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver; canceled = false;} ~solver() { if(m_solver) dealloc(m_solver); @@ -788,12 +789,18 @@ namespace Duality { the_model = s.the_model; return *this; } + struct cancel_exception {}; + void checkpoint(){ + if(canceled) + throw(cancel_exception()); + } // void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); } void push() { m_solver->push(); } void pop(unsigned n = 1) { m_solver->pop(n); } // void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); } void add(expr const & e) { m_solver->assert_expr(e); } check_result check() { + checkpoint(); lbool r = m_solver->check_sat(0,0); model_ref m; m_solver->get_model(m); @@ -808,6 +815,7 @@ namespace Duality { return res; } check_result check(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { + checkpoint(); std::vector< ::expr *> _assumptions(n); for (unsigned i = 0; i < n; i++) { _assumptions[i] = to_expr(assumptions[i]); @@ -854,6 +862,11 @@ namespace Duality { int get_num_decisions(); + void cancel(){ + canceled = true; + if(m_solver) + m_solver->cancel(); + } }; #if 0 diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index c171b66e4..70610f04c 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -937,6 +937,7 @@ namespace datalog { if (m_bmc.get()) m_bmc->cancel(); if (m_rel.get()) m_rel->cancel(); if (m_tab.get()) m_tab->cancel(); + if (m_duality.get()) m_duality->cancel(); } void context::cleanup() { diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp index e59baa4c5..f0a5c5b6b 100644 --- a/src/muz_qe/duality_dl_interface.cpp +++ b/src/muz_qe/duality_dl_interface.cpp @@ -201,7 +201,13 @@ lbool dl_interface::query(::expr * query) { } // Solve! - bool ans = rs->Solve(); + bool ans; + try { + ans = rs->Solve(); + } + catch (Duality::solver::cancel_exception &exn){ + throw default_exception("duality canceled"); + } // profile! @@ -361,6 +367,8 @@ expr_ref dl_interface::get_answer() { } void dl_interface::cancel() { + if(_d && _d->ls) + _d->ls->cancel(); } void dl_interface::cleanup() {