From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 11 Mar 2020 22:54:07 +0000 (-0500)
Subject: Guard against null relevancy condition in SyGuS (#4033)
X-Git-Tag: cvc5-1.0.0~3508
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=98178c539c4eb502d3f3c3c4f1fcf0600d229b46;p=cvc5.git

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 76832e369..24288216f 100644
--- 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 07340841c..bfb6c0f39 100644
--- 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 efd378596..36b2718a3 100644
--- 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
index 000000000..a7c864544
--- /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)