This PR modifies the rcons algorithm to loop over terms to reconstruct instead of obligations. It also modifies the Obs data structure to reflect this change. The rest of the PR is mostly updating documentation and refactoring the affected code.
theory/quantifiers/sygus/example_infer.h
theory/quantifiers/sygus/example_min_eval.cpp
theory/quantifiers/sygus/example_min_eval.h
- theory/quantifiers/sygus/rcons_obligation_info.cpp
- theory/quantifiers/sygus/rcons_obligation_info.h
+ theory/quantifiers/sygus/rcons_obligation.cpp
+ theory/quantifiers/sygus/rcons_obligation.h
theory/quantifiers/sygus/rcons_type_info.cpp
theory/quantifiers/sygus/rcons_type_info.h
theory/quantifiers/sygus/sygus_abduct.cpp
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * RConsObligation class implementation.
+ */
+
+#include "rcons_obligation.h"
+
+#include <sstream>
+
+#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
+#include "theory/datatypes/sygus_datatype_utils.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+RConsObligation::RConsObligation(TypeNode stn, Node t) : d_ts({t})
+{
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+ d_k = sm->mkDummySkolem("sygus_rcons", stn);
+}
+
+TypeNode RConsObligation::getType() const { return d_k.getType(); }
+
+Node RConsObligation::getSkolem() const { return d_k; }
+
+void RConsObligation::addBuiltin(Node builtin) { d_ts.emplace(builtin); }
+
+const std::unordered_set<Node>& RConsObligation::getBuiltins() const
+{
+ return d_ts;
+}
+
+void RConsObligation::addCandidateSolution(Node candSol)
+{
+ d_candSols.emplace(candSol);
+}
+
+const std::unordered_set<Node>& RConsObligation::getCandidateSolutions() const
+{
+ return d_candSols;
+}
+
+void RConsObligation::addCandidateSolutionToWatchSet(Node candSol)
+{
+ d_watchSet.emplace(candSol);
+}
+
+const std::unordered_set<Node>& RConsObligation::getWatchSet() const
+{
+ return d_watchSet;
+}
+
+void RConsObligation::printCandSols(
+ const RConsObligation* root,
+ const std::vector<std::unique_ptr<RConsObligation>>& obs)
+{
+ std::unordered_set<Node> visited;
+ std::vector<const RConsObligation*> stack;
+ stack.push_back(root);
+ Trace("sygus-rcons") << std::endl << "Eq classes: " << std::endl << '[';
+
+ while (!stack.empty())
+ {
+ const RConsObligation* curr = stack.back();
+ stack.pop_back();
+ visited.emplace(curr->getSkolem());
+
+ Trace("sygus-rcons") << std::endl
+ << " " << *curr << std::endl
+ << " {" << std::endl;
+
+ for (const Node& candSol : curr->getCandidateSolutions())
+ {
+ Trace("sygus-rcons") << " "
+ << datatypes::utils::sygusToBuiltin(candSol)
+ << std::endl;
+ std::unordered_set<TNode> vars;
+ expr::getVariables(candSol, vars);
+ for (TNode var : vars)
+ {
+ if (visited.find(var) == visited.cend())
+ for (const std::unique_ptr<RConsObligation>& ob : obs)
+ {
+ if (ob->getSkolem() == var)
+ {
+ stack.push_back(ob.get());
+ }
+ }
+ }
+ }
+ Trace("sygus-rcons") << " }" << std::endl;
+ }
+
+ Trace("sygus-rcons") << ']' << std::endl;
+}
+
+std::ostream& operator<<(std::ostream& out, const RConsObligation& ob)
+{
+ out << '(' << ob.getType() << ", " << ob.getSkolem() << ", {";
+ std::unordered_set<Node>::const_iterator it = ob.getBuiltins().cbegin();
+ out << *it;
+ ++it;
+ while (it != ob.getBuiltins().cend())
+ {
+ out << ", " << *it;
+ ++it;
+ }
+ out << "})";
+ return out;
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Utility class for Sygus Reconstruct module.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_H
+#define CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_H
+
+#include "expr/node.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * A class for holding Sygus Reconstruct obligations. An obligation is a builtin
+ * term t and a SyGuS type T, and indicates that we are trying to build a term
+ * of type T whose builtin analog is equivalent to t. This class encodes each
+ * obligation (T, t) as a skolem k of type T to embed obligations in candidate
+ * solutions (see d_candSols below). Notice that the SyGuS type T of an
+ * obligation is not stored in this class as it can be inferred from the type of
+ * the skolem k.
+ */
+class RConsObligation
+{
+ public:
+ /**
+ * Constructor. Default value needed for maps.
+ *
+ * @param stn sygus datatype type to reconstruct `t` into
+ * @param t builtin term to reconstruct
+ */
+ RConsObligation(TypeNode stn, Node t);
+
+ /**
+ * @return sygus datatype type to reconstruct equivalent builtin terms into
+ */
+ TypeNode getType() const;
+
+ /**
+ * @return skolem representing this obligation
+ */
+ Node getSkolem() const;
+
+ /**
+ * Add `t` to the set of equivalent builtins this obligation solves.
+ *
+ * \note `t` MUST be equivalent to the builtin terms in `d_ts`
+ *
+ * @param t builtin term to add
+ */
+ void addBuiltin(Node t);
+
+ /**
+ * @return equivalent builtin terms to reconstruct for this obligation
+ */
+ const std::unordered_set<Node>& getBuiltins() const;
+
+ /**
+ * Add candidate solution to the set of candidate solutions for the
+ * corresponding obligation.
+ *
+ * @param candSol the candidate solution to add
+ */
+ void addCandidateSolution(Node candSol);
+
+ /**
+ * @return set of candidate solutions for this obligation
+ */
+ const std::unordered_set<Node>& getCandidateSolutions() const;
+
+ /**
+ * Add candidate solution to the set of candidate solutions waiting for the
+ * corresponding obligation to be solved.
+ *
+ * @param candSol the candidate solution to add to watch set
+ */
+ void addCandidateSolutionToWatchSet(Node candSol);
+
+ /**
+ * @return set of candidate solutions waiting for this obligation to be solved
+ */
+ const std::unordered_set<Node>& getWatchSet() const;
+
+ /**
+ * Print all reachable obligations and their candidate solutions from
+ * the `root` obligation and its candidate solutions.
+ *
+ * An obligation is reachable from the `root` obligation if it is the `root`
+ * obligation or is needed by one of the candidate solutions of other
+ * reachable obligations.
+ *
+ * For example, if we have:
+ *
+ * Obs = [(k1, {(+ 1 (- x))}, (k2, (- x)), (k3, x), (k4, 0)]
+ * CandSols = {k1 -> {(c_+ c_1 k2)}, k2 -> {(c_- k3)},
+ * k3 -> {c_x}, k4 -> {c_0}}
+ * root = k1
+ *
+ * Then, the set of reachable obligations from `root` is {k1, k2, k3}
+ *
+ * \note requires enabling "sygus-rcons" trace
+ *
+ * @param root the root obligation to start from
+ * @param obs a list of obligations containing at least 1 obligation
+ * @param
+ */
+ static void printCandSols(
+ const RConsObligation* root,
+ const std::vector<std::unique_ptr<RConsObligation>>& obs);
+
+ private:
+ /** Skolem representing this obligation used to embed obligations in candidate
+ * solutions. */
+ Node d_k;
+ /** Equivalent builtin terms for this obligation.
+ *
+ * To solve the obligation, one of these builtin terms must be reconstructed
+ * in the specified grammar (sygus datatype type) of the obligation.
+ */
+ std::unordered_set<Node> d_ts;
+ /** A set of candidate solutions to this obligation.
+ *
+ * Each candidate solution is a sygus datatype term containing skolem subterms
+ * (sub-obligations). By replacing all sub-obligations with their
+ * corresponding solutions, we get a term whose builtin analog rewrites to
+ * a term in `d_ts` and hence solves this obligation. For example, given:
+ * d_ts = {(+ x y)}
+ * a possible set of candidate solutions would be:
+ * d_candSols = {(c_+ k1 k2), (c_+ c_x k2), (c_+ k1 c_y), (c_+ c_x c_y)}
+ * where k1 and k2 are skolems. Notice that `d_candSols` may contain a
+ * pure term that solves the obligation ((c_+ c_x c_y) in this example).
+ */
+ std::unordered_set<Node> d_candSols;
+ /** A set of candidate solutions waiting for this obligation to be solved.
+ *
+ * In the example above, (c_+ k1 k2) and (c_+ c_x k2) are in the watch-set of
+ * k2. Similarly, (c_+ k1 k2) and (c_+ k1 c_y) are in the watch-set of k1.
+ */
+ std::unordered_set<Node> d_watchSet;
+};
+
+/**
+ * Print obligation `ob` into the given output stream `out`
+ *
+ * @param out the output stream to print `ob` into
+ * @param ob the obligation to print
+ * @return a reference to the given output stream `out`
+ */
+std::ostream& operator<<(std::ostream& out, const RConsObligation& ob);
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
+
+#endif // CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_H
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Abdalrhman Mohamed
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Reconstruct Obligation Info class implementation.
- */
-
-#include "rcons_obligation_info.h"
-
-#include <sstream>
-
-#include "expr/node_algorithm.h"
-#include "theory/datatypes/sygus_datatype_utils.h"
-
-namespace cvc5 {
-namespace theory {
-namespace quantifiers {
-
-RConsObligationInfo::RConsObligationInfo(Node builtin) : d_builtins({builtin})
-{
-}
-
-const std::unordered_set<Node>& RConsObligationInfo::getBuiltins() const
-{
- return d_builtins;
-}
-
-void RConsObligationInfo::addCandidateSolution(Node candSol)
-{
- d_candSols.emplace(candSol);
-}
-
-void RConsObligationInfo::addBuiltin(Node builtin)
-{
- d_builtins.emplace(builtin);
-}
-
-const std::unordered_set<Node>& RConsObligationInfo::getCandidateSolutions()
- const
-{
- return d_candSols;
-}
-
-void RConsObligationInfo::addCandidateSolutionToWatchSet(Node candSol)
-{
- d_watchSet.emplace(candSol);
-}
-
-const std::unordered_set<Node>& RConsObligationInfo::getWatchSet() const
-{
- return d_watchSet;
-}
-
-std::string RConsObligationInfo::obToString(Node k,
- const RConsObligationInfo& obInfo)
-{
- std::stringstream ss;
- ss << "([";
- std::unordered_set<Node>::const_iterator it = obInfo.getBuiltins().cbegin();
- ss << *it;
- ++it;
- while (it != obInfo.getBuiltins().cend())
- {
- ss << ", " << *it;
- ++it;
- }
- ss << "]), " << k.getType() << ')' << std::endl;
- return ss.str();
-}
-
-void RConsObligationInfo::printCandSols(
- const Node& root,
- const std::unordered_map<Node, RConsObligationInfo>& obInfo)
-{
- std::unordered_set<Node> visited;
- std::vector<Node> stack;
- stack.push_back(root);
-
- Trace("sygus-rcons") << "\nEq classes: \n[";
-
- while (!stack.empty())
- {
- const Node& k = stack.back();
- stack.pop_back();
- visited.emplace(k);
-
- Trace("sygus-rcons") << std::endl
- << datatypes::utils::sygusToBuiltin(k) << " "
- << obToString(k, obInfo.at(k)) << ":\n [";
-
- for (const Node& j : obInfo.at(k).getCandidateSolutions())
- {
- Trace("sygus-rcons") << datatypes::utils::sygusToBuiltin(j) << " ";
- std::unordered_set<TNode> subObs;
- expr::getVariables(j, subObs);
- for (const TNode& l : subObs)
- {
- if (visited.find(l) == visited.cend()
- && obInfo.find(l) != obInfo.cend())
- {
- stack.push_back(l);
- }
- }
- }
- Trace("sygus-rcons") << "]" << std::endl;
- }
-
- Trace("sygus-rcons") << "]" << std::endl;
-}
-
-} // namespace quantifiers
-} // namespace theory
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Abdalrhman Mohamed
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Utility class for Sygus Reconstruct module.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
-#define CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
-
-#include "expr/node.h"
-
-namespace cvc5 {
-namespace theory {
-namespace quantifiers {
-
-/**
- * A utility class for Sygus Reconstruct obligations. An obligation is a builtin
- * term t and a SyGuS type T, and indicates that we are trying to build a term
- * of type T whose builtin analog is equivalent to t. The main algorithm encodes
- * each obligation (t, T) as a skolem k of type T to embed obligations in
- * candidate solutions (see d_candSols below). It mainly operates over skolems
- * and stores cooresponding builtin terms and other info in instances of this
- * class. Notice that the SyGuS type T of an obligation is not stored in this
- * class as it can be inferred from the type of the skolem k.
- */
-class RConsObligationInfo
-{
- public:
- /**
- * Constructor. Default value needed for maps.
- *
- * @param builtin builtin term to reconstruct
- */
- explicit RConsObligationInfo(Node builtin = Node::null());
-
- /**
- * Add `builtin` to the set of equivalent builtins this class' obligation
- * solves.
- *
- * \note `builtin` MUST be equivalent to the builtin terms in `d_builtins`
- *
- * @param builtin builtin term to add
- */
- void addBuiltin(Node builtin);
-
- /**
- * @return equivalent builtin terms to reconstruct for this class' obligation
- */
- const std::unordered_set<Node>& getBuiltins() const;
-
- /**
- * Add candidate solution to the set of candidate solutions for the
- * corresponding obligation.
- *
- * @param candSol the candidate solution to add
- */
- void addCandidateSolution(Node candSol);
-
- /**
- * @return set of candidate solutions for this class' obligation
- */
- const std::unordered_set<Node>& getCandidateSolutions() const;
-
- /**
- * Add candidate solution to the set of candidate solutions waiting for the
- * corresponding obligation to be solved.
- *
- * @param candSol the candidate solution to add to watch set
- */
- void addCandidateSolutionToWatchSet(Node candSol);
-
- /**
- * @return set of candidate solutions waiting for this class' obligation
- * to be solved
- */
- const std::unordered_set<Node>& getWatchSet() const;
-
- /**
- * Return a string representation of an obligation.
- *
- * @param k An obligation
- * @param obInfo Obligation `k`'s info
- * @return A string representation of `k`
- */
- static std::string obToString(Node k, const RConsObligationInfo& obInfo);
-
- /**
- * Print all reachable obligations and their candidate solutions from
- * the `root` obligation and its candidate solutions.
- *
- * An obligation is reachable from the `root` obligation if it is the `root`
- * obligation or is needed by one of the candidate solutions of other
- * reachable obligations.
- *
- * For example, if we have:
- *
- * Obs = {c_z1, c_z2, c_z3, c_z4} // list of obligations in rcons algorithm
- * CandSols = {c_z1 -> {(c_+ c_1 c_z2)}, c_z2 -> {(c_- c_z3)},
- * c_z3 -> {c_x}, c_z4 -> {}}
- * root = c_z1
- *
- * Then, the set of reachable obligations from `root` is {c_z1, c_z2, c_z3}
- *
- * \note requires enabling "sygus-rcons" trace
- *
- * @param root The root obligation to start from
- * @param obInfo a map from obligations to their corresponding infos
- */
- static void printCandSols(
- const Node& root,
- const std::unordered_map<Node, RConsObligationInfo>& obInfo);
-
- private:
- /** Equivalent builtin terms for this class' obligation.
- *
- * To solve the obligation, one of these builtin terms must be reconstructed
- * in the specified grammar (sygus datatype type) of the obligation.
- */
- std::unordered_set<Node> d_builtins;
- /** A set of candidate solutions to this class' obligation.
- *
- * Each candidate solution is a sygus datatype term containing skolem subterms
- * (sub-obligations). By replacing all sub-obligations with their
- * corresponding solutions, we get a term whose builtin analog rewrites to
- * `d_builtin` and hence solves this obligation. For example, given:
- * d_builtin = (+ x y)
- * a possible set of candidate solutions would be:
- * d_candSols = {(c_+ c_z1 c_z2), (c_+ c_x c_z2), (c_+ c_z1 c_y),
- * (c_+ c_x c_y)}
- * where c_z1 and c_z2 are skolems. Notice that `d_candSols` may contain a
- * pure term that solves the obligation ((c_+ c_x c_y) in this example).
- */
- std::unordered_set<Node> d_candSols;
- /** A set of candidate solutions waiting for this class' obligation to
- * be solved.
- *
- * In the example above, (c_+ c_z1 c_z2) and (c_+ c_x c_z2) are in
- * the watch-set of c_z2. Similarly, (c_+ c_z1 c_z2) and (c_+ c_z1 c_y) are in
- * the watch-set of c_z1.
- */
- std::unordered_set<Node> d_watchSet;
-};
-
-} // namespace quantifiers
-} // namespace theory
-} // namespace cvc5
-
-#endif // CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
#include "expr/skolem_manager.h"
#include "theory/datatypes/sygus_datatype_utils.h"
+#include "theory/quantifiers/sygus/rcons_obligation.h"
namespace cvc5 {
namespace theory {
return d_crd->addTerm(n, false, out);
}
-void RConsTypeInfo::setBuiltinToOb(Node builtin, Node ob)
+void RConsTypeInfo::setBuiltinToOb(Node t, RConsObligation* ob)
{
- d_ob[builtin] = ob;
+ d_ob.emplace(t, ob);
}
-Node RConsTypeInfo::builtinToOb(Node builtin) { return d_ob[builtin]; }
+RConsObligation* RConsTypeInfo::builtinToOb(Node t)
+{
+ auto it = d_ob.find(t);
+ if (it != d_ob.cend())
+ {
+ return it->second;
+ }
+ return nullptr;
+}
} // namespace quantifiers
} // namespace theory
namespace theory {
namespace quantifiers {
+class RConsObligation;
+
/**
* A utility class for Sygus Reconstruct datatype types (grammar non-terminals).
* This class is mainly responsible for enumerating sygus datatype type terms
/**
* Set the obligation responsible for solving the given builtin term.
*
- * @param builtin The builtin term
+ * @param t The builtin term
* @param ob The corresponding obligation
*/
- void setBuiltinToOb(Node builtin, Node ob);
+ void setBuiltinToOb(Node t, RConsObligation* ob);
/**
* Return the obligation responsible for solving the given builtin term.
*
- * @param builtin The builtin term
+ * @param t The builtin term
* @return The corresponding obligation
*/
- Node builtinToOb(Node builtin);
+ RConsObligation* builtinToOb(Node t);
private:
/** Sygus terms enumerator for this class' Sygus datatype type */
* possible to have multiple obligations to reconstruct the same builtin term
* from different sygus datatype types.
*/
- std::unordered_map<Node, Node> d_ob;
+ std::unordered_map<Node, RConsObligation*> d_ob;
};
} // namespace quantifiers
#include "theory/quantifiers/sygus/sygus_reconstruct.h"
#include "expr/node_algorithm.h"
-#include "expr/skolem_manager.h"
#include "smt/command.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/rewriter.h"
initialize(stn);
- NodeManager* nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
+ /** a set of builtin terms to reconstruct satisfied for each sygus datatype */
+ TypeBuiltinSetMap termsToRecons;
- /** a set of obligations that are not yet satisfied for each sygus datatype */
- TypeObligationSetMap unsolvedObs;
-
- // paramaters sol and stn constitute the main obligation to satisfy
- Node mainOb = sm->mkDummySkolem("sygus_rcons", stn);
-
- // add the main obligation to the set of obligations that are not yet
- // satisfied
- unsolvedObs[stn].emplace(mainOb);
- d_obInfo.emplace(mainOb, RConsObligationInfo(sol));
- d_stnInfo[stn].setBuiltinToOb(sol, mainOb);
+ // 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<RConsObligation>(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();
// 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
uint64_t count = 0;
// algorithm
- while (d_sol[mainOb].isNull() && count < enumLimit)
+ while (d_sol[k0].isNull() && count < enumLimit)
{
// enumeration phase
- // a temporary set of new obligations cached for processing in the match
- // phase
- TypeObligationSetMap obsPrime;
- for (const std::pair<const TypeNode, ObligationSet>& pair : unsolvedObs)
+ // a temporary set of new terms to reconstruct cached for processing in the
+ // match phase
+ TypeBuiltinSetMap termsToReconsPrime;
+ for (const std::pair<const TypeNode, BuiltinSet>& pair : termsToRecons)
{
// enumerate a new term
Trace("sygus-rcons") << "enum: " << stn << ": ";
if (sz.isConst())
{
Node rep = d_stnInfo[pair.first].addTerm(builtin);
- Node k = d_stnInfo[pair.first].builtinToOb(rep);
+ RConsObligation* ob = d_stnInfo[pair.first].builtinToOb(rep);
// check if the enumerated term solves an obligation
- if (k.isNull())
+ if (ob == nullptr)
{
// if not, create an "artifical" obligation whose solution would be
// the enumerated term
- k = sm->mkDummySkolem("sygus_rcons", pair.first);
- d_obInfo.emplace(k, RConsObligationInfo(builtin));
- d_stnInfo[pair.first].setBuiltinToOb(builtin, k);
+ d_obs.push_back(
+ std::make_unique<RConsObligation>(pair.first, builtin));
+ d_stnInfo[pair.first].setBuiltinToOb(builtin, d_obs.back().get());
+ ob = d_obs.back().get();
}
// mark the obligation as solved
- markSolved(k, sz);
+ markSolved(ob, sz);
// Since we added the term to the candidate rewrite database, there is
// no point in adding it to the pool too
continue;
// then, this is a new term and we should add it to pool
d_poolTrie.addTerm(builtin);
pool[pair.first].push_back(sz);
- for (Node k : pair.second)
+ for (const Node& t : pair.second)
{
- if (d_sol[k].isNull())
+ RConsObligation* ob = d_stnInfo[pair.first].builtinToOb(t);
+ if (d_sol[ob->getSkolem()].isNull())
{
- Trace("sygus-rcons")
- << "ob: " << RConsObligationInfo::obToString(k, d_obInfo[k])
- << std::endl;
- // try to match obligation k with the enumerated term sz
- TypeObligationSetMap temp = matchNewObs(k, sz);
+ Trace("sygus-rcons") << "ob: " << *ob << std::endl;
+ // try to match builtin term `t` with the enumerated term sz
+ TypeBuiltinSetMap temp = matchNewObs(t, sz);
// cache the new obligations for processing in the match phase
- for (const std::pair<const TypeNode, ObligationSet>& tempPair :
- temp)
+ for (const std::pair<const TypeNode, BuiltinSet>& tempPair : temp)
{
- obsPrime[tempPair.first].insert(tempPair.second.cbegin(),
- tempPair.second.cend());
+ termsToReconsPrime[tempPair.first].insert(
+ tempPair.second.cbegin(), tempPair.second.cend());
}
}
}
}
}
// match phase
- while (!obsPrime.empty())
+ while (!termsToReconsPrime.empty())
{
- // a temporary set of new obligations cached for later processing
- TypeObligationSetMap obsDPrime;
- for (const std::pair<const TypeNode, ObligationSet>& pair : obsPrime)
+ // a temporary set of new terms to reconstruct cached for later processing
+ TypeBuiltinSetMap obsDPrime;
+ for (const std::pair<const TypeNode, BuiltinSet>& pair :
+ termsToReconsPrime)
{
- for (const Node& k : pair.second)
+ for (const Node& t : pair.second)
{
- unsolvedObs[pair.first].emplace(k);
- if (d_sol[k].isNull())
+ termsToRecons[pair.first].emplace(t);
+ RConsObligation* ob = d_stnInfo[pair.first].builtinToOb(t);
+ if (d_sol[ob->getSkolem()].isNull())
{
- Trace("sygus-rcons")
- << "ob: " << RConsObligationInfo::obToString(k, d_obInfo[k])
- << std::endl;
- for (Node sz : pool[pair.first])
+ Trace("sygus-rcons") << "ob: " << *ob << std::endl;
+ for (const Node& sz : pool[pair.first])
{
- // try to match each newly generated and cached obligation
- // with patterns in pool
- TypeObligationSetMap temp = matchNewObs(k, sz);
- // cache the new obligations for later processing
- for (const std::pair<const TypeNode, ObligationSet>& tempPair :
- temp)
+ // 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<const TypeNode, BuiltinSet>& tempPair : temp)
{
obsDPrime[tempPair.first].insert(tempPair.second.cbegin(),
tempPair.second.cend());
}
}
}
- obsPrime = std::move(obsDPrime);
+ termsToReconsPrime = std::move(obsDPrime);
}
- // remove solved obligations from unsolvedObs
- removeSolvedObs(unsolvedObs);
+ // remove reconstructed terms from termsToRecons
+ removeReconstructedTerms(termsToRecons);
++count;
}
if (Trace("sygus-rcons").isConnected())
{
- RConsObligationInfo::printCandSols(mainOb, d_obInfo);
+ RConsObligation::printCandSols(ob0, d_obs);
printPool(pool);
}
// if the main obligation is solved, return the solution
- if (!d_sol[mainOb].isNull())
+ 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[mainOb].isConst() ? Node(d_sol[mainOb])
- : mkGround(d_sol[mainOb]);
+ 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 d_sol[mainOb];
+ return Node::null();
}
-TypeObligationSetMap SygusReconstruct::matchNewObs(Node k, Node sz)
+TypeBuiltinSetMap SygusReconstruct::matchNewObs(Node t, Node sz)
{
- NodeManager* nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
- TypeObligationSetMap obsPrime;
+ TypeBuiltinSetMap termsToReconsPrime;
- // obligations generated by match. Note that we might have already seen (and
- // even solved) those obligations, hence the name "candidate obligations"
- std::unordered_map<Node, Node> candObs;
+ // substitutions generated by match. Note that we might have already seen (and
+ // even solved) obligations corresponsing to those substitutions
+ NodePairMap matches;
// the builtin terms corresponding to sygus variables in the grammar are bound
// variables. However, we want the `match` method to treat them as ground
// terms. So, we add redundant substitutions
- candObs.insert(d_sygusVars.cbegin(), d_sygusVars.cend());
+ matches.insert(d_sygusVars.cbegin(), d_sygusVars.cend());
- // try to match the obligation's builtin terms with the pattern sz
- for (Node builtin : d_obInfo[k].getBuiltins())
+ // try to match the builtin term with the pattern sz
+ if (expr::match(
+ Rewriter::rewrite(datatypes::utils::sygusToBuiltin(sz)), t, matches))
{
- if (expr::match(Rewriter::rewrite(datatypes::utils::sygusToBuiltin(sz)),
- builtin,
- candObs))
+ // the bound variables z generated by the enumerators are reused across
+ // enumerated terms, so we need to replace them with our own skolems
+ NodePairMap subs;
+ Trace("sygus-rcons") << "-- ct: " << sz << std::endl;
+ // remove redundant substitutions
+ for (const std::pair<const Node, Node>& pair : d_sygusVars)
+ {
+ matches.erase(pair.first);
+ }
+ // for each match
+ for (const std::pair<const Node, Node>& match : matches)
{
- // the bound variables z generated by the enumerators are reused across
- // enumerated terms, so we need to replace them with our own skolems
- std::vector<std::pair<Node, Node>> subs;
- Trace("sygus-rcons") << "-- ct: " << sz << std::endl;
- // remove redundant substitutions
- for (const std::pair<const Node, Node>& pair : d_sygusVars)
+ TypeNode stn = datatypes::utils::builtinVarToSygus(match.first).getType();
+ RConsObligation* newOb;
+ // did we come across an equivalent obligation before?
+ Node rep = d_stnInfo[stn].addTerm(match.second);
+ RConsObligation* repOb = d_stnInfo[stn].builtinToOb(rep);
+ if (repOb != nullptr)
{
- candObs.erase(pair.first);
+ // if so, use the original obligation
+ newOb = repOb;
+ // while `match.second` is equivalent to `rep`, it may be easier to
+ // reconstruct than `rep`. For example:
+ //
+ // Grammar: S -> p | q | (not S) | (and S S) | (or S S)
+ // rep = (= p q)
+ // match.second = (or (and p q) (and (not p) (not q)))
+ //
+ // In this case, `match.second` is easy to reconstruct by matching
+ // because it only uses operators that are already in the grammar.
+ // `rep`, on the other hand, cannot be reconstructed by matching and
+ // can only be solved by enumeration (currently).
+ //
+ // At this point, we do not know which one is easier to reconstruct by
+ // matching, so we add `match.second` to the set of equivalent builtin
+ // terms in `repOb` and match against both terms.
+ if (repOb->getBuiltins().find(match.second)
+ == repOb->getBuiltins().cend())
+ {
+ repOb->addBuiltin(match.second);
+ d_stnInfo[stn].setBuiltinToOb(match.second, repOb);
+ termsToReconsPrime[stn].emplace(match.second);
+ }
}
- // for each candidate obligation
- for (const std::pair<const Node, Node>& candOb : candObs)
+ else
{
- TypeNode stn =
- datatypes::utils::builtinVarToSygus(candOb.first).getType();
- Node newVar;
- // did we come across an equivalent obligation before?
- Node rep = d_stnInfo[stn].addTerm(candOb.second);
- Node repOb = d_stnInfo[stn].builtinToOb(rep);
- if (!repOb.isNull())
+ // otherwise, create a new obligation of the corresponding sygus type
+ d_obs.push_back(std::make_unique<RConsObligation>(stn, match.second));
+ d_stnInfo[stn].setBuiltinToOb(match.second, d_obs.back().get());
+ newOb = d_obs.back().get();
+ // if the match is a constant and the grammar allows random constants
+ if (match.second.isConst() && stn.getDType().getSygusAllowConst())
{
- // if so, use the original obligation
- newVar = repOb;
- // while `candOb.second` is equivalent to `rep`, it may be easier to
- // reconstruct than `rep`. For example:
- //
- // Grammar: S -> p | q | (not S) | (and S S) | (or S S)
- // rep = (= p q)
- // candOb.second = (or (and p q) (and (not p) (not q)))
- //
- // In this case, `candOb.second` is easy to reconstruct by matching
- // because it only uses operators that are already in the grammar.
- // `rep`, on the other hand, is cannot be reconstructed by matching
- // and can only be solved by enumeration (currently).
- //
- // At this point, we do not know which one is easier to reconstruct by
- // matching, so we add `candOb.second` to the set of equivalent
- // builtin terms corresponding to `k` and match against both terms.
- d_obInfo[repOb].addBuiltin(candOb.second);
- d_stnInfo[stn].setBuiltinToOb(candOb.second, repOb);
+ // then immediately solve the obligation
+ markSolved(newOb, d_tds->getProxyVariable(stn, match.second));
}
else
{
- // otherwise, create a new obligation of the corresponding sygus type
- newVar = sm->mkDummySkolem("sygus_rcons", stn);
- d_obInfo.emplace(newVar, candOb.second);
- d_stnInfo[stn].setBuiltinToOb(candOb.second, newVar);
- // if the candidate obligation is a constant and the grammar allows
- // random constants
- if (candOb.second.isConst()
- && k.getType().getDType().getSygusAllowConst())
- {
- // then immediately solve the obligation
- markSolved(newVar, d_tds->getProxyVariable(stn, candOb.second));
- }
- else
- {
- // otherwise, add this candidate obligation to this list of
- // obligations
- obsPrime[stn].emplace(newVar);
- }
+ // otherwise, add this match to the list of obligations
+ termsToReconsPrime[stn].emplace(match.second);
}
- subs.emplace_back(datatypes::utils::builtinVarToSygus(candOb.first),
- newVar);
}
- // replace original free vars in sz with new ones
- if (!subs.empty())
- {
- sz = sz.substitute(subs.cbegin(), subs.cend());
- }
- // sz is solved if it has no sub-obligations or if all of them are solved
- bool isSolved = true;
- for (const std::pair<Node, Node>& sub : subs)
+ subs.emplace(datatypes::utils::builtinVarToSygus(match.first),
+ newOb->getSkolem());
+ }
+ // replace original free vars in sz with new ones
+ if (!subs.empty())
+ {
+ sz = sz.substitute(subs.cbegin(), subs.cend());
+ }
+ // sz is solved if it has no sub-obligations or if all of them are solved
+ bool isSolved = true;
+ for (const std::pair<const Node, Node>& match : matches)
+ {
+ TypeNode stn = datatypes::utils::builtinVarToSygus(match.first).getType();
+ RConsObligation* ob = d_stnInfo[stn].builtinToOb(match.second);
+ if (d_sol[ob->getSkolem()].isNull())
{
- if (d_sol[sub.second].isNull())
- {
- isSolved = false;
- d_subObs[sz].push_back(sub.second);
- }
+ isSolved = false;
+ d_subObs[sz].push_back(ob);
}
+ }
- if (isSolved)
- {
- // As it traverses sz, substitute populates its input cache with TNodes
- // that are not preserved by this module and maybe destroyed after the
- // method call. To avoid referencing those unsafe TNodes throughout this
- // module, we pass a iterators of d_sol instead.
- Node s = sz.substitute(d_sol.cbegin(), d_sol.cend());
- markSolved(k, s);
- }
- else
- {
- // add sz as a possible solution to obligation k
- d_obInfo[k].addCandidateSolution(sz);
- d_parentOb[sz] = k;
- d_obInfo[d_subObs[sz].back()].addCandidateSolutionToWatchSet(sz);
- }
+ RConsObligation* ob = d_stnInfo[sz.getType()].builtinToOb(t);
+
+ if (isSolved)
+ {
+ // As it traverses sz, substitute populates its input cache with TNodes
+ // that are not preserved by this module and maybe destroyed after the
+ // method call. To avoid referencing those unsafe TNodes throughout this
+ // module, we pass a iterators of d_sol instead.
+ Node s = sz.substitute(d_sol.cbegin(), d_sol.cend());
+ markSolved(ob, s);
+ }
+ else
+ {
+ // add sz as a possible solution to ob
+ ob->addCandidateSolution(sz);
+ d_parentOb[sz] = ob;
+ d_subObs[sz].back()->addCandidateSolutionToWatchSet(sz);
}
}
- return obsPrime;
+ return termsToReconsPrime;
}
-void SygusReconstruct::markSolved(Node k, Node s)
+void SygusReconstruct::markSolved(RConsObligation* ob, Node s)
{
- // return if obligation k is already solved
- if (!d_sol[k].isNull())
+ // return if ob is already solved
+ if (!d_sol[ob->getSkolem()].isNull())
{
return;
}
Trace("sygus-rcons") << "builtin sol: " << datatypes::utils::sygusToBuiltin(s)
<< std::endl;
- // First, mark `k` as solved
- d_obInfo[k].addCandidateSolution(s);
- d_sol[k] = s;
- d_parentOb[s] = k;
+ // First, mark ob as solved
+ ob->addCandidateSolution(s);
+ d_sol[ob->getSkolem()] = s;
+ d_parentOb[s] = ob;
- std::vector<Node> stack;
- stack.push_back(k);
+ std::vector<RConsObligation*> stack;
+ stack.push_back(ob);
while (!stack.empty())
{
- Node curr = stack.back();
+ RConsObligation* curr = stack.back();
stack.pop_back();
// for each partial solution/parent of the now solved obligation `curr`
- for (Node parent : d_obInfo[curr].getWatchSet())
+ for (const Node& parent : curr->getWatchSet())
{
// remove `curr` and (possibly) other solved obligations from its list
// of children
while (!d_subObs[parent].empty()
- && !d_sol[d_subObs[parent].back()].isNull())
+ && !d_sol[d_subObs[parent].back()->getSkolem()].isNull())
{
d_subObs[parent].pop_back();
}
// corresponding obligation
// pass iterators of d_sol to avoid populating it with unsafe TNodes
Node parentSol = parent.substitute(d_sol.cbegin(), d_sol.cend());
- Node parentOb = d_parentOb[parent];
+ RConsObligation* parentOb = d_parentOb[parent];
// proceed only if parent obligation is not already solved
- if (d_sol[parentOb].isNull())
+ if (d_sol[parentOb->getSkolem()].isNull())
{
- d_obInfo[parentOb].addCandidateSolution(parentSol);
- d_sol[parentOb] = parentSol;
+ parentOb->addCandidateSolution(parentSol);
+ d_sol[parentOb->getSkolem()] = parentSol;
d_parentOb[parentSol] = parentOb;
// repeat the same process for the parent obligation
stack.push_back(parentOb);
{
// if it does have remaining children, add it to the watch list of one
// of them (picked arbitrarily)
- d_obInfo[d_subObs[parent].back()].addCandidateSolutionToWatchSet(
- parent);
+ d_subObs[parent].back()->addCandidateSolutionToWatchSet(parent);
}
}
}
}
}
-void SygusReconstruct::removeSolvedObs(TypeObligationSetMap& unsolvedObs)
+void SygusReconstruct::removeReconstructedTerms(
+ TypeBuiltinSetMap& termsToRecons)
{
- for (std::pair<const TypeNode, ObligationSet>& tempPair : unsolvedObs)
+ for (std::pair<const TypeNode, BuiltinSet>& pair : termsToRecons)
{
- ObligationSet::iterator it = tempPair.second.begin();
- while (it != tempPair.second.end())
+ BuiltinSet::iterator it = pair.second.begin();
+ while (it != pair.second.end())
{
- if (d_sol[*it].isNull())
+ if (d_sol[d_stnInfo[pair.first].builtinToOb(*it)->getSkolem()].isNull())
{
++it;
}
else
{
- it = tempPair.second.erase(it);
+ it = pair.second.erase(it);
}
}
}
void SygusReconstruct::clear()
{
- d_obInfo.clear();
+ d_obs.clear();
d_stnInfo.clear();
d_sol.clear();
d_subObs.clear();
void SygusReconstruct::printPool(
const std::unordered_map<TypeNode, std::vector<Node>>& pool) const
{
- Trace("sygus-rcons") << "\nPool:\n[";
+ Trace("sygus-rcons") << std::endl << "Pool:" << std::endl << '{';
for (const std::pair<const TypeNode, std::vector<Node>>& pair : pool)
{
- Trace("sygus-rcons") << std::endl << pair.first << ":\n[" << std::endl;
+ Trace("sygus-rcons") << std::endl
+ << " " << pair.first << ':' << std::endl
+ << " [" << std::endl;
for (const Node& sygusTerm : pair.second)
{
- Trace("sygus-rcons") << " "
+ Trace("sygus-rcons") << " "
<< Rewriter::rewrite(
datatypes::utils::sygusToBuiltin(sygusTerm))
.toString()
<< std::endl;
}
- Trace("sygus-rcons") << "]" << std::endl;
+ Trace("sygus-rcons") << " ]" << std::endl;
}
- Trace("sygus-rcons") << "]" << std::endl;
+ Trace("sygus-rcons") << '}' << std::endl;
}
} // namespace quantifiers
#include <map>
#include <vector>
-#include "theory/quantifiers/sygus/rcons_obligation_info.h"
+#include "theory/quantifiers/sygus/rcons_obligation.h"
#include "theory/quantifiers/sygus/rcons_type_info.h"
namespace cvc5 {
namespace theory {
namespace quantifiers {
-using ObligationSet = std::unordered_set<Node>;
-using TypeObligationSetMap = std::unordered_map<TypeNode, ObligationSet>;
+using BuiltinSet = std::unordered_set<Node>;
+using TypeBuiltinSetMap = std::unordered_map<TypeNode, BuiltinSet>;
/** SygusReconstruct
*
* the reconstructed term is equivalent to the original term and its syntax
* matches a specified grammar.
*
- * Goal: find a term g in sygus type T_0 that is equivalent to builtin term t_0.
+ * Goal: find a term g in sygus type T0 that is equivalent to builtin term t0.
*
- * rcons(t_0, T_0) returns g
+ * rcons(t0, T0) returns g
* {
- * Obs: A map from sygus types T to a set of triples to reconstruct into T,
- * where each triple is of the form (k, ts, s), where k is a skolem of
- * type T, ts is a set of builtin terms of the type encoded by T, and s
- * is a possibly null sygus term of type T representing the solution.
+ * Obs: A set of pairs to reconstruct into T, where each pair is of the form
+ * (k, ts), where k is a skolem of a sygus type T and ts is a set of
+ * builtin terms of the type encoded by T.
*
- * Sol: A map from skolems k to solutions s in the triples (k, ts, s). That
- * is, Sol[k] = s.
+ * Terms: A map from skolems k to a set of builtin terms in the pairs (k, ts).
+ * That is, Terms[k] = ts.
*
- * Terms: A map from skolems k to a set of builtin terms in the triples
- * (k, ts, s). That is, Terms[k] = ts
+ * Sol: A map from skolems k to (possibly null) sygus terms of type T
+ * representing solutions to the obligations.
*
* CandSols : A map from a skolem k to a set of possible solutions for its
* corresponding obligation. Whenever there is a successful match,
*
* Pool : A map from a sygus type T to a set of enumerated terms in T.
* The terms in this pool are patterns whose builtin analogs are used
- * for matching against the terms to reconstruct t in (k, t, s).
+ * for matching against the terms to reconstruct ts in (k, ts).
*
- * let k_0 be a fresh skolem of sygus type T_0
- * Obs[T_0] += (k_0, [t_0], null)
+ * let k0 be a fresh skolem of sygus type T0
+ * Obs[T0] += (k0, {t0})
*
- * while Sol[k_0] == null
- * Obs' = {} // map from T to sets of triples pending addition to Obs
+ * TermsToRecons[T0] = {t0}
+ *
+ * while Sol[k0] == null
+ * // map from T to terms pending addition to TermsToRecons
+ * TermsToRecons' = {}
* // enumeration phase
- * for each subfield type T of T_0
+ * for each subfield type T of T0
* // enumerated terms may contain variables zs ranging over all terms of
- * // their type (subfield types of T_0)
+ * // their type (subfield types of T0)
* s[zs] = nextEnum(T)
* if (s[zs] is ground)
* builtin = rewrite(toBuiltIn(s[zs]))
* // let X be the theory the solver is invoked with
- * find (k, ts, s) in Obs[T] s.t. |=_X ts[0] = builtin
- * if no such triple exists
- * let k be a new variable of type : T
- * Obs[T] += (k, [builtin], null)
- * markSolved(k, s[zs])
+ * find (k, ts) in Obs s.t. |=_X ts[0] = builtin
+ * if no such pair exists
+ * k = newVar(T)
+ * ts = {builtin}
+ * Obs += (k, ts)
+ * markSolved((k, ts), s[zs])
* else if no s' in Pool[T] and matcher sigma s.t.
* rewrite(toBuiltIn(s')) * sigma = rewrite(toBuiltIn(s[zs]))
* Pool[T] += s[zs]
- * for each (k, ts, null) in Obs[T]
- * Obs' += matchNewObs(k, s[zs])
+ * for each t in TermsToRecons[T]
+ * TermsToRecons' += matchNewObs(t, s[zs])
* // match phase
- * while Obs' != {}
- * Obs'' = {}
- * for each (k, ts, null) in Obs' // s = null for all triples in Obs'
- * Obs[T] += (k, ts, null)
- * for each s[zs] in Pool[T]
- * Obs'' += matchNewObs(k, s[zs])
- * Obs' = Obs''
- * g = Sol[k_0]
+ * while TermsToRecons' != {}
+ * TermsToRecons'' = {}
+ * for each subfield type T of T0
+ * for each t in TermsToRecons'[T]
+ * TermsToRecons'[T] += t
+ * for each s[zs] in Pool[T]
+ * TermsToRecons'' += matchNewObs(t, s[zs])
+ * TermsToRecons' = TermsToRecons''
+ * g = Sol[k0]
* instantiate free variables of g with arbitrary sygus datatype values
* }
*
- * matchNewObs(k, s[zs]) returns Obs'
+ * matchNewObs(t, s[zs]) returns TermsToRecons'
* {
* u = rewrite(toBuiltIn(s[zs]))
- * for each t in Terms[k]
- * if match(u, t) == {toBuiltin(zs) -> sts}
- * Sub = {} // substitution map from zs to corresponding new vars ks
- * for each (z, st) in {zs -> sts}
- * // let X be the theory the solver is invoked with
- * if exists (k', ts', s') in Obs[T] !=_X ts'[0] = st
- * ts' += st
- * Sub[z] = k'
- * else
- * let sk be a new variable of type : typeOf(z)
- * Sub[z] = sk
- * Obs'[typeOf(z)] += (sk, [st], null)
- * if Sol[sk] != null forall (z, sk) in Sub
- * markSolved(k, s{Sub})
+ * if match(u, t) == {toBuiltin(zs) -> sts}
+ * Sub = {} // substitution map from zs to corresponding new vars ks
+ * for each (z, st) in {zs -> sts}
+ * // let X be the theory the solver is invoked with
+ * if exists (k, ts) in Obs s.t. !=_X ts[0] = st
+ * ts += st
+ * Sub[z] = k
* else
- * CandSol[k] += s{Sub}
+ * sk = newVar(typeOf(z))
+ * Sub[z] = sk
+ * TermsToRecons'[typeOf(z)] += st
+ * if Sol[sk] != null forall (z, sk) in Sub
+ * markSolved(k, s{Sub})
+ * else
+ * CandSol[k] += s{Sub}
* }
*
- * markSolved(k, s)
+ * markSolved((k, ts), s)
* {
* if Sol[k] != null
* return
/**
* Constructor.
*
- * @param tds Database for sygus terms
- * @param s Statistics managed for the synth engine
+ * @param tds database for sygus terms
+ * @param s statistics managed for the synth engine
*/
SygusReconstruct(TermDbSygus* tds, SygusStatistics& s);
* Start -> (c_PLUS Start Start) | c_x | c_0 | c_1
* This method may return (c_PLUS c_x c_x) and set reconstructed to 1.
*
- * @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
+ * @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
+ * @param enumLimit a value to limit the effort spent by this class (roughly
* equal to the number of intermediate terms to try)
- * @return The reconstructed sygus term
+ * @return the reconstructed sygus term
*/
Node reconstructSolution(Node sol,
TypeNode stn,
uint64_t enumLimit);
private:
- /** Match obligation `k`'s builtin term with pattern `sz`.
+ /** Match builtin term `t` with pattern `sz`.
*
- * This function matches the builtin term to reconstruct for obligation `k`
- * with the builtin analog of the pattern `sz`. If the match succeeds, `sz` is
- * added to the set of candidate solutions for `k` and a set of new
- * sub-obligations to satisfy is returned. If there are no new sub-obligations
- * to satisfy, then `sz` is considered a solution to obligation `k` and
- * `matchNewObs(k, sz)` is called. For example, given:
+ * This function matches the builtin term to reconstruct `t` with the builtin
+ * analog of the pattern `sz`. If the match succeeds, `sz` is added to the set
+ * of candidate solutions for the obligation `ob` corresponding to the builtin
+ * term `t` and a set of new sub-terms to reconstruct is returned. If there
+ * are no new sub-terms to reconstruct, then `sz` is considered a solution to
+ * obligation `ob` and `markSolved(ob, sz)` is called. For example, given:
*
- * Obs[typeOf(c_z1)] = {(c_z1, (+ 1 1), null)}
- * Pool[typeOf(c_z1)] = {(c_+ c_z2 c_z3)}
+ * Obs = [(k0, {(+ 1 1)})]
+ * Pool[T0] = {(c_+ z1 z2)}
* CandSols = {}
*
- * Then calling `matchNewObs(c_z1, (c_+ c_z2 c_z3))` will result in:
+ * Then calling `matchNewObs((+ 1 1), (c_+ z1 z2))` will result in:
*
- * Obs[typeOf(c_z1)] = {(c_z1, (+ 1 1), null), (c_z4, 1, null)}
- * Pool[typeOf(c_z1)] = {(c_+ c_z2 c_z3)}
- * CandSols = {c_z1 -> {(c_+ c_z4 c_z4)}}
+ * Obs = [(k0, {(+ 1 1)}), (k1, {1})]
+ * Pool[T0] = {(c_+ z1 z2)}
+ * CandSols = {k0 -> {(c_+ k1 k1)}}
*
- * and will return `{typeOf(c_z4) -> {c_z4}}`.
+ * and will return `{T0 -> {1}}`.
*
- * Notice that `c_z2` and `c_z3` are not returned as new sub-obligations.
- * Instead, `(c_+ c_z2 c_z3)` is instantiated with a new skolem `c_z4`, which
- * is then added to the set of obligations. This is done to allow the reuse of
- * patterns in `Pool`. Also, notice that only one new skolem/sub-obligation is
- * generated. That's because the builtin analogs of `c_z2` and `c_z3` match
- * with the same builtin term `1`.
+ * Notice that the patterns/shapes in pool are generic, and thus, contain vars
+ * `z` as opposed to skolems `k`. Also, notice that `(c_+ z1 z2)` is
+ * instantiated with only one skolem `k1`, which is then added to the set of
+ * obligations. That's because the builtin analogs of `z1` and `z2` match with
+ * the same builtin term `1`.
*
- * @param k free var whose builtin term we need to match
- * @param sz a pattern to match `ob`s builtin term with
- * @return a set of new obligations to satisfy if the match succeeds
+ * @param t builtin term we need to reconstruct
+ * @param sz a pattern to match against `t`
+ * @return a set of new builtin terms to reconstruct if the match succeeds
*/
- TypeObligationSetMap matchNewObs(Node k, Node sz);
+ TypeBuiltinSetMap matchNewObs(Node t, Node sz);
- /** mark obligation `k` as solved.
+ /** mark obligation `ob` as solved.
*
* This function first marks `s` as the complete/constant solution for
* `ob`. Then it substitutes all instances of `ob` in partial solutions to
* example, given:
*
* CandSols = {
- * mainOb -> {(+ z1 1)},
- * z1 -> {(* z2 x)},
- * z2 -> {2}
+ * k0 -> {(c_+ k1 c_1)},
+ * k1 -> {(c_* k2 c_x)},
+ * k2 -> {c_2}
* }
- * Sol = {z2 -> 2}
+ * Sol = {}
*
- * Then calling `markSolved(z2, 2)` will result in:
+ * Then calling `markSolved(k2, c_2)` will result in:
*
* CandSols = {
- * mainOb -> {(+ z1 1), (+ (* 2 x) 1)},
- * z1 -> {(* z2 x), (* 2 x)},
- * z2 -> {2}
+ * k0 -> {(c_+ k1 c_1), (c_+ (c_* c_2 c_x) c_1)},
+ * k1 -> {(c_* k2 c_x), (c_* c_2 c_x)},
+ * k2 -> {c_2}
+ * }
+ * Sol = {
+ * k0 -> (c_+ (c_* c_2 c_x) c_1),
+ * k1 -> (c_* c_2 c_x),
+ * k2 -> c_2
* }
- * Sol = {mainOb -> (+ (* 2 x) 1), z1 -> (* 2 x), z2 -> 2}
- *
- * Note: example uses builtin terms instead of sygus terms for simplicity.
*
* @param ob free var to mark as solved and substitute
- * @param sol constant solution to `ob`
+ * @param sol solution to `ob`
*/
- void markSolved(Node k, Node s);
+ void markSolved(RConsObligation* ob, Node s);
/**
* Initialize a sygus enumerator and a candidate rewrite database for each
void initialize(TypeNode stn);
/**
- * Remove solved obligations from the given set of obligations.
+ * Remove reconstructed terms from the given set of terms to reconstruct.
*
- * @param unsolvedObs A set of obligations containing solved ones
+ * @param termsToRecons a set of terms to reconstruct possibly containing
+ * already reconstructed ones
*/
- void removeSolvedObs(TypeObligationSetMap& obs);
+ void removeReconstructedTerms(TypeBuiltinSetMap& termsToRecons);
/**
* Replace all variables in `n` with ground values. Before, calling `match`,
* `matchNewObs` rewrites the builtin analog of `n` which contains variables.
* The rewritten term, however, may contain fewer variables:
*
- * rewrite((ite true z1 z2)) = z1 // n = (c_ite c_true c_z1 c_z2)
+ * rewrite((ite true z1 z2)) = z1 // n = (c_ite c_true z1 z2)
*
- * In such cases, `matchNewObs` replaces the remaining variables (`c_z1`) with
- * obligations and ignores the eliminated ones (`c_z2`). Since the values of
- * the eliminated variables do not matter, they are replaced with some ground
+ * In such cases, `matchNewObs` replaces the remaining variables (`z1`) with
+ * obligations and ignores the eliminated ones (`z2`). Since the values of the
+ * eliminated variables do not matter, they are replaced with some ground
* values by calling this method.
*
- * @param n A term containing variables
+ * @param n a term containing variables
* @return `n` with all vars in `n` replaced with ground values
*/
Node mkGround(Node n) const;
/** reference to the statistics of parent */
SygusStatistics& d_stats;
- /** a map from an obligation to its reconstruction info */
- std::unordered_map<Node, RConsObligationInfo> d_obInfo;
+ /** a list of obligations to solve */
+ std::vector<std::unique_ptr<RConsObligation>> d_obs;
/** a map from a sygus datatype type to its reconstruction info */
std::unordered_map<TypeNode, RConsTypeInfo> d_stnInfo;
- /** a map from an obligation to its sygus solution (if it exists) */
+ /** a map from an obligation's skolem to its sygus solution (if it exists) */
std::unordered_map<TNode, TNode> d_sol;
/** a map from a candidate solution to its sub-obligations */
- std::unordered_map<Node, std::vector<Node>> d_subObs;
+ std::unordered_map<Node, std::vector<RConsObligation*>> d_subObs;
/** a map from a candidate solution to its parent obligation */
- std::unordered_map<Node, Node> d_parentOb;
+ std::unordered_map<Node, RConsObligation*> d_parentOb;
/** a cache of sygus variables treated as ground terms by matching */
std::unordered_map<Node, Node> d_sygusVars;
(set-logic UF)
-(synth-fun f ((p Bool) (q Bool) (r Bool)) Bool
+(synth-fun f ((p Bool) (q Bool) (r Bool) (s Bool)) Bool
((Start Bool))
- ((Start Bool (true false p q r (not Start) (and Start Start) (or Start Start)))))
+ ((Start Bool (p q r s (not Start) (and Start Start)
+ (or Start Start) (ite Start Start Start)))))
-(define-fun eqReduce ((p Bool) (q Bool)) Bool (or (and p q) (and (not p) (not q))))
+(define-fun eqReduce ((p Bool) (q Bool)) Bool
+ (and (or p (not q)) (or (not p) q)))
(declare-var p Bool)
(declare-var q Bool)
(declare-var r Bool)
+(declare-var s Bool)
-(constraint (= (f p q r) (and (= (and p q) (and q r)) (eqReduce (and p q) (and q r)))))
+(constraint (= (f p q r s) (and (= (and p q) (and q r))
+ (ite s (eqReduce (and p q) (and q r))
+ (eqReduce (and p q) (and p r))))))
(check-synth)
projects / cvc5.git / commitdiff