-
Notifications
You must be signed in to change notification settings - Fork 1.5k
/
Copy pathsat_config.h
209 lines (176 loc) · 6.11 KB
/
sat_config.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
sat_config.h
Abstract:
SAT main configuration options.
Sub-components have their own options.
Author:
Leonardo de Moura (leonardo) 2011-05-21.
Revision History:
--*/
#pragma once
#include "util/params.h"
namespace sat {
enum phase_selection {
PS_ALWAYS_TRUE,
PS_ALWAYS_FALSE,
PS_BASIC_CACHING,
PS_SAT_CACHING,
PS_LOCAL_SEARCH,
PS_FROZEN,
PS_RANDOM
};
enum restart_strategy {
RS_GEOMETRIC,
RS_LUBY,
RS_EMA,
RS_STATIC
};
enum gc_strategy {
GC_DYN_PSM,
GC_PSM,
GC_GLUE,
GC_GLUE_PSM,
GC_PSM_GLUE
};
enum branching_heuristic {
BH_VSIDS,
BH_CHB
};
enum pb_resolve {
PB_CARDINALITY,
PB_ROUNDING
};
enum pb_lemma_format {
PB_LEMMA_CARDINALITY,
PB_LEMMA_PB
};
enum reward_t {
ternary_reward,
unit_literal_reward,
heule_schur_reward,
heule_unit_reward,
march_cu_reward
};
enum cutoff_t {
depth_cutoff,
freevars_cutoff,
psat_cutoff,
adaptive_freevars_cutoff,
adaptive_psat_cutoff
};
enum local_search_mode {
gsat,
wsat
};
struct config {
unsigned long long m_max_memory;
phase_selection m_phase;
unsigned m_search_sat_conflicts;
unsigned m_search_unsat_conflicts;
bool m_phase_sticky;
unsigned m_rephase_base;
unsigned m_reorder_base;
double m_reorder_itau;
unsigned m_reorder_activity_scale;
bool m_propagate_prefetch;
restart_strategy m_restart;
bool m_restart_fast;
unsigned m_restart_initial;
double m_restart_factor; // for geometric case
double m_restart_margin; // for ema
unsigned m_restart_max;
unsigned m_activity_scale;
double m_fast_glue_avg;
double m_slow_glue_avg;
unsigned m_inprocess_max;
symbol m_inprocess_out;
double m_random_freq;
unsigned m_random_seed;
unsigned m_burst_search;
bool m_enable_pre_simplify;
unsigned m_max_conflicts;
unsigned m_num_threads;
bool m_ddfw_search;
unsigned m_ddfw_threads;
bool m_prob_search;
unsigned m_local_search_threads;
bool m_local_search;
local_search_mode m_local_search_mode;
bool m_local_search_dbg_flips;
bool m_cut_simplify;
unsigned m_cut_delay;
bool m_cut_aig;
bool m_cut_lut;
bool m_cut_xor;
bool m_cut_npn3;
bool m_cut_dont_cares;
bool m_cut_redundancies;
bool m_cut_force;
bool m_anf_simplify;
unsigned m_anf_delay;
bool m_anf_exlin;
bool m_lookahead_simplify;
bool m_lookahead_simplify_bca;
cutoff_t m_lookahead_cube_cutoff;
double m_lookahead_cube_fraction;
unsigned m_lookahead_cube_depth;
double m_lookahead_cube_freevars;
double m_lookahead_cube_psat_var_exp;
double m_lookahead_cube_psat_clause_base;
double m_lookahead_cube_psat_trigger;
reward_t m_lookahead_reward;
bool m_lookahead_double;
bool m_lookahead_global_autarky;
double m_lookahead_delta_fraction;
bool m_lookahead_use_learned;
bool m_incremental;
unsigned m_next_simplify1;
double m_simplify_mult2;
unsigned m_simplify_max;
unsigned m_simplify_delay;
unsigned m_variable_decay;
gc_strategy m_gc_strategy;
unsigned m_gc_initial;
unsigned m_gc_increment;
unsigned m_gc_small_lbd;
unsigned m_gc_k;
bool m_gc_burst;
bool m_gc_defrag;
bool m_force_cleanup;
// backtracking
unsigned m_backtrack_scopes;
unsigned m_backtrack_init_conflicts;
bool m_minimize_lemmas;
bool m_dyn_sub_res;
bool m_core_minimize;
bool m_core_minimize_partial;
// drat proofs
bool m_drat;
bool m_drat_disable;
bool m_drat_binary;
symbol m_drat_file;
bool m_smt_proof_check;
bool m_drat_check_unsat;
bool m_drat_check_sat;
bool m_drat_activity;
bool m_card_solver;
bool m_xor_solver;
pb_resolve m_pb_resolve;
pb_lemma_format m_pb_lemma_format;
// branching heuristic settings.
branching_heuristic m_branching_heuristic;
bool m_anti_exploration;
double m_step_size_init;
double m_step_size_dec;
double m_step_size_min;
double m_reward_multiplier;
double m_reward_offset;
// simplifier configurations used outside of sat_simplifier
bool m_elim_vars;
config(params_ref const & p);
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);
};
};