Quickly recognize when PBE conjectures are infeasible (#2718)

Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE.

This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust.

After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible.

1 files changed, 10 insertions, 4 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index e21c9263f..a62100692 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -240,11 +240,17 @@ class SygusPbe : public SygusModule
    * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 )
    */
   std::map<Node, std::vector<Node> > d_examples_term;
+  /**
+   * Map from example input terms to their output, for example [EX#1] above,
+   * this is { f( 0 ) -> 2, f( 5 ) -> 7, f( 6 ) -> 8 }.
+   */
+  std::map<Node, Node> d_exampleTermMap;
   /** collect the PBE examples in n
-  * This is called on the input conjecture, and will populate the above vectors.
-  *   hasPol/pol denote the polarity of n in the conjecture.
-  */
-  void collectExamples(Node 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.
+   */
+  bool collectExamples(Node n,
                        std::map<Node, bool>& visited,
                        bool hasPol,
                        bool pol);