From: Andrew Reynolds Date: Thu, 19 Nov 2020 18:27:40 +0000 (-0600) Subject: Add nested quantifier elimination module (#5422) X-Git-Tag: cvc5-1.0.0~2580 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f172b30bfe18a24416fd61f4aa5ce3dea583296e;p=cvc5.git Add nested quantifier elimination module (#5422) This has static utilities for doing nested quantifier elimination and some data structures for maintaining a context-dependent set of quantified formulas that have been processed. This is work towards CVC4/cvc4-wishues#26, and work reimplementation of the option --ceqgi-nested-qe. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c570dfdb4..aaa1f04f8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -616,6 +616,8 @@ libcvc4_add_sources( theory/quantifiers/cegqi/ceg_instantiator.h theory/quantifiers/cegqi/inst_strategy_cegqi.cpp theory/quantifiers/cegqi/inst_strategy_cegqi.h + theory/quantifiers/cegqi/nested_qe.cpp + theory/quantifiers/cegqi/nested_qe.h theory/quantifiers/cegqi/vts_term_cache.cpp theory/quantifiers/cegqi/vts_term_cache.h theory/quantifiers/conjecture_generator.cpp diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index fb3df5327..430303f6b 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -112,6 +112,8 @@ libcvc4_add_sources( record.h sequence.cpp sequence.h + subs.cpp + subs.h sygus_datatype.cpp sygus_datatype.h uninterpreted_constant.cpp diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp new file mode 100644 index 000000000..7f77a1daf --- /dev/null +++ b/src/theory/quantifiers/cegqi/nested_qe.cpp @@ -0,0 +1,148 @@ +/********************* */ +/*! \file nested_qe.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Methods for counterexample-guided quantifier instantiation + ** based on nested quantifier elimination. + **/ + +#include "theory/quantifiers/cegqi/nested_qe.h" + +#include "expr/node_algorithm.h" +#include "expr/subs.h" +#include "theory/smt_engine_subsolver.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +NestedQe::NestedQe(context::UserContext* u) : d_qnqe(u) {} + +bool NestedQe::process(Node q, std::vector& lems) +{ + NodeNodeMap::iterator it = d_qnqe.find(q); + if (it != d_qnqe.end()) + { + // already processed + return (*it).second != q; + } + Trace("cegqi-nested-qe") << "Check nested QE on " << q << std::endl; + Node qqe = doNestedQe(q, true); + d_qnqe[q] = qqe; + if (qqe == q) + { + Trace("cegqi-nested-qe") << "...did not apply nested QE" << std::endl; + return false; + } + Trace("cegqi-nested-qe") << "...applied nested QE" << std::endl; + Trace("cegqi-nested-qe") << "Result is " << qqe << std::endl; + + // add as lemma + lems.push_back(q.eqNode(qqe)); + return true; +} + +bool NestedQe::hasProcessed(Node q) const +{ + return d_qnqe.find(q) != d_qnqe.end(); +} + +bool NestedQe::getNestedQuantification( + Node q, std::unordered_set& nqs) +{ + expr::getKindSubterms(q[1], kind::FORALL, true, nqs); + return !nqs.empty(); +} + +bool NestedQe::hasNestedQuantification(Node q) +{ + std::unordered_set nqs; + return getNestedQuantification(q, nqs); +} + +Node NestedQe::doNestedQe(Node q, bool keepTopLevel) +{ + Assert(q.getKind() == kind::FORALL); + std::unordered_set nqs; + if (!getNestedQuantification(q, nqs)) + { + Trace("cegqi-nested-qe-debug") + << "...no nested quantification" << std::endl; + if (keepTopLevel) + { + return q; + } + // just do ordinary quantifier elimination + Node qqe = doQe(q); + Trace("cegqi-nested-qe-debug") << "...did ordinary qe" << std::endl; + return qqe; + } + Trace("cegqi-nested-qe-debug") + << "..." << nqs.size() << " nested quantifiers" << std::endl; + // otherwise, skolemize the arguments of this and apply + std::vector vars(q[0].begin(), q[0].end()); + Subs sk; + sk.add(vars); + // do nested quantifier elimination on each nested quantifier, skolemizing the + // free variables + Subs snqe; + for (const Node& nq : nqs) + { + Node nqk = sk.apply(nq); + Node nqqe = doNestedQe(nqk); + if (nqqe == nqk) + { + // failed + Trace("cegqi-nested-qe-debug") + << "...failed to apply to nested" << std::endl; + return q; + } + snqe.add(nqk, nqqe); + } + // get the result of nested quantifier elimination + Node qeBody = sk.apply(q[1]); + qeBody = snqe.apply(qeBody); + // undo the skolemization + qeBody = sk.rapply(qeBody, true); + // reconstruct the body + std::vector qargs; + qargs.push_back(q[0]); + qargs.push_back(qeBody); + if (q.getNumChildren() == 3) + { + qargs.push_back(q[2]); + } + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::FORALL, qargs); +} + +Node NestedQe::doQe(Node q) +{ + Assert(q.getKind() == kind::FORALL); + Trace("cegqi-nested-qe") << " Apply qe to " << q << std::endl; + NodeManager* nm = NodeManager::currentNM(); + q = nm->mkNode(kind::EXISTS, q[0], q[1].negate()); + std::unique_ptr smt_qe; + initializeSubsolver(smt_qe); + Node qqe = smt_qe->getQuantifierElimination(q, true, false); + if (expr::hasBoundVar(qqe)) + { + Trace("cegqi-nested-qe") << " ...failed QE" << std::endl; + //...failed to apply + return q; + } + Node res = qqe.negate(); + Trace("cegqi-nested-qe") << " ...success, result = " << res << std::endl; + return res; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h new file mode 100644 index 000000000..ef690afd5 --- /dev/null +++ b/src/theory/quantifiers/cegqi/nested_qe.h @@ -0,0 +1,86 @@ +/********************* */ +/*! \file nested_qe.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Methods for counterexample-guided quantifier instantiation + ** based on nested quantifier elimination. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H +#define CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H + +#include + +#include "context/cdhashmap.h" +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class NestedQe +{ + using NodeNodeMap = context::CDHashMap; + + public: + NestedQe(context::UserContext* u); + ~NestedQe() {} + /** + * Process quantified formula. If this returns true, then q was processed + * via nested quantifier elimination (either during this call or previously + * in this user context). If q was processed in this call, the lemma: + * (= q qqe) + * is added to lem, where qqe is the result of nested quantifier elimination + * on q. + */ + bool process(Node q, std::vector& lems); + /** + * Have we processed q using the above method? + */ + bool hasProcessed(Node q) const; + + /** + * Get nested quantification. Returns true if q has nested quantifiers. + * Adds each nested quantifier in the body of q to nqs. + */ + static bool getNestedQuantification( + Node q, std::unordered_set& nqs); + /** + * Does quantified formula q have nested quantification? + */ + static bool hasNestedQuantification(Node q); + /** + * Do nested quantifier elimination. Returns a formula that is equivalent to + * q and has no nested quantification. If keepTopLevel is false, then the + * returned formula is quantifier-free. Otherwise, it is a quantified formula + * with no nested quantification. + */ + static Node doNestedQe(Node q, bool keepTopLevel = false); + /** + * Run quantifier elimination on quantified formula q, where q has no nested + * quantification. This method invokes a subsolver for performing quantifier + * elimination. + */ + static Node doQe(Node q); + + private: + /** + * Mapping from quantified formulas q to the result of doNestedQe(q, true). + */ + NodeNodeMap d_qnqe; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif