diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-03 08:51:26 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-03 08:51:26 -0600 |
commit | 413bd34cee7aad26b1138e4412b5ceb44ae74405 (patch) | |
tree | 4341ac1d9658e9086a951ec07910ef6f09d80b5d /src/theory/quantifiers/sygus/example_infer.cpp | |
parent | bdb685d928d1f4bb570acdc6c8427217a6b6cbe3 (diff) |
Example inference utility (#3670)
Diffstat (limited to 'src/theory/quantifiers/sygus/example_infer.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/example_infer.cpp | 278 |
1 files changed, 278 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/example_infer.cpp b/src/theory/quantifiers/sygus/example_infer.cpp new file mode 100644 index 000000000..50d2bf3d2 --- /dev/null +++ b/src/theory/quantifiers/sygus/example_infer.cpp @@ -0,0 +1,278 @@ +/********************* */ +/*! \file example_infer.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Haniel Barbosa, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 utility for inferring whether a formula is in + ** examples form (functions applied to concrete arguments only). + ** + **/ +#include "theory/quantifiers/sygus/example_infer.h" + +#include "theory/quantifiers/quant_util.h" + +using namespace CVC4; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +ExampleInfer::ExampleInfer(TermDbSygus* tds) : d_tds(tds) +{ + d_isExamples = false; +} + +ExampleInfer::~ExampleInfer() {} + +bool ExampleInfer::initialize(Node n, const std::vector<Node>& candidates) +{ + Trace("ex-infer") << "Initialize example inference : " << n << std::endl; + + for (const Node& v : candidates) + { + d_examples[v].clear(); + d_examplesOut[v].clear(); + d_examplesTerm[v].clear(); + } + std::map<std::pair<bool, bool>, std::unordered_set<Node, NodeHashFunction>> + visited; + // n is negated conjecture + if (!collectExamples(n, visited, true, false)) + { + Trace("ex-infer") << "...conflicting examples" << std::endl; + return false; + } + + if (Trace.isOn("ex-infer")) + { + for (unsigned i = 0; i < candidates.size(); i++) + { + Node v = candidates[i]; + Trace("ex-infer") << " examples for " << v << " : "; + if (d_examples_invalid.find(v) != d_examples_invalid.end()) + { + Trace("ex-infer") << "INVALID" << std::endl; + } + else + { + Trace("ex-infer") << std::endl; + for (unsigned j = 0; j < d_examples[v].size(); j++) + { + Trace("ex-infer") << " "; + for (unsigned k = 0; k < d_examples[v][j].size(); k++) + { + Trace("ex-infer") << d_examples[v][j][k] << " "; + } + if (!d_examplesOut[v][j].isNull()) + { + Trace("ex-infer") << " -> " << d_examplesOut[v][j]; + } + Trace("ex-infer") << std::endl; + } + } + Trace("ex-infer") << "Initialize " << d_examples[v].size() + << " example points for " << v << "..." << std::endl; + } + } + return true; +} + +bool ExampleInfer::collectExamples( + Node n, + std::map<std::pair<bool, bool>, std::unordered_set<Node, NodeHashFunction>>& + visited, + bool hasPol, + bool pol) +{ + std::pair<bool, bool> cacheIndex = std::pair<bool, bool>(hasPol, pol); + if (visited[cacheIndex].find(n) != visited[cacheIndex].end()) + { + // already visited + return true; + } + visited[cacheIndex].insert(n); + NodeManager* nm = NodeManager::currentNM(); + Node neval; + Node n_output; + bool neval_is_evalapp = false; + if (n.getKind() == DT_SYGUS_EVAL) + { + neval = n; + if (hasPol) + { + n_output = nm->mkConst(pol); + } + neval_is_evalapp = true; + } + else if (n.getKind() == EQUAL && hasPol && pol) + { + for (unsigned r = 0; r < 2; r++) + { + if (n[r].getKind() == DT_SYGUS_EVAL) + { + neval = n[r]; + if (n[1 - r].isConst()) + { + n_output = n[1 - r]; + } + neval_is_evalapp = true; + break; + } + } + } + // is it an evaluation function? + if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end()) + { + Trace("ex-infer-debug") + << "Process head: " << n << " == " << n_output << std::endl; + // If n_output is null, then neval does not have a constant value + // If n_output is non-null, then neval is constrained to always be + // that value. + if (!n_output.isNull()) + { + std::map<Node, Node>::iterator itet = d_exampleTermMap.find(neval); + if (itet == d_exampleTermMap.end()) + { + d_exampleTermMap[neval] = n_output; + } + else if (itet->second != n_output) + { + // We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2, + // the conjecture is infeasible. + return false; + } + } + // get the evaluation head + Node eh = neval[0]; + std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh); + if (itx == d_examples_invalid.end()) + { + // have we already processed this as an example term? + if (std::find(d_examplesTerm[eh].begin(), d_examplesTerm[eh].end(), neval) + == d_examplesTerm[eh].end()) + { + // collect example + bool success = true; + std::vector<Node> ex; + for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++) + { + if (!neval[j].isConst()) + { + success = false; + break; + } + ex.push_back(neval[j]); + } + if (success) + { + d_examples[eh].push_back(ex); + d_examplesOut[eh].push_back(n_output); + d_examplesTerm[eh].push_back(neval); + if (n_output.isNull()) + { + d_examplesOut_invalid[eh] = true; + } + else + { + Assert(n_output.isConst()); + // finished processing this node if it was an I/O pair + return true; + } + } + else + { + d_examples_invalid[eh] = true; + d_examplesOut_invalid[eh] = true; + } + } + } + } + for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + bool newHasPol; + bool newPol; + QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol); + if (!collectExamples(n[i], visited, newHasPol, newPol)) + { + return false; + } + } + return true; +} + +bool ExampleInfer::hasExamples(Node f) const +{ + std::map<Node, bool>::const_iterator itx = d_examples_invalid.find(f); + if (itx == d_examples_invalid.end()) + { + return d_examples.find(f) != d_examples.end(); + } + return false; +} + +unsigned ExampleInfer::getNumExamples(Node f) const +{ + std::map<Node, std::vector<std::vector<Node>>>::const_iterator it = + d_examples.find(f); + if (it != d_examples.end()) + { + return it->second.size(); + } + return 0; +} + +void ExampleInfer::getExample(Node f, unsigned i, std::vector<Node>& ex) const +{ + Assert(!f.isNull()); + std::map<Node, std::vector<std::vector<Node>>>::const_iterator it = + d_examples.find(f); + if (it != d_examples.end()) + { + Assert(i < it->second.size()); + ex.insert(ex.end(), it->second[i].begin(), it->second[i].end()); + } + else + { + Assert(false); + } +} + +void ExampleInfer::getExampleTerms(Node f, std::vector<Node>& exTerms) const +{ + std::map<Node, std::vector<Node>>::const_iterator itt = + d_examplesTerm.find(f); + if (itt == d_examplesTerm.end()) + { + return; + } + exTerms.insert(exTerms.end(), itt->second.begin(), itt->second.end()); +} + +Node ExampleInfer::getExampleOut(Node f, unsigned i) const +{ + Assert(!f.isNull()); + std::map<Node, std::vector<Node>>::const_iterator it = d_examplesOut.find(f); + if (it != d_examplesOut.end()) + { + Assert(i < it->second.size()); + return it->second[i]; + } + Assert(false); + return Node::null(); +} + +bool ExampleInfer::hasExamplesOut(Node f) const +{ + return d_examplesOut_invalid.find(f) == d_examplesOut_invalid.end(); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 |