diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-27 10:32:32 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-27 10:32:32 -0600 |
commit | 8795787c2ef337e73b46778b99f5bfa6c2a19f93 (patch) | |
tree | 0989e95f24c2eeedd177d2281069d266b31d971d /src/theory/quantifiers/skolemize.cpp | |
parent | a6d3c9e7fb765704f34815900712b10e85687edc (diff) |
(proof-new) Improvements to quantifiers engine and instantiate interfaces (#5814)
This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).
Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.
Diffstat (limited to 'src/theory/quantifiers/skolemize.cpp')
-rw-r--r-- | src/theory/quantifiers/skolemize.cpp | 29 |
1 files changed, 9 insertions, 20 deletions
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 901b7ad82..3ddfc4c9f 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -378,29 +378,18 @@ bool Skolemize::isInductionTerm(Node n) return false; } -bool Skolemize::printSkolemization(std::ostream& out) +void Skolemize::getSkolemTermVectors( + std::map<Node, std::vector<Node> >& sks) const { - bool printed = false; - for (NodeNodeMap::iterator it = d_skolemized.begin(); - it != d_skolemized.end(); - ++it) + std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::const_iterator + itk; + for (const std::pair<const Node, Node>& p : d_skolemized) { - Node q = (*it).first; - printed = true; - out << "(skolem " << q << std::endl; - out << " ( "; - for (unsigned i = 0; i < d_skolem_constants[q].size(); i++) - { - if (i > 0) - { - out << " "; - } - out << d_skolem_constants[q][i]; - } - out << " )" << std::endl; - out << ")" << std::endl; + Node q = p.first; + itk = d_skolem_constants.find(q); + Assert(itk != d_skolem_constants.end()); + sks[q].insert(sks[q].end(), itk->second.begin(), itk->second.end()); } - return printed; } bool Skolemize::isProofEnabled() const { return d_epg != nullptr; } |