This utility will be used to track pools for pool-based instantiation.
theory/quantifiers/skolemize.h
theory/quantifiers/solution_filter.cpp
theory/quantifiers/solution_filter.h
+ theory/quantifiers/term_pools.cpp
+ theory/quantifiers/term_pools.h
theory/quantifiers/term_tuple_enumerator.cpp
theory/quantifiers/term_tuple_enumerator.h
theory/quantifiers/sygus/ce_guided_single_inv.cpp
--- /dev/null
+/********************* */
+/*! \file term_pools.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 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.\endverbatim
+ **
+ ** \brief utilities for term enumeration
+ **/
+
+#include "theory/quantifiers/term_pools.h"
+
+#include "theory/quantifiers/quantifiers_state.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+void TermPoolDomain::initialize() { d_terms.clear(); }
+void TermPoolDomain::add(Node n)
+{
+ if (std::find(d_terms.begin(), d_terms.end(), n) == d_terms.end())
+ {
+ d_terms.push_back(n);
+ }
+}
+
+void TermPoolQuantInfo::initialize()
+{
+ d_instAddToPool.clear();
+ d_skolemAddToPool.clear();
+}
+
+TermPools::TermPools(QuantifiersState& qs) : d_qs(qs) {}
+
+bool TermPools::reset(Theory::Effort e)
+{
+ for (std::pair<const Node, TermPoolDomain>& p : d_pools)
+ {
+ p.second.d_currTerms.clear();
+ }
+ return true;
+}
+
+void TermPools::registerQuantifier(Node q)
+{
+ if (q.getNumChildren() < 3)
+ {
+ return;
+ }
+ TermPoolQuantInfo& qi = d_qinfo[q];
+ qi.initialize();
+ for (const Node& p : q[2])
+ {
+ Kind pk = p.getKind();
+ if (pk == kind::INST_ADD_TO_POOL)
+ {
+ qi.d_instAddToPool.push_back(p);
+ }
+ else if (pk == kind::SKOLEM_ADD_TO_POOL)
+ {
+ qi.d_skolemAddToPool.push_back(p);
+ }
+ }
+ if (qi.d_instAddToPool.empty() && qi.d_skolemAddToPool.empty())
+ {
+ d_qinfo.erase(q);
+ }
+}
+
+std::string TermPools::identify() const { return "TermPools"; }
+
+void TermPools::registerPool(Node p, const std::vector<Node>& initValue)
+{
+ TermPoolDomain& d = d_pools[p];
+ d.initialize();
+ for (const Node& i : initValue)
+ {
+ d.add(i);
+ }
+}
+
+void TermPools::getTermsForPool(Node p, std::vector<Node>& terms)
+{
+ // for now, we assume p is a variable
+ Assert(p.isVar());
+ TermPoolDomain& dom = d_pools[p];
+ if (dom.d_terms.empty())
+ {
+ return;
+ }
+ // if we have yet to compute terms on this round
+ if (dom.d_currTerms.empty())
+ {
+ std::unordered_set<Node, NodeHashFunction> reps;
+ // eliminate modulo equality
+ for (const Node& t : dom.d_terms)
+ {
+ Node r = d_qs.getRepresentative(t);
+ if (reps.find(r) == reps.end())
+ {
+ reps.insert(r);
+ dom.d_currTerms.push_back(t);
+ }
+ }
+ Trace("pool-terms") << "* Domain for pool " << p << " is "
+ << dom.d_currTerms << std::endl;
+ }
+ terms.insert(terms.end(), dom.d_currTerms.begin(), dom.d_currTerms.end());
+}
+
+void TermPools::processInstantiation(Node q, const std::vector<Node>& terms)
+{
+ processInternal(q, terms, true);
+}
+
+void TermPools::processSkolemization(Node q, const std::vector<Node>& skolems)
+{
+ processInternal(q, skolems, false);
+}
+
+void TermPools::processInternal(Node q,
+ const std::vector<Node>& ts,
+ bool isInst)
+{
+ Assert(q.getKind() == kind::FORALL);
+ std::map<Node, TermPoolQuantInfo>::iterator it = d_qinfo.find(q);
+ if (it == d_qinfo.end())
+ {
+ // does not impact
+ return;
+ }
+ std::vector<Node> vars(q[0].begin(), q[0].end());
+ Assert(vars.size() == ts.size());
+ std::vector<Node>& cmds =
+ isInst ? it->second.d_instAddToPool : it->second.d_skolemAddToPool;
+ for (const Node& c : cmds)
+ {
+ Assert(c.getNumChildren() == 2);
+ Node t = c[0];
+ // substitute the term
+ Node st = t.substitute(vars.begin(), vars.end(), ts.begin(), ts.end());
+ // add to pool
+ Trace("pool-terms") << "Due to "
+ << (isInst ? "instantiation" : "skolemization")
+ << ", add " << st << " to pool " << c[1] << std::endl;
+ TermPoolDomain& dom = d_pools[c[1]];
+ dom.d_terms.push_back(st);
+ }
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file term_pools.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 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.\endverbatim
+ **
+ ** \brief utilities for term enumeration
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H
+#define CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H
+
+#include <unordered_set>
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/quantifiers/quant_util.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+class QuantifiersState;
+
+/**
+ * Information concerning a pool variable.
+ */
+class TermPoolDomain
+{
+ public:
+ /** initialize, which clears the data below */
+ void initialize();
+ /** add node to this pool */
+ void add(Node n);
+ /** The list in this pool */
+ std::vector<Node> d_terms;
+ /**
+ * The list of terms on this round. This is cleared at the beginning of an
+ * instantiation round. The members are unique modulo equality.
+ */
+ std::vector<Node> d_currTerms;
+};
+
+/**
+ * Contains all annotations that pertain to pools for a given quantified
+ * formula.
+ */
+class TermPoolQuantInfo
+{
+ public:
+ /** initialize, which clears the data below */
+ void initialize();
+ /** Annotations of kind INST_ADD_TO_POOL */
+ std::vector<Node> d_instAddToPool;
+ /** Annotations of kind SKOLEM_ADD_TO_POOL */
+ std::vector<Node> d_skolemAddToPool;
+};
+
+/**
+ * Term pools, which tracks the values of "pools", which are used for
+ * pool-based instantiation.
+ */
+class TermPools : public QuantifiersUtil
+{
+ public:
+ TermPools(QuantifiersState& qs);
+ ~TermPools() {}
+ /** reset, which resets the current values of pools */
+ bool reset(Theory::Effort e) override;
+ /** Called for new quantifiers, which computes TermPoolQuantInfo above */
+ void registerQuantifier(Node q) override;
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ std::string identify() const override;
+ /** Register pool p with initial value initValue. */
+ void registerPool(Node p, const std::vector<Node>& initValue);
+ /** Get terms for pool p, adds them to the vector terms. */
+ void getTermsForPool(Node p, std::vector<Node>& terms);
+ /**
+ * Process instantiation, called at the moment we successfully instantiate
+ * q with terms. This adds terms to pools based on INST_ADD_TO_POOL
+ * annotations.
+ */
+ void processInstantiation(Node q, const std::vector<Node>& terms);
+ /** Same as above, for SKOLEM_ADD_TO_POOL. */
+ void processSkolemization(Node q, const std::vector<Node>& skolems);
+ private:
+ void processInternal(Node q, const std::vector<Node>& ts, bool isInst);
+ /** reference to the quantifiers state */
+ QuantifiersState& d_qs;
+ /** Maps pools to a domain */
+ std::map<Node, TermPoolDomain> d_pools;
+ /** Maps quantifiers to info */
+ std::map<Node, TermPoolQuantInfo> d_qinfo;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC5
+
+#endif /* CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H */
#include "options/smt_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/first_order_model_fmc.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_util.h"
namespace cvc5 {
namespace theory {
d_useFmcModel(false),
d_presolveCache(qs.getUserContext()),
d_termEnum(new TermEnumeration),
+ d_termPools(new TermPools(qs)),
d_termDb(new TermDb(qs, qr)),
d_sygusTdb(nullptr)
{
return d_termDb->getOrMakeTypeGroundTerm(tn);
}
+void TermRegistry::declarePool(Node p, const std::vector<Node>& initValue)
+{
+ d_termPools->registerPool(p, initValue);
+}
+
+void TermRegistry::processInstantiation(Node q, const std::vector<Node>& terms)
+{
+ d_termPools->processInstantiation(q, terms);
+}
+void TermRegistry::processSkolemization(Node q,
+ const std::vector<Node>& skolems)
+{
+ d_termPools->processSkolemization(q, skolems);
+}
+
TermDb* TermRegistry::getTermDatabase() const { return d_termDb.get(); }
TermDbSygus* TermRegistry::getTermDatabaseSygus() const
return d_termEnum.get();
}
+TermPools* TermRegistry::getTermPools() const { return d_termPools.get(); }
+
FirstOrderModel* TermRegistry::getModel() const { return d_qmodel.get(); }
bool TermRegistry::useFmcModel() const { return d_useFmcModel; }
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_pools.h"
namespace cvc5 {
namespace theory {
* one exists, or otherwise a fresh variable.
*/
Node getTermForType(TypeNode tn);
+ /**
+ * Declare pool p with initial value initValue.
+ */
+ void declarePool(Node p, const std::vector<Node>& initValue);
+ /**
+ * Process instantiation
+ */
+ void processInstantiation(Node q, const std::vector<Node>& terms);
+ void processSkolemization(Node q, const std::vector<Node>& skolems);
/** Whether we use the full model check builder and corresponding model */
bool useFmcModel() const;
TermDbSygus* getTermDatabaseSygus() const;
/** get term enumeration utility */
TermEnumeration* getTermEnumeration() const;
+ /** get the term pools utility */
+ TermPools* getTermPools() const;
/** get the model utility */
FirstOrderModel* getModel() const;
NodeSet d_presolveCache;
/** term enumeration utility */
std::unique_ptr<TermEnumeration> d_termEnum;
+ /** term enumeration utility */
+ std::unique_ptr<TermPools> d_termPools;
/** term database */
std::unique_ptr<TermDb> d_termDb;
/** sygus term database */
projects / cvc5.git / commitdiff