mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
commit
fda39bffe2
|
@ -307,7 +307,7 @@ class set_option_cmd : public set_get_option_cmd {
|
|||
try {
|
||||
gparams::set(m_option, value);
|
||||
env_params::updt_params();
|
||||
ctx.params().updt_params();
|
||||
ctx.global_params_updated();
|
||||
}
|
||||
catch (gparams::exception ex) {
|
||||
throw cmd_exception(ex.msg());
|
||||
|
@ -517,7 +517,7 @@ public:
|
|||
}
|
||||
else {
|
||||
try {
|
||||
std::string val = gparams::get_value(opt);
|
||||
ctx.regular_stream() << gparams::get_value(opt) << std::endl;
|
||||
}
|
||||
catch (gparams::exception ex) {
|
||||
ctx.print_unsupported(opt);
|
||||
|
|
|
@ -342,6 +342,16 @@ cmd_context::~cmd_context() {
|
|||
m_check_sat_result = 0;
|
||||
}
|
||||
|
||||
void cmd_context::global_params_updated() {
|
||||
m_params.updt_params();
|
||||
if (m_solver) {
|
||||
params_ref p;
|
||||
if (!m_params.m_auto_config)
|
||||
p.set_bool("auto_config", false);
|
||||
m_solver->updt_params(p);
|
||||
}
|
||||
}
|
||||
|
||||
void cmd_context::set_produce_models(bool f) {
|
||||
if (m_solver)
|
||||
m_solver->set_produce_models(f);
|
||||
|
|
|
@ -249,6 +249,7 @@ public:
|
|||
cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
|
||||
~cmd_context();
|
||||
context_params & params() { return m_params; }
|
||||
void global_params_updated(); // this method should be invoked when global (and module) params are updated.
|
||||
void set_logic(symbol const & s);
|
||||
bool has_logic() const { return m_logic != symbol::null; }
|
||||
symbol const & get_logic() const { return m_logic; }
|
||||
|
|
|
@ -35,6 +35,7 @@ namespace smt2 {
|
|||
|
||||
class parser {
|
||||
cmd_context & m_ctx;
|
||||
params_ref m_params;
|
||||
scanner m_scanner;
|
||||
scanner::token m_curr;
|
||||
cmd * m_curr_cmd;
|
||||
|
@ -2285,6 +2286,10 @@ namespace smt2 {
|
|||
shrink(m_sexpr_stack, sexpr_spos);
|
||||
m_symbol_stack.shrink(sym_spos);
|
||||
m_num_bindings = 0;
|
||||
// HACK for propagating the update of parser parameters
|
||||
if (norm_param_name(s) == "set_option") {
|
||||
updt_params();
|
||||
}
|
||||
return;
|
||||
}
|
||||
else {
|
||||
|
@ -2357,9 +2362,10 @@ namespace smt2 {
|
|||
}
|
||||
|
||||
public:
|
||||
parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & _p):
|
||||
parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & p):
|
||||
m_ctx(ctx),
|
||||
m_scanner(ctx, is, interactive, _p),
|
||||
m_params(p),
|
||||
m_scanner(ctx, is, interactive, p),
|
||||
m_curr(scanner::NULL_TOKEN),
|
||||
m_curr_cmd(0),
|
||||
m_num_bindings(0),
|
||||
|
@ -2397,15 +2403,19 @@ namespace smt2 {
|
|||
// the following assertion does not hold if ctx was already attached to an AST manager before the parser object is created.
|
||||
// SASSERT(!m_ctx.has_manager());
|
||||
|
||||
parser_params p(_p);
|
||||
m_ignore_user_patterns = p.ignore_user_patterns();
|
||||
m_ignore_bad_patterns = p.ignore_bad_patterns();
|
||||
m_display_error_for_vs = p.error_for_visual_studio();
|
||||
updt_params();
|
||||
}
|
||||
|
||||
~parser() {
|
||||
reset_stack();
|
||||
}
|
||||
|
||||
void updt_params() {
|
||||
parser_params p(m_params);
|
||||
m_ignore_user_patterns = p.ignore_user_patterns();
|
||||
m_ignore_bad_patterns = p.ignore_bad_patterns();
|
||||
m_display_error_for_vs = p.error_for_visual_studio();
|
||||
}
|
||||
|
||||
void reset() {
|
||||
reset_stack();
|
||||
|
|
|
@ -35,6 +35,7 @@ def_module_params(module_name='smt',
|
|||
('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic'),
|
||||
('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'),
|
||||
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
|
||||
('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
|
||||
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
|
||||
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
|
||||
('arith.ignore_int', BOOL, False, 'treat integer variables as real')))
|
||||
|
|
|
@ -32,6 +32,7 @@ void theory_arith_params::updt_params(params_ref const & _p) {
|
|||
m_arith_branch_cut_ratio = p.arith_branch_cut_ratio();
|
||||
m_arith_int_eq_branching = p.arith_int_eq_branch();
|
||||
m_arith_ignore_int = p.arith_ignore_int();
|
||||
m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -312,7 +312,7 @@ namespace smt {
|
|||
TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n";
|
||||
tout << "model:\n"; model_pp(tout, *m_curr_model););
|
||||
if (m_params.m_mbqi_trace) {
|
||||
verbose_stream() << "[mbqi] started\n";
|
||||
verbose_stream() << "(smt.mbqi \"started\")\n";
|
||||
}
|
||||
|
||||
init_aux_context();
|
||||
|
@ -324,13 +324,12 @@ namespace smt {
|
|||
quantifier * q = *it;
|
||||
if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) {
|
||||
if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
|
||||
verbose_stream() << "[mbqi] checking: " << q->get_qid() << "\n";
|
||||
verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
|
||||
}
|
||||
found_relevant = true;
|
||||
if (!check(q)) {
|
||||
IF_VERBOSE(5, verbose_stream() << "current model does not satisfy: " << q->get_qid() << "\n";);
|
||||
if (m_params.m_mbqi_trace) {
|
||||
verbose_stream() << "[mbqi] failed " << q->get_qid() << "\n";
|
||||
if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
|
||||
verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n";
|
||||
}
|
||||
num_failures++;
|
||||
}
|
||||
|
@ -347,9 +346,9 @@ namespace smt {
|
|||
m_curr_model->cleanup();
|
||||
if (m_params.m_mbqi_trace) {
|
||||
if (num_failures == 0)
|
||||
verbose_stream() << "[mbqi] succeeded\n";
|
||||
verbose_stream() << "(smt.mbqi :succeeded true)\n";
|
||||
else
|
||||
verbose_stream() << "[mbqi] num failures " << num_failures << "\n";
|
||||
verbose_stream() << "(smt.mbqi :num-failures " << num_failures << ")\n";
|
||||
}
|
||||
return num_failures == 0;
|
||||
}
|
||||
|
@ -360,7 +359,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void model_checker::restart_eh() {
|
||||
IF_VERBOSE(100, verbose_stream() << "instantiating new instances...\n";);
|
||||
IF_VERBOSE(100, verbose_stream() << "(smt.mbqi \"instantiating new instances...\")\n";);
|
||||
assert_new_instances();
|
||||
reset_new_instances();
|
||||
}
|
||||
|
|
|
@ -562,7 +562,7 @@ namespace smt {
|
|||
virtual quantifier_manager::check_model_result
|
||||
check_model(proto_model * m, obj_map<enode, app *> const & root2value) {
|
||||
if (m_fparams->m_mbqi) {
|
||||
IF_VERBOSE(10, verbose_stream() << "model based quantifier instantiation...\n";);
|
||||
IF_VERBOSE(10, verbose_stream() << "(smt.mbqi)\n";);
|
||||
if (m_model_checker->check(m, root2value)) {
|
||||
return quantifier_manager::SAT;
|
||||
}
|
||||
|
@ -594,7 +594,6 @@ namespace smt {
|
|||
final_check_status final_check_quant() {
|
||||
if (use_ematching()) {
|
||||
if (m_lazy_matching_idx < m_fparams->m_qi_max_lazy_multipattern_matching) {
|
||||
IF_VERBOSE(100, verbose_stream() << "matching delayed multi-patterns... \n";);
|
||||
m_lazy_mam->rematch();
|
||||
m_context->push_trail(value_trail<context, unsigned>(m_lazy_matching_idx));
|
||||
m_lazy_matching_idx++;
|
||||
|
|
|
@ -120,7 +120,7 @@ tactic * mk_snf_tactic(ast_manager & m, params_ref const & p) {
|
|||
|
||||
tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref new_p(p);
|
||||
new_p.set_sym("nnf_mode", symbol("full"));
|
||||
new_p.set_sym("mode", symbol("full"));
|
||||
TRACE("nnf", tout << "mk_nnf: " << new_p << "\n";);
|
||||
return using_params(mk_snf_tactic(m, p), new_p);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue