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