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
newPol = pol;
}else{
newHasPol = false;
- newPol = pol;
+ newPol = false;
}
}
newPol = !pol;
}else{
newHasPol = false;
- newPol = pol;
+ newPol = false;
}
}
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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<Node>& 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<Node>& 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<Node>& 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::pair<bool, bool>,
+ std::unordered_set<Node, NodeHashFunction>>& 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<Node, bool> 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<Node, bool> d_examplesOut_invalid;
+ /**
+ * For each function-to-synthesize f, the list of concrete inputs to f.
+ */
+ std::map<Node, std::vector<std::vector<Node>>> 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<Node, std::vector<Node>> 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<Node, std::vector<Node>> 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<Node, Node> d_exampleTermMap;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} /* namespace CVC4 */
+
+#endif
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<n.getNumChildren(); i++ ){
regress2/sygus/array_sum_dd.sy
regress2/sygus/cegisunif-depth1-bv.sy
regress2/sygus/ex23.sy
+ regress2/sygus/examples-deq.sy
regress2/sygus/icfp_easy_mt_ite.sy
regress2/sygus/inv_gen_n_c11.sy
regress2/sygus/lustre-real.sy
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+(synth-fun f ((x Int) (y Int)) Int)
+
+(constraint (not (= (f 0 4) (f 6 7))))
+(constraint (= (f 5 7) (f 1 4)))
+
+(check-synth)
projects / cvc5.git / commitdiff