1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 spacer_manager.h
7
8 Abstract:
9
10 A manager class for SPACER, taking care of creating of AST
11 objects and conversions between them.
12
13 Author:
14
15 Krystof Hoder (t-khoder) 2011-8-25.
16 Arie Gurfinkel
17
18 Revision History:
19
20 --*/
21
22 #pragma once
23
24 #include <utility>
25 #include <map>
26 #include <vector>
27
28 #include "ast/rewriter/bool_rewriter.h"
29 #include "ast/rewriter/expr_replacer.h"
30 #include "ast/expr_substitution.h"
31 #include "util/map.h"
32 #include "util/ref_vector.h"
33 #include "smt/smt_kernel.h"
34 #include "muz/spacer/spacer_util.h"
35 #include "muz/spacer/spacer_sym_mux.h"
36 #include "muz/spacer/spacer_farkas_learner.h"
37 #include "muz/base/dl_rule.h"
38 #include "solver/solver.h"
39 #include "solver/solver_pool.h"
40 namespace smt {class context;}
41
42 namespace spacer {
43
44 struct relation_info {
45 func_decl_ref m_pred;
46 func_decl_ref_vector m_vars;
47 expr_ref m_body;
relation_inforelation_info48 relation_info(ast_manager& m, func_decl* pred, ptr_vector<func_decl> const& vars, expr* b):
49 m_pred(pred, m), m_vars(m, vars.size(), vars.data()), m_body(b, m) {}
50 };
51
52 class unknown_exception {};
53
54 class inductive_property {
55 ast_manager& m;
56 model_converter_ref m_mc;
57 vector<relation_info> m_relation_info;
58 expr_ref fixup_clauses(expr* property) const;
59 expr_ref fixup_clause(expr* clause) const;
60 public:
inductive_property(ast_manager & m,model_converter_ref & mc,vector<relation_info> const & relations)61 inductive_property(ast_manager& m, model_converter_ref& mc, vector<relation_info> const& relations):
62 m(m),
63 m_mc(mc),
64 m_relation_info(relations) {}
65
66 std::string to_string() const;
67 expr_ref to_expr() const;
68 void to_model(model_ref& md) const;
69 void display(datalog::rule_manager& rm,
70 ptr_vector<datalog::rule> const& rules,
71 std::ostream& out) const;
72 };
73
74 class manager {
75 ast_manager& m;
76
77 // manager of multiplexed names
78 sym_mux m_mux;
79
80
n_index()81 unsigned n_index() const { return 0; }
o_index(unsigned i)82 unsigned o_index(unsigned i) const { return i + 1; }
83
84 public:
85 manager(ast_manager & manager);
86
get_manager()87 ast_manager& get_manager() const { return m; }
88
89 // management of mux names
90
91 //"o" predicates stand for the old states and "n" for the new states
92 func_decl * get_o_pred(func_decl * s, unsigned idx);
93 func_decl * get_n_pred(func_decl * s);
94
is_n_formula(expr * f)95 bool is_n_formula(expr * f) const
96 {return m_mux.is_homogenous_formula(f, n_index());}
97
o2n(func_decl * p,unsigned o_idx)98 func_decl * o2n(func_decl * p, unsigned o_idx) const
99 {return m_mux.shift_decl(p, o_index(o_idx), n_index());}
o2o(func_decl * p,unsigned src_idx,unsigned tgt_idx)100 func_decl * o2o(func_decl * p, unsigned src_idx, unsigned tgt_idx) const
101 {return m_mux.shift_decl(p, o_index(src_idx), o_index(tgt_idx));}
n2o(func_decl * p,unsigned o_idx)102 func_decl * n2o(func_decl * p, unsigned o_idx) const
103 {return m_mux.shift_decl(p, n_index(), o_index(o_idx));}
104
105 void formula_o2n(expr * f, expr_ref & result, unsigned o_idx,
106 bool homogenous = true) const
107 {m_mux.shift_expr(f, o_index(o_idx), n_index(), result, homogenous);}
108
109 void formula_n2o(expr * f, expr_ref & result, unsigned o_idx,
110 bool homogenous = true) const
111 {m_mux.shift_expr(f, n_index(), o_index(o_idx), result, homogenous);}
112
formula_n2o(unsigned o_idx,bool homogenous,expr_ref & result)113 void formula_n2o(unsigned o_idx, bool homogenous, expr_ref & result) const
114 {m_mux.shift_expr(result.get(), n_index(), o_index(o_idx),
115 result, homogenous);}
116
117 void formula_o2o(expr * src, expr_ref & tgt, unsigned src_idx,
118 unsigned tgt_idx, bool homogenous = true) const
119 {m_mux.shift_expr(src, o_index(src_idx), o_index(tgt_idx),
120 tgt, homogenous);}
121
122 };
123
124 /** Skolem constants for quantified spacer */
125 app* mk_zk_const (ast_manager &m, unsigned idx, sort *s);
126 int find_zk_const(expr* e, app_ref_vector &out);
find_zk_const(expr_ref_vector const & v,app_ref_vector & out)127 inline int find_zk_const(expr_ref_vector const &v, app_ref_vector &out)
128 {return find_zk_const (mk_and(v), out);}
129
130 bool has_zk_const(expr* e);
131 bool is_zk_const (const app *a, int &n);
132
133 struct sk_lt_proc {bool operator()(const app* a1, const app* a2);};
134
135 }
136
137