mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Merge pull request #1182 from agurfinkel/spacer-z3

Browse source 
Spacer
This commit is contained in:
Nikolaj Bjorner 2017-07-31 17:10:09 -07:00 • committed by GitHub
commit 0eb2915e83
80 changed files with 19399 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -49,6 +49,9 @@ void smt_params::updt_local_params(params_ref const & _p) {
else if (_p.get_bool("arith.least_error_pivot", false))
m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR;
theory_array_params::updt_params(_p);
m_dump_benchmarks = false;
m_dump_min_time = 0.5;
m_dump_recheck = false;
}
void smt_params::updt_params(params_ref const & p) {

9
src/smt/params/smt_params.h
View file

@ -217,6 +217,15 @@ struct smt_params : public preprocessor_params,
bool m_dump_goal_as_smt;
bool m_auto_config;
// -----------------------------------
//
// Spacer hacking
//
// -----------------------------------
bool m_dump_benchmarks;
double m_dump_min_time;
bool m_dump_recheck;
// -----------------------------------
//
// Solver selection

4
src/smt/smt_context.cpp
View file

@ -3548,7 +3548,7 @@ namespace smt {
return false;
}
if (cmr == quantifier_manager::UNKNOWN) {
IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";);
IF_VERBOSE(2, verbose_stream() << "(smt.giveup quantifiers)\n";);
// giving up
m_last_search_failure = QUANTIFIERS;
status = l_undef;
@ -3558,7 +3558,7 @@ namespace smt {
inc_limits();
if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
SASSERT(!inconsistent());
IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
<< " :decisions " << m_stats.m_num_decisions
<< " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {