Example inference utility (#3670)

7 files changed, 463 insertions, 6 deletions

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<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
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<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
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<n.getNumChildren(); i++ ){
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e64bafe5f..012fde3b8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1966,6 +1966,7 @@ set(regress_2_tests
   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
diff --git a/test/regress/regress2/sygus/examples-deq.sy b/test/regress/regress2/sygus/examples-deq.sy
new file mode 100644
index 000000000..3f1295df6
--- /dev/null
+++ b/test/regress/regress2/sygus/examples-deq.sy
@@ -0,0 +1,9 @@
+; 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)