diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/trust_substitutions.cpp | 17 | ||||
-rw-r--r-- | src/theory/trust_substitutions.h | 2 |
2 files changed, 16 insertions, 3 deletions
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index 7934231b9..c73265095 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -162,8 +162,12 @@ TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite) return TrustNode::mkTrustRewrite(n, ns, nullptr); } Node eq = n.eqNode(ns); - // remember the index - d_eqtIndex[eq] = d_tsubs.size(); + // If we haven't already stored an index, remember the index. Otherwise, a + // (possibly shorter) prefix of the substitution already suffices to show eq + if (d_eqtIndex.find(eq) == d_eqtIndex.end()) + { + d_eqtIndex[eq] = d_tsubs.size(); + } // this class will provide a proof if asked return TrustNode::mkTrustRewrite(n, ns, this); } @@ -194,11 +198,16 @@ std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq) { return d_subsPg->getProofFor(eq); } + Trace("trust-subs-pf") << "getProofFor " << eq << std::endl; + AlwaysAssert(d_proving.find(eq) == d_proving.end()) + << "Repeat getProofFor in TrustSubstitutionMap " << eq; + d_proving.insert(eq); NodeUIntMap::iterator it = d_eqtIndex.find(eq); Assert(it != d_eqtIndex.end()); Trace("trust-subs-pf") << "TrustSubstitutionMap::getProofFor, # assumptions= " << it->second << std::endl; Node cs = getSubstitution(it->second); + Trace("trust-subs-pf") << "getProofFor substitution is " << cs << std::endl; Assert(eq != cs); std::vector<Node> pfChildren; if (!cs.isConst()) @@ -252,7 +261,9 @@ std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq) d_applyPg->addSteps(*d_tspb.get()); d_tspb->clear(); Trace("trust-subs-pf") << "...finish, make proof" << std::endl; - return d_applyPg->getProofFor(eq); + std::shared_ptr<ProofNode> ret = d_applyPg->getProofFor(eq); + d_proving.erase(eq); + return ret; } std::string TrustSubstitutionMap::identify() const { return d_name; } diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index 2a6997d1d..cc08c870d 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -143,6 +143,8 @@ class TrustSubstitutionMap : public ProofGenerator * two substitutions but not the third when asked to prove this equality. */ NodeUIntMap d_eqtIndex; + /** Debugging, catches potential for infinite loops */ + std::unordered_set<Node> d_proving; }; } // namespace theory |