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.
theory/theory_test_utils.h
theory/trust_node.cpp
theory/trust_node.h
+ theory/trust_substitutions.cpp
+ theory/trust_substitutions.h
theory/type_enumerator.h
theory/type_set.cpp
theory/type_set.h
#include "smt_util/boolean_simplification.h"
#include "theory/booleans/circuit_propagator.h"
#include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
namespace CVC4 {
namespace preprocessing {
const booleans::CircuitPropagator::BackEdgesMap& backEdges =
propagator->getBackEdges();
unordered_set<unsigned long> removeAssertions;
+
SubstitutionMap& top_level_substs =
d_preprocContext->getTopLevelSubstitutions();
NodeManager::SKOLEM_EXACT_NAME);
Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero));
Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
+ TrustNode tgeq = TrustNode::mkTrustLemma(geq, nullptr);
+ TrustNode tleq = TrustNode::mkTrustLemma(leq, nullptr);
Node n = Rewriter::rewrite(geq.andNode(leq));
assertionsToPreprocess->push_back(n);
{
ProofManager::currentPM()->addDependence(n, Node::null());
}
- SubstitutionMap nullMap(&fakeContext);
+ TrustSubstitutionMap tnullMap(&fakeContext, nullptr);
+ CVC4_UNUSED SubstitutionMap& nullMap = tnullMap.get();
Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
- status = te->solve(geq, nullMap);
+ status = te->solve(tgeq, tnullMap);
Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED)
<< "unexpected solution from arith's ppAssert()";
Assert(nullMap.empty())
<< "unexpected substitution from arith's ppAssert()";
- status = te->solve(leq, nullMap);
+ status = te->solve(tleq, tnullMap);
Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED)
<< "unexpected solution from arith's ppAssert()";
Assert(nullMap.empty())
#include "context/cdo.h"
#include "smt/smt_statistics_registry.h"
#include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
using namespace CVC4;
using namespace CVC4::theory;
SubstitutionMap& top_level_substs =
d_preprocContext->getTopLevelSubstitutions();
SubstitutionMap constantPropagations(d_preprocContext->getUserContext());
- SubstitutionMap newSubstitutions(d_preprocContext->getUserContext());
+ TrustSubstitutionMap tnewSubstituions(d_preprocContext->getUserContext(),
+ nullptr);
+ SubstitutionMap& newSubstitutions = tnewSubstituions.get();
SubstitutionMap::iterator pos;
size_t j = 0;
std::vector<Node>& learned_literals = propagator->getLearnedLiterals();
// Solve it with the corresponding theory, possibly adding new
// substitutions to newSubstitutions
Trace("non-clausal-simplify") << "solving " << learnedLiteral << std::endl;
-
+ TrustNode tlearnedLiteral =
+ TrustNode::mkTrustLemma(learnedLiteral, nullptr);
Theory::PPAssertStatus solveStatus =
- d_preprocContext->getTheoryEngine()->solve(learnedLiteral,
- newSubstitutions);
+ d_preprocContext->getTheoryEngine()->solve(tlearnedLiteral,
+ tnewSubstituions);
switch (solveStatus)
{
return d_arithPreproc.eliminate(n);
}
-Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
- return d_internal->ppAssert(in, outSubstitutions);
+Theory::PPAssertStatus TheoryArith::ppAssert(
+ TrustNode tin, TrustSubstitutionMap& outSubstitutions)
+{
+ return d_internal->ppAssert(tin, outSubstitutions);
}
void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
void presolve() override;
void notifyRestart() override;
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+ PPAssertStatus ppAssert(TrustNode tin,
+ TrustSubstitutionMap& outSubstitutions) override;
TrustNode ppRewrite(TNode atom) override;
void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
}
}
-Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheoryArithPrivate::ppAssert(
+ TrustNode tin, TrustSubstitutionMap& outSubstitutions)
+{
TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
+ TNode in = tin.getNode();
Debug("simplify") << "TheoryArithPrivate::solve(" << in << ")" << endl;
Debug("simplify") << "TheoryArithPrivate::solve(): substitution "
<< minVar << " |-> " << elim << endl;
- outSubstitutions.addSubstitution(minVar, elim);
+ outSubstitutions.addSubstitutionSolved(minVar, elim, tin);
return Theory::PP_ASSERT_STATUS_SOLVED;
}
else
void presolve();
void notifyRestart();
- Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ Theory::PPAssertStatus ppAssert(TrustNode tin,
+ TrustSubstitutionMap& outSubstitutions);
void ppStaticLearn(TNode in, NodeBuilder<>& learned);
std::string identify() const { return std::string("TheoryArith"); }
return TrustNode::null();
}
-
-Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheoryArrays::ppAssert(
+ TrustNode tin, TrustSubstitutionMap& outSubstitutions)
+{
+ TNode in = tin.getNode();
switch(in.getKind()) {
case kind::EQUAL:
{
d_ppEqualityEngine.assertEquality(in, true, in);
if (in[0].isVar() && isLegalElimination(in[0], in[1]))
{
- outSubstitutions.addSubstitution(in[0], in[1]);
+ outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
return PP_ASSERT_STATUS_SOLVED;
}
if (in[1].isVar() && isLegalElimination(in[1], in[0]))
{
- outSubstitutions.addSubstitution(in[1], in[0]);
+ outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
return PP_ASSERT_STATUS_SOLVED;
}
break;
InferenceManager d_im;
public:
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+ PPAssertStatus ppAssert(TrustNode tin,
+ TrustSubstitutionMap& outSubstitutions) override;
TrustNode ppRewrite(TNode atom) override;
/////////////////////////////////////////////////////////////////////////////
}
}
-Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
-
+Theory::PPAssertStatus TheoryBool::ppAssert(
+ TrustNode tin, TrustSubstitutionMap& outSubstitutions)
+{
+ TNode in = tin.getNode();
if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) {
// If we get a false literal, we're in conflict
return PP_ASSERT_STATUS_CONFLICT;
if (in.getKind() == kind::NOT) {
if (in[0].isVar())
{
- outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false));
+ outSubstitutions.addSubstitutionSolved(
+ in[0], NodeManager::currentNM()->mkConst<bool>(false), tin);
return PP_ASSERT_STATUS_SOLVED;
}
} else {
if (in.isVar())
{
- outSubstitutions.addSubstitution(in, NodeManager::currentNM()->mkConst<bool>(true));
+ outSubstitutions.addSubstitutionSolved(
+ in, NodeManager::currentNM()->mkConst<bool>(true), tin);
return PP_ASSERT_STATUS_SOLVED;
}
}
- return Theory::ppAssert(in, outSubstitutions);
+ return Theory::ppAssert(tin, outSubstitutions);
}
}/* CVC4::theory::booleans namespace */
TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+ PPAssertStatus ppAssert(TrustNode tin,
+ TrustSubstitutionMap& outSubstitutions) override;
std::string identify() const override { return std::string("TheoryBool"); }
virtual std::string identify() const = 0;
virtual Theory::PPAssertStatus ppAssert(
- TNode in, SubstitutionMap& outSubstitutions) = 0;
+ TrustNode in, TrustSubstitutionMap& outSubstitutions) = 0;
virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
}
}
-Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in,
- SubstitutionMap& outSubstitutions)
+Theory::PPAssertStatus BVSolverLazy::ppAssert(
+ TrustNode tin, TrustSubstitutionMap& outSubstitutions)
{
+ TNode in = tin.getNode();
switch (in.getKind())
{
case kind::EQUAL:
if (in[0].isVar() && d_bv.isLegalElimination(in[0], in[1]))
{
++(d_statistics.d_solveSubstitutions);
- outSubstitutions.addSubstitution(in[0], in[1]);
+ outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
return Theory::PP_ASSERT_STATUS_SOLVED;
}
if (in[1].isVar() && d_bv.isLegalElimination(in[1], in[0]))
{
++(d_statistics.d_solveSubstitutions);
- outSubstitutions.addSubstitution(in[1], in[0]);
+ outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
return Theory::PP_ASSERT_STATUS_SOLVED;
}
Node node = Rewriter::rewrite(in);
Assert(utils::getSize(concat) == utils::getSize(extract[0]));
if (d_bv.isLegalElimination(extract[0], concat))
{
- outSubstitutions.addSubstitution(extract[0], concat);
+ outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
return Theory::PP_ASSERT_STATUS_SOLVED;
}
}
std::string identify() const override { return std::string("BVSolverLazy"); }
- Theory::PPAssertStatus ppAssert(TNode in,
- SubstitutionMap& outSubstitutions) override;
+ Theory::PPAssertStatus ppAssert(
+ TrustNode tin, TrustSubstitutionMap& outSubstitutions) override;
TrustNode ppRewrite(TNode t) override;
std::string identify() const override { return "BVSolverSimple"; };
- Theory::PPAssertStatus ppAssert(TNode in,
- SubstitutionMap& outSubstitutions) override
+ Theory::PPAssertStatus ppAssert(
+ TrustNode in, TrustSubstitutionMap& outSubstitutions) override
{
return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
}
d_ufRemByZero(),
d_rewriter(),
d_state(c, u, valuation),
- d_inferMgr(*this, d_state, pnm)
+ d_inferMgr(*this, d_state, nullptr)
{
switch (options::bvSolver())
{
void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
-Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
- SubstitutionMap& outSubstitutions)
+Theory::PPAssertStatus TheoryBV::ppAssert(
+ TrustNode tin, TrustSubstitutionMap& outSubstitutions)
{
- return d_internal->ppAssert(in, outSubstitutions);
+ return d_internal->ppAssert(tin, outSubstitutions);
}
TrustNode TheoryBV::ppRewrite(TNode t) { return d_internal->ppRewrite(t); }
std::string identify() const override { return std::string("TheoryBV"); }
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+ PPAssertStatus ppAssert(TrustNode in,
+ TrustSubstitutionMap& outSubstitutions) override;
TrustNode ppRewrite(TNode t) override;
d_lemmas_produced_c(u),
d_bounds_init(false),
d_state(c, u, valuation),
- d_im(*this, d_state, pnm),
+ d_im(*this, d_state, nullptr),
d_notify(*this),
d_reduce(u),
d_spatial_assertions(c)
}
}
-/////////////////////////////////////////////////////////////////////////////
-// PREPROCESSING
-/////////////////////////////////////////////////////////////////////////////
-
-
-Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
-
- return PP_ASSERT_STATUS_UNSOLVED;
-}
-
/////////////////////////////////////////////////////////////////////////////
// T-PROPAGATION / REGISTRATION
/////////////////////////////////////////////////////////////////////////////
public:
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
-
void ppNotifyAssertions(const std::vector<Node>& assertions) override;
/////////////////////////////////////////////////////////////////////////////
// T-PROPAGATION / REGISTRATION
: Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
d_skCache(),
d_state(c, u, valuation, d_skCache),
- d_im(*this, d_state, pnm),
+ d_im(*this, d_state, nullptr),
d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache)),
d_notify(*d_internal.get(), d_im)
{
return d_internal->expandDefinition(n);
}
-Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheorySets::ppAssert(
+ TrustNode tin, TrustSubstitutionMap& outSubstitutions)
+{
+ TNode in = tin.getNode();
Debug("sets-proc") << "ppAssert : " << in << std::endl;
Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
// regress0/sets/pre-proc-univ.smt2
if (!in[0].getType().isSet() || !options::setsExt())
{
- outSubstitutions.addSubstitution(in[0], in[1]);
+ outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
status = Theory::PP_ASSERT_STATUS_SOLVED;
}
}
{
if (!in[0].getType().isSet() || !options::setsExt())
{
- outSubstitutions.addSubstitution(in[1], in[0]);
+ outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
status = Theory::PP_ASSERT_STATUS_SOLVED;
}
}
std::string identify() const override { return "THEORY_SETS"; }
void preRegisterTerm(TNode node) override;
TrustNode expandDefinition(Node n) override;
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+ PPAssertStatus ppAssert(TrustNode tin,
+ TrustSubstitutionMap& outSubstitutions) override;
void presolve() override;
bool isEntailed(Node n, bool pol);
return true;
}
-Theory::PPAssertStatus Theory::ppAssert(TNode in,
- SubstitutionMap& outSubstitutions)
+Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
+ TrustSubstitutionMap& outSubstitutions)
{
+ TNode in = tin.getNode();
if (in.getKind() == kind::EQUAL)
{
// (and (= x t) phi) can be replaced by phi[x/t] if
#include "theory/theory_rewriter.h"
#include "theory/theory_state.h"
#include "theory/trust_node.h"
+#include "theory/trust_substitutions.h"
#include "theory/valuation.h"
#include "util/statistics_registry.h"
};
/**
- * Given a literal, add the solved substitutions to the map, if any.
- * The method should return true if the literal can be safely removed.
+ * Given a literal and its proof generator (encapsulated by trust node tin),
+ * add the solved substitutions to the map, if any. The method should return
+ * true if the literal can be safely removed from the input problem.
+ *
+ * Note that tin has trude node kind LEMMA. Its proof generator should be
+ * take into account when adding a substitution to outSubstitutions when
+ * proofs are enabled.
*/
- virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ virtual PPAssertStatus ppAssert(TrustNode tin,
+ TrustSubstitutionMap& outSubstitutions);
/**
* Given an atom of the theory coming from the input formula, this
d_tpp.clearCache();
}
-theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
+theory::Theory::PPAssertStatus TheoryEngine::solve(
+ TrustNode tliteral, TrustSubstitutionMap& substitutionOut)
+{
// Reset the interrupt flag
d_interrupted = false;
+ TNode literal = tliteral.getNode();
TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
throw LogicException(ss.str());
}
- Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut);
+ Theory::PPAssertStatus solveStatus =
+ theoryOf(atom)->ppAssert(tliteral, substitutionOut);
Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
return solveStatus;
}
void shutdown();
/**
- * Solve the given literal with a theory that owns it.
+ * Solve the given literal with a theory that owns it. The proof of tliteral
+ * is carried in the trust node. The proof added to substitutionOut should
+ * take this proof into account (when proofs are enabled).
*/
- theory::Theory::PPAssertStatus solve(TNode literal,
- theory::SubstitutionMap& substitutionOut);
+ theory::Theory::PPAssertStatus solve(
+ theory::TrustNode tliteral,
+ theory::TrustSubstitutionMap& substitutionOut);
/**
* Preregister a Theory atom with the responsible theory (or
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
projects / cvc5.git / commitdiff