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/preprocessing/passes/miplib_trick.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/preprocessing/passes/miplib_trick.cpp')
| -rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 4c91297a1..3d7fd120a 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -23,6 +23,7 @@ #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 { @@ -187,6 +188,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( const booleans::CircuitPropagator::BackEdgesMap& backEdges = propagator->getBackEdges(); unordered_set<unsigned long> removeAssertions; + SubstitutionMap& top_level_substs = d_preprocContext->getTopLevelSubstitutions(); @@ -519,6 +521,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( 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); @@ -526,14 +530,15 @@ PreprocessingPassResult MipLibTrick::applyInternal( { 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()) |