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.cpp | |
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.cpp')
-rw-r--r-- | src/theory/trust_substitutions.cpp | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp new file mode 100644 index 000000000..de8fc2ceb --- /dev/null +++ b/src/theory/trust_substitutions.cpp @@ -0,0 +1,60 @@ +/********************* */ +/*! \file trust_substitutions.cpp + ** \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 "theory/trust_substitutions.h" + +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { + +TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c, + ProofNodeManager* pnm) + : d_subs(c) +{ +} + +void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg) +{ + d_subs.addSubstitution(x, t); +} + +TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite) +{ + Node ns = d_subs.apply(n); + if (doRewrite) + { + ns = Rewriter::rewrite(ns); + } + return TrustNode::mkTrustRewrite(n, ns, nullptr); +} + +void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn) +{ + if (!isProofEnabled() || tn.getGenerator() == nullptr) + { + // no generator or not proof enabled, nothing to do + addSubstitution(x, t, nullptr); + return; + } + // NOTE: can try to transform tn.getProven() to (= x t) here + addSubstitution(x, t, nullptr); +} + +SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; } + +bool TrustSubstitutionMap::isProofEnabled() const { return false; } + +} // namespace theory +} // namespace CVC4 |