This also moves some methods from TermEnumeration to QuantifiersBoundInference.
This is required for breaking several cyclic dependencies within quantifiers.
theory/quantifiers/lazy_trie.h
theory/quantifiers/proof_checker.cpp
theory/quantifiers/proof_checker.h
+ theory/quantifiers/quant_bound_inference.cpp
+ theory/quantifiers/quant_bound_inference.h
theory/quantifiers/quant_conflict_find.cpp
theory/quantifiers/quant_conflict_find.h
theory/quantifiers/quant_relevance.cpp
else
{
// can we complete it?
- if (d_qe->getTermEnumeration()->mayComplete(tn))
+ if (d_qreg.getQuantifiersBoundInference().mayComplete(tn))
{
Trace("fm-debug") << " do complete, since cardinality is small ("
<< tn.getCardinality() << ")..." << std::endl;
if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
TypeNode tn = f[0][i].getType();
if ((tn.isSort() && tn.isInterpretedFinite())
- || d_quantEngine->getTermEnumeration()->mayComplete(tn))
+ || d_qreg.getQuantifiersBoundInference().mayComplete(tn))
{
success = true;
setBoundedVar( f, f[0][i], BOUND_FINITE );
#include "options/theory_options.h"
#include "options/uf_options.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_rep_bound_ext.h"
+#include "theory/quantifiers/quantifiers_registry.h"
+#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
}
}
-FullModelChecker::FullModelChecker(QuantifiersEngine* qe, QuantifiersState& qs)
- : QModelBuilder(qe, qs)
+FullModelChecker::FullModelChecker(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersRegistry& qr)
+ : QModelBuilder(qe, qs, qr)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
class RepBoundFmcEntry : public QRepBoundExt
{
public:
- RepBoundFmcEntry(QuantifiersEngine* qe, Node e, FirstOrderModelFmc* f)
- : QRepBoundExt(qe), d_entry(e), d_fm(f)
+ RepBoundFmcEntry(QuantifiersBoundInference& qbi,
+ Node e,
+ FirstOrderModelFmc* f)
+ : QRepBoundExt(qbi, f), d_entry(e), d_fm(f)
{
}
~RepBoundFmcEntry() {}
Trace("fmc-exh") << "----Exhaustive instantiate based on " << c << " ";
debugPrintCond("fmc-exh", c, true);
Trace("fmc-exh")<< std::endl;
- RepBoundFmcEntry rbfe(d_qe, c, fm);
- RepSetIterator riter(d_qe->getModel()->getRepSet(), &rbfe);
+ QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
+ RepBoundFmcEntry rbfe(qbi, c, fm);
+ RepSetIterator riter(fm->getRepSet(), &rbfe);
Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;
//initialize
if (riter.setQuantifier(f))
Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
public:
- FullModelChecker(QuantifiersEngine* qe, QuantifiersState& qs);
+ FullModelChecker(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersRegistry& qr);
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-QModelBuilder::QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs)
+QModelBuilder::QModelBuilder(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersRegistry& qr)
: TheoryEngineModelBuilder(),
d_qe(qe),
d_addedLemmas(0),
d_triedLemmas(0),
- d_qstate(qs)
+ d_qstate(qs),
+ d_qreg(qr)
{
}
Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
int tests = 0;
int bad = 0;
+ QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
std::vector< Node > vars;
for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
vars.push_back( f[0][j] );
}
- QRepBoundExt qrbe(d_qe);
- RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
+ QRepBoundExt qrbe(qbi, fm);
+ RepSetIterator riter(fm->getRepSet(), &qrbe);
if( riter.setQuantifier( f ) ){
while( !riter.isFinished() ){
tests++;
class FirstOrderModel;
class QuantifiersState;
+class QuantifiersRegistry;
class QModelBuilder : public TheoryEngineModelBuilder
{
unsigned d_triedLemmas;
public:
- QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs);
+ QModelBuilder(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersRegistry& qr);
//do exhaustive instantiation
// 0 : failed, but resorting to true exhaustive instantiation may work
protected:
/** The quantifiers state object */
QuantifiersState& d_qstate;
+ /** Reference to the quantifiers registry */
+ QuantifiersRegistry& d_qreg;
};
}/* CVC4::theory::quantifiers namespace */
quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
unsigned prev_alem = mb->getNumAddedLemmas();
unsigned prev_tlem = mb->getNumTriedLemmas();
- int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort );
+ FirstOrderModel* fm = d_quantEngine->getModel();
+ int retEi = mb->doExhaustiveInstantiation(fm, f, effort);
if( retEi!=0 ){
if( retEi<0 ){
Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
}
Trace("fmf-exh-inst-debug") << std::endl;
}
+ QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
//create a rep set iterator and iterate over the (relevant) domain of the quantifier
- QRepBoundExt qrbe(d_quantEngine);
- RepSetIterator riter(d_quantEngine->getModel()->getRepSet(), &qrbe);
+ QRepBoundExt qrbe(qbi, fm);
+ RepSetIterator riter(fm->getRepSet(), &qrbe);
if( riter.setQuantifier( f ) ){
Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
if( !riter.isIncomplete() ){
--- /dev/null
+/********************* */
+/*! \file quant_bound_inference.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Tim King, Morgan Deters
+ ** 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 Implementation of quantifiers bound inference
+ **/
+
+#include "theory/quantifiers/quant_bound_inference.h"
+
+#include "theory/quantifiers/fmf/bounded_integers.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+QuantifiersBoundInference::QuantifiersBoundInference(unsigned cardMax,
+ bool isFmf)
+ : d_cardMax(cardMax), d_isFmf(isFmf), d_bint(nullptr)
+{
+}
+
+void QuantifiersBoundInference::finishInit(BoundedIntegers* b) { d_bint = b; }
+
+bool QuantifiersBoundInference::mayComplete(TypeNode tn)
+{
+ std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
+ d_may_complete.find(tn);
+ if (it == d_may_complete.end())
+ {
+ // cache
+ bool mc = mayComplete(tn, d_cardMax);
+ d_may_complete[tn] = mc;
+ return mc;
+ }
+ return it->second;
+}
+
+bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard)
+{
+ bool mc = false;
+ if (tn.isClosedEnumerable() && tn.isInterpretedFinite())
+ {
+ Cardinality c = tn.getCardinality();
+ if (!c.isLargeFinite())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
+ // check if less than fixed upper bound
+ Node oth = nm->mkConst(Rational(maxCard));
+ Node eq = nm->mkNode(LEQ, card, oth);
+ eq = Rewriter::rewrite(eq);
+ mc = eq.isConst() && eq.getConst<bool>();
+ }
+ }
+ return mc;
+}
+
+bool QuantifiersBoundInference::isFiniteBound(Node q, Node v)
+{
+ if (d_bint && d_bint->isBound(q, v))
+ {
+ return true;
+ }
+ TypeNode tn = v.getType();
+ if (tn.isSort() && d_isFmf)
+ {
+ return true;
+ }
+ else if (mayComplete(tn))
+ {
+ return true;
+ }
+ return false;
+}
+
+BoundVarType QuantifiersBoundInference::getBoundVarType(Node q, Node v)
+{
+ if (d_bint)
+ {
+ return d_bint->getBoundVarType(q, v);
+ }
+ return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
+}
+
+void QuantifiersBoundInference::getBoundVarIndices(
+ Node q, std::vector<unsigned>& indices) const
+{
+ Assert(indices.empty());
+ // we take the bounded variables first
+ if (d_bint)
+ {
+ d_bint->getBoundVarIndices(q, indices);
+ }
+ // then get the remaining ones
+ for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
+ {
+ if (std::find(indices.begin(), indices.end(), i) == indices.end())
+ {
+ indices.push_back(i);
+ }
+ }
+}
+
+bool QuantifiersBoundInference::getBoundElements(
+ RepSetIterator* rsi,
+ bool initial,
+ Node q,
+ Node v,
+ std::vector<Node>& elements) const
+{
+ if (d_bint)
+ {
+ return d_bint->getBoundElements(rsi, initial, q, v, elements);
+ }
+ return false;
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file quant_bound_inference.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 Quantifiers bound inference
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
+#define CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
+
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+
+class RepSetIterator;
+
+namespace quantifiers {
+
+class BoundedIntegers;
+
+/** Types of bounds that can be inferred for quantified formulas */
+enum BoundVarType
+{
+ // a variable has a finite bound because it has finite cardinality
+ BOUND_FINITE,
+ // a variable has a finite bound because it is in an integer range, e.g.
+ // forall x. u <= x <= l => P(x)
+ BOUND_INT_RANGE,
+ // a variable has a finite bound because it is a member of a set, e.g.
+ // forall x. x in S => P(x)
+ BOUND_SET_MEMBER,
+ // a variable has a finite bound because only a fixed set of terms are
+ // relevant for it in the domain of the quantified formula, e.g.
+ // forall x. ( x = t1 OR ... OR x = tn ) => P(x)
+ BOUND_FIXED_SET,
+ // a bound has not been inferred for the variable
+ BOUND_NONE
+};
+
+/**
+ * This class is the central utility for determining if the domain of a
+ * quantified formula is finite, or whether its domain can be restricted to
+ * a finite subdomain based on one of the above types.
+ */
+class QuantifiersBoundInference
+{
+ public:
+ /**
+ * @param cardMax The maximum cardinality we consider to be small enough
+ * to "complete" below.
+ * @param isFmf Whether finite model finding (for uninterpreted sorts) is
+ * enabled.
+ */
+ QuantifiersBoundInference(unsigned cardMax, bool isFmf = false);
+ /** finish initialize */
+ void finishInit(BoundedIntegers* b);
+ /** may complete type
+ *
+ * Returns true if the type tn is closed enumerable, is interpreted as a
+ * finite type, and has cardinality less than some reasonable value
+ * (currently < 1000). This method caches the results of whether each type
+ * may be completed.
+ */
+ bool mayComplete(TypeNode tn);
+ /**
+ * Static version of the above method where maximum cardinality is
+ * configurable.
+ */
+ static bool mayComplete(TypeNode tn, unsigned cardMax);
+ /** does variable v of quantified formula q have a finite bound? */
+ bool isFiniteBound(Node q, Node v);
+ /** get bound var type
+ *
+ * This returns the type of bound that was inferred for variable v of
+ * quantified formula q.
+ */
+ BoundVarType getBoundVarType(Node q, Node v);
+ /**
+ * Get the indices of bound variables, in the order they should be processed
+ * in a RepSetIterator.
+ *
+ * For details, see BoundedIntegers::getBoundVarIndices.
+ */
+ void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
+ /**
+ * Get bound elements
+ *
+ * This gets the (finite) enumeration of the range of variable v of quantified
+ * formula q and adds it into the vector elements in the context of the
+ * iteration being performed by rsi. It returns true if it could successfully
+ * determine this range.
+ *
+ * For details, see BoundedIntegers::getBoundElements.
+ */
+ bool getBoundElements(RepSetIterator* rsi,
+ bool initial,
+ Node q,
+ Node v,
+ std::vector<Node>& elements) const;
+
+ private:
+ /** The maximum cardinality for which we complete */
+ unsigned d_cardMax;
+ /** Whether finite model finding is enabled */
+ bool d_isFmf;
+ /** may complete */
+ std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_may_complete;
+ /** The bounded integers module, which may help infer bounds */
+ BoundedIntegers* d_bint;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */
#include "theory/quantifiers/quant_rep_bound_ext.h"
-#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quant_bound_inference.h"
+#include "theory/quantifiers_engine.h"
using namespace CVC4::kind;
namespace theory {
namespace quantifiers {
-QRepBoundExt::QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
+QRepBoundExt::QRepBoundExt(QuantifiersBoundInference& qbi, FirstOrderModel* m)
+ : d_qbi(qbi), d_model(m)
+{
+}
RsiEnumType QRepBoundExt::setBound(Node owner,
unsigned i,
// builtin: check if it is bound by bounded integer module
if (owner.getKind() == FORALL)
{
- BoundVarType bvt = d_qe->getBoundVarType(owner, owner[0][i]);
+ BoundVarType bvt = d_qbi.getBoundVarType(owner, owner[0][i]);
if (bvt != BOUND_FINITE)
{
d_bound_int[i] = true;
return true;
}
Assert(owner.getKind() == FORALL);
- if (!d_qe->getBoundElements(rsi, initial, owner, owner[0][i], elements))
+ if (!d_qbi.getBoundElements(rsi, initial, owner, owner[0][i], elements))
{
return false;
}
bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn)
{
- return d_qe->getModel()->initializeRepresentativesForType(tn);
+ return d_model->initializeRepresentativesForType(tn);
}
bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
return false;
}
Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
- d_qe->getBoundVarIndices(owner, varOrder);
+ d_qbi.getBoundVarIndices(owner, varOrder);
return true;
}
#include <map>
#include "expr/node.h"
-#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/rep_set.h"
#include "theory/theory_model.h"
namespace CVC4 {
namespace theory {
-
-class QuantifiersEngine;
-
namespace quantifiers {
+class QuantifiersBoundInference;
+class FirstOrderModel;
+
/** Quantifiers representative bound
*
* This class is used for computing (finite) bounds for the domain of a
class QRepBoundExt : public RepBoundExt
{
public:
- QRepBoundExt(QuantifiersEngine* qe);
+ QRepBoundExt(QuantifiersBoundInference& qbi, FirstOrderModel* m);
virtual ~QRepBoundExt() {}
/** set bound */
RsiEnumType setBound(Node owner,
bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override;
private:
- /** Quantifiers engine associated with this bound */
- QuantifiersEngine* d_qe;
+ /** Reference to the quantifiers bound inference */
+ QuantifiersBoundInference& d_qbi;
+ /** Pointer to the quantifiers model */
+ FirstOrderModel* d_model;
/** indices that are bound integer enumeration */
std::map<unsigned, bool> d_bound_int;
};
}
bool takeOwnership = false;
bool doSplit = false;
+ QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
TypeNode tn = q[0][i].getType();
else if (options::quantDynamicSplit()
== options::QuantDSplitMode::DEFAULT)
{
- if (!d_quantEngine->isFiniteBound(q, q[0][i]))
+ if (!qbi.isFiniteBound(q, q[0][i]))
{
if (dt.isInterpretedFinite(tn))
{
static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
};
-/** Types of bounds that can be inferred for quantified formulas */
-enum BoundVarType
-{
- // a variable has a finite bound because it has finite cardinality
- BOUND_FINITE,
- // a variable has a finite bound because it is in an integer range, e.g.
- // forall x. u <= x <= l => P(x)
- BOUND_INT_RANGE,
- // a variable has a finite bound because it is a member of a set, e.g.
- // forall x. x in S => P(x)
- BOUND_SET_MEMBER,
- // a variable has a finite bound because only a fixed set of terms are
- // relevant for it in the domain of the quantified formula, e.g.
- // forall x. ( x = t1 OR ... OR x = tn ) => P(x)
- BOUND_FIXED_SET,
- // a bound has not been inferred for the variable
- BOUND_NONE
-};
}
}
#include "theory/quantifiers/quantifiers_registry.h"
+#include "options/quantifiers_options.h"
#include "theory/quantifiers/quant_module.h"
#include "theory/quantifiers/term_util.h"
namespace theory {
namespace quantifiers {
-QuantifiersRegistry::QuantifiersRegistry() : d_quantAttr() {}
+QuantifiersRegistry::QuantifiersRegistry()
+ : d_quantAttr(),
+ d_quantBoundInf(options::fmfTypeCompletionThresh(),
+ options::finiteModelFind())
+{
+}
void QuantifiersRegistry::registerQuantifier(Node q)
{
{
return d_quantAttr;
}
+
+QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference()
+{
+ return d_quantBoundInf;
+}
+
Node QuantifiersRegistry::getNameForQuant(Node q) const
{
Node name = d_quantAttr.getQuantName(q);
#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
#include "expr/node.h"
+#include "theory/quantifiers/quant_bound_inference.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/quantifiers_attributes.h"
//----------------------------- end instantiation constants
/** Get quantifiers attributes utility class */
QuantAttributes& getQuantAttributes();
+ /** Get quantifiers bound inference utility */
+ QuantifiersBoundInference& getQuantifiersBoundInference();
/**
* Get quantifiers name, which returns a variable corresponding to the name of
* quantified formula q if q has a name, or otherwise returns q itself.
std::map<Node, std::vector<Node> > d_inst_constants;
/** The quantifiers attributes class */
QuantAttributes d_quantAttr;
+ /** The quantifiers bound inference class */
+ QuantifiersBoundInference d_quantBoundInf;
};
} // namespace quantifiers
#include "theory/quantifiers/term_enumeration.h"
-#include "options/quantifiers_options.h"
-#include "theory/quantifiers/term_util.h"
-#include "theory/rewriter.h"
+#include "theory/quantifiers/quant_bound_inference.h"
using namespace CVC4::kind;
namespace theory {
namespace quantifiers {
+TermEnumeration::TermEnumeration(QuantifiersBoundInference* qbi) : d_qbi(qbi) {}
+
Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index)
{
Trace("term-db-enum") << "Get enumerate term " << tn << " " << index
return d_enum_terms[tn][index];
}
-bool TermEnumeration::mayComplete(TypeNode tn)
-{
- std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
- d_may_complete.find(tn);
- if (it == d_may_complete.end())
- {
- // cache
- bool mc = mayComplete(tn, options::fmfTypeCompletionThresh());
- d_may_complete[tn] = mc;
- return mc;
- }
- return it->second;
-}
-
-bool TermEnumeration::mayComplete(TypeNode tn, unsigned maxCard)
-{
- bool mc = false;
- if (tn.isClosedEnumerable() && tn.isInterpretedFinite())
- {
- Cardinality c = tn.getCardinality();
- if (!c.isLargeFinite())
- {
- NodeManager* nm = NodeManager::currentNM();
- Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
- // check if less than fixed upper bound
- Node oth = nm->mkConst(Rational(maxCard));
- Node eq = nm->mkNode(LEQ, card, oth);
- eq = Rewriter::rewrite(eq);
- mc = eq.isConst() && eq.getConst<bool>();
- }
- }
- return mc;
-}
-
bool TermEnumeration::getDomain(TypeNode tn, std::vector<Node>& dom)
{
- if (!mayComplete(tn))
+ if (!d_qbi || !d_qbi->mayComplete(tn))
{
return false;
}
namespace theory {
namespace quantifiers {
+class QuantifiersBoundInference;
+
/** Term enumeration
*
* This class has utilities for enumerating terms. It stores
class TermEnumeration
{
public:
- TermEnumeration() {}
+ TermEnumeration(QuantifiersBoundInference* qbi = nullptr);
~TermEnumeration() {}
/** get i^th term for type tn */
Node getEnumerateTerm(TypeNode tn, unsigned i);
- /** may complete type
- *
- * Returns true if the type tn is closed enumerable, is interpreted as a
- * finite type, and has cardinality less than some reasonable value
- * (currently < 1000). This method caches the results of whether each type
- * may be completed.
- */
- bool mayComplete(TypeNode tn);
- /**
- * Static version of the above method where maximum cardinality is
- * configurable.
- */
- static bool mayComplete(TypeNode tn, unsigned cardMax);
/** get domain
*
- * If tn is a type such that mayComplete(tn) returns true, this method
+ * If tn is a type such that d_qbi.mayComplete(tn) returns true, this method
* adds all domain elements of tn to dom and returns true. Otherwise, this
* method returns false.
*/
bool getDomain(TypeNode tn, std::vector<Node>& dom);
private:
+ /**
+ * Reference to quantifiers bound inference, which determines when it is
+ * possible to enumerate the entire domain of a type. If this is not provided,
+ * getDomain above always returns false.
+ */
+ QuantifiersBoundInference* d_qbi;
/** ground terms enumerated for types */
std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
d_enum_terms;
std::unordered_map<TypeNode, size_t, TypeNodeHashFunction> d_typ_enum_map;
/** type enumerators */
std::vector<TypeEnumerator> d_typ_enum;
- /** closed enumerable type cache */
- std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_typ_closed_enum;
- /** may complete */
- std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_may_complete;
};
} /* CVC4::theory::quantifiers namespace */
{
Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
- this, qstate, d_qreg, "FirstOrderModelFmc"));
- d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this, qstate));
+ this, qstate, qr, "FirstOrderModelFmc"));
+ d_builder.reset(
+ new quantifiers::fmcheck::FullModelChecker(this, qstate, qr));
}else{
Trace("quant-engine-debug") << "...make default model builder." << std::endl;
d_model.reset(new quantifiers::FirstOrderModel(
- this, qstate, d_qreg, "FirstOrderModel"));
- d_builder.reset(new quantifiers::QModelBuilder(this, qstate));
+ this, qstate, qr, "FirstOrderModel"));
+ d_builder.reset(new quantifiers::QModelBuilder(this, qstate, qr));
}
}else{
d_model.reset(new quantifiers::FirstOrderModel(
{
d_util.push_back(d_qmodules->d_rel_dom.get());
}
+
+ // handle any circular dependencies
+
+ // quantifiers bound inference needs to be informed of the bounded integers
+ // module, which has information about which quantifiers have finite bounds
+ d_qreg.getQuantifiersBoundInference().finishInit(d_qmodules->d_bint.get());
}
DecisionManager* QuantifiersEngine::getDecisionManager()
return d_tr_trie.get();
}
-bool QuantifiersEngine::isFiniteBound(Node q, Node v) const
-{
- quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
- if (bi && bi->isBound(q, v))
- {
- return true;
- }
- TypeNode tn = v.getType();
- if (tn.isSort() && options::finiteModelFind())
- {
- return true;
- }
- else if (d_treg.getTermEnumeration()->mayComplete(tn))
- {
- return true;
- }
- return false;
-}
-
-BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const
-{
- quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
- if (bi)
- {
- return bi->getBoundVarType(q, v);
- }
- return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
-}
-
-void QuantifiersEngine::getBoundVarIndices(Node q,
- std::vector<unsigned>& indices) const
-{
- Assert(indices.empty());
- // we take the bounded variables first
- quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
- if (bi)
- {
- bi->getBoundVarIndices(q, indices);
- }
- // then get the remaining ones
- for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
- {
- if (std::find(indices.begin(), indices.end(), i) == indices.end())
- {
- indices.push_back(i);
- }
- }
-}
-
-bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi,
- bool initial,
- Node q,
- Node v,
- std::vector<Node>& elements) const
-{
- quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
- if (bi)
- {
- return bi->getBoundElements(rsi, initial, q, v, elements);
- }
- return false;
-}
-
void QuantifiersEngine::presolve() {
Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
d_qim.clearPending();
*/
void finishInit(TheoryEngine* te, DecisionManager* dm);
//---------------------- end private initialization
- public:
- /** does variable v of quantified formula q have a finite bound? */
- bool isFiniteBound(Node q, Node v) const;
- /** get bound var type
- *
- * This returns the type of bound that was inferred for variable v of
- * quantified formula q.
- */
- BoundVarType getBoundVarType(Node q, Node v) const;
- /**
- * Get the indices of bound variables, in the order they should be processed
- * in a RepSetIterator.
- *
- * For details, see BoundedIntegers::getBoundVarIndices.
- */
- void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
- /**
- * Get bound elements
- *
- * This gets the (finite) enumeration of the range of variable v of quantified
- * formula q and adds it into the vector elements in the context of the
- * iteration being performed by rsi. It returns true if it could successfully
- * determine this range.
- *
- * For details, see BoundedIntegers::getBoundElements.
- */
- bool getBoundElements(RepSetIterator* rsi,
- bool initial,
- Node q,
- Node v,
- std::vector<Node>& elements) const;
public:
/** presolve */
projects / cvc5.git / commitdiff