From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 15 Feb 2022 18:14:13 +0000 (-0600) Subject: Support `try` and `all` reconstruction modes. (#8098) X-Git-Tag: cvc5-1.0.0~424 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fb7cc27d4ae39d224c739c912ccd76563f374999;p=cvc5.git Support `try` and `all` reconstruction modes. (#8098) This PR adds a simple procedure to quickly reconstruct Sygus terms that are already in the grammar. This new procedure fails if the terms are not in the grammar. --- diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 312fc606b..7bf0875fd 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -964,7 +964,7 @@ name = "Quantifiers" category = "regular" long = "sygus-si-rcons=MODE" type = "CegqiSingleInvRconsMode" - default = "ALL_LIMIT" + default = "ALL" help = "policy for reconstructing solutions for single invocation conjectures" help_mode = "Modes for reconstruction solutions while using single invocation techniques." [[option.mode.NONE]] @@ -975,7 +975,7 @@ name = "Quantifiers" help = "Try to reconstruct solutions in the original grammar when using single invocation techniques in an incomplete (fail-fast) manner." [[option.mode.ALL_LIMIT]] name = "all-limit" - help = "Try to reconstruct solutions in the original grammar, but termintate if a maximum number of rounds for reconstruction is exceeded." + help = "Try to reconstruct solutions in the original grammar, but terminate if a maximum number of rounds for reconstruction is exceeded." [[option.mode.ALL]] name = "all" help = "Try to reconstruct solutions in the original grammar. In this mode, we do not terminate until a solution is successfully reconstructed." diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 127edac52..7eff21314 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -339,7 +339,7 @@ Node CegSingleInv::getSolution(size_t sol_index, sol = sol.substitute( vars.begin(), vars.end(), sygusVars.begin(), sygusVars.end()); sol = reconstructToSyntax(sol, stn, reconstructed, rconsSygus); - return s.getKind() == LAMBDA + return !sol.isNull() && s.getKind() == LAMBDA ? NodeManager::currentNM()->mkNode(LAMBDA, s[0], sol) : sol; } diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp index 01454786a..e5f3f398e 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp @@ -10,12 +10,14 @@ * directory for licensing information. * **************************************************************************** * - * Implementation for reconstruct. + * Implementation for Sygus reconstruct. */ #include "theory/quantifiers/sygus/sygus_reconstruct.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" +#include "options/quantifiers_options.h" #include "smt/command.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/rewriter.h" @@ -49,30 +51,71 @@ Node SygusReconstruct::reconstructSolution(Node sol, initialize(stn); - /** a set of builtin terms to reconstruct satisfied for each sygus datatype */ - TypeBuiltinSetMap termsToRecons; - // add the main obligation to the set of obligations // paramaters stn and sol constitute the main obligation to satisfy d_obs.push_back(std::make_unique(stn, sol)); - termsToRecons[stn].emplace(sol); d_stnInfo[stn].setBuiltinToOb(sol, d_obs[0].get()); RConsObligation* ob0 = d_obs[0].get(); Node k0 = ob0->getSkolem(); + if (options().quantifiers.cegqiSingleInvReconstruct + == cvc5::options::CegqiSingleInvRconsMode::TRY) + { + fast(sol, stn, reconstructed); + } + else + { + main(sol, stn, reconstructed, enumLimit); + } + + if (Trace("sygus-rcons").isConnected()) + { + RConsObligation::printCandSols(ob0, d_obs); + printPool(); + } + + // if the main obligation is solved, return the solution + if (!d_sol[k0].isNull()) + { + reconstructed = 1; + // The algorithm mostly works with rewritten terms and may not notice that + // the original terms contain variables eliminated by the rewriter. For + // example, rewrite((ite true 0 z)) = 0. In such cases, we replace those + // variables with ground values. + return d_sol[k0].isConst() ? Node(d_sol[k0]) : mkGround(d_sol[k0]); + } + + // we ran out of elements, return null + reconstructed = -1; + warning() << CommandFailure( + "Cannot get synth function: reconstruction to syntax failed."); + return Node::null(); +} + +void SygusReconstruct::main(Node sol, + TypeNode stn, + int8_t& reconstructed, + uint64_t enumLimit) +{ + bool noLimit = options().quantifiers.cegqiSingleInvReconstruct + == cvc5::options::CegqiSingleInvRconsMode::ALL; + + // Skolem of the main obligation + Node k0 = d_obs[0]->getSkolem(); + + // a set of builtin terms to reconstruct for each sygus datatype + TypeBuiltinSetMap termsToRecons; + termsToRecons[stn].emplace(sol); + + uint64_t count = 0; + // We need to add the main obligation to the crd in case it cannot be broken // down by matching. By doing so, we can solve the obligation using // enumeration and crd (if it is in the grammar) d_stnInfo[stn].addTerm(sol); - // the set of unique (up to rewriting) patterns/shapes in the grammar used by - // matching - std::unordered_map> pool; - - uint64_t count = 0; - - // algorithm - while (d_sol[k0].isNull() && count < enumLimit) + // procedure + while (d_sol[k0].isNull() && (noLimit || count < enumLimit)) { // enumeration phase // a temporary set of new terms to reconstruct cached for processing in the @@ -115,7 +158,7 @@ Node SygusReconstruct::reconstructSolution(Node sol, { // then, this is a new term and we should add it to pool d_poolTrie.addTerm(builtin); - pool[pair.first].push_back(sz); + d_pool[pair.first].push_back(sz); for (const Node& t : pair.second) { RConsObligation* ob = d_stnInfo[pair.first].builtinToOb(t); @@ -138,7 +181,7 @@ Node SygusReconstruct::reconstructSolution(Node sol, while (!termsToReconsPrime.empty()) { // a temporary set of new terms to reconstruct cached for later processing - TypeBuiltinSetMap obsDPrime; + TypeBuiltinSetMap termsToReconsDPrime; for (const std::pair& pair : termsToReconsPrime) { @@ -149,7 +192,7 @@ Node SygusReconstruct::reconstructSolution(Node sol, if (d_sol[ob->getSkolem()].isNull()) { Trace("sygus-rcons") << "ob: " << *ob << std::endl; - for (const Node& sz : pool[pair.first]) + for (const Node& sz : d_pool[pair.first]) { // try to match each newly generated and cached term with patterns // in pool @@ -157,42 +200,109 @@ Node SygusReconstruct::reconstructSolution(Node sol, // cache the new terms for later processing for (const std::pair& tempPair : temp) { - obsDPrime[tempPair.first].insert(tempPair.second.cbegin(), - tempPair.second.cend()); + termsToReconsDPrime[tempPair.first].insert( + tempPair.second.cbegin(), tempPair.second.cend()); } } } } } - termsToReconsPrime = std::move(obsDPrime); + termsToReconsPrime = std::move(termsToReconsDPrime); } // remove reconstructed terms from termsToRecons removeReconstructedTerms(termsToRecons); ++count; } +} - if (Trace("sygus-rcons").isConnected()) +void SygusReconstruct::fast(Node sol, TypeNode stn, int8_t& reconstructed) +{ + NodeManager* nm = NodeManager::currentNM(); + + Assert(stn.isDatatype()); + Assert(stn.getDType().isSygus()); + SygusTypeInfo sti; + sti.initialize(d_tds, stn); + std::vector stns; + sti.getSubfieldTypes(stns); + std::map varCount; + + // add the constructors for each sygus datatype to the pool + for (const TypeNode& cstn : stns) { - RConsObligation::printCandSols(ob0, d_obs); - printPool(pool); + for (const std::shared_ptr& cons : + cstn.getDType().getConstructors()) + { + if (cons->getNumArgs() == 0) + { + // just like in the main procedure, add no-argument constructors + // directly to the crd + Node sz = nm->mkNode(Kind::APPLY_CONSTRUCTOR, cons->getConstructor()); + Node builtin = datatypes::utils::sygusToBuiltin(sz); + Node rep = d_stnInfo[cstn].addTerm(builtin); + RConsObligation* ob = d_stnInfo[cstn].builtinToOb(rep); + // check if the enumerated term solves an obligation + if (ob == nullptr) + { + // if not, create an "artifical" obligation whose solution would be + // the enumerated term + d_obs.push_back(std::make_unique(cstn, builtin)); + d_stnInfo[cstn].setBuiltinToOb(builtin, d_obs.back().get()); + ob = d_obs.back().get(); + } + // mark the obligation as solved + markSolved(ob, sz); + } + else + { + std::vector args; + args.push_back(cons->getConstructor()); + // populate each constructor argument with a free variable of the + // corresponding type + for (const std::shared_ptr& arg : cons->getArgs()) + { + args.push_back(d_tds->getFreeVarInc(arg->getRangeType(), varCount)); + } + Node sz = nm->mkNode(Kind::APPLY_CONSTRUCTOR, args); + d_pool[cstn].push_back(sz); + } + } } - // if the main obligation is solved, return the solution - if (!d_sol[k0].isNull()) + // a set of builtin terms to reconstruct for each sygus datatype + TypeBuiltinSetMap termsToRecons; + termsToRecons[stn].emplace(sol); + + // match phase of the rcons procedure + while (!termsToRecons.empty()) { - reconstructed = 1; - // The algorithm mostly works with rewritten terms and may not notice that - // the original terms contain variables eliminated by the rewriter. For - // example, rewrite((ite true 0 z)) = 0. In such cases, we replace those - // variables with ground values. - return d_sol[k0].isConst() ? Node(d_sol[k0]) : mkGround(d_sol[k0]); + // a temporary set of new terms to reconstruct cached for later processing + TypeBuiltinSetMap termsToReconsPrime; + for (const std::pair& pair : termsToRecons) + { + for (const Node& t : pair.second) + { + RConsObligation* ob = d_stnInfo[pair.first].builtinToOb(t); + if (d_sol[ob->getSkolem()].isNull()) + { + Trace("sygus-rcons") << "ob: " << *ob << std::endl; + for (const Node& sz : d_pool[pair.first]) + { + // try to match each newly generated and cached term with patterns + // in pool + TypeBuiltinSetMap temp = matchNewObs(t, sz); + // cache the new terms for later processing + for (const std::pair& tempPair : temp) + { + termsToReconsPrime[tempPair.first].insert( + tempPair.second.cbegin(), tempPair.second.cend()); + } + } + } + } + } + termsToRecons = std::move(termsToReconsPrime); } - - // we ran out of elements, return null - reconstructed = -1; - warning() << CommandFailure( - "Cannot get synth function: reconstruction to syntax failed."); - return Node::null(); } TypeBuiltinSetMap SygusReconstruct::matchNewObs(Node t, Node sz) @@ -470,15 +580,15 @@ void SygusReconstruct::clear() d_subObs.clear(); d_parentOb.clear(); d_sygusVars.clear(); + d_pool.clear(); d_poolTrie.clear(); } -void SygusReconstruct::printPool( - const std::unordered_map>& pool) const +void SygusReconstruct::printPool() const { Trace("sygus-rcons") << std::endl << "Pool:" << std::endl << '{'; - for (const std::pair>& pair : pool) + for (const std::pair>& pair : d_pool) { Trace("sygus-rcons") << std::endl << " " << pair.first << ':' << std::endl diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h index dca68844f..cda856259 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.h +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -176,6 +176,29 @@ class SygusReconstruct : public expr::NotifyMatch, protected EnvObj uint64_t enumLimit); private: + /** + * Implements the reconstruction procedure. + * + * @param sol the target term + * @param stn the sygus datatype type encoding the syntax restrictions + * @param reconstructed the flag to update, set to 1 if we successfully return + * a node, otherwise it is set to -1 + * @param enumLimit a value to limit the effort spent by this class (roughly + * equal to the number of intermediate terms to try) + */ + void main(Node sol, TypeNode stn, int8_t& reconstructed, uint64_t enumLimit); + + /** + * Implements the match phase of the reconstruction procedure with the pool + * prepopulated with sygus datatype type constructors (grammar rules). + * + * @param sol the target term + * @param stn the sygus datatype type encoding the syntax restrictions + * @param reconstructed the flag to update, set to 1 if we successfully return + * a node, otherwise it is set to -1 + */ + void fast(Node sol, TypeNode stn, int8_t& reconstructed); + /** Match builtin term `t` with pattern `sz`. * * This function matches the builtin term to reconstruct `t` with the builtin @@ -293,11 +316,8 @@ class SygusReconstruct : public expr::NotifyMatch, protected EnvObj * Print the pool of patterns/shape used in the matching phase. * * \note requires enabling "sygus-rcons" trace - * - * @param pool a pool of patterns/shapes to print */ - void printPool( - const std::unordered_map>& pool) const; + void printPool() const; /** pointer to the sygus term database */ TermDbSygus* d_tds; @@ -320,6 +340,9 @@ class SygusReconstruct : public expr::NotifyMatch, protected EnvObj /** a cache of sygus variables treated as ground terms by matching */ std::unordered_map d_sygusVars; + /** a set of unique (up to rewriting) patterns/shapes in the grammar used by + * matching */ + std::unordered_map> d_pool; /** A trie for filtering out redundant terms from the paterns pool */ expr::MatchTrie d_poolTrie; }; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8d9af1db5..9d925f97c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2592,6 +2592,10 @@ set(regress_1_tests regress1/sygus/list-head-x.sy regress1/sygus/list_recursor.sy regress1/sygus/logiccell_help.sy + regress1/sygus/max-all.sy + regress1/sygus/max-limit.sy + regress1/sygus/max-try1.sy + regress1/sygus/max-try2.sy regress1/sygus/max.sy regress1/sygus/max2-bv.sy regress1/sygus/multi-fun-polynomial2.sy diff --git a/test/regress/regress1/sygus/max-all.sy b/test/regress/regress1/sygus/max-all.sy new file mode 100644 index 000000000..aaf0e3bf0 --- /dev/null +++ b/test/regress/regress1/sygus/max-all.sy @@ -0,0 +1,21 @@ +; COMMAND-LINE: --sygus-si=all --sygus-si-rcons-limit=0 --sygus-out=status +; EXPECT: unsat + +(set-logic LIA) + +(synth-fun max ((x Int) (y Int)) Int + ((Start Int) (StartBool Bool)) + ((Start Int (0 1 x y + (+ Start Start) + (- Start Start) + (ite StartBool Start Start))) + (StartBool Bool ((and StartBool StartBool) + (not StartBool) + (<= Start Start))))) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (max x y) (ite (<= x y) y x))) + +(check-synth) diff --git a/test/regress/regress1/sygus/max-limit.sy b/test/regress/regress1/sygus/max-limit.sy new file mode 100644 index 000000000..da5b3a1a0 --- /dev/null +++ b/test/regress/regress1/sygus/max-limit.sy @@ -0,0 +1,23 @@ +; COMMAND-LINE: --sygus-si=all --sygus-si-rcons=all-limit --sygus-si-rcons-limit=0 --sygus-out=status +; ERROR-SCRUBBER: grep -o "reconstruction to syntax failed." +; EXPECT-ERROR: reconstruction to syntax failed. +; EXPECT: unknown + +(set-logic LIA) + +(synth-fun max ((x Int) (y Int)) Int + ((Start Int) (StartBool Bool)) + ((Start Int (0 1 x y + (+ Start Start) + (- Start Start) + (ite StartBool Start Start))) + (StartBool Bool ((and StartBool StartBool) + (not StartBool) + (<= Start Start))))) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (max x y) (ite (<= x y) y x))) + +(check-synth) diff --git a/test/regress/regress1/sygus/max-try1.sy b/test/regress/regress1/sygus/max-try1.sy new file mode 100644 index 000000000..8c1153ba0 --- /dev/null +++ b/test/regress/regress1/sygus/max-try1.sy @@ -0,0 +1,15 @@ +; COMMAND-LINE: --sygus-si=all --sygus-si-rcons=try --sygus-out=status +; EXPECT: unsat + +(set-logic LIA) + +(synth-fun sum ((x Int) (y Int)) Int + ((Start Int)) + ((Start Int (0 1 x y (+ Start Start))))) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (sum x y) (+ x y))) + +(check-synth) diff --git a/test/regress/regress1/sygus/max-try2.sy b/test/regress/regress1/sygus/max-try2.sy new file mode 100644 index 000000000..f57c3d1be --- /dev/null +++ b/test/regress/regress1/sygus/max-try2.sy @@ -0,0 +1,14 @@ +; COMMAND-LINE: --sygus-si=all --sygus-si-rcons=try --sygus-out=status +; ERROR-SCRUBBER: grep -o "reconstruction to syntax failed." +; EXPECT-ERROR: reconstruction to syntax failed. +; EXPECT: unknown + +(set-logic LIA) + +(synth-fun two () Int + ((Start Int)) + ((Start Int (0 1 (+ Start Start))))) + +(constraint (= two 2)) + +(check-synth) diff --git a/test/regress/regress1/sygus/simple-rewrite-not-in-db.sy b/test/regress/regress1/sygus/simple-rewrite-not-in-db.sy index 04d35fa71..5b4dbbee1 100644 --- a/test/regress/regress1/sygus/simple-rewrite-not-in-db.sy +++ b/test/regress/regress1/sygus/simple-rewrite-not-in-db.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-si=all --sygus-si-rcons-limit=10000 --sygus-out=status +; COMMAND-LINE: --sygus-si=all --sygus-out=status ; EXPECT: unsat (set-logic UF)