| /dports/math/boolector/boolector-3.2.2/src/ |
| H A D | btorsat.h | 21 typedef struct BtorSATMgr BtorSATMgr; typedef
23 struct BtorSATMgr struct
58 void (*assume) (BtorSATMgr *, int32_t);
63 int32_t (*inc_max_var) (BtorSATMgr *);
65 void (*melt) (BtorSATMgr *, int32_t);
71 void (*stats) (BtorSATMgr *);
73 void (*setterm) (BtorSATMgr *);
94 BtorSATMgr *btor_sat_mgr_new (Btor *btor);
105 BtorSATMgr *btor_sat_mgr_clone (Btor *btor, BtorSATMgr *smgr);
125 void btor_sat_init (BtorSATMgr *smgr);
[all …]
|
| H A D | btorsat.c | 41 add (BtorSATMgr *smgr, int32_t lit) in add()
95 inc_max_var (BtorSATMgr *smgr) in inc_max_var()
102 init (BtorSATMgr *smgr) in init()
123 reset (BtorSATMgr *smgr) in reset()
149 setterm (BtorSATMgr *smgr) in setterm()
155 stats (BtorSATMgr *smgr) in stats()
162 BtorSATMgr *
167 BtorSATMgr *smgr; in btor_sat_mgr_new()
200 BtorSATMgr *
206 BtorSATMgr *res; in btor_sat_mgr_clone()
[all …]
|
| H A D | btoraig.h | 55 BtorSATMgr *smgr;
170 BtorSATMgr *btor_aig_get_sat_mgr (const BtorAIGMgr *amgr);
|
| H A D | btorcore.h | 291 BtorSATMgr *btor_get_sat_mgr (const Btor *btor);
|
| H A D | btorcore.c | 269 BtorSATMgr *
813 BtorSATMgr *smgr; in btor_set_term()
1782 BtorSATMgr *smgr; in exp_to_cnf_lit()
1888 BtorSATMgr *smgr; in btor_failed_exp()
2780 BtorSATMgr *smgr; in btor_add_again_assumptions()
2858 BtorSATMgr *smgr;
|
| H A D | btoraig.c | 1117 BtorSATMgr *smgr; in btor_aig_to_sat_tseitin()
1351 BtorSATMgr *smgr; in btor_aig_add_toplevel_to_sat()
1461 BtorSATMgr *
|
| H A D | btorclone.c | 1017 + sizeof (BtorSATMgr) in clone_aux_btor()
1031 + sizeof (BtorSATMgr) in clone_aux_btor()
1052 sizeof (BtorCnfPrinter) + sizeof (BtorSATMgr) in clone_aux_btor()
|
| H A D | btorslvfun.c | 214 BtorSATMgr *smgr; in configure_sat_mgr()
253 BtorSATMgr *smgr; in timed_sat_sat()
844 BtorSATMgr *smgr; in search_initial_applies_dual_prop()
|
| /dports/math/boolector/boolector-3.2.2/src/sat/ |
| H A D | btorpicosat.c | 20 init (BtorSATMgr *smgr) in init()
37 add (BtorSATMgr *smgr, int32_t lit) in add()
43 sat (BtorSATMgr *smgr, int32_t limit) in sat()
49 deref (BtorSATMgr *smgr, int32_t lit) in deref()
55 reset (BtorSATMgr *smgr) in reset()
62 set_output (BtorSATMgr *smgr, FILE *output) in set_output()
80 inc_max_var (BtorSATMgr *smgr) in inc_max_var()
86 stats (BtorSATMgr *smgr) in stats()
92 fixed (BtorSATMgr *smgr, int32_t lit) in fixed()
100 assume (BtorSATMgr *smgr, int32_t lit) in assume()
[all …]
|
| H A D | btorcadical.c | 20 init (BtorSATMgr *smgr) in init()
33 add (BtorSATMgr *smgr, int32_t lit) in add()
39 assume (BtorSATMgr *smgr, int32_t lit) in assume()
45 deref (BtorSATMgr *smgr, int32_t lit) in deref()
66 failed (BtorSATMgr *smgr, int32_t lit) in failed()
72 reset (BtorSATMgr *smgr) in reset()
79 sat (BtorSATMgr *smgr, int32_t limit) in sat()
86 setterm (BtorSATMgr *smgr) in setterm()
97 inc_max_var (BtorSATMgr *smgr) in inc_max_var()
108 melt (BtorSATMgr *smgr, int32_t lit) in melt()
[all …]
|
| H A D | btorlgl.c | 35 init (BtorSATMgr *smgr) in init()
57 add (BtorSATMgr *smgr, int32_t lit) in add()
64 sat (BtorSATMgr *smgr, int32_t limit) in sat()
171 deref (BtorSATMgr *smgr, int32_t lit) in deref()
178 repr (BtorSATMgr *smgr, int32_t lit) in repr()
185 reset (BtorSATMgr *smgr) in reset()
217 inc_max_var (BtorSATMgr *smgr) in inc_max_var()
226 stats (BtorSATMgr *smgr) in stats()
243 melt (BtorSATMgr *smgr, int32_t lit) in melt()
264 clone (Btor *btor, BtorSATMgr *smgr) in clone()
[all …]
|
| H A D | btorminisat.cc | 137 init (BtorSATMgr* smgr) in init()
145 add (BtorSATMgr* smgr, int32_t lit) in add()
152 sat (BtorSATMgr* smgr, int32_t limit) in sat()
163 deref (BtorSATMgr* smgr, int32_t lit) in deref()
170 reset (BtorSATMgr* smgr) in reset()
177 inc_max_var (BtorSATMgr* smgr) in inc_max_var()
184 assume (BtorSATMgr* smgr, int32_t lit) in assume()
191 fixed (BtorSATMgr* smgr, int32_t lit) in fixed()
198 failed (BtorSATMgr* smgr, int32_t lit) in failed()
212 stats (BtorSATMgr* smgr) in stats()
[all …]
|
| H A D | btorcms.cc | 157 init (BtorSATMgr* smgr) in init()
168 add (BtorSATMgr* smgr, int32_t lit) in add()
175 sat (BtorSATMgr* smgr, int32_t limit) in sat()
183 deref (BtorSATMgr* smgr, int32_t lit) in deref()
190 reset (BtorSATMgr* smgr) in reset()
197 inc_max_var (BtorSATMgr* smgr) in inc_max_var()
204 assume (BtorSATMgr* smgr, int32_t lit) in assume()
211 fixed (BtorSATMgr* smgr, int32_t lit) in fixed()
218 failed (BtorSATMgr* smgr, int32_t lit) in failed()
232 stats (BtorSATMgr* smgr) in stats()
[all …]
|
| H A D | btorcadical.h | 18 bool btor_sat_enable_cadical (BtorSATMgr* smgr);
|
| H A D | btorpicosat.h | 18 bool btor_sat_enable_picosat (BtorSATMgr* smgr);
|
| H A D | btorcms.h | 18 bool btor_sat_enable_cms (BtorSATMgr* smgr);
|
| H A D | btorminisat.h | 18 bool btor_sat_enable_minisat (BtorSATMgr* smgr);
|
| H A D | btorlgl.h | 27 bool btor_sat_enable_lingeling (BtorSATMgr* smgr);
|
| /dports/math/boolector/boolector-3.2.2/test/ |
| H A D | test_satmgr.cpp | 29 BtorSATMgr *d_smgr = nullptr;
|
| H A D | test_aig.cpp | 125 BtorSATMgr *smgr = btor_aig_get_sat_mgr (amgr); in TEST_F()
|
| /dports/math/boolector/boolector-3.2.2/src/api/python/ |
| H A D | boolector_py.c | 48 BtorSATMgr *smgr; in boolector_py_set_term()
|
| /dports/math/boolector/boolector-3.2.2/src/preprocess/ |
| H A D | btorskel.c | 23 BtorSATMgr *smgr; in fixed_exp()
|