1 /********************* */
2 /*! \file trust_substitutions.h
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Trust substitutions
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__TRUST_SUBSTITUTIONS_H
18 #define CVC4__THEORY__TRUST_SUBSTITUTIONS_H
20 #include "context/cdlist.h"
21 #include "context/context.h"
22 #include "expr/lazy_proof.h"
23 #include "expr/lazy_proof_set.h"
24 #include "expr/proof_node_manager.h"
25 #include "expr/term_conversion_proof_generator.h"
26 #include "theory/eager_proof_generator.h"
27 #include "theory/substitutions.h"
28 #include "theory/theory_proof_step_buffer.h"
29 #include "theory/trust_node.h"
35 * A layer on top of SubstitutionMap that tracks proofs.
37 class TrustSubstitutionMap
40 TrustSubstitutionMap(context::Context
* c
,
41 ProofNodeManager
* pnm
,
42 std::string name
= "TrustSubstitutionMap",
43 PfRule trustId
= PfRule::TRUST_SUBS_MAP
,
44 MethodId ids
= MethodId::SB_DEFAULT
);
45 /** Gets a reference to the underlying substitution map */
46 SubstitutionMap
& get();
48 * Add substitution x -> t, where pg can provide a closed proof of (= x t)
49 * in the remainder of this user context.
51 void addSubstitution(TNode x
, TNode t
, ProofGenerator
* pg
= nullptr);
53 * Add substitution x -> t from a single proof step with rule id, no children
56 void addSubstitution(TNode x
,
59 const std::vector
<Node
>& args
);
61 * Add substitution x -> t, which was derived from the proven field of
62 * trust node tn. In other words, (= x t) is the solved form of
63 * tn.getProven(). This method is a helper function for methods (e.g.
64 * ppAssert) that put literals into solved form. It should be the case
65 * that (= x t) and tn.getProven() can be shown equivalent by rewriting.
67 * This ensures that we add a substitution with a proof
68 * based on transforming the tn.getProven() to (= x t) if tn has a
69 * non-null proof generator; otherwise if tn has no proof generator
70 * we simply add the substitution.
72 void addSubstitutionSolved(TNode x
, TNode t
, TrustNode tn
);
74 * Add substitutions from trust substitution map t. This adds all
75 * substitutions from the map t and carries over its information about proofs.
77 void addSubstitutions(TrustSubstitutionMap
& t
);
79 * Apply substitutions in this class to node n. Returns a trust node
80 * proving n = n*sigma, where the proof generator is provided by this class
81 * (when proofs are enabled).
83 TrustNode
apply(Node n
, bool doRewrite
= true);
86 /** Are proofs enabled? */
87 bool isProofEnabled() const;
89 * Get current substitution. This returns a node of the form:
90 * (and (= x1 t1) ... (= xn tn))
91 * where (x1, t1) ... (xn, tn) have been registered via addSubstitution above.
92 * Moreover, it ensures that d_subsPg has a proof of the returned value.
94 Node
getCurrentSubstitution();
95 /** The substitution map */
96 SubstitutionMap d_subs
;
97 /** The proof node manager */
98 ProofNodeManager
* d_pnm
;
99 /** A context-dependent list of trust nodes */
100 context::CDList
<TrustNode
> d_tsubs
;
101 /** Theory proof step buffer */
102 std::unique_ptr
<TheoryProofStepBuffer
> d_tspb
;
103 /** A lazy proof for substitution steps */
104 std::unique_ptr
<LazyCDProof
> d_subsPg
;
105 /** A lazy proof for apply steps */
106 std::unique_ptr
<LazyCDProof
> d_applyPg
;
108 * A context-dependent list of LazyCDProof, allocated for internal steps.
110 LazyCDProofSet d_helperPf
;
112 * The formula corresponding to the current substitution. This is of the form
113 * (and (= x1 t1) ... (= xn tn))
114 * when the substitution map contains { x1 -> t1, ... xn -> tn }. This field
115 * is updated on demand. When this class applies a substitution to a node,
116 * this formula is computed and recorded as the premise of a
117 * MACRO_SR_EQ_INTRO step.
119 context::CDO
<Node
> d_currentSubs
;
120 /** Name for debugging */
123 * The placeholder trusted PfRule identifier for calls to addSubstitution
124 * that are not given proof generators.
127 /** The method id for which form of substitution to apply */
131 } // namespace theory
134 #endif /* CVC4__THEORY__TRUST_SUBSTITUTIONS_H */