#include "expr/type.h"
#include "options/datatypes_options.h"
#include "options/set_language.h"
+#include "theory/type_enumerator.h"
using namespace std;
Expr Datatype::mkGroundTerm(Type t) const
{
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
+ return mkGroundTermInternal(t, false);
+}
+
+Expr Datatype::mkGroundValue(Type t) const
+{
+ PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
+ return mkGroundTermInternal(t, true);
+}
+
+Expr Datatype::mkGroundTermInternal(Type t, bool isValue) const
+{
ExprManagerScope ems(d_self);
- Debug("datatypes") << "mkGroundTerm of type " << t << std::endl;
+ Debug("datatypes") << "mkGroundTerm of type " << t
+ << ", isValue = " << isValue << std::endl;
// is this already in the cache ?
- std::map< Type, Expr >::iterator it = d_ground_term.find( t );
- if( it != d_ground_term.end() ){
+ std::map<Type, Expr>& cache = isValue ? d_ground_value : d_ground_term;
+ std::map<Type, Expr>::iterator it = cache.find(t);
+ if (it != cache.end())
+ {
Debug("datatypes") << "\nin cache: " << d_self << " => " << it->second << std::endl;
return it->second;
- } else {
- std::vector< Type > processing;
- Expr groundTerm = computeGroundTerm( t, processing );
- if(!groundTerm.isNull() ) {
- // we found a ground-term-constructing constructor!
- d_ground_term[t] = groundTerm;
- Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
- }
- if( groundTerm.isNull() ){
- if( !d_isCo ){
- // if we get all the way here, we aren't well-founded
- IllegalArgument(*this, "datatype is not well-founded, cannot construct a ground term!");
- }else{
- return groundTerm;
- }
- }else{
- return groundTerm;
+ }
+ std::vector<Type> processing;
+ Expr groundTerm = computeGroundTerm(t, processing, isValue);
+ if (!groundTerm.isNull())
+ {
+ // we found a ground-term-constructing constructor!
+ cache[t] = groundTerm;
+ Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm
+ << std::endl;
+ }
+ if (groundTerm.isNull())
+ {
+ if (!d_isCo)
+ {
+ // if we get all the way here, we aren't well-founded
+ IllegalArgument(
+ *this,
+ "datatype is not well-founded, cannot construct a ground term!");
}
}
+ return groundTerm;
}
Expr getSubtermWithType( Expr e, Type t, bool isTop ){
}
}
-Expr Datatype::computeGroundTerm(Type t, std::vector<Type>& processing) const
+Expr Datatype::computeGroundTerm(Type t,
+ std::vector<Type>& processing,
+ bool isValue) const
{
if( std::find( processing.begin(), processing.end(), t )==processing.end() ){
processing.push_back( t );
//do nullary constructors first
if( ((*i).getNumArgs()==0)==(r==0)){
Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl;
- Expr e = (*i).computeGroundTerm( t, processing, d_ground_term );
+ Expr e =
+ (*i).computeGroundTerm(t, processing, d_ground_term, isValue);
if( !e.isNull() ){
//must check subterms for the same type to avoid infinite loops in type enumeration
Expr se = getSubtermWithType( e, t, true );
Expr DatatypeConstructor::computeGroundTerm(Type t,
std::vector<Type>& processing,
- std::map<Type, Expr>& gt) const
+ std::map<Type, Expr>& gt,
+ bool isValue) const
{
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_constructor);
// for each selector, get a ground term
std::vector< Type > instTypes;
std::vector< Type > paramTypes;
- if( DatatypeType(t).isParametric() ){
+ bool isParam = static_cast<DatatypeType>(t).isParametric();
+ if (isParam)
+ {
paramTypes = DatatypeType(t).getDatatype().getParameters();
instTypes = DatatypeType(t).getParamTypes();
}
for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
Type selType = SelectorType((*i).getSelector().getType()).getRangeType();
- if( DatatypeType(t).isParametric() ){
+ if (isParam)
+ {
selType = selType.substitute( paramTypes, instTypes );
}
Expr arg;
arg = itgt->second;
}else{
const Datatype & dt = DatatypeType(selType).getDatatype();
- arg = dt.computeGroundTerm( selType, processing );
+ arg = dt.computeGroundTerm(selType, processing, isValue);
}
- }else{
- arg = selType.mkGroundTerm();
+ }
+ else
+ {
+ // call mkGroundValue or mkGroundTerm based on isValue
+ arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm();
}
if( arg.isNull() ){
Debug("datatypes") << "...unable to construct arg of " << (*i).getName() << std::endl;
}
Expr groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
- if( groundTerm.getType()!=t ){
- Assert(Datatype::datatypeOf(d_constructor).isParametric());
- //type is ambiguous, must apply type ascription
+ if (isParam)
+ {
+ Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
+ // type is parametric, must apply type ascription
Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl;
groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))),
Cardinality computeCardinality(Type t, std::vector<Type>& processing) const;
/** compute whether this datatype is well-founded */
bool computeWellFounded(std::vector<Type>& processing) const;
- /** compute ground term */
+ /** compute ground term
+ *
+ * This method is used for constructing a term that is an application
+ * of this constructor whose type is t.
+ *
+ * The argument processing is the set of datatype types we are currently
+ * traversing. This is used to avoid infinite loops.
+ *
+ * The argument gt caches the ground terms we have computed so far.
+ *
+ * The argument isValue is whether we are constructing a constant value. If
+ * this flag is false, we are constructing a canonical ground term that is
+ * not necessarily constant.
+ */
Expr computeGroundTerm(Type t,
std::vector<Type>& processing,
- std::map<Type, Expr>& gt) const;
+ std::map<Type, Expr>& gt,
+ bool isValue) const;
/** compute shared selectors
* This computes the maps d_shared_selectors and d_shared_selector_index.
*/
* type if this datatype is parametric.
*/
Expr mkGroundTerm(Type t) const;
+ /** Make ground value
+ *
+ * Same as above, but constructs a constant value instead of a ground term.
+ * These two notions typically coincide. However, for uninterpreted sorts,
+ * they do not: mkGroundTerm returns a fresh variable whereas mkValue returns
+ * an uninterpreted constant. The motivation for mkGroundTerm is that
+ * unintepreted constants should never appear in lemmas. The motivation for
+ * mkGroundValue is for things like type enumeration and model construction.
+ */
+ Expr mkGroundValue(Type t) const;
/**
* Get the DatatypeType associated to this Datatype. Can only be
mutable int d_well_founded;
/** cache of ground term for this datatype */
mutable std::map<Type, Expr> d_ground_term;
+ /** cache of ground values for this datatype */
+ mutable std::map<Type, Expr> d_ground_value;
/** cache of shared selectors for this datatype */
mutable std::map<Type, std::map<Type, std::map<unsigned, Expr> > >
d_shared_sel;
std::vector<Type>& u_assume) const;
/** compute whether this datatype is well-founded */
bool computeWellFounded(std::vector<Type>& processing) const;
- /** compute ground term */
- Expr computeGroundTerm(Type t, std::vector<Type>& processing) const;
+ /** compute ground term
+ *
+ * This method checks if there is a term of this datatype whose type is t
+ * that is finitely constructable. As needed, it traverses its subfield types.
+ *
+ * The argument processing is the set of datatype types we are currently
+ * traversing.
+ *
+ * The argument isValue is whether we are constructing a constant value. If
+ * this flag is false, we are constructing a canonical ground term that is
+ * not necessarily constant.
+ */
+ Expr computeGroundTerm(Type t,
+ std::vector<Type>& processing,
+ bool isValue) const;
/** Get the shared selector
*
* This returns the index^th (constructor-agnostic)
* this returns the term sel_{dtt}^{t,index}.
*/
Expr getSharedSelector(Type dtt, Type t, unsigned index) const;
+ /**
+ * Helper for mkGroundTerm and mkGroundValue above.
+ */
+ Expr mkGroundTermInternal(Type t, bool isValue) const;
};/* class Datatype */
/**
return d_typeNode->mkGroundTerm().toExpr();
}
+Expr Type::mkGroundValue() const
+{
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->mkGroundValue().toExpr();
+}
+
bool Type::isSubtypeOf(Type t) const {
NodeManagerScope nms(d_nodeManager);
return d_typeNode->isSubtypeOf(*t.d_typeNode);
*/
Expr mkGroundTerm() const;
+ /**
+ * Construct and return a ground value for this Type. Throws an
+ * exception if this type is not well-founded.
+ *
+ * This is the same as mkGroundTerm, but constructs a constant value instead
+ * of a canonical ground term. These two notions typically coincide. However,
+ * for uninterpreted sorts, they do not: mkGroundTerm returns a fresh variable
+ * whereas mkValue returns an uninterpreted constant. The motivation for
+ * mkGroundTerm is that unintepreted constants should never appear in lemmas.
+ * The motivation for mkGroundValue is for e.g. type enumeration and model
+ * construction.
+ */
+ Expr mkGroundValue() const;
+
/**
* Is this type a subtype of the given type?
*/
#include "options/expr_options.h"
#include "options/quantifiers_options.h"
#include "options/uf_options.h"
+#include "theory/type_enumerator.h"
using namespace std;
return kind::mkGroundTerm(*this);
}
+Node TypeNode::mkGroundValue() const
+{
+ theory::TypeEnumerator te(*this);
+ return *te;
+}
+
bool TypeNode::isSubtypeOf(TypeNode t) const {
if(*this == t) {
return true;
*/
Node mkGroundTerm() const;
+ /**
+ * Construct and return a ground value of this type. If the type is
+ * not well founded, this function throws an exception.
+ *
+ * @return a ground value of the type
+ */
+ Node mkGroundValue() const;
+
/**
* Is this type a subtype of the given type?
*/
}
}
- Node DatatypesEnumerator::getCurrentTerm( unsigned index ){
- Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type << std::endl;
+ Node DatatypesEnumerator::getCurrentTerm(unsigned index)
+ {
+ Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type
+ << std::endl;
Node ret;
- if( index<d_has_debruijn ){
- if( d_child_enum ){
- ret = NodeManager::currentNM()->mkConst(UninterpretedConstant(d_type.toType(), d_size_limit));
- }else{
- //no top-level variables
+ if (index < d_has_debruijn)
+ {
+ if (d_child_enum)
+ {
+ ret = NodeManager::currentNM()->mkConst(
+ UninterpretedConstant(d_type.toType(), d_size_limit));
+ }
+ else
+ {
+ // no top-level variables
return Node::null();
}
- }else{
- Debug("dt-enum-debug") << "Look at constructor " << (index - d_has_debruijn) << std::endl;
+ }
+ else
+ {
+ Debug("dt-enum-debug")
+ << "Look at constructor " << (index - d_has_debruijn) << std::endl;
DatatypeConstructor ctor = d_datatype[index - d_has_debruijn];
Debug("dt-enum-debug") << "Check last term..." << std::endl;
- //we first check if the last argument (which is forced to make sum of iterated arguments equal to d_size_limit) is defined
+ // we first check if the last argument (which is forced to make sum of
+ // iterated arguments equal to d_size_limit) is defined
Node lc;
- if( ctor.getNumArgs()>0 ){
+ if (ctor.getNumArgs() > 0)
+ {
Assert(index < d_sel_types.size());
Assert(ctor.getNumArgs() - 1 < d_sel_types[index].size());
- lc = getTermEnum( d_sel_types[index][ctor.getNumArgs()-1], d_size_limit - d_sel_sum[index] );
- if( lc.isNull() ){
+ lc = getTermEnum(d_sel_types[index][ctor.getNumArgs() - 1],
+ d_size_limit - d_sel_sum[index]);
+ if (lc.isNull())
+ {
Debug("dt-enum-debug") << "Current infeasible." << std::endl;
return Node::null();
}
Debug("dt-enum-debug") << "Get constructor..." << std::endl;
NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
Type typ;
- if( d_datatype.isParametric() ){
+ if (d_datatype.isParametric())
+ {
typ = ctor.getSpecializedConstructorType(d_type.toType());
- b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
- NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) );
- }else{
+ b << NodeManager::currentNM()->mkNode(
+ kind::APPLY_TYPE_ASCRIPTION,
+ NodeManager::currentNM()->mkConst(AscriptionType(typ)),
+ Node::fromExpr(ctor.getConstructor()));
+ }
+ else
+ {
b << ctor.getConstructor();
}
Debug("dt-enum-debug") << "Get arguments..." << std::endl;
- if( ctor.getNumArgs()>0 ){
+ if (ctor.getNumArgs() > 0)
+ {
Assert(index < d_sel_types.size());
Assert(index < d_sel_index.size());
Assert(d_sel_types[index].size() == ctor.getNumArgs());
Assert(d_sel_index[index].size() == ctor.getNumArgs() - 1);
- for( int i=0; i<(int)(ctor.getNumArgs()-1); i++ ){
- Node c = getTermEnum( d_sel_types[index][i], d_sel_index[index][i] );
+ for (int i = 0; i < (int)(ctor.getNumArgs() - 1); i++)
+ {
+ Node c = getTermEnum(d_sel_types[index][i], d_sel_index[index][i]);
Assert(!c.isNull());
b << c;
}
b << lc;
}
Node nnn = Node(b);
- Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
+ Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
ret = nnn;
}
- if( !d_child_enum && d_has_debruijn ){
- Node nret = DatatypesRewriter::normalizeCodatatypeConstant( ret );
- if( nret!=ret ){
- if( nret.isNull() ){
+ if (!d_child_enum && d_has_debruijn)
+ {
+ Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret);
+ if (nret != ret)
+ {
+ if (nret.isNull())
+ {
Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl;
- }else{
+ }
+ else
+ {
Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl;
Trace("dt-enum-nn") << " ...normal form is : " << nret << std::endl;
}
return ret;
}
- void DatatypesEnumerator::init(){
- //Assert(type.isDatatype());
- Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
+ void DatatypesEnumerator::init()
+ {
+ Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype()
+ << std::endl;
Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
Debug("dt-enum") << "datatype is " << d_type << std::endl;
- Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton( d_type.toType() );
- Debug("dt-enum") << " " << d_datatype.isInterpretedFinite( d_type.toType() ) << std::endl;
+ Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " "
+ << d_datatype.isRecursiveSingleton(d_type.toType());
+ Debug("dt-enum") << " " << d_datatype.isInterpretedFinite(d_type.toType())
+ << std::endl;
- if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
- //start with uninterpreted constant
- d_zeroCtor = 0;
+ if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype))
+ {
+ // start with uninterpreted constant
d_has_debruijn = 1;
- d_sel_types.push_back( std::vector< TypeNode >() );
- d_sel_index.push_back( std::vector< unsigned >() );
- d_sel_sum.push_back( -1 );
- }else{
- // find the "zero" constructor via mkGroundTerm
+ d_sel_types.push_back(std::vector<TypeNode>());
+ d_sel_index.push_back(std::vector<unsigned>());
+ d_sel_sum.push_back(-1);
+ }
+ else
+ {
+ // find the "zero" term via mkGroundTerm
Debug("dt-enum-debug") << "make ground term..." << std::endl;
- Node t = d_type.mkGroundTerm();
- Debug("dt-enum-debug") << "done : " << t << std::endl;
- Assert(t.getKind() == kind::APPLY_CONSTRUCTOR);
- // start with the constructor for which a ground term is constructed
- d_zeroCtor = datatypes::utils::indexOf(t.getOperator());
+ // Start with the ground term constructed via mkGroundValue, which does
+ // a traversal over the structure of the datatype to find a finite term.
+ // Notice that mkGroundValue may be dependent upon extracting the first
+ // value of type enumerators for *other non-datatype* subfield types of
+ // this datatype. Since datatypes can not be embedded in non-datatype
+ // types (e.g. (Array D D) cannot be a subfield type of datatype D), this
+ // call is guaranteed to avoid infinite recursion.
+ d_zeroTerm = Node::fromExpr(d_datatype.mkGroundValue(d_type.toType()));
+ d_zeroTermActive = true;
+ Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl;
+ Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR);
d_has_debruijn = 0;
}
- Debug("dt-enum") << "zero ctor : " << d_zeroCtor << std::endl;
- d_ctor = d_zeroCtor;
- for( unsigned i=0; i<d_datatype.getNumConstructors(); ++i ){
- d_sel_types.push_back( std::vector< TypeNode >() );
- d_sel_index.push_back( std::vector< unsigned >() );
- d_sel_sum.push_back( -1 );
+ Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl;
+ d_ctor = 0;
+ for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++i)
+ {
+ d_sel_types.push_back(std::vector<TypeNode>());
+ d_sel_index.push_back(std::vector<unsigned>());
+ d_sel_sum.push_back(-1);
DatatypeConstructor ctor = d_datatype[i];
Type typ;
- if( d_datatype.isParametric() ){
+ if (d_datatype.isParametric())
+ {
typ = ctor.getSpecializedConstructorType(d_type.toType());
}
- for( unsigned a = 0; a < ctor.getNumArgs(); ++a ){
+ for (unsigned a = 0; a < ctor.getNumArgs(); ++a)
+ {
TypeNode tn;
- if( d_datatype.isParametric() ){
- tn = TypeNode::fromType( typ )[a];
- }else{
+ if (d_datatype.isParametric())
+ {
+ tn = TypeNode::fromType(typ)[a];
+ }
+ else
+ {
tn = Node::fromExpr(ctor[a].getSelector()).getType()[1];
}
- d_sel_types.back().push_back( tn );
- d_sel_index.back().push_back( 0 );
+ d_sel_types.back().push_back(tn);
+ d_sel_index.back().push_back(0);
}
- if( !d_sel_index.back().empty() ){
+ if (!d_sel_index.back().empty())
+ {
d_sel_index.back().pop_back();
}
}
d_size_limit = 0;
- //set up initial conditions (should always succeed)
- ++*this; //increment( d_ctor );
+ if (!d_zeroTermActive)
+ {
+ // Set up initial conditions (should always succeed). Here, we are calling
+ // the increment function of this class, which ensures a term is ready to
+ // read via a dereference of this class. We use the same method for
+ // setting up the first term, if it is not already set up
+ // (d_zeroTermActive) using the increment function, for uniformity.
+ ++*this;
+ }
AlwaysAssert(!isFinished());
-}
+ }
+
+ DatatypesEnumerator& DatatypesEnumerator::operator++()
+ {
+ Debug("dt-enum-debug") << ": increment " << this << std::endl;
+ if (d_zeroTermActive)
+ {
+ d_zeroTermActive = false;
+ }
+ unsigned prevSize = d_size_limit;
+ while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
+ {
+ // increment at index
+ while (increment(d_ctor))
+ {
+ Node n = getCurrentTerm(d_ctor);
+ if (!n.isNull())
+ {
+ if (n == d_zeroTerm)
+ {
+ d_zeroTerm = Node::null();
+ }
+ else
+ {
+ return *this;
+ }
+ }
+ }
+ // Here, we need to step from the current constructor to the next one
+ // Go to the next constructor
+ d_ctor = d_ctor + 1;
+ if (d_ctor >= d_has_debruijn + d_datatype.getNumConstructors())
+ {
+ // try next size limit as long as new terms were generated at last size,
+ // or other cases
+ if (prevSize == d_size_limit
+ || (d_size_limit == 0 && d_datatype.isCodatatype())
+ || !d_datatype.isInterpretedFinite(d_type.toType()))
+ {
+ d_size_limit++;
+ d_ctor = 0;
+ for (unsigned i = 0; i < d_sel_sum.size(); i++)
+ {
+ d_sel_sum[i] = -1;
+ }
+ }
+ }
+ }
+ return *this;
+ }
TypeNode d_type;
/** The datatype constructor we're currently enumerating */
unsigned d_ctor;
- /** The "first" constructor to consider; it's non-recursive */
- unsigned d_zeroCtor;
+ /** The first term to consider in the enumeration */
+ Node d_zeroTerm;
+ /** Whether we are currently considering the above term */
+ bool d_zeroTermActive;
/** list of type enumerators (one for each type in a selector argument) */
std::map< TypeNode, unsigned > d_te_index;
std::vector< TypeEnumerator > d_children;
: TypeEnumeratorBase<DatatypesEnumerator>(type),
d_tep(tep),
d_datatype(DatatypeType(type.toType()).getDatatype()),
- d_type(type)
+ d_type(type),
+ d_ctor(0),
+ d_zeroTermActive(false)
{
d_child_enum = false;
init();
: TypeEnumeratorBase<DatatypesEnumerator>(type),
d_tep(tep),
d_datatype(DatatypeType(type.toType()).getDatatype()),
- d_type(type)
+ d_type(type),
+ d_ctor(0),
+ d_zeroTermActive(false)
{
d_child_enum = childEnum;
init();
}
- DatatypesEnumerator(const DatatypesEnumerator& de) :
- TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
- d_tep(de.d_tep),
- d_datatype(de.d_datatype),
- d_type(de.d_type),
- d_ctor(de.d_ctor),
- d_zeroCtor(de.d_zeroCtor) {
-
+ DatatypesEnumerator(const DatatypesEnumerator& de)
+ : TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
+ d_tep(de.d_tep),
+ d_datatype(de.d_datatype),
+ d_type(de.d_type),
+ d_ctor(de.d_ctor),
+ d_zeroTerm(de.d_zeroTerm),
+ d_zeroTermActive(de.d_zeroTermActive)
+ {
for( std::map< TypeNode, unsigned >::const_iterator it = de.d_te_index.begin(); it != de.d_te_index.end(); ++it ){
d_te_index[it->first] = it->second;
}
Node operator*() override
{
Debug("dt-enum-debug") << ": get term " << this << std::endl;
- if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) {
+ if (d_zeroTermActive)
+ {
+ return d_zeroTerm;
+ }
+ else if (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
+ {
return getCurrentTerm( d_ctor );
- } else {
- throw NoMoreValuesException(getType());
}
+ throw NoMoreValuesException(getType());
}
- DatatypesEnumerator& operator++() override
- {
- Debug("dt-enum-debug") << ": increment " << this << std::endl;
- unsigned prevSize = d_size_limit;
- while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) {
- //increment at index
- while( increment( d_ctor ) ){
- Node n = getCurrentTerm( d_ctor );
- if( !n.isNull() ){
- return *this;
- }
- }
- // Here, we need to step from the current constructor to the next one
-
- // Find the next constructor (only complicated by the notion of the "zero" constructor
- d_ctor = (d_ctor == d_zeroCtor) ? 0 : d_ctor + 1;
- if(d_ctor == d_zeroCtor) {
- ++d_ctor;
- }
- if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){
- //try next size limit as long as new terms were generated at last size, or other cases
- if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite( d_type.toType() ) ){
- d_size_limit++;
- d_ctor = d_zeroCtor;
- for( unsigned i=0; i<d_sel_sum.size(); i++ ){
- d_sel_sum[i] = -1;
- }
- }
- }
- }
- return *this;
- }
+ DatatypesEnumerator& operator++() override;
bool isFinished() override
{
}
//must ensure model basis terms exists in model for each relevant type
+ Trace("fmc") << "preInitialize types..." << std::endl;
fm->initialize();
for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
Node op = it->first;
for( unsigned i=0; i<tno.getNumChildren(); i++) {
Trace("fmc") << "preInitializeType " << tno[i] << std::endl;
preInitializeType( fm, tno[i] );
+ Trace("fmc") << "finished preInitializeType " << tno[i] << std::endl;
}
}
+ Trace("fmc") << "Finish preInitialize types" << std::endl;
//do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
if( !options::fmfEmptySorts() ){
for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
d_preinitialized_types[tn] = true;
if (!tn.isFunction() || options::ufHo())
{
+ Trace("fmc") << "Get model basis term " << tn << "..." << std::endl;
Node mb = fm->getModelBasisTerm(tn);
+ Trace("fmc") << "...return " << mb << std::endl;
// if the model basis term does not exist in the model,
// either add it directly to the model's equality engine if no other terms
// of this type exist, or otherwise assert that it is equal to the first
return false;
}
+ Trace("model-builder")
+ << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl;
// model-builder specific initialization
if (!preProcessBuildModel(tm))
{
return false;
}
+ Trace("model-builder")
+ << "TheoryEngineModelBuilder: Add assignable subterms..." << std::endl;
// Loop through all terms and make sure that assignable sub-terms are in the
// equality engine
// Also, record #eqc per type (for finite model finding)
regress1/datatypes/dt-param-card4-unsat.smt2
regress1/datatypes/error.cvc
regress1/datatypes/issue3266-small.smt2
+ regress1/datatypes/issue-variant-dt-zero.smt2
regress1/datatypes/manos-model.smt2
regress1/decision/error3.smtv1.smt2
regress1/decision/quant-Arrays_Q1-noinfer.smt2
regress1/quantifiers/isaplanner-goal20.smt2
regress1/quantifiers/issue2970-string-var-elim.smt2
regress1/quantifiers/issue3250-syg-inf-q.smt2
+ regress1/quantifiers/issue3316.smt2
regress1/quantifiers/issue3317.smt2
regress1/quantifiers/issue993.smt2
regress1/quantifiers/javafe.ast.StmtVec.009.smt2
--- /dev/null
+; COMMAND-LINE: --fmf-fun-rlv --no-check-models
+; EXPECT: sat
+(set-info :smt-lib-version 2.5)
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatypes () ((a0(c0$0)(c0$1(c0$1$0 String)(c0$1$1 Int))(c0$2(c0$2$0 Bool)(c0$2$1 Int)(c0$2$2 String)))
+ (a1(c1$0)(c1$1)(c1$2))
+ (a2(c2$0(c2$0$0 Int)(c2$0$1 a0)(c2$0$2 String)(c2$0$3 a3)(c2$0$4 String)(c2$0$5 Bool)))
+ (a3(c3$0(c3$0$0 a7)(c3$0$1 a1)(c3$0$2 a5)(c3$0$3 a6)(c3$0$4 Int)(c3$0$5 Bool)(c3$0$6 Bool))(c3$1(c3$1$0 String)))
+ (a4(c4$0(c4$0$0 String)(c4$0$1 a2)(c4$0$2 String))(c4$1(c4$1$0 a0)(c4$1$1 a4)(c4$1$2 a4)(c4$1$3 a7))(c4$2))
+ (a5(c5$0(c5$0$0 a2))(c5$1)(c5$2)(c5$3(c5$3$0 a0))(c5$4)(c5$5(c5$5$0 a4)(c5$5$1 Int))(c5$6))
+ (a6(c6$0(c6$0$0 a7)(c6$0$1 a7)(c6$0$2 String))(c6$1)(c6$2)(c6$3)(c6$4)(c6$5)(c6$6))
+ (a7(c7$0(c7$0$0 a2)(c7$0$1 Int))(c7$1(c7$1$0 a4)(c7$1$1 Int)(c7$1$2 Bool)))))
+(define-funs-rec ((f0((v0 a6))a4))
+ (c4$2))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --fmf-fun-rlv --no-check-models
+; EXPECT: sat
+(set-info :smt-lib-version 2.5)
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatypes () ((a0(c0$0)(c0$1(c0$1$0 String)(c0$1$1 Int))(c0$2(c0$2$0 Bool)(c0$2$1 Int)(c0$2$2 String)))
+ (a1(c1$0)(c1$1)(c1$2))
+ (a2(c2$0(c2$0$0 Int)(c2$0$1 a0)(c2$0$2 String)(c2$0$3 a3)(c2$0$4 String)(c2$0$5 Bool)))
+ (a3(c3$0(c3$0$0 a7)(c3$0$1 a1)(c3$0$2 a5)(c3$0$3 a6)(c3$0$4 Int)(c3$0$5 Bool)(c3$0$6 Bool))(c3$1(c3$1$0 String)))
+ (a4(c4$0(c4$0$0 String)(c4$0$1 a2)(c4$0$2 String))(c4$1(c4$1$0 a0)(c4$1$1 a4)(c4$1$2 a4)(c4$1$3 a7))(c4$2))
+ (a5(c5$0(c5$0$0 a2))(c5$1)(c5$2)(c5$3(c5$3$0 a0))(c5$4)(c5$5(c5$5$0 a4)(c5$5$1 Int))(c5$6))
+ (a6(c6$0(c6$0$0 a7)(c6$0$1 a7)(c6$0$2 String))(c6$1)(c6$2)(c6$3)(c6$4)(c6$5)(c6$6))
+ (a7(c7$0(c7$0$0 a2)(c7$0$1 Int))(c7$1(c7$1$0 a4)(c7$1$1 Int)(c7$1$2 Bool)))))
+(define-funs-rec ((f3((v4 Bool))a7)
+ (f2()a6)
+ (f1((v1 a3)(v2 a1)(v3 Bool))String)
+ (f0((v0 a6))a4))
+ ((c7$0 (c2$0 0 c0$0 "" (c3$1 "") "" true) 0)
+ c6$2
+ ""
+ c4$2))
+(check-sat)
projects / cvc5.git / commitdiff