diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-06 10:02:54 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-06 10:02:54 -0500 |
commit | 2d8889f935ca78ef4a5555f0e6bbed76dbc559d7 (patch) | |
tree | 2d83522cd3d1e0d711773a45de0d2be2952dbb7c /src/theory/trust_substitutions.h | |
parent | 6d663abe421c07976755c224180b1a1ee93442f6 (diff) |
(proof-new) Add interface for trusted substitution and update ppAssert (#5193)
The current work on proof-new involves proofs for preprocessing. The biggest issue currently is that our preprocessing passes do not track proofs for substitutions.
This adds a "trusted substitution" class with is a layer on substitution map. The proof aspect of this class is not yet implemented, this PR just adds its interface.
This also updates Theory::ppAssert to take a TrustSubstitutionMap instead of a SubstitutionMap, since eventually we will require proofs to be provided for substitutions that are added to this map.
Diffstat (limited to 'src/theory/trust_substitutions.h')
-rw-r--r-- | src/theory/trust_substitutions.h | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h new file mode 100644 index 000000000..0eacc50f5 --- /dev/null +++ b/src/theory/trust_substitutions.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file trust_substitutions.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Trust substitutions + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__TRUST_SUBSTITUTIONS_H +#define CVC4__THEORY__TRUST_SUBSTITUTIONS_H + +#include "context/context.h" +#include "expr/proof_node_manager.h" +#include "theory/substitutions.h" +#include "theory/trust_node.h" + +namespace CVC4 { +namespace theory { + +/** + * A layer on top of SubstitutionMap that tracks proofs. + */ +class TrustSubstitutionMap +{ + public: + TrustSubstitutionMap(context::Context* c, ProofNodeManager* pnm); + /** Gets a reference to the underlying substitution map */ + SubstitutionMap& get(); + /** + * Add substitution x -> t, where pg can provide a closed proof of (= x t) + * in the remainder of this user context. + */ + void addSubstitution(TNode x, TNode t, ProofGenerator* pg = nullptr); + /** + * Add substitution x -> t, which was derived from the proven field of + * trust node tn. In other words, (= x t) is the solved form of + * tn.getProven(). This method is a helper function for methods (e.g. + * ppAssert) that put literals into solved form. It should be the case + * that (= x t) and tn.getProven() can be shown equivalent by rewriting. + * + * This ensures that we add a substitution with a proof + * based on transforming the tn.getProven() to (= x t) if tn has a + * non-null proof generator; otherwise if tn has no proof generator + * we simply add the substitution. + */ + void addSubstitutionSolved(TNode x, TNode t, TrustNode tn); + /** + * Apply substitutions in this class to node n. Returns a trust node + * proving n = n*sigma, where the proof generator is provided by this class + * (when proofs are enabled). + */ + TrustNode apply(Node n, bool doRewrite = true); + + private: + /** Are proofs enabled? */ + bool isProofEnabled() const; + /** The substitution map */ + SubstitutionMap d_subs; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__TRUST_SUBSTITUTIONS_H */ |