From 5122b2da7ebe7f38681306d14150676ccec9930b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Oct 2019 09:01:02 -0700 Subject: [PATCH] add solver.timeout as another entry point #2354 Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 6 +++++- src/solver/solver.cpp | 4 ++-- src/solver/solver_params.pyg | 1 + 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index a26fff388..18402b49b 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -35,6 +35,7 @@ Revision History: #include "smt/smt_implied_equalities.h" #include "solver/smt_logics.h" #include "solver/tactic2solver.h" +#include "solver/solver_params.hpp" #include "cmd_context/cmd_context.h" #include "parsers/smt2/smt2parser.h" #include "sat/dimacs.h" @@ -548,7 +549,10 @@ extern "C" { } } expr * const * _assumptions = to_exprs(num_assumptions, assumptions); - unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); + solver_params sp(to_solver(s)->m_params); + unsigned timeout = mk_c(c)->get_timeout(); + timeout = to_solver(s)->m_params.get_uint("timeout", timeout); + timeout = sp.timeout() != UINT_MAX ? sp.timeout() : timeout; unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", true); cancel_eh eh(mk_c(c)->m().limit()); diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index ebb8e1723..36a0dd80c 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -226,8 +226,8 @@ void solver::assert_expr(expr* f, expr* t) { void solver::collect_param_descrs(param_descrs & r) { - r.insert("solver.enforce_model_conversion", CPK_BOOL, "(default: false) enforce model conversion when asserting formulas"); - r.insert("solver.smtlib2_log", CPK_SYMBOL, "(default: None) file to log solver interaction in smtlib2 format"); + solver_params sp(m_params); + sp.collect_param_descrs(r); insert_timeout(r); insert_rlimit(r); insert_max_memory(r); diff --git a/src/solver/solver_params.pyg b/src/solver/solver_params.pyg index 04ffaf1c6..b852afbaa 100644 --- a/src/solver/solver_params.pyg +++ b/src/solver/solver_params.pyg @@ -5,5 +5,6 @@ def_module_params('solver', params=(('enforce_model_conversion', BOOL, False, "apply model transformation on new assertions"), ('smtlib2_log', SYMBOL, '', "file to save solver interaction"), ('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"), + ('timeout', UINT, UINT_MAX, "timeout on the solver object; overwrites a global timeout"), ))