1 /*++
2 Copyright (c) 2017 Microsoft Corporation and Arie Gurfinkel
3 
4 Module Name:
5 
6     spacer_dl_interface.h
7 
8 Abstract:
9 
10     SMT2 interface for the datalog SPACER
11 
12 Author:
13 
14 
15 Revision History:
16 
17 --*/
18 
19 #pragma once
20 
21 #include "util/lbool.h"
22 #include "muz/base/dl_rule.h"
23 #include "muz/base/dl_rule_set.h"
24 #include "muz/base/dl_engine_base.h"
25 #include "util/statistics.h"
26 
27 namespace datalog {
28 class context;
29 }
30 
31 namespace spacer {
32 
33 class context;
34 
35 class dl_interface : public datalog::engine_base {
36     datalog::context& m_ctx;
37     datalog::rule_set m_spacer_rules;
38     datalog::rule_set m_old_rules;
39     context*          m_context;
40     obj_map<func_decl, func_decl*> m_pred2slice;
41     ast_ref_vector    m_refs;
42 
43     void check_reset();
44 
45 public:
46     dl_interface(datalog::context& ctx);
47     ~dl_interface() override;
48 
49     lbool query(expr* query) override;
50 
51     lbool query_from_lvl(expr* query, unsigned lvl) override;
52 
53     void display_certificate(std::ostream& out) const override;
54 
55     void collect_statistics(statistics& st) const override;
56 
57     void reset_statistics() override;
58 
59     expr_ref get_answer() override;
60 
61     expr_ref get_ground_sat_answer() override;
62 
63     void get_rules_along_trace(datalog::rule_ref_vector& rules) override;
64 
65     unsigned get_num_levels(func_decl* pred) override;
66 
67     expr_ref get_cover_delta(int level, func_decl* pred) override;
68 
69     void add_cover(int level, func_decl* pred, expr* property) override;
70 
71     void add_invariant(func_decl* pred, expr* property) override;
72 
73     expr_ref get_reachable(func_decl *pred) override;
74 
75     void updt_params() override;
76 
77     model_ref get_model() override;
78 
79     proof_ref get_proof() override;
80 
81     void add_callback(void *state,
82                       const datalog::t_new_lemma_eh new_lemma_eh,
83                       const datalog::t_predecessor_eh predecessor_eh,
84                       const datalog::t_unfold_eh unfold_eh) override;
85 
86     void add_constraint (expr *c, unsigned lvl) override;
87 
88 };
89 }
90 
91 
92