mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 21:31:22 +00:00
Code Activity

(Re-)added option to disable lemma deletion in the smt_context.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-08-23 12:14:19 +01:00
parent ed5058d225
commit 3e960eadd2
2 changed files with 295 additions and 292 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -31,7 +31,7 @@ Revision History:
#include "smt/params/preprocessor_params.h" #include "smt/params/preprocessor_params.h"
#include "cmd_context/context_params.h" #include "cmd_context/context_params.h"
enum phase_selection { enum phase_selection {
PS_ALWAYS_FALSE, PS_ALWAYS_FALSE,
PS_ALWAYS_TRUE, PS_ALWAYS_TRUE,
PS_CACHING, PS_CACHING,
@ -52,7 +52,8 @@ enum restart_strategy {
enum lemma_gc_strategy { enum lemma_gc_strategy {
LGC_FIXED, LGC_FIXED,
LGC_GEOMETRIC, LGC_GEOMETRIC,
LGC_AT_RESTART LGC_AT_RESTART,
LGC_NONE
}; };
enum initial_activity { enum initial_activity {
@ -71,11 +72,11 @@ enum case_split_strategy {
CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity
}; };
struct smt_params : public preprocessor_params, struct smt_params : public preprocessor_params,
public dyn_ack_params, public dyn_ack_params,
public qi_params, public qi_params,
public theory_arith_params, public theory_arith_params,
public theory_array_params, public theory_array_params,
public theory_bv_params, public theory_bv_params,
public theory_str_params, public theory_str_params,
public theory_pb_params, public theory_pb_params,
@ -153,12 +154,12 @@ struct smt_params : public preprocessor_params,
unsigned m_lemma_gc_initial; unsigned m_lemma_gc_initial;
double m_lemma_gc_factor; double m_lemma_gc_factor;
unsigned m_new_old_ratio; //!< the ratio of new and old clauses. unsigned m_new_old_ratio; //!< the ratio of new and old clauses.
unsigned m_new_clause_activity; unsigned m_new_clause_activity;
unsigned m_old_clause_activity; unsigned m_old_clause_activity;
unsigned m_new_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant. unsigned m_new_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant.
unsigned m_old_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant. unsigned m_old_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant.
double m_inv_clause_decay; //!< clause activity decay double m_inv_clause_decay; //!< clause activity decay
// ----------------------------------- // -----------------------------------
// //
// SMT-LIB (debug) pretty printer // SMT-LIB (debug) pretty printer
@ -166,7 +167,7 @@ struct smt_params : public preprocessor_params,
// ----------------------------------- // -----------------------------------
bool m_smtlib_dump_lemmas; bool m_smtlib_dump_lemmas;
symbol m_logic; symbol m_logic;
// ----------------------------------- // -----------------------------------
// //
// Statistics for Profiling // Statistics for Profiling
@ -179,10 +180,10 @@ struct smt_params : public preprocessor_params,
// ----------------------------------- // -----------------------------------
// //
// Model generation // Model generation
// //
// ----------------------------------- // -----------------------------------
bool m_model; bool m_model;
bool m_model_compact; bool m_model_compact;
bool m_model_on_timeout; bool m_model_on_timeout;
bool m_model_on_final_check; bool m_model_on_final_check;
@ -213,7 +214,7 @@ struct smt_params : public preprocessor_params,
unsigned m_timeout; unsigned m_timeout;
unsigned m_rlimit; unsigned m_rlimit;
bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples. bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples. bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
bool m_dump_goal_as_smt; bool m_dump_goal_as_smt;
bool m_auto_config; bool m_auto_config;
@ -237,7 +238,7 @@ struct smt_params : public preprocessor_params,
m_display_proof(false), m_display_proof(false),
m_display_dot_proof(false), m_display_dot_proof(false),
m_display_unsat_core(false), m_display_unsat_core(false),
m_check_proof(false), m_check_proof(false),
m_eq_propagation(true), m_eq_propagation(true),
m_binary_clause_opt(true), m_binary_clause_opt(true),
m_relevancy_lvl(2), m_relevancy_lvl(2),
@ -279,7 +280,7 @@ struct smt_params : public preprocessor_params,
m_new_old_ratio(16), m_new_old_ratio(16),
m_new_clause_activity(10), m_new_clause_activity(10),
m_old_clause_activity(500), m_old_clause_activity(500),
m_new_clause_relevancy(45), m_new_clause_relevancy(45),
m_old_clause_relevancy(6), m_old_clause_relevancy(6),
m_inv_clause_decay(1), m_inv_clause_decay(1),
m_smtlib_dump_lemmas(false), m_smtlib_dump_lemmas(false),

556
src/smt/smt_context.cpp
View file

File diff suppressed because it is too large Load diff