From cba449b75e5e0aaffcbb5df533afabb3151608e3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 7 Dec 2012 15:16:46 -0800
Subject: [PATCH] more parameter issues
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
scripts/mk_win_dist.py | 2 +-
src/cmd_context/cmd_context.cpp | 3 +++
src/smt/params/smt_params.cpp | 2 +-
src/smt/params/smt_params_helper.pyg | 1 +
4 files changed, 6 insertions(+), 2 deletions(-)
diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py
index 3cebce7f6..57ae66b03 100644
--- a/scripts/mk_win_dist.py
+++ b/scripts/mk_win_dist.py
@@ -100,7 +100,7 @@ def mk_build_dirs():
def check_vc_cmd_prompt():
try:
DEVNULL = open(os.devnull, 'wb')
- subprocess.call(['cl'], stdin=DEVNULL, stderr=DEVNULL)
+ subprocess.call(['cl'], stdout=DEVNULL, stderr=DEVNULL)
except:
raise MKException("You must execute the mk_win_dist.py script on a Visual Studio Command Prompt")
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index e14d5139c..ae375fc99 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -37,6 +37,7 @@ Notes:
#include"well_sorted.h"
#include"model_evaluator.h"
#include"for_each_expr.h"
+#include"scoped_timer.h"
func_decls::func_decls(ast_manager & m, func_decl * f):
m_decls(TAG(func_decl*, f, 0)) {
@@ -1304,9 +1305,11 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
if (m_solver) {
m_check_sat_result = m_solver.get(); // solver itself stores the result.
m_solver->set_progress_callback(this);
+ unsigned timeout = m_params.m_timeout;
scoped_watch sw(*this);
cancel_eh<solver> eh(*m_solver);
scoped_ctrl_c ctrlc(eh);
+ scoped_timer timer(timeout, &eh);
lbool r;
try {
r = m_solver->check_sat(num_assumptions, assumptions);
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 22122cd83..ec2fbc93c 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -32,6 +32,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_delay_units = p.delay_units();
m_delay_units_threshold = p.delay_units_threshold();
m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
+ m_soft_timeout = p.soft_timeout();
if (_p.get_bool("arith.greatest_error_pivot", false))
m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
else if (_p.get_bool("arith.least_error_pivot", false))
@@ -48,7 +49,6 @@ void smt_params::updt_params(params_ref const & p) {
void smt_params::updt_params(context_params const & p) {
m_auto_config = p.m_auto_config;
- m_soft_timeout = p.m_timeout;
m_model = p.m_model;
m_model_validate = p.m_model_validate;
}
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 1b8058b44..43dd1b586 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -14,6 +14,7 @@ def_module_params(module_name='smt',
('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
+ ('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'),
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),