In preparation for breaking more dependencies on TheoryEngine.
#include "context/context.h"
#include "expr/node.h"
#include "options/base_options.h"
+#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "printer/printer.h"
#include "proof/conv_proof_generator.h"
return n;
}
+bool Env::isFiniteType(TypeNode tn) const
+{
+ return isCardinalityClassFinite(tn.getCardinalityClass(),
+ d_options.quantifiers.finiteModelFind);
+}
+
} // namespace cvc5
*/
Node rewriteViaMethod(TNode n, MethodId idr = MethodId::RW_REWRITE);
+ //---------------------- information about cardinality of types
+ /**
+ * Is the cardinality of type tn finite? This method depends on whether
+ * finite model finding is enabled. If finite model finding is enabled, then
+ * we assume that all uninterpreted sorts have finite cardinality.
+ *
+ * Notice that if finite model finding is enabled, this method returns true
+ * if tn is an uninterpreted sort. It also returns true for the sort
+ * (Array Int U) where U is an uninterpreted sort. This type
+ * is finite if and only if U has cardinality one; for cases like this,
+ * we conservatively return that tn has finite cardinality.
+ *
+ * This method does *not* depend on the state of the theory engine, e.g.
+ * if U in the above example currently is entailed to have cardinality >1
+ * based on the assertions.
+ */
+ bool isFiniteType(TypeNode tn) const;
+
private:
/* Private initialization ------------------------------------------------- */
TypeNode tnc = children[c1].getType();
// we may only apply this symmetry breaking scheme (which introduces
// disequalities) if the types are infinite.
- if (tnc == children[c2].getType() && !d_state.isFiniteType(tnc))
+ if (tnc == children[c2].getType() && !d_env.isFiniteType(tnc))
{
Node sym_lem_deq = children[c1].eqNode(children[c2]).negate();
// notice that this symmetry breaking still allows for
for( unsigned i=0; i<pcons.size(); i++ ){
// must try the infinite ones first
bool cfinite =
- d_state.isFiniteType(dt[i].getSpecializedConstructorType(tt));
+ d_env.isFiniteType(dt[i].getSpecializedConstructorType(tt));
if( pcons[i] && (r==1)==cfinite ){
neqc = utils::getInstCons(eqc, dt, i);
break;
// supported for finite element types #1123). Regardless, this is
// typically not a limitation since this variable can be bound in a
// standard way below since its type is finite.
- if (!d_qstate.isFiniteType(v.getType()))
+ if (!d_env.isFiniteType(v.getType()))
{
setBoundedVar(f, v, BOUND_SET_MEMBER);
setBoundVar = true;
for( unsigned i=0; i<f[0].getNumChildren(); i++) {
if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
TypeNode tn = f[0][i].getType();
- if ((tn.isSort() && d_qstate.isFiniteType(tn))
+ if ((tn.isSort() && d_env.isFiniteType(tn))
|| d_qreg.getQuantifiersBoundInference().mayComplete(tn))
{
success = true;
for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
TypeNode tn = f[0][i].getType();
if( !tn.isSort() ){
- if (!d_qstate.isFiniteType(tn))
+ if (!d_env.isFiniteType(tn))
{
if( tn.isInteger() ){
if( !options::fmfBound() ){
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
TypeNode tn = q[0][i].getType();
if( tn.isDatatype() ){
- bool isFinite = d_qstate.isFiniteType(tn);
+ bool isFinite = d_env.isFiniteType(tn);
const DType& dt = tn.getDType();
if (dt.isRecursiveSingleton(tn))
{
if( d_pto_model[l].isNull() ){
Trace("sep-model") << "_";
TypeEnumerator te_range( data_type );
- if (d_state.isFiniteType(data_type))
+ if (d_env.isFiniteType(data_type))
{
pto_children.push_back( *te_range );
}else{
{
TypeNode data_type = d_loc_to_data_type[it->first];
// if the data type is finite
- if (!d_state.isFiniteType(data_type))
+ if (!d_env.isFiniteType(data_type))
{
continue;
}
{
NodeManager* nm = NodeManager::currentNM();
TypeNode setType = nm->mkSetType(t);
- bool finiteType = d_state.isFiniteType(t);
+ bool finiteType = d_env.isFiniteType(t);
// skip infinite types that do not have univset terms
if (!finiteType && d_state.getUnivSetEqClass(setType).isNull())
{
TheoryModel* model)
{
TypeNode elementType = eqc.getType().getSetElementType();
- bool elementTypeFinite = d_state.isFiniteType(elementType);
+ bool elementTypeFinite = d_env.isFiniteType(elementType);
if (isModelValueBasic(eqc))
{
std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
}
for (const Node& set : getOrderedSetsEqClasses())
{
- if (!d_state.isFiniteType(set.getType()))
+ if (!d_env.isFiniteType(set.getType()))
{
continue;
}
d_te(te),
d_logicInfo(logicInfo()),
d_sharedTerms(env, &d_te),
- d_preRegistrationVisitor(&te, context()),
- d_sharedTermsVisitor(&te, d_sharedTerms, context()),
+ d_preRegistrationVisitor(env, &te),
+ d_sharedTermsVisitor(env, &te, d_sharedTerms),
d_im(te.theoryOf(THEORY_BUILTIN)->getInferenceManager())
{
}
{
Assert(tn.isSequence());
TypeNode etn = tn.getSequenceElementType();
- if (!d_state.isFiniteType(etn))
+ if (!d_env.isFiniteType(etn))
{
// infinite cardinality, we are fine
return;
c = sel->getCurrent();
// if we are a sequence with infinite element type
if (tn.isSequence()
- && !d_state.isFiniteType(tn.getSequenceElementType()))
+ && !d_env.isFiniteType(tn.getSequenceElementType()))
{
// Make a skeleton instead. In particular, this means that
// a value:
* current. This method is used by PreRegisterVisitor and SharedTermsVisitor
* below.
*/
-bool isAlreadyVisited(TheoryEngine* te,
+bool isAlreadyVisited(Env& env,
TheoryIdSet visitedTheories,
TNode current,
TNode parent)
// do we need to consider the type?
TypeNode type = current.getType();
- if (currentTheoryId == parentTheoryId && !te->isFiniteType(type))
+ if (currentTheoryId == parentTheoryId && !env.isFiniteType(type))
{
// current and parent are the same theory, and we are infinite, return true
return true;
return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories);
}
+PreRegisterVisitor::PreRegisterVisitor(Env& env, TheoryEngine* engine)
+ : EnvObj(env), d_engine(engine), d_visited(context())
+{
+}
+
bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
}
TheoryIdSet visitedTheories = (*find).second;
- return isAlreadyVisited(d_engine, visitedTheories, current, parent);
+ return isAlreadyVisited(d_env, visitedTheories, current, parent);
}
void PreRegisterVisitor::visit(TNode current, TNode parent) {
// call the preregistration on current, parent or type theories and update
// visitedTheories. The set of preregistering theories coincides with
// visitedTheories here.
- preRegister(d_engine, visitedTheories, current, parent, visitedTheories);
+ preRegister(
+ d_env, d_engine, visitedTheories, current, parent, visitedTheories);
Debug("register::internal")
<< "PreRegisterVisitor::visit(" << current << "," << parent
Assert(alreadyVisited(current, parent));
}
-void PreRegisterVisitor::preRegister(TheoryEngine* te,
+void PreRegisterVisitor::preRegister(Env& env,
+ TheoryEngine* te,
TheoryIdSet& visitedTheories,
TNode current,
TNode parent,
// Note that if enclosed by different theories it's shared, for example,
// in read(a, f(a)), f(a) should be shared with integers.
TypeNode type = current.getType();
- if (currentTheoryId != parentTheoryId || te->isFiniteType(type))
+ if (currentTheoryId != parentTheoryId || env.isFiniteType(type))
{
// preregister with the type's theory, if necessary
TheoryId typeTheoryId = Theory::theoryOf(type);
void PreRegisterVisitor::start(TNode node) {}
+SharedTermsVisitor::SharedTermsVisitor(Env& env,
+ TheoryEngine* te,
+ SharedTermsDatabase& sharedTerms)
+ : EnvObj(env),
+ d_engine(te),
+ d_sharedTerms(sharedTerms),
+ d_preregistered(context())
+{
+}
+
std::string SharedTermsVisitor::toString() const {
std::stringstream ss;
TNodeVisitedMap::const_iterator it = d_visited.begin();
}
TheoryIdSet visitedTheories = (*find).second;
- return isAlreadyVisited(d_engine, visitedTheories, current, parent);
+ return isAlreadyVisited(d_env, visitedTheories, current, parent);
}
void SharedTermsVisitor::visit(TNode current, TNode parent) {
// preregister the term with the current, parent or type theories, as needed
PreRegisterVisitor::preRegister(
- d_engine, visitedTheories, current, parent, preregTheories);
+ d_env, d_engine, visitedTheories, current, parent, preregTheories);
// Record the new theories that we visited
d_visited[current] = visitedTheories;
#pragma once
+#include <unordered_map>
+
#include "context/context.h"
+#include "smt/env_obj.h"
#include "theory/shared_terms_database.h"
-#include <unordered_map>
-
namespace cvc5 {
class TheoryEngine;
* Computation of the set of theories in the original term are computed in the alreadyVisited method
* so as no to skip any theories.
*/
-class PreRegisterVisitor {
-
+class PreRegisterVisitor : protected EnvObj
+{
/** The engine */
TheoryEngine* d_engine;
/** required to instantiate template for NodeVisitor */
using return_type = void;
- PreRegisterVisitor(TheoryEngine* engine, context::Context* c)
- : d_engine(engine), d_visited(c)
- {
- }
+ PreRegisterVisitor(Env& env, TheoryEngine* engine);
/**
* Returns true is current has already been pre-registered with both current
* If there is no theory sharing, this coincides with visitedTheories.
* Otherwise, visitedTheories may be a subset of preregTheories.
*/
- static void preRegister(TheoryEngine* te,
+ static void preRegister(Env& env,
+ TheoryEngine* te,
theory::TheoryIdSet& visitedTheories,
TNode current,
TNode parent,
theory::TheoryIdSet preregTheories);
};
-
/**
* The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to
* be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has
* been visited already, we need to visit it again, since we need to associate it with both atoms.
*/
-class SharedTermsVisitor {
+class SharedTermsVisitor : protected EnvObj
+{
using TNodeVisitedMap = std::unordered_map<TNode, theory::TheoryIdSet>;
using TNodeToTheorySetMap = context::CDHashMap<TNode, theory::TheoryIdSet>;
/**
/** required to instantiate template for NodeVisitor */
using return_type = void;
- SharedTermsVisitor(TheoryEngine* te,
- SharedTermsDatabase& sharedTerms,
- context::Context* c)
- : d_engine(te), d_sharedTerms(sharedTerms), d_preregistered(c)
- {
- }
+ SharedTermsVisitor(Env& env,
+ TheoryEngine* te,
+ SharedTermsDatabase& sharedTerms);
/**
* Returns true is current has already been pre-registered with both current and parent theories.
}
}
-bool TheoryEngine::isFiniteType(TypeNode tn) const
-{
- return isCardinalityClassFinite(tn.getCardinalityClass(),
- options::finiteModelFind());
-}
-
void TheoryEngine::spendResource(Resource r)
{
d_env.getResourceManager()->spendResource(r);
*/
std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
- //---------------------- information about cardinality of types
- /**
- * Is the cardinality of type tn finite? This method depends on whether
- * finite model finding is enabled. If finite model finding is enabled, then
- * we assume that all uninterpreted sorts have finite cardinality.
- *
- * Notice that if finite model finding is enabled, this method returns true
- * if tn is an uninterpreted sort. It also returns true for the sort
- * (Array Int U) where U is an uninterpreted sort. This type
- * is finite if and only if U has cardinality one; for cases like this,
- * we conservatively return that tn has finite cardinality.
- *
- * This method does *not* depend on the state of the theory engine, e.g.
- * if U in the above example currently is entailed to have cardinality >1
- * based on the assertions.
- */
- bool isFiniteType(TypeNode tn) const;
- //---------------------- end information about cardinality of types
-
theory::SortInference* getSortInference() { return d_sortInfer.get(); }
/** Prints the assertions to the debug stream */
return false;
}
-bool TheoryEngineModelBuilder::isFiniteType(TypeNode tn) const
-{
- return isCardinalityClassFinite(tn.getCardinalityClass(),
- options::finiteModelFind());
-}
-
bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) const
{
if (tn.isSort())
if (t.isDatatype())
{
const DType& dt = t.getDType();
- isCorecursive = dt.isCodatatype()
- && (!isFiniteType(t) || dt.isRecursiveSingleton(t));
+ isCorecursive =
+ dt.isCodatatype()
+ && (!d_env.isFiniteType(t) || dt.isRecursiveSingleton(t));
}
#ifdef CVC5_ASSERTIONS
bool isUSortFiniteRestricted = false;
n = itAssigner->second.getNextAssignment();
Assert(!n.isNull());
}
- else if (t.isSort() || !isFiniteType(t))
+ else if (t.isSort() || !d_env.isFiniteType(t))
{
// If its interpreted as infinite, we get a fresh value that does
// not occur in the model.
bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m);
//------------------------------------end for codatatypes
- /**
- * Is the given type constrained to be finite? This depends on whether
- * finite model finding is enabled.
- */
- bool isFiniteType(TypeNode tn) const;
//---------------------------------for debugging finite model finding
/** does type tn involve an uninterpreted sort? */
bool involvesUSort(TypeNode tn) const;
return d_valuation.factsEnd(tid);
}
-bool TheoryState::isFiniteType(TypeNode tn) const
-{
- return d_valuation.isFiniteType(tn);
-}
-
Valuation& TheoryState::getValuation() { return d_valuation; }
} // namespace theory
context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
/** The beginning iterator of facts for theory tid.*/
context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
- /**
- * Is the cardinality of type tn finite? This method depends on whether
- * finite model finding is enabled. For details, see theory_engine.h.
- */
- bool isFiniteType(TypeNode tn) const;
/** Get the underlying valuation class */
Valuation& getValuation();
hasFunctions = true;
// if during collect model, must have an infinite type
// if not during collect model, must have a finite type
- if (d_state.isFiniteType(tn) != isCollectModel)
+ if (d_env.isFiniteType(tn) != isCollectModel)
{
func_eqcs[tn].push_back(eqc);
Trace("uf-ho-debug")
return theory->facts_end();
}
-bool Valuation::isFiniteType(TypeNode tn) const
-{
- return d_engine->isFiniteType(tn);
-}
-
} // namespace theory
} // namespace cvc5
context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
/** The beginning iterator of facts for theory tid.*/
context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
- /**
- * Is the cardinality of type tn finite? This method depends on whether
- * finite model finding is enabled. For details, see theory_engine.h.
- */
- bool isFiniteType(TypeNode tn) const;
};/* class Valuation */
} // namespace theory
projects / cvc5.git / commitdiff