| /dports/math/z3/z3-z3-4.8.13/src/tactic/ |
| H A D | tactical.h | 27 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4);
28 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5);
29 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6);
30 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
31 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
32 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
33 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
34 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
43 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tact…
44 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tact…
[all …]
|
| H A D | tactical.cpp | 185 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6) { in and_then()
189 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac… in and_then()
193 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac… in and_then()
197 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac… in and_then()
201 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac… in and_then()
205 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac… in and_then()
334 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6) { in or_else()
339 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tact… in or_else()
344 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tact… in or_else()
349 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tact… in or_else()
[all …]
|
| H A D | tactic.h | 33 class tactic {
36 tactic():m_ref_count(0) {} in tactic() function
37 virtual ~tactic() {} in ~tactic()
86 typedef ref<tactic> tactic_ref;
87 typedef sref_vector<tactic> tactic_ref_vector;
88 typedef sref_buffer<tactic> tactic_ref_buffer;
103 class skip_tactic : public tactic {
110 tactic * mk_skip_tactic();
111 tactic * mk_fail_tactic();
112 tactic * mk_fail_if_undecided_tactic();
[all …]
|
| H A D | tactic.cpp | 81 tactic * mk_skip_tactic() { in mk_skip_tactic()
85 class fail_tactic : public tactic {
93 tactic * translate(ast_manager & m) override { return this; } in translate()
96 tactic * mk_fail_tactic() { in mk_fail_tactic()
112 tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl) { in mk_report_verbose_tactic()
128 tactic * mk_trace_tactic(char const * tag) { in mk_trace_tactic()
143 tactic * mk_fail_if_undecided_tactic() { in mk_fail_if_undecided_tactic()
147 void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result) { in exec()
161 lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr… in check_sat()
255 void tactic::checkpoint(ast_manager& m) { in checkpoint()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/ |
| H A D | tactical.h | 27 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4);
28 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5);
29 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6);
30 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
31 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac… in fm_muram_alloc()
32 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
33 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
34 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
43 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tact…
44 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tact…
[all …]
|
| H A D | tactical.cpp | 188 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6) {
192 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
196 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
200 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
204 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
208 tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tac…
341 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6) {
346 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tact…
351 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tact…
356 tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tact…
[all …]
|
| H A D | tactic.h | 33 class tactic { in mk_quant_preprocessor()
36 tactic():m_ref_count(0) {} in mk_quant_preprocessor()
37 virtual ~tactic() {} in mk_quant_preprocessor()
86 typedef ref<tactic> tactic_ref;
87 typedef sref_vector<tactic> tactic_ref_vector;
88 typedef sref_buffer<tactic> tactic_ref_buffer;
103 class skip_tactic : public tactic {
110 tactic * mk_skip_tactic();
111 tactic * mk_fail_tactic();
112 tactic * mk_fail_if_undecided_tactic();
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/smtlogics/ |
| H A D | quant_tactics.cpp | 41 tactic * solve_eqs; in mk_quant_preprocessor()
59 static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) { in mk_no_solve_eq_preprocessor()
63 tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) { in mk_ufnia_tactic()
64 tactic * st = and_then(mk_no_solve_eq_preprocessor(m), in mk_ufnia_tactic()
72 tactic * st = and_then(mk_quant_preprocessor(m), in mk_uflra_tactic()
82 tactic * st = and_then(mk_no_solve_eq_preprocessor(m), in mk_auflia_tactic()
92 tactic * st = and_then(mk_quant_preprocessor(m), in mk_auflira_tactic()
99 tactic * st = and_then(mk_quant_preprocessor(m), in mk_aufnira_tactic()
105 tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) { in mk_lra_tactic()
106 tactic * st = and_then(mk_quant_preprocessor(m), in mk_lra_tactic()
[all …]
|
| H A D | quant_tactics.h | 23 class tactic; variable
25 tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p);
26 tactic * mk_uflra_tactic(ast_manager & m, params_ref const & p);
27 tactic * mk_auflia_tactic(ast_manager & m, params_ref const & p);
28 tactic * mk_auflira_tactic(ast_manager & m, params_ref const & p);
29 tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p);
30 tactic * mk_lra_tactic(ast_manager & m, params_ref const & p);
31 tactic * mk_lia_tactic(ast_manager & m, params_ref const & p);
32 tactic * mk_lira_tactic(ast_manager & m, params_ref const & p);
|
| H A D | qfbv_tactic.cpp | 36 static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { in mk_qfbv_preamble()
76 static tactic * main_p(tactic* t) { in main_p()
85 static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) { in mk_qfbv_tactic()
96 tactic* preamble_st = mk_qfbv_preamble(m, p); in mk_qfbv_tactic()
97 tactic * st = main_p(and_then(preamble_st, in mk_qfbv_tactic()
123 tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { in mk_qfbv_tactic()
124 tactic * new_sat = cond(mk_produce_proofs_probe(), in mk_qfbv_tactic()
|
| H A D | qfbv_tactic.h | 23 class tactic; variable
25 tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p = params_ref());
31 tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p);
33 tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p, tactic* sat, tactic* smt);
|
| H A D | qfufbv_tactic.cpp | 45 class qfufbv_ackr_tactic : public tactic {
105 tactic* translate(ast_manager& m) override { in translate()
138 static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) { in mk_qfufbv_preamble1()
165 static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) { in mk_qfufbv_preamble()
177 tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { in mk_qfufbv_tactic()
182 tactic * const preamble_st = mk_qfufbv_preamble(m, p); in mk_qfufbv_tactic()
184 tactic * st = using_params( in mk_qfufbv_tactic()
195 tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) { in mk_qfufbv_ackr_tactic()
196 tactic * const preamble_t = mk_qfufbv_preamble1(m, p); in mk_qfufbv_ackr_tactic()
198 tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p); in mk_qfufbv_ackr_tactic()
|
| H A D | qflia_tactic.cpp | 61 static tactic * mk_no_cut_smt_tactic(ast_manager& m, unsigned rs) { in mk_no_cut_smt_tactic()
70 static tactic * mk_no_cut_no_relevancy_smt_tactic(ast_manager& m, unsigned rs) { in mk_no_cut_no_relevancy_smt_tactic()
78 static tactic * mk_bv2sat_tactic(ast_manager & m) { in mk_bv2sat_tactic()
99 static tactic * mk_pb_tactic(ast_manager & m) { in mk_pb_tactic()
121 static tactic * mk_lia2sat_tactic(ast_manager & m) { in mk_lia2sat_tactic()
143 static tactic * mk_ilp_model_finder_tactic(ast_manager & m) { in mk_ilp_model_finder_tactic()
169 static tactic * mk_bounded_tactic(ast_manager & m) { in mk_bounded_tactic()
180 tactic * mk_preamble_tactic(ast_manager& m) { in mk_preamble_tactic()
203 tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) { in mk_qflia_tactic()
217 tactic* st = using_params( in mk_qflia_tactic()
|
| H A D | qfnia_tactic.cpp | 35 static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { in mk_qfnia_bv_solver()
50 tactic * r = using_params(and_then(mk_simplify_tactic(m), in mk_qfnia_bv_solver()
60 static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) { in mk_qfnia_preamble()
85 static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) { in mk_qfnia_sat_solver()
97 static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) { in mk_qfnia_nlsat_solver()
109 static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) { in mk_qfnia_smt_solver()
117 tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { in mk_qfnia_tactic()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/smtlogics/ |
| H A D | quant_tactics.cpp | 42 tactic * solve_eqs;
60 static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) {
64 tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) {
65 tactic * st = and_then(mk_no_solve_eq_preprocessor(m),
73 tactic * st = and_then(mk_quant_preprocessor(m),
83 tactic * st = and_then(mk_no_solve_eq_preprocessor(m),
93 tactic * st = and_then(mk_quant_preprocessor(m),
100 tactic * st = and_then(mk_quant_preprocessor(m),
106 tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
107 tactic * st = and_then(mk_quant_preprocessor(m),
[all …]
|
| H A D | quant_tactics.h | 23 class tactic; variable
25 tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p);
26 tactic * mk_uflra_tactic(ast_manager & m, params_ref const & p);
27 tactic * mk_auflia_tactic(ast_manager & m, params_ref const & p);
28 tactic * mk_auflira_tactic(ast_manager & m, params_ref const & p);
29 tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p);
30 tactic * mk_lra_tactic(ast_manager & m, params_ref const & p);
31 tactic * mk_lia_tactic(ast_manager & m, params_ref const & p);
32 tactic * mk_lira_tactic(ast_manager & m, params_ref const & p);
|
| H A D | qfbv_tactic.cpp | 37 static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { in mk_qfbv_preamble()
77 static tactic * main_p(tactic* t) { in main_p()
86 static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) { in mk_qfbv_tactic()
97 tactic* preamble_st = mk_qfbv_preamble(m, p); in mk_qfbv_tactic()
98 tactic * st = main_p(and_then(preamble_st, in mk_qfbv_tactic()
124 tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { in mk_qfbv_tactic()
125 tactic * new_sat = cond(mk_produce_proofs_probe(), in mk_qfbv_tactic()
|
| H A D | qfbv_tactic.h | 23 class tactic;
25 tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p = params_ref());
31 tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p);
33 tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p, tactic* sat, tactic* smt);
|
| H A D | qflia_tactic.cpp | 61 static tactic * mk_no_cut_smt_tactic(ast_manager& m, unsigned rs) {
78 static tactic * mk_bv2sat_tactic(ast_manager & m) {
99 static tactic * mk_pb_tactic(ast_manager & m) {
121 static tactic * mk_lia2sat_tactic(ast_manager & m) {
143 static tactic * mk_ilp_model_finder_tactic(ast_manager & m) {
169 static tactic * mk_bounded_tactic(ast_manager & m) {
180 tactic * mk_preamble_tactic(ast_manager& m) {
196 tactic * preamble_st = and_then(mk_simplify_tactic(m),
211 tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
224 tactic * preamble_st = mk_preamble_tactic(m);
[all …]
|
| H A D | qfufbv_tactic.cpp | 46 class qfufbv_ackr_tactic : public tactic {
106 tactic* translate(ast_manager& m) override {
139 static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
166 static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) {
178 tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
183 tactic * const preamble_st = mk_qfufbv_preamble(m, p);
185 tactic * st = using_params(
196 tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) {
197 tactic * const preamble_t = mk_qfufbv_preamble1(m, p);
199 tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p);
|
| H A D | qfnia_tactic.cpp | 35 static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { in mk_qfnia_bv_solver()
50 tactic * r = using_params(and_then(mk_simplify_tactic(m), in mk_qfnia_bv_solver()
60 static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) { in mk_qfnia_preamble()
85 static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) { in mk_qfnia_sat_solver()
97 static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) { in mk_qfnia_nlsat_solver()
109 static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) { in mk_qfnia_smt_solver()
117 tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { in mk_qfnia_tactic()
|
| /dports/math/teyjus/teyjus-2.1-7-ge63f40a/examples/ndprover/ |
| H A D | script | 34 Enter tactic: imp_i_tac.
41 Enter tactic: exists_i_tac.
48 Enter tactic: or_e_tac 1.
55 Enter tactic: close_tac.
62 Enter tactic: backup.
69 Enter tactic: backup.
76 Enter tactic: backup.
83 Enter tactic: or_e_tac 1.
90 Enter tactic: exists_i_tac.
97 Enter tactic: close_tac.
[all …]
|
| /dports/games/biniax2/biniax2-1.30_9/ |
| H A D | hof.c | 100 strcpy( Hof.tactic[ i ].name, "JORDAN " ); in hofInit()
101 Hof.tactic[ i ].score = (cHofEntries - i) * cHofInitScore; in hofInit()
124 Hof.tactic[ i ].name[ j ] = sysFGet8( file ); in hofInit()
127 Hof.tactic[ i ].score = sysFGet32( file ); in hofInit()
159 sysFPut8( Hof.tactic[ i ].name[ j ], file ); in hofSave()
162 sysFPut32( Hof.tactic[ i ].score, file ); in hofSave()
200 if ( Hof.tactic[ i ].score < game->score[ cPlayer1 ] ) in hofEnter()
202 recEntry = &Hof.tactic[ i ]; in hofEnter()
209 strcpy( Hof.tactic[ j ].name, Hof.tactic[ j-1 ].name ); in hofEnter()
210 Hof.arcade[ j ].score = Hof.tactic[ j-1 ].score; in hofEnter()
|
| /dports/security/s2n/s2n-tls-1.1.2/tests/saw/bike_r1/proof/ |
| H A D | base.saw | 7 let tactic unints =
20 crucible_llvm_verify m func overrides false spec (tactic unints)
35 crucible_llvm_verify m func overrides true spec (tactic unints)
53 tactic unints;
72 crucible_llvm_verify m func overrides false spec (tactic []);
75 crucible_llvm_verify m func overrides true spec (tactic []);
80 tactic unints;
84 crucible_llvm_verify m func overrides false spec (tactic unints);
87 crucible_llvm_verify m func overrides true spec (tactic unints);
106 tactic unints; };
|
| /dports/security/s2n/s2n-tls-1.1.2/tests/saw/bike_r2/proof/ |
| H A D | base.saw | 7 let tactic unints =
20 crucible_llvm_verify m func overrides false spec (tactic unints)
35 crucible_llvm_verify m func overrides true spec (tactic unints)
53 tactic unints;
72 crucible_llvm_verify m func overrides false spec (tactic []);
75 crucible_llvm_verify m func overrides true spec (tactic []);
80 tactic unints;
84 crucible_llvm_verify m func overrides false spec (tactic unints);
87 crucible_llvm_verify m func overrides true spec (tactic unints);
106 tactic unints; };
|