Fix rewrite rule synthesis for 0-ary operators (#8221)

Fixes cvc5/cvc5-projects#422.

Also changes the default setting for rewrite rule synthesis to check correct of rewrite rules by default.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 7bf0875fd6cbaf7708fcea4c707266b71edb22e4..660170c4d9ab4fb091b70e2aba1f1cf994e7b8e4 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1421,7 +1421,7 @@ name   = "Quantifiers"
   category   = "regular"
   long       = "sygus-rr-synth-check"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "use satisfiability check to verify correctness of candidate rewrites"
 
 [[option]]

diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 6386e402afd8898933aa7e3b800d8a5794fe00cc..6e752b853e4499d43981cc3bbe1e5365a71ad4a3 100644 (file)
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -24,6 +24,7 @@
 #include "options/quantifiers_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "printer/printer.h"
+#include "printer/smt2/smt2_printer.h"
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
@@ -156,6 +157,12 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   for (std::pair<const TypeNode, bool> tfp : typesFound)
   {
     TypeNode tn = tfp.first;
+    // we do not allocate variables for non-first class types, e.g. regular
+    // expressions
+    if (!tn.isFirstClass())
+    {
+      continue;
+    }
     // If we are not interested in purely propositional rewrites, we only
     // need to make one Boolean variable if the input has a Boolean variable.
     // This ensures that no type in our grammar has zero constructors. If
@@ -181,6 +188,8 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
       }
       varCounter++;
       Node v = nm->mkBoundVar(ssv.str(), tn);
+      Trace("srs-input") << "Make variable " << v << " of type " << tn
+                         << std::endl;
       tvars[tn].push_back(v);
       allVars.push_back(v);
       allVarTypes.push_back(tn);
@@ -286,20 +295,25 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     if (!ctt.isBoolean() || options().quantifiers.sygusRewSynthInputUseBool
         || ct.getKind() == BOUND_VARIABLE)
     {
-      Assert(tvars.find(ctt) != tvars.end())
-          << "Unexpected type " << ctt << " for " << ct;
-      for (const Node& v : tvars[ctt])
+      // may or may not have variables for this type
+      if (tvars.find(ctt) != tvars.end())
       {
-        std::stringstream ssc;
-        ssc << "C_" << i << "_" << v;
-        sdts[i].addConstructor(v, ssc.str(), argList);
+        for (const Node& v : tvars[ctt])
+        {
+          std::stringstream ssc;
+          ssc << "C_" << i << "_" << v;
+          sdts[i].addConstructor(v, ssc.str(), argList);
+        }
       }
     }
     // add the constructor for the operator if it is not a variable
     if (ct.getKind() != BOUND_VARIABLE)
     {
       Assert(!ct.isVar());
-      Node op = ct.hasOperator() ? ct.getOperator() : ct;
+      // note that some terms like re.allchar have operators despite having
+      // no children, we should take ct itself in these cases
+      Node op =
+          (ct.getNumChildren() > 0 && ct.hasOperator()) ? ct.getOperator() : ct;
       // iterate over the original term
       for (const Node& tc : t)
       {
@@ -341,6 +355,8 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
           argListc.push_back(arg);
           std::stringstream sscs;
           sscs << "C_factor_" << i << "_" << j;
+          Trace("srs-input-cons") << "Add (nested chain) " << lambdaOp << " "
+                                  << lambdaOp.getType() << std::endl;
           // ID function is not printed and does not count towards weight
           sdts[i].addConstructor(lambdaOp,
                                  sscs.str(),
@@ -355,12 +371,16 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
         argListc.push_back(recType);
         std::stringstream ssc;
         ssc << "C_" << i << "_rec_" << op;
+        Trace("srs-input-cons")
+            << "Add (chain) " << op << " " << op.getType() << std::endl;
         sdts[i].addConstructor(op, ssc.str(), argListc);
       }
       else
       {
         std::stringstream ssc;
         ssc << "C_" << i << "_" << op;
+        Trace("srs-input-cons")
+            << "Add " << op << " " << op.getType() << std::endl;
         sdts[i].addConstructor(op, ssc.str(), argList);
       }
     }
@@ -426,7 +446,8 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
         nm->mkDatatypeType(dttl, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
     tlGrammarTypes[t] = tlt;
     Trace("srs-input") << "Grammar is: " << std::endl;
-    Trace("srs-input") << tlt.getDType() << std::endl;
+    Trace("srs-input") << printer::smt2::Smt2Printer::sygusGrammarString(tlt)
+                       << std::endl;
   }
   Trace("srs-input") << "...finished." << std::endl;
 

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index bc5ab5f08dcb368e5c94487a6bacef8b3c38f889..ecfa76142338eee724b5b78df64b5709c78eb7f7 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -464,8 +464,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
 
   // cases where we need produce models
   if (!opts.smt.produceModels
-      && (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck
-          || usesSygus(opts)))
+      && (opts.smt.produceAssignments || usesSygus(opts)))
   {
     verbose(1) << "SolverEngine: turning on produce-models" << std::endl;
     opts.smt.produceModels = true;

diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index a1f66d24d0e2ff6c44a261daf26b8482cb96b98b..f9023ba62ecbced9c34211d1703d27a9cc10d9f4 100644 (file)
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -173,7 +173,8 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
     TypeNode gtn = g.getType();
     AlwaysAssert(gtn.isSubtypeOf(btn))
         << "Sygus datatype " << dt.getName()
-        << " encodes terms that are not of type " << btn << std::endl;
+        << " encodes terms that are not of type " << btn << std::endl
+        << "Due to " << g << " of type " << gtn << std::endl;
     Trace("sygus-db") << "...done register Operator #" << i << std::endl;
     Kind gk = g.getKind();
     if (gk == ITE)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 07883f373e6b6fe058a47e5c37ff7b8de5e86c0b..0fc41583d2377ffa215cd3b150fccf66016c99ab 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2663,6 +2663,7 @@ set(regress_1_tests
   regress1/sygus/issue4083-var-shadow.smt2
   regress1/sygus/issue4425-sets-sygus-infer.smt2
   regress1/sygus/issue7925-dt-share-config.sy
+  regress1/sygus/issue8216-rr-input-re.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/rr-verify/bv-term-32.sy b/test/regress/regress1/rr-verify/bv-term-32.sy
index 95296463b80f15a933221f597231cbefb6c011e6..4cf4e3488b11ea092ee16b3d2d829735be42b707 100644 (file)
--- a/test/regress/regress1/rr-verify/bv-term-32.sy
+++ b/test/regress/regress1/rr-verify/bv-term-32.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --no-sygus-rr-synth-check
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1

diff --git a/test/regress/regress1/sygus/issue8216-rr-input-re.smt2 b/test/regress/regress1/sygus/issue8216-rr-input-re.smt2
new file mode 100644 (file)
index 0000000..b9c1893
--- /dev/null
+++ b/test/regress/regress1/sygus/issue8216-rr-input-re.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --sygus-rr-synth-input --sygus-abort-size=1
+; SCRUBBER: grep -v -E '\(define-fun'
+; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
+; EXIT: 1
+(set-logic ALL)
+(declare-fun a () String)
+(assert (str.in_re (str.replace_re a (str.to_re "") a) (re.++ re.allchar (str.to_re "A"))))
+(check-sat)

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index fa573f5da2b24a57cafe0e32d258812fffd6bd7c..15b5accac324ae4965b259d543f4cc6affc895bc 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -3142,5 +3142,42 @@ TEST_F(TestApiBlackSolver, proj_issue431)
   ASSERT_THROW(slv.blockModelValues({t103}), CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSolver, proj_issue422)
+{
+  Solver slv;
+  slv.setOption("sygus-rr-synth-input", "true");
+  Sort s1 = slv.mkBitVectorSort(36);
+  Sort s2 = slv.getStringSort();
+  Term t1 = slv.mkConst(s2, "_x0");
+  Term t2 = slv.mkConst(s1, "_x1");
+  Term t11;
+  {
+    uint32_t bw = s1.getBitVectorSize();
+    std::string val(bw, '1');
+    val[0] = '0';
+    t11 = slv.mkBitVector(bw, val, 2);
+  }
+  Term t60 = slv.mkTerm(Kind::SET_SINGLETON, {t1});
+  Term t66 = slv.mkTerm(Kind::BITVECTOR_COMP, {t2, t11});
+  Term t92 = slv.mkRegexpAll();
+  Term t96 = slv.mkTerm(slv.mkOp(Kind::BITVECTOR_ZERO_EXTEND, 51), {t66});
+  Term t105 = slv.mkTerm(Kind::BITVECTOR_ADD, {t96, t96});
+  Term t113 = slv.mkTerm(Kind::BITVECTOR_SUB, {t105, t105});
+  Term t137 = slv.mkTerm(Kind::BITVECTOR_XOR, {t113, t105});
+  Term t211 = slv.mkTerm(Kind::BITVECTOR_SLTBV, {t137, t137});
+  Term t212 = slv.mkTerm(Kind::SET_MINUS, {t60, t60});
+  Term t234 = slv.mkTerm(Kind::SET_CHOOSE, {t212});
+  Term t250 = slv.mkTerm(Kind::STRING_REPLACE_RE_ALL, {t1, t92, t1});
+  Term t259 = slv.mkTerm(Kind::STRING_REPLACE_ALL, {t234, t234, t250});
+  Term t263 = slv.mkTerm(Kind::STRING_TOLOWER, {t259});
+  Term t272 = slv.mkTerm(Kind::BITVECTOR_SDIV, {t211, t66});
+  Term t276 = slv.mkTerm(slv.mkOp(Kind::BITVECTOR_ZERO_EXTEND, 71), {t272});
+  Term t288 = slv.mkTerm(Kind::EQUAL, {t263, t1});
+  Term t300 = slv.mkTerm(Kind::BITVECTOR_SLT, {t276, t276});
+  Term t301 = slv.mkTerm(Kind::EQUAL, {t288, t300});
+  slv.assertFormula({t301});
+  slv.push(4);
+}
+
 }  // namespace test
 }  // namespace cvc5