1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 qffpa_tactic.cpp
7
8 Abstract:
9
10 Tactic for QF_FP benchmarks.
11
12 Author:
13
14 Christoph (cwinter) 2012-01-16
15
16 Notes:
17
18 --*/
19 #include "tactic/tactical.h"
20 #include "tactic/fpa/fpa2bv_tactic.h"
21 #include "tactic/core/simplify_tactic.h"
22 #include "tactic/core/propagate_values_tactic.h"
23 #include "tactic/arith/probe_arith.h"
24 #include "tactic/bv/bit_blaster_tactic.h"
25 #include "tactic/smtlogics/qfnra_tactic.h"
26 #include "sat/tactic/sat_tactic.h"
27 #include "sat/sat_solver/inc_sat_solver.h"
28 #include "smt/tactic/smt_tactic.h"
29 #include "ackermannization/ackermannize_bv_tactic.h"
30
31 #include "tactic/fpa/qffp_tactic.h"
32
33
34 struct is_non_fp_qfnra_predicate {
35 struct found {};
36 ast_manager & m;
37 bv_util bu;
38 fpa_util fu;
39 arith_util au;
40
is_non_fp_qfnra_predicateis_non_fp_qfnra_predicate41 is_non_fp_qfnra_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {}
42
operator ()is_non_fp_qfnra_predicate43 void operator()(var *) { throw found(); }
operator ()is_non_fp_qfnra_predicate44 void operator()(quantifier *) { throw found(); }
45
operator ()is_non_fp_qfnra_predicate46 void operator()(app * n) {
47 family_id fid = n->get_family_id();
48 if (fid != null_family_id && fid != fu.get_family_id())
49 throw found();
50
51 sort * s = get_sort(n);
52 if (fid == fu.get_family_id()) {
53 if (!fu.is_float(s) && !fu.is_rm(s) &&
54 to_app(n)->get_decl_kind() != OP_FPA_TO_REAL)
55 throw found();
56 }
57 else if (fid == null_family_id) {
58 if (!fu.is_float(s) && !fu.is_rm(s) && !m.is_bool(s))
59 throw found();
60 }
61 else if (fid == m.get_basic_family_id())
62 return;
63 else
64 throw found();
65 }
66 };
67
68 class is_fp_qfnra_probe : public probe {
69 public:
operator ()(goal const & g)70 result operator()(goal const & g) override {
71 return !test<is_non_fp_qfnra_predicate>(g);
72 }
~is_fp_qfnra_probe()73 ~is_fp_qfnra_probe() override {}
74 };
75
mk_is_fp_qfnra_probe()76 probe * mk_is_fp_qfnra_probe() {
77 return alloc(is_fp_qfnra_probe);
78 }
79
80
mk_qffp_tactic(ast_manager & m,params_ref const & p)81 tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
82 params_ref simp_p = p;
83 simp_p.set_bool("arith_lhs", true);
84 simp_p.set_bool("elim_and", true);
85
86 tactic * preamble = and_then(mk_simplify_tactic(m, simp_p),
87 mk_propagate_values_tactic(m, p),
88 mk_fpa2bv_tactic(m, p),
89 mk_propagate_values_tactic(m, p),
90 using_params(mk_simplify_tactic(m, p), simp_p),
91 if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m, p))));
92
93 tactic * st = and_then(preamble,
94 mk_bit_blaster_tactic(m, p),
95 using_params(mk_simplify_tactic(m, p), simp_p),
96 cond(mk_is_propositional_probe(),
97 cond(mk_produce_proofs_probe(),
98 mk_smt_tactic(m, p), // `sat' does not support proofs.
99 mk_psat_tactic(m, p)),
100 cond(mk_is_fp_qfnra_probe(),
101 mk_qfnra_tactic(m, p),
102 mk_smt_tactic(m, p))));
103
104 st->updt_params(p);
105 return st;
106 }
107
mk_qffpbv_tactic(ast_manager & m,params_ref const & p)108 tactic * mk_qffpbv_tactic(ast_manager & m, params_ref const & p) {
109 return mk_qffp_tactic(m, p);
110 }
111
112 struct is_non_qffp_predicate {
113 struct found {};
114 ast_manager & m;
115 bv_util bu;
116 fpa_util fu;
117 arith_util au;
118
is_non_qffp_predicateis_non_qffp_predicate119 is_non_qffp_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {}
120
operator ()is_non_qffp_predicate121 void operator()(var *) { throw found(); }
122
operator ()is_non_qffp_predicate123 void operator()(quantifier *) { throw found(); }
124
operator ()is_non_qffp_predicate125 void operator()(app * n) {
126 sort * s = get_sort(n);
127 if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s) && !au.is_real(s))
128 throw found();
129 family_id fid = n->get_family_id();
130 if (fid == m.get_basic_family_id())
131 return;
132 if (fid == fu.get_family_id() || fid == bu.get_family_id())
133 return;
134 if (is_uninterp_const(n))
135 return;
136 if (au.is_real(s) && au.is_numeral(n))
137 return;
138
139 throw found();
140 }
141 };
142
143 class is_qffp_probe : public probe {
144 public:
operator ()(goal const & g)145 result operator()(goal const & g) override {
146 return !test<is_non_qffp_predicate>(g);
147 }
148
~is_qffp_probe()149 ~is_qffp_probe() override {}
150 };
151
mk_is_qffp_probe()152 probe * mk_is_qffp_probe() {
153 return alloc(is_qffp_probe);
154 }
155
mk_is_qffpbv_probe()156 probe * mk_is_qffpbv_probe() {
157 return alloc(is_qffp_probe);
158 }
159