diff options
Diffstat (limited to 'src/preprocessing/passes/miplib_trick.cpp')
| -rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index f64fce118..f55665bc5 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -5,7 +5,7 @@ ** Mathias Preiner, Tim King, Morgan Deters ** 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. + ** 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 ** @@ -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,8 +188,10 @@ PreprocessingPassResult MipLibTrick::applyInternal( const booleans::CircuitPropagator::BackEdgesMap& backEdges = propagator->getBackEdges(); unordered_set<unsigned long> removeAssertions; - SubstitutionMap& top_level_substs = + + theory::TrustSubstitutionMap& tlsm = d_preprocContext->getTopLevelSubstitutions(); + SubstitutionMap& top_level_substs = tlsm.get(); NodeManager* nm = NodeManager::currentNM(); Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); @@ -519,19 +522,24 @@ 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); - PROOF(ProofManager::currentPM()->addDependence(n, Node::null())); - - SubstitutionMap nullMap(&fakeContext); + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(n, Node::null()); + } + 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()) @@ -591,9 +599,11 @@ PreprocessingPassResult MipLibTrick::applyInternal( Debug("miplib") << " " << newAssertion << endl; assertionsToPreprocess->push_back(newAssertion); - PROOF(ProofManager::currentPM()->addDependence(newAssertion, - Node::null())); - + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(newAssertion, + Node::null()); + } Debug("miplib") << " assertions to remove: " << endl; for (vector<TNode>::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); |