Generalize example-based sym breaking to conjectures with constant function apps...

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 5c0985f7ef2f4c886d82741ff8812c2c6fec03ab..0fa857c916aad65b063b3b279ef038b7a8686693 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -313,13 +313,16 @@ Node SygusPbe::PbeTrie::addTerm(Node b, const std::vector<Node>& exOut)
 
 bool SygusPbe::hasExamples(Node e)
 {
-  if (isPbe()) {
-    e = d_tds->getSynthFunForEnumerator(e);
-    Assert(!e.isNull());
-    std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
-    if (itx == d_examples_invalid.end()) {
-      return d_examples.find(e) != d_examples.end();
-    }
+  e = d_tds->getSynthFunForEnumerator(e);
+  if (e.isNull())
+  {
+    // enumerator is not associated with synthesis function?
+    return false;
+  }
+  std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
+  if (itx == d_examples_invalid.end())
+  {
+    return d_examples.find(e) != d_examples.end();
   }
   return false;
 }
@@ -367,7 +370,6 @@ Node SygusPbe::getExampleOut(Node e, unsigned i)
 
 Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr)
 {
-  Assert(isPbe());
   Assert(!e.isNull());
   if (d_tds->isVariableAgnosticEnumerator(e))
   {
@@ -379,20 +381,44 @@ Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr)
   Assert(!e.isNull());
   std::map<Node, bool>::iterator itx = d_examples_invalid.find(ee);
   if (itx == d_examples_invalid.end()) {
-    // compute example values with the I/O utility
     std::vector<Node> vals;
     Trace("sygus-pbe-debug")
         << "Compute examples " << bvr << "..." << std::endl;
-    d_sygus_unif[ee].computeExamples(e, bvr, vals);
+    if (d_is_pbe)
+    {
+      // Compute example values with the I/O utility, which ensures they are
+      // not later recomputed when the enumerated term is given the I/O utility.
+      d_sygus_unif[ee].computeExamples(e, bvr, vals);
+    }
+    else
+    {
+      // If the I/O utility is not enabled (if the conjecture is not PBE),
+      // compute them separately. This handles the case when all applications
+      // of a function-to-synthesize are applied to constant arguments but
+      // the conjecture is not PBE.
+      TypeNode etn = e.getType();
+      std::vector<std::vector<Node>>& exs = d_examples[ee];
+      for (size_t i = 0, esize = exs.size(); i < esize; i++)
+      {
+        Node res = d_tds->evaluateBuiltin(etn, bvr, exs[i]);
+        vals.push_back(res);
+      }
+    }
     Assert(vals.size() == d_examples[ee].size());
     Trace("sygus-pbe-debug") << "...got " << vals << std::endl;
     Trace("sygus-pbe-debug") << "Add to trie..." << std::endl;
     Node ret = d_pbe_trie[e][tn].addTerm(bvr, vals);
     Trace("sygus-pbe-debug") << "...got " << ret << std::endl;
-    if (ret != bvr)
+    if (d_is_pbe)
     {
-      Trace("sygus-pbe-debug") << "...clear example cache" << std::endl;
-      d_sygus_unif[ee].clearExampleCache(e, bvr);
+      // Clean up the cache data if necessary: if the enumerated term
+      // is redundant, its cached data will not be used later and thus should
+      // be cleared now.
+      if (ret != bvr)
+      {
+        Trace("sygus-pbe-debug") << "...clear example cache" << std::endl;
+        d_sygus_unif[ee].clearExampleCache(e, bvr);
+      }
     }
     Assert(ret.getType() == bvr.getType());
     return ret;

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 258fe017b7baed3da4e92896b3372b4bcb889862..2e6ca2659b525545cfc3a8c7ea9b5bfd4b4a1f64 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -153,32 +153,54 @@ class SygusPbe : public SygusModule
                            std::vector<Node>& lems) override;
   /** is PBE enabled for any enumerator? */
   bool isPbe() { return d_is_pbe; }
-  /** is the enumerator e associated with I/O example pairs? */
+  /**
+   * 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 e);
-  /** get number of I/O example pairs for enumerator e */
+  /** get number of examples for enumerator e */
   unsigned getNumExamples(Node e);
-  /** get the input arguments for i^th I/O example for e, which is added to the
-   * vector ex */
+  /**
+   * Get the input arguments for i^th example for e, which is added to the
+   * vector ex
+   */
   void getExample(Node e, unsigned i, std::vector<Node>& ex);
-  /** get the output value of the i^th I/O example for enumerator e */
+  /**
+   * 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 e, unsigned i);
 
   /** add the search val
-  * This function is called by the extension of quantifier-free datatypes
-  * procedure for SyGuS datatypes when we are considering a value of
-  * enumerator e of sygus type tn whose analog in the signature of builtin
-  * theory is bvr.
-  *
-  * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() ) and
-  * tn is a sygus datatype that encodes a subsignature of the integers.
-  *
-  * This returns either:
-  * - A SyGuS term whose analog is equivalent to bvr up to examples
-  *   In the above example,
-  *   it may return a term t of the form Plus( One(), x() ), such that this
-  *   function was previously called with t as input.
-  * - e, indicating that no previous terms are equivalent to e up to examples.
-  */
+   * This function is called by the extension of quantifier-free datatypes
+   * procedure for SyGuS datatypes or the SyGuS fast enumerator when we are
+   * considering a value of enumerator e of sygus type tn whose analog in the
+   * signature of builtin theory is bvr.
+   *
+   * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() )
+   * and tn is a sygus datatype that encodes a subsignature of the integers.
+   *
+   * This returns either:
+   * - A SyGuS term whose analog is equivalent to bvr up to examples
+   *   In the above example,
+   *   it may return a term t of the form Plus( One(), x() ), such that this
+   *   function was previously called with t as input.
+   * - e, indicating that no previous terms are equivalent to e up to examples.
+   *
+   * This method should only be called if hasExamples(e) returns true.
+   */
   Node addSearchVal(TypeNode tn, Node e, Node bvr);
   /** evaluate builtin
   * This returns the evaluation of bn on the i^th example for the

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 03d38df5ef114c0ea455de6053c7de70d91bcf8a..a046193421c7771d0dd9a073b3706052fab24676 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1804,6 +1804,7 @@ set(regress_1_tests
   regress1/sygus/phone-1-long.sy
   regress1/sygus/planning-unif.sy
   regress1/sygus/process-10-vars.sy
+  regress1/sygus/pLTL_5_trace.sy
   regress1/sygus/qe.sy
   regress1/sygus/qf_abv.smt2
   regress1/sygus/real-any-const.sy

diff --git a/test/regress/regress1/sygus/pLTL_5_trace.sy b/test/regress/regress1/sygus/pLTL_5_trace.sy
new file mode 100644 (file)
index 0000000..532a8f3
--- /dev/null
+++ b/test/regress/regress1/sygus/pLTL_5_trace.sy
@@ -0,0 +1,90 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
+(set-logic BV)
+
+;Trace length 
+(define-sort Stream () (_ BitVec 48))
+(define-fun ZERO () Stream (_ bv0 48))
+(define-fun ONE () Stream (_ bv1 48))
+
+
+(define-fun S_FALSE () Stream ZERO)
+(define-fun S_TRUE () Stream (bvnot S_FALSE))
+
+; Yesterday: X << 1
+(define-fun
+  Y ( (X Stream) ) Stream
+  (bvshl X ONE)
+)
+
+; Once: X|-X
+(define-fun
+  O ( (X Stream) ) Stream
+  (bvor X (bvneg X))
+)
+
+; Historically: X & ~(1 + X)
+(define-fun
+  H ( (X Stream) ) Stream
+  (bvand X (bvnot (bvadd ONE X)))
+)
+
+; Since: Z | (X & ~((X | Z) + Z))
+(define-fun
+S ( (X Stream) (Z Stream) ) Stream
+  (bvor Z
+    (bvand X 
+      (bvnot (bvadd  (bvor X Z) Z ))
+    )
+  )
+)
+
+(define-fun
+  bvimpl ( (X Stream) (Z Stream) ) Stream
+  (bvor (bvnot X) Z)
+)
+
+(synth-fun phi ((ulInformationTransfer Stream) (dlInformationTransfer Stream) (rrcConnectionReconfiguration Stream) (measurementReport Stream) (systemInformationBlockType1 Stream) (securityModeComplete Stream) (systemInformation Stream) (rrcConnectionReestablishmentReject Stream) (rrcConnectionRequest Stream) (rrcConnectionSetupComplete Stream) (rrcConnectionRelease Stream) (ueCapabilityInformation Stream) (rrcConnectionSetup Stream) (securityModeCommand Stream) (ueCapabilityEnquiry Stream) (rrcConnectionReconfigurationComplete Stream) (rrcConnectionReestablishmentRequest Stream)) Stream
+   ((<F> Stream))
+   ((<F> Stream (
+     S_TRUE 
+     S_FALSE
+     ( Variable Stream ) 
+     (bvnot <F>)
+     (bvand <F> <F>) 
+     (bvor <F> <F>)
+     (bvimpl <F> <F>)
+     (Y <F>)
+     (O <F>)
+     (H <F>)
+     (S <F> <F>)
+   )))
+)
+
+;; Positive examples
+;Positive Trace Data
+(constraint
+   (and
+    (= ((_ extract 8 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000000000000000000000000000000000000011000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 8 0) S_TRUE))
+    (= (phi #b000000000000000000000100000000100000000000000000 #b000000000000000000000010000000000000000000000000 #b000000101000000001010000000100000100001000100000 #b000000000100000000001000000000000010100000000000 #b000010000001000100000001000000010000000000000000 #b000000000000000000000000000000000000000000010000 #b001100000010111000000000110011000001000000000000 #b100000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000010000000 #b000001010000000010100000001000001000010001000000 #b010000000000000000000000000000000000000000000000) S_TRUE)
+    (= ((_ extract 15 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000010000010100000 #b000000000000000000000000000000000001100000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000001000000000000000 #b000000000000000000000000000000000000010000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000000100000101000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 15 0) S_TRUE))
+    (= ((_ extract 15 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000010001000000 #b000000000000000000000000000000000111000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000001000000000000000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000000000000000001010 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000100010000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 15 0) S_TRUE))
+    (= ((_ extract 20 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000001001001010100000 #b000000000000000000000000000000000000100000000000 #b000000000000000000000000000010000100000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000001100000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000100000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000010010010101000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 20 0) S_TRUE)) 
+   )
+)
+
+;; Negative examples
+
+;Negative Trace Data
+(constraint
+   (and
+    (not (= ((_ extract 6 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000110000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 6 0) S_TRUE)))
+    (not (= ((_ extract 45 0) (phi #b000000000000000000000001000000001000000000000000 #b000000000000000000000000100000000000000000000000 #b000000001010000000010100000001000001000010001000 #b000000000001000000000010000000000000101000000000 #b000000100000010001000000010000000100000000000000 #b000000000000000000000000000000000000000000000000 #b000011000000101110000000001100110000010000000000 #b001000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000010100000000101000000010000010000100010000 #b000100000000000000000000000000000000000000000000)) ((_ extract 45 0) S_TRUE)))
+    (not (= ((_ extract 13 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000100000101000 #b000000000000000000000000000000000000011000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000010000000000000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000010000000 #b000000000000000000000000000000000001000001010000 #b000000000000000000000000000000000000000000000000)) ((_ extract 13 0) S_TRUE)))
+    (not (= ((_ extract 13 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000100010000 #b000000000000000000000000000000000001110000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000010000000000000 #b000000000000000000000000000000000000000010000000 #b000000000000000000000000000000000000000000001010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000001000100000 #b000000000000000000000000000000000000000000000000)) ((_ extract 13 0) S_TRUE)))
+    (not (= ((_ extract 18 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000010010010101000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000100001000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000011000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000001000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000100100101010000 #b000000000000000000000000000000000000000000000000)) ((_ extract 18 0) S_TRUE))) 
+   )
+)
+
+; Solution: G (p -> O f) 
+(check-synth)