Adds an instantiation strategy based on user-provided pool annotations.
The next PR will connect this to quantifiers engine.
theory/quantifiers/inst_match_trie.h
theory/quantifiers/inst_strategy_enumerative.cpp
theory/quantifiers/inst_strategy_enumerative.h
+ theory/quantifiers/inst_strategy_pool.cpp
+ theory/quantifiers/inst_strategy_pool.h
theory/quantifiers/instantiate.cpp
theory/quantifiers/instantiate.h
theory/quantifiers/instantiation_list.cpp
name = "agg"
help = "Consider the phase requirements aggressively for all triggers."
+[[option]]
+ name = "poolInst"
+ category = "regular"
+ long = "pool-inst"
+ type = "bool"
+ default = "true"
+ help = "pool-based instantiation: instantiate with ground terms occurring in user-specified pools"
+
### Finite model finding options
[[option]]
case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI";
case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI";
case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM";
+ case InferenceId::QUANTIFIERS_INST_POOL: return "QUANTIFIERS_INST_POOL";
case InferenceId::QUANTIFIERS_BINT_PROXY: return "QUANTIFIERS_BINT_PROXY";
case InferenceId::QUANTIFIERS_BINT_MIN_NG: return "QUANTIFIERS_BINT_MIN_NG";
case InferenceId::QUANTIFIERS_CEGQI_CEX: return "QUANTIFIERS_CEGQI_CEX";
QUANTIFIERS_INST_SYQI,
// instantiations from enumerative instantiation
QUANTIFIERS_INST_ENUM,
+ // instantiations from pool instantiation
+ QUANTIFIERS_INST_POOL,
//-------------------- bounded integers
// a proxy lemma from bounded integers, used to control bounds on ground terms
QUANTIFIERS_BINT_PROXY,
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Pool-based instantiation strategy
+ */
+
+#include "theory/quantifiers/inst_strategy_pool.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/term_pools.h"
+#include "theory/quantifiers/term_registry.h"
+#include "theory/quantifiers/term_tuple_enumerator.h"
+
+using namespace cvc5::kind;
+using namespace cvc5::context;
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+InstStrategyPool::InstStrategyPool(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr)
+ : QuantifiersModule(qs, qim, qr, tr)
+{
+}
+
+void InstStrategyPool::presolve() {}
+
+bool InstStrategyPool::needsCheck(Theory::Effort e)
+{
+ return d_qstate.getInstWhenNeedsCheck(e);
+}
+
+void InstStrategyPool::reset_round(Theory::Effort e) {}
+
+void InstStrategyPool::registerQuantifier(Node q)
+{
+ // take into account user pools
+ if (q.getNumChildren() == 3)
+ {
+ Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q);
+ // add patterns
+ for (const Node& p : subsPat)
+ {
+ if (p.getKind() == INST_POOL)
+ {
+ d_userPools[q].push_back(p);
+ }
+ }
+ }
+}
+
+void InstStrategyPool::check(Theory::Effort e, QEffort quant_e)
+{
+ if (d_userPools.empty())
+ {
+ return;
+ }
+ double clSet = 0;
+ if (Trace.isOn("pool-engine"))
+ {
+ clSet = double(clock()) / double(CLOCKS_PER_SEC);
+ Trace("pool-engine") << "---Pool instantiation, effort = " << e << "---"
+ << std::endl;
+ }
+ FirstOrderModel* fm = d_treg.getModel();
+ bool inConflict = false;
+ uint64_t addedLemmas = 0;
+ size_t nquant = fm->getNumAssertedQuantifiers();
+ std::map<Node, std::vector<Node> >::iterator uit;
+ for (size_t i = 0; i < nquant; i++)
+ {
+ Node q = fm->getAssertedQuantifier(i, true);
+ uit = d_userPools.find(q);
+ if (uit == d_userPools.end())
+ {
+ // no user pools for this
+ continue;
+ }
+ if (!d_qreg.hasOwnership(q, this) || !fm->isQuantifierActive(q))
+ {
+ // quantified formula is not owned by this or is inactive
+ continue;
+ }
+ // process with each user pool
+ for (const Node& p : uit->second)
+ {
+ inConflict = process(q, p, addedLemmas);
+ if (inConflict)
+ {
+ break;
+ }
+ }
+ if (inConflict)
+ {
+ break;
+ }
+ }
+ if (Trace.isOn("pool-engine"))
+ {
+ Trace("pool-engine") << "Added lemmas = " << addedLemmas << std::endl;
+ double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
+ Trace("pool-engine") << "Finished pool instantiation, time = "
+ << (clSet2 - clSet) << std::endl;
+ }
+}
+
+std::string InstStrategyPool::identify() const
+{
+ return std::string("InstStrategyPool");
+}
+
+bool InstStrategyPool::process(Node q, Node p, uint64_t& addedLemmas)
+{
+ TermTupleEnumeratorEnv ttec;
+ ttec.d_fullEffort = true;
+ ttec.d_increaseSum = options::fullSaturateSum();
+ TermPools* tp = d_treg.getTermPools();
+ std::shared_ptr<TermTupleEnumeratorInterface> enumerator(
+ mkTermTupleEnumeratorPool(q, &ttec, tp, p));
+ Instantiate* ie = d_qim.getInstantiate();
+ std::vector<Node> terms;
+ std::vector<bool> failMask;
+ // we instantiate exhaustively
+ enumerator->init();
+ while (enumerator->hasNext())
+ {
+ if (d_qstate.isInConflict())
+ {
+ // could be conflicting for an internal reason
+ return true;
+ }
+ enumerator->next(terms);
+ // try instantiation
+ failMask.clear();
+ if (ie->addInstantiationExpFail(
+ q, terms, failMask, InferenceId::QUANTIFIERS_INST_POOL))
+ {
+ Trace("pool-inst") << "Success with " << terms << std::endl;
+ addedLemmas++;
+ }
+ else
+ {
+ Trace("pool-inst") << "Fail with " << terms << std::endl;
+ // notify the enumerator of the failure
+ enumerator->failureReason(failMask);
+ }
+ }
+ return false;
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Pool-based instantiation strategy
+ */
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
+#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
+
+#include "theory/quantifiers/quant_module.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * Pool-based instantiation. This implements a strategy for instantiating
+ * quantifiers based on user-provided pool annotations.
+ *
+ * When check is invoked, this strategy considers each
+ * INST_POOL annotation on quantified formulas. For each annotation, it
+ * instantiates the associated quantified formula with the Cartesian
+ * product of terms currently in the pool, using efficient techniques for
+ * enumerating over tuples of terms, as implemented in the term tuple
+ * enumerator utilities (see quantifiers/term_tuple_enumerator.h).
+ */
+class InstStrategyPool : public QuantifiersModule
+{
+ public:
+ InstStrategyPool(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr);
+ ~InstStrategyPool() {}
+ /** Presolve */
+ void presolve() override;
+ /** Needs check. */
+ bool needsCheck(Theory::Effort e) override;
+ /** Reset round. */
+ void reset_round(Theory::Effort e) override;
+ /** Register quantified formula q */
+ void registerQuantifier(Node q) override;
+ /** Check.
+ * Adds instantiations for all currently asserted
+ * quantified formulas via calls to process(...)
+ */
+ void check(Theory::Effort e, QEffort quant_e) override;
+ /** Identify. */
+ std::string identify() const override;
+
+ private:
+ /** Process quantified formula with user pool */
+ bool process(Node q, Node p, uint64_t& addedLemmas);
+ /** Map from quantified formulas to user pools */
+ std::map<Node, std::vector<Node> > d_userPools;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
+
+#endif
* Returns false if the reset failed. When reset fails, the utility should
* have added a lemma via a call to d_qim.addPendingLemma.
*/
- virtual bool reset( Theory::Effort e ) = 0;
+ virtual bool reset(Theory::Effort e) { return true; }
/* Called for new quantifiers */
- virtual void registerQuantifier(Node q) = 0;
+ virtual void registerQuantifier(Node q) {}
/** Identify this module (for debugging, dynamic configuration, etc..) */
virtual std::string identify() const = 0;
/** Check complete?
d_sg_gen(nullptr),
d_synth_e(nullptr),
d_fs(nullptr),
+ d_ipool(nullptr),
d_i_cbqi(nullptr),
d_qsplit(nullptr),
d_sygus_inst(nullptr)
d_fs.reset(new InstStrategyEnum(qs, qim, qr, tr, d_rel_dom.get()));
modules.push_back(d_fs.get());
}
+ if (options::poolInst())
+ {
+ d_ipool.reset(new InstStrategyPool(qs, qim, qr, tr));
+ modules.push_back(d_ipool.get());
+ }
if (options::sygusInst())
{
d_sygus_inst.reset(new SygusInst(qs, qim, qr, tr));
#include "theory/quantifiers/fmf/model_builder.h"
#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/inst_strategy_enumerative.h"
+#include "theory/quantifiers/inst_strategy_pool.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/quant_split.h"
#include "theory/quantifiers/sygus/synth_engine.h"
std::unique_ptr<SynthEngine> d_synth_e;
/** full saturation */
std::unique_ptr<InstStrategyEnum> d_fs;
+ /** pool-based instantiation */
+ std::unique_ptr<InstStrategyPool> d_ipool;
/** counterexample-based quantifier instantiation */
std::unique_ptr<InstStrategyCegqi> d_i_cbqi;
/** quantifiers splitting */
#include "theory/quantifiers/index_trie.h"
#include "theory/quantifiers/quant_module.h"
#include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/term_pools.h"
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
#include "util/statistics_registry.h"
return d_termDbList[type_node][term_index];
}
+/**
+ * Enumerate ground terms as they come from a user-provided term pool
+ */
+class TermTupleEnumeratorPool : public TermTupleEnumeratorBase
+{
+ public:
+ TermTupleEnumeratorPool(Node quantifier,
+ const TermTupleEnumeratorEnv* env,
+ TermPools* tp,
+ Node pool)
+ : TermTupleEnumeratorBase(quantifier, env), d_tp(tp), d_pool(pool)
+ {
+ Assert(d_pool.getKind() == kind::INST_POOL);
+ }
+
+ virtual ~TermTupleEnumeratorPool() = default;
+
+ protected:
+ /** Pointer to the term pool utility */
+ TermPools* d_tp;
+ /** The pool annotation */
+ Node d_pool;
+ /** a list of terms for each id */
+ std::map<size_t, std::vector<Node> > d_poolList;
+ /** gets the terms from the pool */
+ size_t prepareTerms(size_t variableIx) override
+ {
+ Assert(d_pool.getNumChildren() > variableIx);
+ // prepare terms from pool
+ d_poolList[variableIx].clear();
+ d_tp->getTermsForPool(d_pool[variableIx], d_poolList[variableIx]);
+ Trace("pool-inst") << "Instantiation Terms for child " << variableIx << ": "
+ << d_poolList[variableIx] << std::endl;
+ return d_poolList[variableIx].size();
+ }
+ Node getTerm(size_t variableIx, size_t term_index) override
+ {
+ Assert(term_index < d_poolList[variableIx].size());
+ return d_poolList[variableIx][term_index];
+ }
+};
+
TermTupleEnumeratorInterface* mkTermTupleEnumerator(
Node q, const TermTupleEnumeratorEnv* env, QuantifiersState& qs, TermDb* td)
{
new TermTupleEnumeratorRD(q, env, rd));
}
+TermTupleEnumeratorInterface* mkTermTupleEnumeratorPool(
+ Node q, const TermTupleEnumeratorEnv* env, TermPools* tp, Node pool)
+{
+ return static_cast<TermTupleEnumeratorInterface*>(
+ new TermTupleEnumeratorPool(q, env, tp, pool));
+}
+
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
namespace theory {
namespace quantifiers {
+class TermPools;
class QuantifiersState;
class TermDb;
class RelevantDomain;
TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd(
Node q, const TermTupleEnumeratorEnv* env, RelevantDomain* rd);
+/** Make term pool enumerator */
+TermTupleEnumeratorInterface* mkTermTupleEnumeratorPool(
+ Node q, const TermTupleEnumeratorEnv* env, TermPools* tp, Node p);
+
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
projects / cvc5.git / commitdiff