summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/preprocessing/assertion_pipeline.cpp12
-rw-r--r--src/preprocessing/passes/apply_substs.cpp42
-rw-r--r--src/preprocessing/passes/ite_removal.cpp4
-rw-r--r--src/preprocessing/passes/ite_simp.cpp8
-rw-r--r--src/preprocessing/passes/miplib_trick.cpp10
-rw-r--r--src/preprocessing/passes/non_clausal_simp.cpp18
-rw-r--r--src/preprocessing/passes/quantifier_macros.cpp4
-rw-r--r--src/prop/minisat/core/Solver.cc3
-rw-r--r--src/prop/minisat/minisat.cpp4
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc3
-rw-r--r--src/prop/prop_engine.cpp2
-rw-r--r--src/prop/theory_proxy.cpp5
-rw-r--r--src/smt/assertions.cpp4
-rw-r--r--src/smt/process_assertions.cpp21
-rw-r--r--src/smt/set_defaults.cpp5
-rw-r--r--src/theory/quantifiers/instantiate.cpp2
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp2
17 files changed, 59 insertions, 90 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 3b304c8b9..4bc3323e5 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -96,19 +96,19 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
}
Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with "
<< n << std::endl;
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(n, d_nodes[i]);
- }
if (isProofEnabled())
{
d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
}
+ else if (options::unsatCores())
+ {
+ ProofManager::currentPM()->addDependence(n, d_nodes[i]);
+ }
d_nodes[i] = n;
}
void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn)
-{
+{
if (trn.isNull())
{
// null trust node denotes no change, nothing to do
@@ -201,7 +201,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
d_pppg->notifyNewAssert(newConjr, lcp);
}
}
- if (options::unsatCores())
+ if (options::unsatCores() && !isProofEnabled())
{
ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]);
}
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 92f31b0b8..c93895e79 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -33,32 +33,28 @@ ApplySubsts::ApplySubsts(PreprocessingPassContext* preprocContext)
PreprocessingPassResult ApplySubsts::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- if (!options::unsatCores())
- {
- Chat() << "applying substitutions..." << std::endl;
- Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): "
- << "applying substitutions" << std::endl;
- // TODO(#1255): Substitutions in incremental mode should be managed with a
- // proper data structure.
+ Chat() << "applying substitutions..." << std::endl;
+ Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): "
+ << "applying substitutions" << std::endl;
+ // TODO(#1255): Substitutions in incremental mode should be managed with a
+ // proper data structure.
- theory::TrustSubstitutionMap& tlsm =
- d_preprocContext->getTopLevelSubstitutions();
- unsigned size = assertionsToPreprocess->size();
- for (unsigned i = 0; i < size; ++i)
+ theory::TrustSubstitutionMap& tlsm =
+ d_preprocContext->getTopLevelSubstitutions();
+ unsigned size = assertionsToPreprocess->size();
+ for (unsigned i = 0; i < size; ++i)
+ {
+ if (assertionsToPreprocess->isSubstsIndex(i))
{
- if (assertionsToPreprocess->isSubstsIndex(i))
- {
- continue;
- }
- Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
- << std::endl;
- d_preprocContext->spendResource(
- ResourceManager::Resource::PreprocessStep);
- assertionsToPreprocess->replaceTrusted(
- i, tlsm.apply((*assertionsToPreprocess)[i]));
- Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i]
- << std::endl;
+ continue;
}
+ Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
+ << std::endl;
+ d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+ assertionsToPreprocess->replaceTrusted(
+ i, tlsm.apply((*assertionsToPreprocess)[i]));
+ Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i]
+ << std::endl;
}
return PreprocessingPassResult::NO_CONFLICT;
}
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index d2f053379..91af2a5b8 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -50,7 +50,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
// process
assertions->replaceTrusted(i, trn);
// rewritten assertion has a dependence on the node (old pf architecture)
- if (options::unsatCores())
+ if (options::unsatCores() && !options::proofNew())
{
ProofManager::currentPM()->addDependence(trn.getNode(), assertion);
}
@@ -61,7 +61,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
imap[newSkolems[j]] = assertions->size();
assertions->pushBackTrusted(newAsserts[j]);
// new assertions have a dependence on the node (old pf architecture)
- if (options::unsatCores())
+ if (options::unsatCores() && !options::proofNew())
{
ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
assertion);
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 5568dcad0..746bf33bd 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -114,13 +114,7 @@ ITESimp::Statistics::~Statistics()
bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
{
- // This pass does not support dependency tracking yet
- // (learns substitutions from all assertions so just
- // adding addDependence is not enough)
- if (options::unsatCores())
- {
- return true;
- }
+ Assert(!options::unsatCores());
bool result = true;
bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
if (simpDidALotOfWork)
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 4ed2aede9..0bb386697 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -180,6 +180,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
Assert(assertionsToPreprocess->getRealAssertionsEnd()
== assertionsToPreprocess->size());
Assert(!options::incrementalSolving());
+ Assert(!options::unsatCores());
context::Context fakeContext;
TheoryEngine* te = d_preprocContext->getTheoryEngine();
@@ -527,10 +528,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
Node n = Rewriter::rewrite(geq.andNode(leq));
assertionsToPreprocess->push_back(n);
- 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
@@ -599,11 +596,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
Debug("miplib") << " " << newAssertion << endl;
assertionsToPreprocess->push_back(newAssertion);
- 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();
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 7ace55c0a..656822299 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -66,7 +66,8 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
PreprocessingPassResult NonClausalSimp::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- Assert(!options::unsatCores());
+ Assert(!options::unsatCores() || isProofEnabled())
+ << "Unsat cores with non-clausal simp only supported with new proofs";
d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
@@ -111,13 +112,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
// If in conflict, just return false
Trace("non-clausal-simplify")
<< "conflict in non-clausal propagation" << std::endl;
- Assert(!options::unsatCores());
assertionsToPreprocess->clear();
assertionsToPreprocess->pushBackTrusted(conf);
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(conf.getNode(), Node::null());
- }
propagator->setNeedsFinish(true);
return PreprocessingPassResult::CONFLICT;
}
@@ -177,14 +173,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
// If the learned literal simplifies to false, we're in conflict
Trace("non-clausal-simplify")
<< "conflict with " << learned_literals[i].getNode() << std::endl;
- Assert(!options::unsatCores());
assertionsToPreprocess->clear();
Node n = NodeManager::currentNM()->mkConst<bool>(false);
assertionsToPreprocess->push_back(n, false, false, d_llpg.get());
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(n, Node::null());
- }
propagator->setNeedsFinish(true);
return PreprocessingPassResult::CONFLICT;
}
@@ -216,14 +207,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
// If in conflict, we return false
Trace("non-clausal-simplify")
<< "conflict while solving " << learnedLiteral << std::endl;
- Assert(!options::unsatCores());
assertionsToPreprocess->clear();
Node n = NodeManager::currentNM()->mkConst<bool>(false);
assertionsToPreprocess->push_back(n);
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(n, Node::null());
- }
propagator->setNeedsFinish(true);
return PreprocessingPassResult::CONFLICT;
}
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 604f8719c..028bfede5 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -80,7 +80,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
for( int i=0; i<(int)assertions.size(); i++ ){
Trace("macros-debug") << " process assertion " << assertions[i] << std::endl;
if( processAssertion( assertions[i] ) ){
- if (options::unsatCores()
+ if (options::unsatCores() && !options::proofNew()
&& std::find(macro_assertions.begin(),
macro_assertions.end(),
assertions[i])
@@ -106,7 +106,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
// is an over-approximation. a more fine-grained unsat core
// computation would require caching dependencies for each subterm of
// the formula, which is expensive.
- if (options::unsatCores())
+ if (options::unsatCores() && !options::proofNew())
{
ProofManager::currentPM()->addDependence(curr, assertions[i]);
for (unsigned j = 0; j < macro_assertions.size(); j++)
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 12246be41..ab3b0cfe7 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -227,8 +227,7 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy,
d_pfManager.reset(
new SatProofManager(this, proxy->getCnfStream(), userContext, pnm));
}
-
- if (options::unsatCores() && !isProofEnabled())
+ else if (options::unsatCores())
{
ProofManager::currentPM()->initSatProof(this);
}
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 8af73140e..c48df4998 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -159,7 +159,9 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
return ClauseIdUndef;
}
d_minisat->addClause(minisat_clause, removable, clause_id);
- Assert(!CVC4::options::unsatCores() || clause_id != ClauseIdError);
+ // FIXME: to be deleted when we kill old proof code for unsat cores
+ Assert(!options::unsatCores() || options::proofNew()
+ || clause_id != ClauseIdError);
return clause_id;
}
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 5c8922360..4649a67aa 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -58,7 +58,8 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy,
subsumption_lim(opt_subsumption_lim),
simp_garbage_frac(opt_simp_garbage_frac),
use_asymm(opt_use_asymm),
- use_rcheck(opt_use_rcheck),
+ // make sure this is not enabled if unsat cores or proofs are on
+ use_rcheck(opt_use_rcheck && !options::unsatCores() && !pnm),
use_elim(options::minisatUseElim() && !enableIncremental),
merges(0),
asymm_lits(0),
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index eeb879a2b..81fadb709 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -117,7 +117,7 @@ PropEngine::PropEngine(TheoryEngine* te,
d_ppm.reset(
new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get()));
}
- if (options::unsatCores())
+ else if (options::unsatCores())
{
ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
}
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 23405675a..7559e4015 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -83,11 +83,12 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
{
d_propEngine->getProofCnfStream()->convertPropagation(tte);
}
- if (options::unsatCores())
+ else if (options::unsatCores())
{
ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
}
- Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
+ Debug("prop-explain") << "explainPropagation() => " << theoryExplanation
+ << std::endl;
explanation.push_back(l);
if (theoryExplanation.getKind() == kind::AND)
{
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index ab2c9ae5d..6776b06e2 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -172,8 +172,8 @@ void Assertions::addFormula(
}
}
- // Give it to proof manager
- if (options::unsatCores())
+ // Give it to the old proof manager
+ if (options::unsatCores() && !isProofEnabled())
{
if (inInput)
{ // n is an input assertion
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 7fd1db797..5faa2a66c 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -207,10 +207,7 @@ bool ProcessAssertions::apply(Assertions& as)
// Since this pass is not robust for the information tracking necessary for
// unsat cores, it's only applied if we are not doing unsat core computation
- if (!options::unsatCores())
- {
- d_passes["apply-substs"]->apply(&assertions);
- }
+ d_passes["apply-substs"]->apply(&assertions);
// Assertions MUST BE guaranteed to be rewritten by this point
d_passes["rewrite"]->apply(&assertions);
@@ -361,15 +358,12 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
if (options::simplificationMode() != options::SimplificationMode::NONE)
{
- if (!options::unsatCores())
+ // Perform non-clausal simplification
+ PreprocessingPassResult res =
+ d_passes["non-clausal-simp"]->apply(&assertions);
+ if (res == PreprocessingPassResult::CONFLICT)
{
- // Perform non-clausal simplification
- PreprocessingPassResult res =
- d_passes["non-clausal-simp"]->apply(&assertions);
- if (res == PreprocessingPassResult::CONFLICT)
- {
- return false;
- }
+ return false;
}
// We piggy-back off of the BackEdgesMap in the CircuitPropagator to
@@ -415,8 +409,7 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
}
if (options::repeatSimp()
- && options::simplificationMode() != options::SimplificationMode::NONE
- && !options::unsatCores())
+ && options::simplificationMode() != options::SimplificationMode::NONE)
{
PreprocessingPassResult res =
d_passes["non-clausal-simp"]->apply(&assertions);
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index a781bc44b..3c70d8a57 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -484,6 +484,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
{
throw OptionException("bitblast-aig not supported with unsat cores");
}
+
+ if (options::doITESimp())
+ {
+ throw OptionException("ITE simp not supported with unsat cores");
+ }
}
else
{
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index fb622452e..7592f22c7 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -683,7 +683,7 @@ void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas)
{
// only if unsat core available
- if (options::unsatCores())
+ if (options::unsatCores() && !isProofEnabled())
{
if (!ProofManager::currentPM()->unsatCoreAvailable())
{
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 81cca34af..1a46b26f5 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -1026,7 +1026,7 @@ void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){
: NodeManager::currentNM()->mkNode(kind::AND, asserts);
if( res!=vec_node[i] ){
res = Rewriter::rewrite( res );
- if (options::unsatCores())
+ if (options::unsatCores() && !options::proofNew())
{
ProofManager::currentPM()->addDependence(res, vec_node[i]);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback