diff options
| author | Andres Notzli <andres.noetzli@gmail.com> | 2016-08-09 19:24:28 -0700 |
|---|---|---|
| committer | Andres Notzli <andres.noetzli@gmail.com> | 2016-08-11 23:28:15 -0700 |
| commit | 1dddbc74f01619928263b42bf4b4ef6a6ccb2f28 (patch) | |
| tree | 9fed432f9e9bcb81dd3b015326d7fa7f73c197f1 /src/smt/smt_engine.cpp | |
| parent | 841acca266b026c9c1d20cb1adf0e73da15a0c10 (diff) | |
Add support for fewer preprocessing holes
This commit adds support for the --fewer-preprocessing-holes flag. This
flag changes the preprocessing part in proofs in two ways: it (1)
removes assertions that are just restating inputs and uses the inputs
directly instead and it (2) changes the form of the preprocessed
assertions to contain the input that they originate from.
The code in this commit is mostly taken from the proofs branch in Guy's
fork.
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b76b90e84..d7b7f9c3e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -57,6 +57,7 @@ #include "options/open_ostream.h" #include "options/option_exception.h" #include "options/printer_options.h" +#include "options/proof_options.h" #include "options/prop_options.h" #include "options/quantifiers_options.h" #include "options/set_language.h" @@ -92,9 +93,9 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/sep/theory_sep.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" -#include "theory/sep/theory_sep.h" #include "theory/substitutions.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" @@ -4283,8 +4284,10 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) PROOF( if( inInput ){ // n is an input assertion - if (inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores()) + if (inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) { + ProofManager::currentPM()->addCoreAssertion(n.toExpr()); + } }else{ // n is the result of an unknown preprocessing step, add it to dependency map to null ProofManager::currentPM()->addDependence(n, Node::null()); |