Fix fast SyGuS enumeration for interpreted constants (#3501)

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 472a82e299588fa24fee695da7683d33cf07f2e4..e4c23977e3c13afc21767c344554a766db4b3532 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -996,6 +996,10 @@ bool SygusEnumerator::TermEnumMasterInterp::initialize(SygusEnumerator* se,
 Node SygusEnumerator::TermEnumMasterInterp::getCurrent() { return *d_te; }
 bool SygusEnumerator::TermEnumMasterInterp::increment()
 {
+  if (d_te.isFinished())
+  {
+    return false;
+  }
   SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
   Node curr = getCurrent();
   tc.addTerm(curr);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e7252834ee690f34abe20cab0ff37003f8d67748..e4b5b8057fa1ecb224c0068e4705e28249182387 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1736,6 +1736,7 @@ set(regress_1_tests
   regress1/sygus/nia-max-square-ns.sy
   regress1/sygus/no-flat-simp.sy
   regress1/sygus/no-mention.sy
+  regress1/sygus/once_2.sy
   regress1/sygus/only-const-grammar.sy
   regress1/sygus/parity-si-rcons.sy
   regress1/sygus/pbe_multi.sy

diff --git a/test/regress/regress1/sygus/once_2.sy b/test/regress/regress1/sygus/once_2.sy
new file mode 100644 (file)
index 0000000..af6d56a
--- /dev/null
+++ b/test/regress/regress1/sygus/once_2.sy
@@ -0,0 +1,44 @@
+; EXPECT: unsat
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic BV)
+
+(define-sort Stream () (_ BitVec 2))
+
+(define-fun BV_ONE () Stream (_ bv1 2))
+
+(define-fun
+  O ( (X Stream) ) Stream
+  (bvneg (bvand X (bvnot (bvsub X BV_ONE))))
+)
+
+(synth-fun op ((x Stream)) Stream
+  (( y_term Stream))
+  (( y_term Stream (
+    ( Constant Stream)
+    ( Variable Stream)
+    ( bvnot y_term )
+    ( bvand y_term y_term )
+    ( bvor y_term y_term )
+    ( bvneg y_term )
+    ( bvadd y_term y_term )
+    ( bvsub y_term y_term )
+    ( bvmul y_term y_term )
+    ( bvudiv y_term y_term )
+    ( bvurem y_term y_term )
+    ( bvshl y_term y_term )
+    ( bvlshr y_term y_term )
+  ))
+))
+
+(define-fun C ((x Stream)) Bool
+  (= (op x) (O x))
+)
+
+(constraint (and
+(C (_ bv0 2))
+(C (_ bv1 2))
+(C (_ bv2 2))
+(C (_ bv3 2))
+))
+
+(check-synth)