diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 12:27:40 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-19 12:27:40 -0600 |
commit | f172b30bfe18a24416fd61f4aa5ce3dea583296e (patch) | |
tree | 3c27f17b24e6095ce7ad4b5ec3f50e407412d378 /src/theory/quantifiers/cegqi | |
parent | 3654512dd8b341c5725e550d438b23508493b991 (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers/cegqi')
-rw-r--r-- | src/theory/quantifiers/cegqi/nested_qe.cpp | 148 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/nested_qe.h | 86 |
2 files changed, 234 insertions, 0 deletions
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<Node>& 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<Node, NodeHashFunction>& nqs) +{ + expr::getKindSubterms(q[1], kind::FORALL, true, nqs); + return !nqs.empty(); +} + +bool NestedQe::hasNestedQuantification(Node q) +{ + std::unordered_set<Node, NodeHashFunction> nqs; + return getNestedQuantification(q, nqs); +} + +Node NestedQe::doNestedQe(Node q, bool keepTopLevel) +{ + Assert(q.getKind() == kind::FORALL); + std::unordered_set<Node, NodeHashFunction> 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<Node> 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<Node> 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<SmtEngine> 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 <unordered_set> + +#include "context/cdhashmap.h" +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class NestedQe +{ + using NodeNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>; + + 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<Node>& 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<Node, NodeHashFunction>& 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 |