1 /*++
2 Copyright (c) 2017 Arie Gurfinkel
3 
4 Module Name:
5 
6     spacer_proof_utils.cpp
7 
8 Abstract:
9     Utilities to traverse and manipulate proofs
10 
11 Author:
12     Bernhard Gleiss
13     Arie Gurfinkel
14 
15 Revision History:
16 
17 --*/
18 
19 #pragma once
20 #include "ast/ast.h"
21 
22 namespace spacer {
23 
24 bool is_arith_lemma(ast_manager& m, proof* pr);
25 bool is_farkas_lemma(ast_manager& m, proof* pr);
26 
27 /// rewrites theory axioms into theory lemmas
28 class theory_axiom_reducer {
29 public:
theory_axiom_reducer(ast_manager & m)30     theory_axiom_reducer(ast_manager& m) : m(m), m_pinned(m) {}
31 
32     // reduce theory axioms and return transformed proof
33     proof_ref reduce(proof* pr);
34 
35 private:
36     ast_manager &m;
37 
38     // tracking all created expressions
39     expr_ref_vector m_pinned;
40 
41     // maps each proof of a clause to the transformed subproof of
42     // that clause
43     obj_map<proof, proof*> m_cache;
44 
45     void reset();
46 };
47 
48 /// reduces the number of hypotheses in a proof
49 class hypothesis_reducer
50 {
51 public:
hypothesis_reducer(ast_manager & m)52     hypothesis_reducer(ast_manager &m) : m(m), m_pinned(m) {}
~hypothesis_reducer()53     ~hypothesis_reducer() {reset();}
54 
55     // reduce hypothesis and return transformed proof
56     proof_ref reduce(proof* pf);
57 
58 private:
59     typedef ptr_vector<proof> proof_ptr_vector;
60 
61     ast_manager &m;
62 
63     proof_ptr_vector m_empty_vector;
64 
65     // created expressions
66     expr_ref_vector m_pinned;
67 
68     // created sets of active hypothesis
69     ptr_vector<proof_ptr_vector> m_pinned_active_hyps;
70 
71     // maps a proof to the transformed proof
72     obj_map<proof, proof*> m_cache;
73 
74     // maps a unit literal to its derivation
75     obj_map<expr, proof*> m_units;
76 
77     // maps a proof node to the set of its  active (i.e., in scope) hypotheses
78     obj_map<proof, proof_ptr_vector*> m_active_hyps;
79 
80     /// marks if an expression is ever used as a hypothesis in a proof
81     expr_mark m_hyp_mark;
82     /// marks a proof as open, i.e., has a non-discharged hypothesis as ancestor
83     expr_mark m_open_mark;
84     expr_mark m_visited;
85 
86     void reset();
87 
88     /// true if p is an ancestor of q
89     bool is_ancestor(proof *p, proof *q);
90     // compute active_hyps and parent_hyps for a given proof node and
91     // all its ancestors
92     void compute_hypsets(proof* pr);
93     // compute m_units
94     void collect_units(proof* pr);
95 
96     // -- rewrite proof to reduce number of hypotheses used
97     proof* reduce_core(proof* pf);
98 
99     proof* mk_lemma_core(proof *pf, expr *fact);
100     proof* mk_unit_resolution_core(proof* ures, ptr_buffer<proof>& args);
101     proof* mk_proof_core(proof* old, ptr_buffer<proof>& args);
102 };
103 }
104