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 |
|
namespace smt { |
29 |
|
|
30 |
|
/** |
31 |
|
* The witness form proof generator, which acts as a wrapper around a |
32 |
|
* TConvProofGenerator for adding rewrite steps for witness introduction. |
33 |
|
* |
34 |
|
* The proof steps managed by this class are stored in a context-independent |
35 |
|
* manager, which matches how witness forms are managed in SkolemManager. |
36 |
|
*/ |
37 |
|
class WitnessFormGenerator : public ProofGenerator |
38 |
|
{ |
39 |
|
public: |
40 |
|
WitnessFormGenerator(ProofNodeManager* pnm); |
41 |
3768 |
~WitnessFormGenerator() {} |
42 |
|
/** |
43 |
|
* Get proof for, which expects an equality of the form t = toWitness(t). |
44 |
|
* This returns a proof based on the term conversion proof generator utility. |
45 |
|
* This proof may contain open assumptions of the form: |
46 |
|
* k = toWitness(k) |
47 |
|
* Each of these assumptions are included in the set getWitnessFormEqs() |
48 |
|
* below after returning this call. |
49 |
|
*/ |
50 |
|
std::shared_ptr<ProofNode> getProofFor(Node eq) override; |
51 |
|
/** Identify */ |
52 |
|
std::string identify() const override; |
53 |
|
/** |
54 |
|
* Does the rewrite require witness form conversion? |
55 |
|
* When calling this method, it should be the case that: |
56 |
|
* Rewriter::rewrite(toWitness(t)) == Rewriter::rewrite(toWitness(s)) |
57 |
|
* The rule MACRO_SR_PRED_TRANSFORM concludes t == s if the above holds. |
58 |
|
* This method returns false if: |
59 |
|
* Rewriter::rewrite(t) == Rewriter::rewrite(s) |
60 |
|
* which means that the proof of the above fact does not need to do |
61 |
|
* witness form conversion to prove conclusions of MACRO_SR_PRED_TRANSFORM. |
62 |
|
*/ |
63 |
|
bool requiresWitnessFormTransform(Node t, Node s) const; |
64 |
|
/** |
65 |
|
* Same as above, with s = true. This is intended for use with |
66 |
|
* MACRO_SR_PRED_INTRO. |
67 |
|
*/ |
68 |
|
bool requiresWitnessFormIntro(Node t) const; |
69 |
|
/** |
70 |
|
* Get witness form equalities. This returns a set of equalities of the form: |
71 |
|
* k = toWitness(k) |
72 |
|
* where k is a skolem, containing all rewrite steps used in calls to |
73 |
|
* getProofFor during the entire lifetime of this generator. |
74 |
|
*/ |
75 |
|
const std::unordered_set<Node>& getWitnessFormEqs() const; |
76 |
|
|
77 |
|
private: |
78 |
|
/** |
79 |
|
* Convert to witness form. This internally constructs rewrite steps that |
80 |
|
* suffice to show t = toWitness(t) using the term conversion proof generator |
81 |
|
* of this class (d_tcpg). |
82 |
|
*/ |
83 |
|
Node convertToWitnessForm(Node t); |
84 |
|
/** |
85 |
|
* Return a proof generator that can prove the given axiom exists. |
86 |
|
*/ |
87 |
|
ProofGenerator* convertExistsInternal(Node exists); |
88 |
|
/** The term conversion proof generator */ |
89 |
|
TConvProofGenerator d_tcpg; |
90 |
|
/** The nodes we have already added rewrite steps for in d_tcpg */ |
91 |
|
std::unordered_set<TNode> d_visited; |
92 |
|
/** The set of equalities added as proof steps */ |
93 |
|
std::unordered_set<Node> d_eqs; |
94 |
|
/** Lazy proof storing witness intro steps */ |
95 |
|
LazyCDProof d_wintroPf; |
96 |
|
/** CDProof for justifying purification existentials */ |
97 |
|
CDProof d_pskPf; |
98 |
|
}; |
99 |
|
|
100 |
|
} // namespace smt |
101 |
|
} // namespace cvc5 |
102 |
|
|
103 |
|
#endif |