diff options
Diffstat (limited to 'src/theory/quantifiers/instantiate.cpp')
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 32 |
1 files changed, 8 insertions, 24 deletions
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 77b61e9dd..04b6e0dda 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -16,6 +16,8 @@ #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" +#include "options/smt_options.h" +#include "proof/proof_manager.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/first_order_model.h" @@ -577,18 +579,21 @@ void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas) { // only if unsat core available - if (options::proof()) + if (options::unsatCores()) { if (!ProofManager::currentPM()->unsatCoreAvailable()) { return false; } } + else + { + return false; + } Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl; - ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, - active_lemmas); + ProofManager::currentPM()->getLemmasInUnsatCore(active_lemmas); if (Trace.isOn("inst-unsat-core")) { Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: " @@ -602,27 +607,6 @@ bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas) return true; } -bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas, - std::map<Node, Node>& weak_imp) -{ - if (getUnsatCoreLemmas(active_lemmas)) - { - for (unsigned i = 0, size = active_lemmas.size(); i < size; ++i) - { - Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore( - active_lemmas[i]); - if (n != active_lemmas[i]) - { - Trace("inst-unsat-core") << " weaken : " << active_lemmas[i] << " -> " - << n << std::endl; - } - weak_imp[active_lemmas[i]] = n; - } - return true; - } - return false; -} - void Instantiate::getInstantiationTermVectors( Node q, std::vector<std::vector<Node> >& tvecs) { |