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/context.h"
21 #include "expr/proof_node_manager.h"
22 #include "theory/substitutions.h"
23 #include "theory/trust_node.h"
29 * A layer on top of SubstitutionMap that tracks proofs.
31 class TrustSubstitutionMap
34 TrustSubstitutionMap(context::Context
* c
, ProofNodeManager
* pnm
);
35 /** Gets a reference to the underlying substitution map */
36 SubstitutionMap
& get();
38 * Add substitution x -> t, where pg can provide a closed proof of (= x t)
39 * in the remainder of this user context.
41 void addSubstitution(TNode x
, TNode t
, ProofGenerator
* pg
= nullptr);
43 * Add substitution x -> t, which was derived from the proven field of
44 * trust node tn. In other words, (= x t) is the solved form of
45 * tn.getProven(). This method is a helper function for methods (e.g.
46 * ppAssert) that put literals into solved form. It should be the case
47 * that (= x t) and tn.getProven() can be shown equivalent by rewriting.
49 * This ensures that we add a substitution with a proof
50 * based on transforming the tn.getProven() to (= x t) if tn has a
51 * non-null proof generator; otherwise if tn has no proof generator
52 * we simply add the substitution.
54 void addSubstitutionSolved(TNode x
, TNode t
, TrustNode tn
);
56 * Apply substitutions in this class to node n. Returns a trust node
57 * proving n = n*sigma, where the proof generator is provided by this class
58 * (when proofs are enabled).
60 TrustNode
apply(Node n
, bool doRewrite
= true);
63 /** Are proofs enabled? */
64 bool isProofEnabled() const;
65 /** The substitution map */
66 SubstitutionMap d_subs
;
72 #endif /* CVC4__THEORY__TRUST_SUBSTITUTIONS_H */