mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

more parameter issues

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-07 15:16:46 -08:00
parent a07b459fdf
commit cba449b75e
4 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_win_dist.py
View file

@ -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")

3
src/cmd_context/cmd_context.cpp
View file

@ -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);

2
src/smt/params/smt_params.cpp
View file

@ -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;
}

1
src/smt/params/smt_params_helper.pyg
View file

@ -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'),