diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 23:20:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 23:20:09 -0500 |
commit | 3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9 (patch) | |
tree | b5c785e9a5e16d430f45b2a40f78e40247111233 /src/theory/quantifiers/quant_epr.cpp | |
parent | 4b580ea3876055f701b13e67e0e4e78abbe47674 (diff) |
(Move-only) Split quant util (#1306)
* Initial draft of splitting quant util.
* Minor
* Document recursive term builder.
* Rename file, minor.
* Clang format
Diffstat (limited to 'src/theory/quantifiers/quant_epr.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_epr.cpp | 187 |
1 files changed, 187 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_epr.cpp b/src/theory/quantifiers/quant_epr.cpp new file mode 100644 index 000000000..187466aaa --- /dev/null +++ b/src/theory/quantifiers/quant_epr.cpp @@ -0,0 +1,187 @@ +/********************* */ +/*! \file quant_epr.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 quantifier EPR. + **/ + +#include "theory/quantifiers/quant_epr.h" + +#include "theory/quantifiers/quant_util.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void QuantEPR::registerNode(Node n, + std::map<int, std::map<Node, bool> >& visited, + bool beneathQuant, + bool hasPol, + bool pol) +{ + int vindex = hasPol ? (pol ? 1 : -1) : 0; + if (visited[vindex].find(n) == visited[vindex].end()) + { + visited[vindex][n] = true; + Trace("quant-epr-debug") << "QuantEPR::registerNode " << n << std::endl; + if (n.getKind() == FORALL) + { + if (beneathQuant || !hasPol || !pol) + { + for (unsigned i = 0; i < n[0].getNumChildren(); i++) + { + TypeNode tn = n[0][i].getType(); + if (d_non_epr.find(tn) == d_non_epr.end()) + { + Trace("quant-epr") << "Sort " << tn + << " is non-EPR because of nested or possible " + "existential quantification." + << std::endl; + d_non_epr[tn] = true; + } + } + } + else + { + beneathQuant = true; + } + } + TypeNode tn = n.getType(); + + if (n.getNumChildren() > 0) + { + if (tn.isSort()) + { + if (d_non_epr.find(tn) == d_non_epr.end()) + { + Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n + << std::endl; + d_non_epr[tn] = true; + } + } + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity(n, i, hasPol, pol, newHasPol, newPol); + registerNode(n[i], visited, beneathQuant, newHasPol, newPol); + } + } + else if (tn.isSort()) + { + if (n.getKind() == BOUND_VARIABLE) + { + if (d_consts.find(tn) == d_consts.end()) + { + // mark that at least one constant must occur + d_consts[tn].clear(); + } + } + else if (std::find(d_consts[tn].begin(), d_consts[tn].end(), n) + == d_consts[tn].end()) + { + d_consts[tn].push_back(n); + Trace("quant-epr") << "...constant of type " << tn << " : " << n + << std::endl; + } + } + } +} + +void QuantEPR::registerAssertion(Node assertion) +{ + std::map<int, std::map<Node, bool> > visited; + registerNode(assertion, visited, false, true, true); +} + +void QuantEPR::finishInit() +{ + Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl; + for (std::map<TypeNode, std::vector<Node> >::iterator it = d_consts.begin(); + it != d_consts.end(); + ++it) + { + Assert(d_epr_axiom.find(it->first) == d_epr_axiom.end()); + Trace("quant-epr-debug") << "process " << it->first << std::endl; + if (d_non_epr.find(it->first) != d_non_epr.end()) + { + Trace("quant-epr-debug") << "...non-epr" << std::endl; + it->second.clear(); + } + else + { + Trace("quant-epr-debug") << "...epr, #consts = " << it->second.size() + << std::endl; + if (it->second.empty()) + { + it->second.push_back(NodeManager::currentNM()->mkSkolem( + "e", it->first, "EPR base constant")); + } + if (Trace.isOn("quant-epr")) + { + Trace("quant-epr") << "Type " << it->first + << " is EPR, with constants : " << std::endl; + for (unsigned i = 0; i < it->second.size(); i++) + { + Trace("quant-epr") << " " << it->second[i] << std::endl; + } + } + } + } +} + +bool QuantEPR::isEPRConstant(TypeNode tn, Node k) +{ + return std::find(d_consts[tn].begin(), d_consts[tn].end(), k) + != d_consts[tn].end(); +} + +void QuantEPR::addEPRConstant(TypeNode tn, Node k) +{ + Assert(isEPR(tn)); + Assert(d_epr_axiom.find(tn) == d_epr_axiom.end()); + if (!isEPRConstant(tn, k)) + { + d_consts[tn].push_back(k); + } +} + +Node QuantEPR::mkEPRAxiom(TypeNode tn) +{ + Assert(isEPR(tn)); + std::map<TypeNode, Node>::iterator ita = d_epr_axiom.find(tn); + if (ita == d_epr_axiom.end()) + { + std::vector<Node> disj; + Node x = NodeManager::currentNM()->mkBoundVar(tn); + for (unsigned i = 0; i < d_consts[tn].size(); i++) + { + disj.push_back( + NodeManager::currentNM()->mkNode(EQUAL, x, d_consts[tn][i])); + } + Assert(!disj.empty()); + d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( + FORALL, + NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, x), + disj.size() == 1 ? disj[0] + : NodeManager::currentNM()->mkNode(OR, disj)); + return d_epr_axiom[tn]; + } + else + { + return ita->second; + } +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ |