1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 qflia_tactic.cpp
7
8 Abstract:
9
10 Tactic for QF_NIA
11
12 Author:
13
14 Leonardo (leonardo) 2012-02-28
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/bv/bit_blaster_tactic.h"
25 #include "tactic/bv/max_bv_sharing_tactic.h"
26 #include "sat/tactic/sat_tactic.h"
27 #include "tactic/arith/nla2bv_tactic.h"
28 #include "tactic/arith/lia2card_tactic.h"
29 #include "tactic/arith/card2bv_tactic.h"
30 #include "tactic/core/ctx_simplify_tactic.h"
31 #include "tactic/core/cofactor_term_ite_tactic.h"
32 #include "tactic/smtlogics/smt_tactic.h"
33 #include "nlsat/tactic/qfnra_nlsat_tactic.h"
34
mk_qfnia_bv_solver(ast_manager & m,params_ref const & p_ref)35 static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
36 params_ref p = p_ref;
37 p.set_bool("flat", false);
38 p.set_bool("hi_div0", true);
39 p.set_bool("elim_and", true);
40 p.set_bool("blast_distinct", true);
41
42 params_ref simp2_p = p;
43 simp2_p.set_bool("local_ctx", true);
44 simp2_p.set_uint("local_ctx_limit", 10000000);
45
46 params_ref mem_p = p;
47 mem_p.set_uint("max_memory", 100);
48
49
50 tactic * r = using_params(and_then(mk_simplify_tactic(m),
51 mk_propagate_values_tactic(m),
52 using_params(mk_simplify_tactic(m), simp2_p),
53 mk_max_bv_sharing_tactic(m),
54 using_params(mk_bit_blaster_tactic(m), mem_p),
55 mk_sat_tactic(m)),
56 p);
57 return r;
58 }
59
mk_qfnia_preamble(ast_manager & m,params_ref const & p_ref)60 static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) {
61 params_ref pull_ite_p = p_ref;
62 pull_ite_p.set_bool("pull_cheap_ite", true);
63 pull_ite_p.set_bool("local_ctx", true);
64 pull_ite_p.set_uint("local_ctx_limit", 10000000);
65
66 params_ref ctx_simp_p = p_ref;
67 ctx_simp_p.set_uint("max_depth", 30);
68 ctx_simp_p.set_uint("max_steps", 5000000);
69
70
71 params_ref elim_p = p_ref;
72 elim_p.set_uint("max_memory",20);
73
74 return
75 and_then(mk_simplify_tactic(m),
76 mk_propagate_values_tactic(m),
77 using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
78 using_params(mk_simplify_tactic(m), pull_ite_p),
79 mk_elim_uncnstr_tactic(m),
80 mk_lia2card_tactic(m),
81 mk_card2bv_tactic(m, p_ref),
82 skip_if_failed(using_params(mk_cofactor_term_ite_tactic(m), elim_p)));
83 }
84
mk_qfnia_sat_solver(ast_manager & m,params_ref const & p)85 static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) {
86 params_ref nia2sat_p = p;
87 nia2sat_p.set_uint("nla2bv_max_bv_size", 64);
88 params_ref simp_p = p;
89 simp_p.set_bool("hoist_mul", true); // hoist multipliers to create smaller circuits.
90
91 return and_then(using_params(mk_simplify_tactic(m), simp_p),
92 mk_nla2bv_tactic(m, nia2sat_p),
93 skip_if_failed(mk_qfnia_bv_solver(m, p)),
94 mk_fail_if_undecided_tactic());
95 }
96
mk_qfnia_nlsat_solver(ast_manager & m,params_ref const & p)97 static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) {
98 params_ref nia2sat_p = p;
99 nia2sat_p.set_uint("nla2bv_max_bv_size", 64);
100 params_ref simp_p = p;
101 simp_p.set_bool("som", true); // expand into sums of monomials
102 simp_p.set_bool("factor", false);
103
104 return and_then(using_params(mk_simplify_tactic(m), simp_p),
105 try_for(mk_qfnra_nlsat_tactic(m, simp_p), 3000),
106 mk_fail_if_undecided_tactic());
107 }
108
mk_qfnia_smt_solver(ast_manager & m,params_ref const & p)109 static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) {
110 params_ref simp_p = p;
111 simp_p.set_bool("som", true); // expand into sums of monomials
112 return and_then(
113 using_params(mk_simplify_tactic(m), simp_p),
114 mk_smt_tactic(m));
115 }
116
mk_qfnia_tactic(ast_manager & m,params_ref const & p)117 tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
118 return and_then(
119 mk_report_verbose_tactic("(qfnia-tactic)", 10),
120 mk_qfnia_preamble(m, p),
121 or_else(mk_qfnia_sat_solver(m, p),
122 try_for(mk_qfnia_smt_solver(m, p), 2000),
123 mk_qfnia_nlsat_solver(m, p),
124 mk_qfnia_smt_solver(m, p))
125 )
126 ;
127 }
128
129