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.

8 files changed, 120 insertions, 20 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f3a6c0c9e..7bf86f092 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1304,6 +1304,14 @@ void SmtEngine::setDefaults() {
       options::unconstrainedSimp.set(uncSimp);
     }
   }
+  if (!options::proof())
+  {
+    // minimizing solutions from single invocation requires proofs
+    if (options::cegqiSolMinCore() && options::cegqiSolMinCore.wasSetByUser())
+    {
+      throw OptionException("cegqi-si-sol-min-core requires --proof");
+    }
+  }
 
   // Disable options incompatible with unsat cores and proofs or output an
   // error if enabled explicitly
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index ee7247121..408f076ac 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -16,9 +16,10 @@
 
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/datatypes/datatypes_rewriter.h"
 #include "util/random.h"
 
 using namespace CVC4;
@@ -40,7 +41,7 @@ SygusPbe::~SygusPbe() {}
 
 //--------------------------------- collecting finite input/output domain information
 
-void SygusPbe::collectExamples(Node n,
+bool SygusPbe::collectExamples(Node n,
                                std::map<Node, bool>& visited,
                                bool hasPol,
                                bool pol)
@@ -54,10 +55,12 @@ void SygusPbe::collectExamples(Node n,
     {
       neval = n;
       if( hasPol ){
-        n_output = !pol ? d_true : d_false;
+        n_output = pol ? d_true : d_false;
       }
       neval_is_evalapp = true;
-    }else if( n.getKind()==EQUAL && hasPol && !pol ){
+    }
+    else if (n.getKind() == EQUAL && hasPol && pol)
+    {
       for( unsigned r=0; r<2; r++ ){
         if (n[r].getKind() == DT_SYGUS_EVAL)
         {
@@ -72,6 +75,25 @@ void SygusPbe::collectExamples(Node n,
     // is it an evaluation function?
     if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
     {
+      Trace("sygus-pbe-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);
@@ -103,7 +125,7 @@ void SygusPbe::collectExamples(Node n,
             Assert(n_output.isConst());
           }
           // finished processing this node
-          return;
+          return true;
         }
         d_examples_invalid[eh] = true;
         d_examples_out_invalid[eh] = true;
@@ -112,10 +134,14 @@ void SygusPbe::collectExamples(Node n,
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       bool newHasPol;
       bool newPol;
-      QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
-      collectExamples( n[i], visited, newHasPol, newPol );
+      QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol);
+      if (!collectExamples(n[i], visited, newHasPol, newPol))
+      {
+        return false;
+      }
     }
   }
+  return true;
 }
 
 bool SygusPbe::initialize(Node n,
@@ -123,6 +149,7 @@ bool SygusPbe::initialize(Node n,
                           std::vector<Node>& lemmas)
 {
   Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
 
   for (unsigned i = 0; i < candidates.size(); i++)
   {
@@ -133,7 +160,14 @@ bool SygusPbe::initialize(Node n,
   }
 
   std::map<Node, bool> visited;
-  collectExamples(n, visited, true, true);
+  // n is negated conjecture
+  if (!collectExamples(n, visited, true, false))
+  {
+    Trace("sygus-pbe") << "...conflicting examples" << std::endl;
+    Node infeasible = d_parent->getGuard().negate();
+    lemmas.push_back(infeasible);
+    return false;
+  }
 
   for (unsigned i = 0; i < candidates.size(); i++)
   {
@@ -198,7 +232,6 @@ bool SygusPbe::initialize(Node n,
       tn_to_strategy_pt[tnsp].push_back(p.first);
     }
     // initialize the enumerators
-    NodeManager* nm = NodeManager::currentNM();
     for (const Node& e : d_candidate_to_enum[c])
     {
       TypeNode etn = e.getType();
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);
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 78892aac8..4bd6cb7fe 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -701,12 +701,12 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
           Trace("sygus-sui-enum")
               << "  ...fail : term is not unique" << std::endl;
         }
-        d_cond_count++;
       }
       if (keep)
       {
         // notify to retry the build of solution
         d_check_sol = true;
+        d_cond_count++;
         ecv.addEnumValue(v, results);
       }
     }
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 2bfde2d80..e1cbed044 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -78,6 +78,12 @@ void SynthConjecture::assign(Node q)
   d_quant = q;
   NodeManager* nm = NodeManager::currentNM();
 
+  // initialize the guard
+  d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
+  d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
+  d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard);
+  AlwaysAssert(!d_feasible_guard.isNull());
+
   // pre-simplify the quantified formula based on the process utility
   d_simp_quant = d_ceg_proc->preSimplify(d_quant);
 
@@ -177,11 +183,6 @@ void SynthConjecture::assign(Node q)
     }
   }
 
-  // initialize the guard
-  d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
-  d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
-  d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard);
-  AlwaysAssert(!d_feasible_guard.isNull());
   // register the strategy
   d_feasible_strategy.reset(
       new DecisionStrategySingleton("sygus_feasible",
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a1d5a35aa..97b1fb99b 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -861,6 +861,7 @@ set(regress_0_tests
   regress0/sygus/real-si-all.sy
   regress0/sygus/strings-unconstrained.sy
   regress0/sygus/uminus_one.sy
+  regress0/sygus/univ_3-long-repeat-conflict.sy
   regress0/test11.cvc
   regress0/test9.cvc
   regress0/tptp/ARI086=1.p
diff --git a/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy
new file mode 100644
index 000000000..c2ed642be
--- /dev/null
+++ b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy
@@ -0,0 +1,50 @@
+; EXPECT: unknown
+; COMMAND-LINE: --sygus-out=status
+(set-logic SLIA)
+ 
+(synth-fun f ((col1 String) (col2 String)) String
+    ((Start String (ntString))
+     (ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY"
+                       (str.++ ntString ntString)
+                       (str.replace ntString ntString ntString)
+                       (str.at ntString ntInt)
+                       (int.to.str ntInt)
+                       (ite ntBool ntString ntString)
+                       (str.substr ntString ntInt ntInt)))
+      (ntInt Int (0 1 2
+                  (+ ntInt ntInt)
+                  (- ntInt ntInt)
+                  (str.len ntString)
+                  (str.to.int ntString)
+                  (str.indexof ntString ntString ntInt)))
+      (ntBool Bool (true false
+                    (str.prefixof ntString ntString)
+                    (str.suffixof ntString ntString)
+                    (str.contains ntString ntString)))))
+
+
+(declare-var col1 String)
+(declare-var col2 String)
+(constraint (= (f "UC Berkeley" "Berkeley, CA") 
+                  "Berkeley, CA, USA"))
+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") 
+                  "Phialdelphia, PA, USA"))
+(constraint (= (f "UCLA" "Los Angeles, CA") 
+                    "UCLA, Los Angeles, CA, USA"))
+(constraint (= (f "Cornell University" "Ithaca, New York, USA") 
+                  "Ithaca, New York, USA"))
+(constraint (= (f "Penn" "Philadelphia, PA, USA") 
+                  "Philadelphia, PA, USA"))
+(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA") 
+                  "Ann Arbor, MI, USA"))
+(constraint (= (f "UC Berkeley" "Berkeley, CA") 
+                  "Berkeley, CA, USA"))
+(constraint (= (f "MIT" "Cambridge, MA") 
+                  "Cambridge, MA, USA"))
+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") 
+                  "Phialdelphia, PA, USA"))
+(constraint (= (f "UCLA" "Los Angeles, CA") 
+                    "Los Angeles, CA, USA"))
+
+; has contradictory examples
+(check-synth)
diff --git a/test/regress/regress1/sygus/array_search_2.sy b/test/regress/regress1/sygus/array_search_2.sy
index 41346e655..93cbf9ce9 100644
--- a/test/regress/regress1/sygus/array_search_2.sy
+++ b/test/regress/regress1/sygus/array_search_2.sy
@@ -1,5 +1,6 @@
+; REQUIRES: proof
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --cegqi-si-sol-min-core --proof
 (set-logic LIA)
 (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)