From 5ef950054212a5fb9759c9137888f95bcadb05fd Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 23 Dec 2020 17:40:48 -0300 Subject: [PATCH] [proof-new] Adding a manager for the new unsat cores (#5723) Based on proof nodes of refutations. --- src/CMakeLists.txt | 2 + src/smt/unsat_core_manager.cpp | 92 ++++++++++++++++++++++++++++++++++ src/smt/unsat_core_manager.h | 73 +++++++++++++++++++++++++++ 3 files changed, 167 insertions(+) create mode 100644 src/smt/unsat_core_manager.cpp create mode 100644 src/smt/unsat_core_manager.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0fb505823..152d2e4ff 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -274,6 +274,8 @@ libcvc4_add_sources( smt/sygus_solver.h smt/term_formula_removal.cpp smt/term_formula_removal.h + smt/unsat_core_manager.cpp + smt/unsat_core_manager.h smt/update_ostream.h smt/witness_form.cpp smt/witness_form.h diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp new file mode 100644 index 000000000..88806ba75 --- /dev/null +++ b/src/smt/unsat_core_manager.cpp @@ -0,0 +1,92 @@ +/********************* */ +/*! \file unsat_core_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** 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. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of the unsat core manager of SmtEngine. + **/ + +#include "unsat_core_manager.h" + +#include "expr/proof_node_algorithm.h" +#include "smt/assertions.h" + +namespace CVC4 { +namespace smt { + +void UnsatCoreManager::getUnsatCore(std::shared_ptr pfn, + Assertions& as, + std::vector& core) +{ + Trace("unsat-core") << "UCManager::getUnsatCore: final proof: " << *pfn.get() + << "\n"; + Assert(pfn->getRule() == PfRule::SCOPE); + std::vector fassumps; + expr::getFreeAssumptions(pfn->getChildren()[0].get(), fassumps); + Trace("unsat-core") << "UCManager::getUnsatCore: free assumptions: " + << fassumps << "\n"; + context::CDList* al = as.getAssertionList(); + Assert(al != nullptr); + for (context::CDList::const_iterator i = al->begin(); i != al->end(); + ++i) + { + Trace("unsat-core") << "is assertion " << *i << " there?\n"; + if (std::find(fassumps.begin(), fassumps.end(), *i) != fassumps.end()) + { + Trace("unsat-core") << "\tyes\n"; + core.push_back(*i); + } + } + if (Trace.isOn("unsat-core")) + { + Trace("unsat-core") << "UCManager::getUnsatCore():\n"; + for (const Node& n : core) + { + Trace("unsat-core") << "- " << n << "\n"; + } + } +} + +void UnsatCoreManager::getRelevantInstantiations( + std::shared_ptr pfn, + std::map>>& insts) +{ + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector> visit; + + std::shared_ptr cur; + visit.push_back(pfn); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur.get()); + if (it != visited.end()) + { + continue; + } + visited[cur.get()] = true; + const std::vector>& cs = cur->getChildren(); + if (cur->getRule() == PfRule::INSTANTIATE) + { + const std::vector& instTerms = cur->getArguments(); + Assert(cs.size() == 1); + Node q = cs[0]->getResult(); + insts[q].push_back({instTerms.begin(), instTerms.end()}); + } + for (const std::shared_ptr& cp : cs) + { + visit.push_back(cp); + } + } while (!visit.empty()); +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h new file mode 100644 index 000000000..25be8b864 --- /dev/null +++ b/src/smt/unsat_core_manager.h @@ -0,0 +1,73 @@ +/********************* */ +/*! \file unsat_core_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** 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. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The unsat core manager of SmtEngine. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__UNSAT_CORE_MANAGER_H +#define CVC4__SMT__UNSAT_CORE_MANAGER_H + +#include "context/cdhashmap.h" +#include "context/cdlist.h" +#include "expr/node.h" +#include "expr/proof_node.h" + +namespace CVC4 { + +namespace smt { + +class Assertions; + +/** + * This class is responsible for managing the proof output of SmtEngine, as + * well as setting up the global proof checker and proof node manager. + */ +class UnsatCoreManager +{ + public: + UnsatCoreManager() {} + ~UnsatCoreManager(){}; + + /** Gets the unsat core. + * + * The unsat core is the intersection of the assertions in as and the free + * assumptions of the underlying refutation proof of pfn. Note that pfn must + * be a "final proof", which means that it's a proof of false under a scope + * containing all assertions. + * + * The unsat core is stored in the core argument. + */ + void getUnsatCore(std::shared_ptr pfn, + Assertions& as, + std::vector& core); + + /** Gets the relevant instaniations for the refutation. + * + * The relevant instantiations are all the conclusions of proof nodes of type + * INSTANTIATE that occur in pfn. + * + * This method populates the insts map from quantified formulas occurring as + * premises of INSTANTIATE proof nodes to its instantiations, which are a + * matrix with each row corresponding to the terms with which the respective + * quantified formula is instiated. + */ + void getRelevantInstantiations( + std::shared_ptr pfn, + std::map>>& insts); + +}; /* class UnsatCoreManager */ + +} // namespace smt +} // namespace CVC4 + +#endif /* CVC4__SMT__UNSAT_CORE_MANAGER_H */ -- 2.30.2