From: Andrew Reynolds Date: Fri, 4 Mar 2022 19:40:30 +0000 (-0600) Subject: Fix rewrite rule synthesis for 0-ary operators (#8221) X-Git-Tag: cvc5-1.0.0~323 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3bc29d4e86534f779f6d94d3cf947a2dded4566f;p=cvc5.git 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 7bf0875fd..660170c4d 100644 --- 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 6386e402a..6e752b853 100644 --- 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 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 bc5ab5f08..ecfa76142 100644 --- 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 a1f66d24d..f9023ba62 100644 --- 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 07883f373..0fc41583d 100644 --- 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 95296463b..4cf4e3488 100644 --- 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 index 000000000..b9c18934e --- /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 fa573f5da..15b5accac 100644 --- 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