sygusComp2018: optimization for invariance test (#2104)

2 files changed, 60 insertions, 19 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index 4c638be0a..54a3cce50 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -27,7 +27,22 @@ namespace quantifiers {
 
 void EvalSygusInvarianceTest::init(Node conj, Node var, Node res)
 {
-  d_conj = conj;
+  d_terms.clear();
+  // simple miniscope
+  if ((conj.getKind() == AND || conj.getKind() == OR) && res.isConst())
+  {
+    for (const Node& c : conj)
+    {
+      d_terms.push_back(c);
+    }
+    d_kind = conj.getKind();
+    d_is_conjunctive = res.getConst<bool>() == (d_kind == AND);
+  }
+  else
+  {
+    d_terms.push_back(conj);
+    d_is_conjunctive = true;
+  }
   d_var = var;
   d_result = res;
 }
@@ -40,21 +55,35 @@ Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n)
 bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
 {
   TNode tnvn = nvn;
-  Node conj_subs = d_conj.substitute(d_var, tnvn);
-  Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs);
-  Trace("sygus-cref-eval2-debug")
-      << "  ...check unfolding : " << conj_subs_unfold << std::endl;
-  Trace("sygus-cref-eval2-debug") << "  ......from : " << conj_subs
-                                  << std::endl;
-  if (conj_subs_unfold == d_result)
+  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
+  for (const Node& c : d_terms)
   {
+    Node conj_subs = c.substitute(d_var, tnvn, cache);
+    Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs);
+    Trace("sygus-cref-eval2-debug")
+        << "  ...check unfolding : " << conj_subs_unfold << std::endl;
+    Trace("sygus-cref-eval2-debug")
+        << "  ......from : " << conj_subs << std::endl;
+    if (conj_subs_unfold != d_result)
+    {
+      if (d_is_conjunctive)
+      {
+        // ti /--> true  implies and( t1, ..., tn ) /--> true, where "/-->" is
+        // "does not evaluate to".
+        return false;
+      }
+    }
+    else if (!d_is_conjunctive)
+    {
+      // ti --> true  implies or( t1, ..., tn ) --> true
+      return true;
+    }
     Trace("sygus-cref-eval2") << "Evaluation min explain : " << conj_subs
                               << " still evaluates to " << d_result
                               << " regardless of ";
     Trace("sygus-cref-eval2") << x << std::endl;
-    return true;
   }
-  return false;
+  return d_is_conjunctive;
 }
 
 void EquivSygusInvarianceTest::init(
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h
index 02bba55a1..9e3553a0b 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.h
+++ b/src/theory/quantifiers/sygus/sygus_invariance.h
@@ -97,30 +97,42 @@ class SygusInvarianceTest
 class EvalSygusInvarianceTest : public SygusInvarianceTest
 {
  public:
-  EvalSygusInvarianceTest() {}
+  EvalSygusInvarianceTest() : d_kind(kind::UNDEFINED_KIND) {}
 
   /** initialize this invariance test
-    * This sets d_conj/d_var/d_result, where
-    * we are checking whether:
-    *   d_conj { d_var -> n } ----> d_result.
-    * for terms n.
-    */
+   *
+   * This sets d_terms/d_var/d_result, where we are checking whether:
+   *   <d_kind>(d_terms) { d_var -> n } ----> d_result.
+   * for terms n.
+   */
   void init(Node conj, Node var, Node res);
 
   /** do evaluate with unfolding, using the cache of this class */
   Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n);
 
  protected:
-  /** does d_conj{ d_var -> nvn } still rewrite to d_result? */
+  /** does d_terms{ d_var -> nvn } still rewrite to d_result? */
   bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
 
  private:
-  /** the formula we are evaluating */
-  Node d_conj;
+  /** the formulas we are evaluating */
+  std::vector<Node> d_terms;
   /** the variable */
   TNode d_var;
   /** the result of the evaluation */
   Node d_result;
+  /** the parent kind we are checking, undefined if size(d_terms) is 1. */
+  Kind d_kind;
+  /** whether we are conjunctive
+   *
+   * If this flag is true, then the evaluation tests:
+   *   d_terms[1] {d_var -> n} = d_result ... d_term[k] {d_var -> n} = d_result
+   * should be processed conjunctively, that is,
+   * <d_kind>(d_terms) { d_var -> n } = d_result only if each of the above
+   * holds. If this flag is false, then these tests are interpreted
+   * disjunctively, i.e. if one child test succeeds, the overall test succeeds.
+   */
+  bool d_is_conjunctive;
   /** cache of n -> the simplified form of eval( n ) */
   std::unordered_map<Node, Node, NodeHashFunction> d_visited;
 };