1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 qflra_tactic.cpp
7
8 Abstract:
9
10 Tactic for QF_LRA
11
12 Author:
13
14 Leonardo (leonardo) 2012-02-26
15
16 Notes:
17
18 --*/
19 #include "tactic/tactical.h"
20 #include "tactic/core/simplify_tactic.h"
21 #include "tactic/core/propagate_values_tactic.h"
22 #include "tactic/core/solve_eqs_tactic.h"
23 #include "tactic/core/elim_uncnstr_tactic.h"
24 #include "tactic/arith/recover_01_tactic.h"
25 #include "tactic/core/ctx_simplify_tactic.h"
26 #include "tactic/arith/probe_arith.h"
27 #include "tactic/smtlogics/smt_tactic.h"
28
mk_qflra_tactic(ast_manager & m,params_ref const & p)29 tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) {
30 params_ref pivot_p;
31 pivot_p.set_bool("arith.greatest_error_pivot", true);
32
33 params_ref main_p = p;
34 main_p.set_bool("elim_and", true);
35 main_p.set_bool("som", true);
36 main_p.set_bool("blast_distinct", true);
37
38 params_ref ctx_simp_p;
39 ctx_simp_p.set_uint("max_depth", 30);
40 ctx_simp_p.set_uint("max_steps", 5000000);
41
42 params_ref lhs_p;
43 lhs_p.set_bool("arith_lhs", true);
44 lhs_p.set_bool("eq2ineq", true);
45
46 params_ref elim_to_real_p;
47 elim_to_real_p.set_bool("elim_to_real", true);
48
49
50 #if 0
51 tactic * mip =
52 and_then(fail_if(mk_produce_proofs_probe()),
53 fail_if(mk_produce_unsat_cores_probe()),
54 using_params(and_then(and_then(mk_simplify_tactic(m),
55 mk_recover_01_tactic(m),
56 using_params(mk_simplify_tactic(m), elim_to_real_p),
57 mk_propagate_values_tactic(m)),
58 using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
59 mk_elim_uncnstr_tactic(m),
60 mk_solve_eqs_tactic(m),
61 using_params(mk_simplify_tactic(m), lhs_p),
62 using_params(mk_simplify_tactic(m), elim_to_real_p)
63 ),
64 main_p),
65 fail_if(mk_not(mk_is_mip_probe())),
66 try_for(mk_mip_tactic(m), 30000),
67 mk_fail_if_undecided_tactic());
68 #endif
69
70 // return using_params(or_else(mip,
71 // using_params(mk_smt_tactic(m), pivot_p)),
72 // p);
73
74 #if 0
75
76 params_ref simplex_0, simplex_1, simplex_2;
77 simplex_0.set_uint("lp.simplex_strategy", 0);
78 simplex_1.set_uint("lp.simplex_strategy", 1);
79 simplex_2.set_uint("lp.simplex_strategy", 2);
80
81 return par(using_params(mk_smt_tactic(), simplex_0),
82 using_params(mk_smt_tactic(), simplex_1),
83 using_params(mk_smt_tactic(), simplex_2));
84 #else
85 return using_params(using_params(mk_smt_tactic(m), pivot_p), p);
86 #endif
87
88 }
89