Guard against null relevancy condition in SyGuS (#4033)

Fixes #4025.

Also makes our sygus default grammar for strings (slightly) better by including a dummy character, which is required for solving the regression added by this PR. A more robust (but unintuitive to the user) solution would be to include str.from_code( Start_Int ).

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 76832e3696d914cf2f83f2a7ee7fea344f9add6e..24288216fdfa474d423f41adf6d8e754101e6b4e 100644 (file)
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -388,10 +388,15 @@ void SygusExtension::assertTesterInternal( int tindex, TNode n, Node exp, std::v
 }
 
 Node SygusExtension::getRelevancyCondition( Node n ) {
+  if (!options::sygusSymBreakRlv())
+  {
+    return Node::null();
+  }
   std::map< Node, Node >::iterator itr = d_rlv_cond.find( n );
   if( itr==d_rlv_cond.end() ){
     Node cond;
-    if( n.getKind()==APPLY_SELECTOR_TOTAL && options::sygusSymBreakRlv() ){
+    if (n.getKind() == APPLY_SELECTOR_TOTAL)
+    {
       TypeNode ntn = n[0].getType();
       const DType& dt = ntn.getDType();
       Node sel = n.getOperator();
@@ -1502,7 +1507,10 @@ void SygusExtension::incrementCurrentSearchSize( Node m, std::vector< Node >& le
                 for (const Node& lem : it->second)
                 {
                   Node slem = lem.substitute(x, t, cache);
-                  slem = nm->mkNode(OR, rlv, slem);
+                  if (!rlv.isNull())
+                  {
+                    slem = nm->mkNode(OR, rlv, slem);
+                  }
                   lemmas.push_back(slem);
                 }
               }

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 07340841cbc650f34cab85ca51f69cf3b3045c81..bfb6c0f3973686ac2472ae63c0cb682941e8a31b 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -408,6 +408,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
   else if (type.isString())
   {
     ops.push_back(nm->mkConst(String("")));
+    // dummy character "A"
+    ops.push_back(nm->mkConst(String("A")));
   }
   else if (type.isArray() || type.isSet())
   {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index efd378596e7db620efb5919378cef87384dd0a9b..36b2718a3573a267a6932593a74eb041bf8f67dd 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1858,6 +1858,7 @@ set(regress_1_tests
   regress1/sygus/issue3944-div-rewrite.smt2
   regress1/sygus/issue3947-agg-miniscope.smt2
   regress1/sygus/issue4009-qep.smt2
+  regress1/sygus/issue4025-no-rlv-cond.smt2
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy

diff --git a/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2
new file mode 100644 (file)
index 0000000..a7c8645
--- /dev/null
+++ b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL)
+(set-option :sygus-inference true)
+(set-option :sygus-sym-break false)
+(set-option :sygus-sym-break-lazy false)
+(set-option :sygus-sym-break-rlv false)
+(set-info :status sat)
+(declare-fun s () String)
+(assert (distinct s ""))
+(check-sat)