1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* The module for managing witness form conversion in proofs. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__SMT__WITNESS_FORM_H |
19 |
|
#define CVC5__SMT__WITNESS_FORM_H |
20 |
|
|
21 |
|
#include <unordered_set> |
22 |
|
|
23 |
|
#include "proof/conv_proof_generator.h" |
24 |
|
#include "proof/proof.h" |
25 |
|
#include "proof/proof_generator.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
|
29 |
|
class Env; |
30 |
|
|
31 |
|
namespace theory { |
32 |
|
class Rewriter; |
33 |
|
} |
34 |
|
|
35 |
|
namespace smt { |
36 |
|
|
37 |
|
/** |
38 |
|
* The witness form proof generator, which acts as a wrapper around a |
39 |
|
* TConvProofGenerator for adding rewrite steps for witness introduction. |
40 |
|
* |
41 |
|
* The proof steps managed by this class are stored in a context-independent |
42 |
|
* manager, which matches how witness forms are managed in SkolemManager. |
43 |
|
*/ |
44 |
|
class WitnessFormGenerator : public ProofGenerator |
45 |
|
{ |
46 |
|
public: |
47 |
|
WitnessFormGenerator(Env& env); |
48 |
7987 |
~WitnessFormGenerator() {} |
49 |
|
/** |
50 |
|
* Get proof for, which expects an equality of the form t = toWitness(t). |
51 |
|
* This returns a proof based on the term conversion proof generator utility. |
52 |
|
* This proof may contain open assumptions of the form: |
53 |
|
* k = toWitness(k) |
54 |
|
* Each of these assumptions are included in the set getWitnessFormEqs() |
55 |
|
* below after returning this call. |
56 |
|
*/ |
57 |
|
std::shared_ptr<ProofNode> getProofFor(Node eq) override; |
58 |
|
/** Identify */ |
59 |
|
std::string identify() const override; |
60 |
|
/** |
61 |
|
* Does the rewrite require witness form conversion? |
62 |
|
* When calling this method, it should be the case that: |
63 |
|
* Rewriter::rewrite(toWitness(t)) == Rewriter::rewrite(toWitness(s)) |
64 |
|
* The rule MACRO_SR_PRED_TRANSFORM concludes t == s if the above holds. |
65 |
|
* This method returns false if: |
66 |
|
* Rewriter::rewrite(t) == Rewriter::rewrite(s) |
67 |
|
* which means that the proof of the above fact does not need to do |
68 |
|
* witness form conversion to prove conclusions of MACRO_SR_PRED_TRANSFORM. |
69 |
|
*/ |
70 |
|
bool requiresWitnessFormTransform(Node t, Node s) const; |
71 |
|
/** |
72 |
|
* Same as above, with s = true. This is intended for use with |
73 |
|
* MACRO_SR_PRED_INTRO. |
74 |
|
*/ |
75 |
|
bool requiresWitnessFormIntro(Node t) const; |
76 |
|
/** |
77 |
|
* Get witness form equalities. This returns a set of equalities of the form: |
78 |
|
* k = toWitness(k) |
79 |
|
* where k is a skolem, containing all rewrite steps used in calls to |
80 |
|
* getProofFor during the entire lifetime of this generator. |
81 |
|
*/ |
82 |
|
const std::unordered_set<Node>& getWitnessFormEqs() const; |
83 |
|
|
84 |
|
private: |
85 |
|
/** |
86 |
|
* Convert to witness form. This internally constructs rewrite steps that |
87 |
|
* suffice to show t = toWitness(t) using the term conversion proof generator |
88 |
|
* of this class (d_tcpg). |
89 |
|
*/ |
90 |
|
Node convertToWitnessForm(Node t); |
91 |
|
/** |
92 |
|
* Return a proof generator that can prove the given axiom exists. |
93 |
|
*/ |
94 |
|
ProofGenerator* convertExistsInternal(Node exists); |
95 |
|
/** The rewriter we are using */ |
96 |
|
theory::Rewriter* d_rewriter; |
97 |
|
/** The term conversion proof generator */ |
98 |
|
TConvProofGenerator d_tcpg; |
99 |
|
/** The nodes we have already added rewrite steps for in d_tcpg */ |
100 |
|
std::unordered_set<TNode> d_visited; |
101 |
|
/** The set of equalities added as proof steps */ |
102 |
|
std::unordered_set<Node> d_eqs; |
103 |
|
/** Lazy proof storing witness intro steps */ |
104 |
|
LazyCDProof d_wintroPf; |
105 |
|
/** CDProof for justifying purification existentials */ |
106 |
|
CDProof d_pskPf; |
107 |
|
}; |
108 |
|
|
109 |
|
} // namespace smt |
110 |
|
} // namespace cvc5 |
111 |
|
|
112 |
|
#endif |