1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
lackr.h
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
#pragma once
#include "util/lbool.h"
#include "util/util.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/bv_decl_plugin.h"
#include "model/model.h"
#include "solver/solver.h"
#include "tactic/tactic_exception.h"
#include "tactic/goal.h"
#include "ackermannization/ackr_info.h"
#include "ackermannization/ackr_helper.h"
struct lackr_stats {
lackr_stats() : m_it(0), m_ackrs_sz(0) {}
void reset() { m_it = m_ackrs_sz = 0; }
unsigned m_it; // number of lazy iterations
unsigned m_ackrs_sz; // number of congruence constraints
};
/** \brief
A class to encode or directly solve problems with uninterpreted functions via ackermannization.
Currently, solving is supported only for QF_UFBV.
**/
class lackr {
public:
lackr(ast_manager& m, const params_ref& p, lackr_stats& st,
const ptr_vector<expr>& formulas, solver * uffree_solver);
~lackr();
void updt_params(params_ref const & _p);
/** \brief
* Solve the formula that the class was initialized with.
**/
lbool operator() ();
/** \brief
Converts function occurrences to constants and encodes all congruence ackermann lemmas.
This procedure guarantees a equisatisfiability with the input formula and it has a worst-case quadratic blowup.
Before ackermannization an upper bound on congruence lemmas is computed and tested against \p lemmas_upper_bound.
If this bound is exceeded, the function returns false, it returns true otherwise.
**/
bool mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound);
//
// getters
//
inline ackr_info_ref get_info() { return m_info; }
inline model_ref get_model() { return m_model; }
//
// timeout mechanism
//
void checkpoint() {
if (!m.inc()) {
throw tactic_exception(TACTIC_CANCELED_MSG);
}
}
private:
typedef ackr_helper::fun2terms_map fun2terms_map;
typedef ackr_helper::sel2terms_map sel2terms_map;
typedef ackr_helper::app_set app_set;
ast_manager& m;
params_ref m_p;
const ptr_vector<expr>& m_formulas;
array_util m_autil;
expr_ref_vector m_abstr;
fun2terms_map m_fun2terms;
sel2terms_map m_sel2terms;
ackr_info_ref m_info;
solver* m_solver;
ackr_helper m_ackr_helper;
th_rewriter m_simp;
expr_ref_vector m_ackrs;
model_ref m_model;
bool m_eager;
expr_mark m_non_select;
ast_mark m_non_funs;
lackr_stats& m_st;
bool m_is_init;
bool init();
lbool eager();
lbool lazy();
//
// Introduce congruence ackermann lemma for the two given terms.
//
bool ackr(app * t1, app * t2);
void ackr(app_set const* ts);
//
// Introduce the ackermann lemma for each pair of terms.
//
void eager_enc();
void abstract();
void push_abstraction();
void add_term(app* a);
//
// Collect all uninterpreted terms, skipping 0-arity.
//
bool collect_terms();
void abstract_sel(sel2terms_map const& apps);
void abstract_fun(fun2terms_map const& apps);
};