Support default sygus grammar for strings (#3148)

5 files changed, 72 insertions, 3 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 00d040af5..3fbb4eaee 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -363,17 +363,27 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
                                            d_single_inv_arg_sk.begin(),
                                            d_single_inv_arg_sk.end());
     Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv << std::endl;
-    if( options::cbqiPreRegInst() && d_single_inv.getKind()==FORALL ){
+    // check whether we can handle this quantified formula
+    CegHandledStatus status = CegInstantiator::isCbqiQuant(d_single_inv);
+    if( status<CEG_HANDLED )
+    {
+      Trace("cegqi-si") << "...do not invoke single invocation techniques since the quantified formula does not have a handled counterexample-guided instantiation strategy!" << std::endl;
+      d_single_invocation = false;
+      d_single_inv = Node::null();
+    }
+    else if( options::cbqiPreRegInst() && d_single_inv.getKind()==FORALL ){
       //just invoke the presolve now
       d_cinst->presolve( d_single_inv );
     }
-  }else{
+  }
+  if( !d_single_invocation )
+  {
     d_single_inv = Node::null();
     Trace("cegqi-si") << "Formula is not single invocation." << std::endl;
     if (options::cegqiSingleInvAbort())
     {
       std::stringstream ss;
-      ss << "Property is not single invocation." << std::endl;
+      ss << "Property is not handled by single invocation." << std::endl;
       throw LogicException(ss.str());
     }
   }
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index bcd0d709e..bb8da59da 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -420,6 +420,12 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor(
         collectSygusGrammarTypesFor(
             TypeNode::fromType(arrayType.getConstituentType()), types);
       }
+      else if (range.isString() )
+      {
+        // theory of strings shares the integer type
+        TypeNode intType = NodeManager::currentNM()->integerType();
+        collectSygusGrammarTypesFor(intType,types);
+      }
     }
   }
 }
@@ -670,6 +676,31 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         weights[i].push_back(-1);
       }
     }
+    else if (types[i].isString())
+    {
+      // concatenation
+      ops[i].push_back(nm->operatorOf(STRING_CONCAT).toExpr());
+      cnames[i].push_back(kindToString(STRING_CONCAT));
+      cargs[i].push_back(std::vector<Type>());
+      cargs[i].back().push_back(unres_t);
+      cargs[i].back().push_back(unres_t);
+      pcs[i].push_back(nullptr);
+      weights[i].push_back(-1);
+      // length
+      TypeNode intType = nm->integerType();
+      Assert(std::find(types.begin(),types.end(),intType)!=types.end());
+      unsigned i_intType = std::distance(
+          types.begin(),
+          std::find(types.begin(),
+                    types.end(),
+                    intType));
+      ops[i_intType].push_back(nm->operatorOf(STRING_LENGTH).toExpr());
+      cnames[i_intType].push_back(kindToString(STRING_LENGTH));
+      cargs[i_intType].push_back(std::vector<Type>());
+      cargs[i_intType].back().push_back(unres_t);
+      pcs[i_intType].push_back(nullptr);
+      weights[i_intType].push_back(-1);
+    }
     else if (types[i].isArray())
     {
       ArrayType arrayType = static_cast<ArrayType>(types[i].toType());
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 99b464d09..19e5fa899 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1696,6 +1696,7 @@ set(regress_1_tests
   regress1/sygus/real-grammar.sy
   regress1/sygus/simple-regexp.sy
   regress1/sygus/stopwatch-bt.sy
+  regress1/sygus/strings-no-syntax.sy
   regress1/sygus/strings-concat-3-args.sy
   regress1/sygus/strings-double-rec.sy
   regress1/sygus/strings-small.sy
@@ -1833,6 +1834,7 @@ set(regress_2_tests
   regress2/sygus/process-10-vars-2fun.sy
   regress2/sygus/process-arg-invariance.sy
   regress2/sygus/real-grammar-neg.sy
+  regress2/sygus/strings-no-syntax-len.sy
   regress2/sygus/three.sy
   regress2/sygus/vcb.sy
   regress2/typed_v1l50016-simp.cvc
diff --git a/test/regress/regress1/sygus/strings-no-syntax.sy b/test/regress/regress1/sygus/strings-no-syntax.sy
new file mode 100644
index 000000000..4959d6fe1
--- /dev/null
+++ b/test/regress/regress1/sygus/strings-no-syntax.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+
+(synth-fun f ((x String) (y String)) String)
+
+(declare-var x String)
+(declare-var y String)
+
+(constraint (>= (str.len (f x y)) (str.len x)))
+(constraint (>= (str.len (f x y)) (str.len y)))
+
+(check-synth)
diff --git a/test/regress/regress2/sygus/strings-no-syntax-len.sy b/test/regress/regress2/sygus/strings-no-syntax-len.sy
new file mode 100644
index 000000000..22048f1ec
--- /dev/null
+++ b/test/regress/regress2/sygus/strings-no-syntax-len.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+
+(synth-fun f ((x String)) Int)
+
+(declare-var x String)
+(constraint (>= (f (str.++ "A" x)) (f x)))
+(constraint (= (f "A") 2))
+(constraint (= (f "BB") 4))
+(constraint (= (f "BCB") 6))
+
+(check-synth)