From 413bd34cee7aad26b1138e4412b5ceb44ae74405 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 3 Feb 2020 08:51:26 -0600 Subject: [PATCH] Example inference utility (#3670) --- src/CMakeLists.txt | 2 + src/theory/quantifiers/quant_util.cpp | 4 +- .../quantifiers/sygus/example_infer.cpp | 278 ++++++++++++++++++ src/theory/quantifiers/sygus/example_infer.h | 164 +++++++++++ src/theory/quantifiers/sygus/sygus_pbe.cpp | 11 +- test/regress/CMakeLists.txt | 1 + test/regress/regress2/sygus/examples-deq.sy | 9 + 7 files changed, 463 insertions(+), 6 deletions(-) create mode 100644 src/theory/quantifiers/sygus/example_infer.cpp create mode 100644 src/theory/quantifiers/sygus/example_infer.h create mode 100644 test/regress/regress2/sygus/examples-deq.sy diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f5f6a83c9..560f79976 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -564,6 +564,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/cegis_unif.h theory/quantifiers/sygus/enum_stream_substitution.cpp theory/quantifiers/sygus/enum_stream_substitution.h + theory/quantifiers/sygus/example_infer.cpp + theory/quantifiers/sygus/example_infer.h theory/quantifiers/sygus/example_min_eval.cpp theory/quantifiers/sygus/example_min_eval.h theory/quantifiers/sygus/sygus_abduct.cpp diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 01f362d25..695d1835c 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -154,7 +154,7 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newPol = pol; }else{ newHasPol = false; - newPol = pol; + newPol = false; } } @@ -170,7 +170,7 @@ void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, newPol = !pol; }else{ newHasPol = false; - newPol = pol; + newPol = false; } } 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& 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::unordered_set> + 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::unordered_set>& + visited, + bool hasPol, + bool pol) +{ + std::pair cacheIndex = std::pair(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::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::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 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::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>>::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& ex) const +{ + Assert(!f.isNull()); + std::map>>::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& exTerms) const +{ + std::map>::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>::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 diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h new file mode 100644 index 000000000..547d41121 --- /dev/null +++ b/src/theory/quantifiers/sygus/example_infer.h @@ -0,0 +1,164 @@ +/********************* */ +/*! \file example_infer.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Haniel Barbosa + ** 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 Utility for inferring whether a formula is in examples form + ** (functions applied to concrete arguments only). + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H +#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H + +#include "context/cdhashmap.h" +#include "theory/quantifiers/sygus/sygus_module.h" +#include "theory/quantifiers/sygus/sygus_unif_io.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Example Inference + * + * This class determines whether a formula "has examples", for details + * see the method hasExamples below. This is important for certain + * optimizations in enumerative SyGuS, include example-based symmetry breaking + * (discarding terms that are equivalent to a previous one up to examples). + * + * Additionally, it provides helper methods for retrieving the examples + * for a function-to-synthesize and for evaluating terms under the inferred + * set of examples. + */ +class ExampleInfer +{ + public: + ExampleInfer(TermDbSygus* tds); + ~ExampleInfer(); + /** initialize + * + * This method initializes the data of this class so that examples are + * inferred for functions-to-synthesize candidates in n, where + * n is the "base instantiation" of the deep-embedding version of the + * synthesis conjecture under candidates (see SynthConjecture::d_base_inst). + * + * Returns false if and only if n has a conflicting example input/output, + * for example if n is ( f(0) = 1 ^ f(0) = 2 ). + */ + bool initialize(Node n, const std::vector& candidates); + /** does the conjecture have examples for all candidates? */ + bool isExamples() const { return d_isExamples; } + /** + * Is the enumerator e associated with examples? This is true if the + * function-to-synthesize associated with e is only applied to concrete + * arguments. Notice that the conjecture need not be in PBE form for this + * to be the case. For example, f has examples in: + * exists f. f( 1 ) = 3 ^ f( 2 ) = 4 + * exists f. f( 45 ) > 0 ^ f( 99 ) > 0 + * exists f. forall x. ( x > 5 => f( 4 ) < x ) + * It does not have examples in: + * exists f. forall x. f( x ) > 5 + * exists f. f( f( 4 ) ) = 5 + * This class implements techniques for functions-to-synthesize that + * have examples. In particular, the method addSearchVal below can be + * called. + */ + bool hasExamples(Node f) const; + /** get number of examples for enumerator e */ + unsigned getNumExamples(Node f) const; + /** + * Get the input arguments for i^th example for function-to-synthesize f, + * which is added to the vector ex. + */ + void getExample(Node f, unsigned i, std::vector& ex) const; + /** get example terms + * + * Add the list of example terms (see d_examplesTerm below) for + * function-to-synthesize f to the vector exTerms. + */ + void getExampleTerms(Node f, std::vector& exTerms) const; + /** + * Get the output value of the i^th example for enumerator e, or null if + * it does not exist (an example does not have an associate output if it is + * not a top-level equality). + */ + Node getExampleOut(Node f, unsigned i) const; + /** + * Is example output valid? Returns true if all examples are associated + * with an output value, e.g. they return a non-null value for getExampleOut + * above. + */ + bool hasExamplesOut(Node f) const; + + private: + /** collect the PBE examples in n + * This is called on the input conjecture, and will populate the above + * vectors, where hasPol/pol denote the polarity of n in the conjecture. This + * function returns false if it finds two examples that are contradictory. + * + * visited[b] stores the cache of nodes we have visited with (hasPol, pol). + */ + bool collectExamples( + Node n, + std::map, + std::unordered_set>& visited, + bool hasPol, + bool pol); + /** Pointer to the sygus term database */ + TermDbSygus* d_tds; + /** is this an examples conjecture for all functions-to-synthesize? */ + bool d_isExamples; + /** + * For each candidate variable f (a function-to-synthesize), whether the + * conjecture has examples for that function. In other words, all occurrences + * of f are applied to constants only. + */ + std::map d_examples_invalid; + /** + * For each function-to-synthesize , whether the conjecture is purely PBE for + * f. In other words, is the specification for f a set of concrete I/O pairs? + * An example of a conjecture for which d_examples_invalid is false but + * d_examplesOut_invalid is true is: + * exists f. forall x. ( f( 0 ) > 2 ) + * another example is: + * exists f. forall x. f( 0 ) = 2 V f( 3 ) = 3 + * since the formula is not a conjunction (the example values are not + * entailed). However, the domain of f in both cases is finite, which can be + * used for search space pruning. + */ + std::map d_examplesOut_invalid; + /** + * For each function-to-synthesize f, the list of concrete inputs to f. + */ + std::map>> d_examples; + /** + * For each function-to-synthesize f, the list of outputs according to the + * I/O specification for f. + * The vector d_examplesOut[f] is valid only if d_examplesOut_invalid[f]=true. + */ + std::map> d_examplesOut; + /** the list of example terms + * For example, if exists f. f( 1 ) = 3 ^ f( 2 ) = 4 is our conjecture, + * this is f( 1 ), f( 2 ). + */ + std::map> d_examplesTerm; + /** + * Map from example input terms to their output, for the example above, + * this is { f( 0 ) -> 2, f( 5 ) -> 7, f( 6 ) -> 8 }. + */ + std::map d_exampleTermMap; +}; + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ + +#endif diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 5468a1e6a..ae019e50f 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -122,12 +122,15 @@ bool SygusPbe::collectExamples(Node n, else { Assert(n_output.isConst()); + // finished processing this node if it was an I/O pair + return true; } - // finished processing this node - return true; } - d_examples_invalid[eh] = true; - d_examples_out_invalid[eh] = true; + else + { + d_examples_invalid[eh] = true; + d_examples_out_invalid[eh] = true; + } } } for( unsigned i=0; i