This simplifies the approach for wrongly-applied selectors whose range type involves e.g. uninterpreted sorts. These cases are particularly tricky since uninterpreted constants should never appear in facts or lemmas.
Previously, the rewriter had special cases for either making a ground term or value, and a purify step was used to eliminate the occurrences of uninterpreted sorts afterwards.
This PR leverages mkGroundTerm in this inference instead, and makes the rewriter uniformly use mkGroundValue.
This also required making the type enumerator for datatypes more uniform. In particular, we require that the first value enumerated by the type enumerator is of the same shape as the term required by mkGroundTerm, or else debug-check-model will fail. This is due to the fact that now the inference for wrongly applied selectors uses terms while the rewriter uses values. The type enumerator is updated so that recursive codatatypes also first take mkGroundValue as the zero term, when they are well-founded. Previously this was skipped since the codatatype enumerator uses a different algorithm for computing its ground terms.
This is in preparation for further work on optimizations and proofs for datatypes.
}
else if (k == kind::APPLY_SELECTOR_TOTAL)
{
- Node gt;
- bool useTe = true;
- // if( !tn.isSort() ){
- // useTe = false;
- //}
- if (tn.isDatatype())
+ // evaluates to the first ground value of type tn.
+ Node gt = tn.mkGroundValue();
+ Assert(!gt.isNull());
+ if (tn.isDatatype() && !tn.isInstantiatedDatatype())
{
- const DType& dta = tn.getDType();
- useTe = !dta.isCodatatype();
- }
- if (useTe)
- {
- TypeEnumerator te(tn);
- gt = *te;
- }
- else
- {
- gt = tn.mkGroundTerm();
- }
- if (!gt.isNull())
- {
- // Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
- if (tn.isDatatype() && !tn.isInstantiatedDatatype())
- {
- gt = NodeManager::currentNM()->mkNode(
- kind::APPLY_TYPE_ASCRIPTION,
- NodeManager::currentNM()->mkConst(AscriptionType(tn.toType())),
- gt);
- }
- Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
- << "Rewrite trivial selector " << in
- << " to distinguished ground term " << gt
- << std::endl;
- return RewriteResponse(REWRITE_DONE, gt);
+ gt = NodeManager::currentNM()->mkNode(
+ kind::APPLY_TYPE_ASCRIPTION,
+ NodeManager::currentNM()->mkConst(AscriptionType(tn.toType())),
+ gt);
}
+ Trace("datatypes-rewrite")
+ << "DatatypesRewriter::postRewrite: "
+ << "Rewrite trivial selector " << in
+ << " to distinguished ground term " << gt << std::endl;
+ return RewriteResponse(REWRITE_DONE, gt);
}
}
return RewriteResponse(REWRITE_DONE, in);
eqc->d_constructor.set( c );
}
-Node TheoryDatatypes::removeUninterpretedConstants( Node n, std::map< Node, Node >& visited ){
- std::map< Node, Node >::iterator it = visited.find( n );
- if( it==visited.end() ){
- Node ret = n;
- if( n.getKind()==UNINTERPRETED_CONSTANT ){
- std::map< Node, Node >::iterator itu = d_uc_to_fresh_var.find( n );
- if( itu==d_uc_to_fresh_var.end() ){
- Node k = NodeManager::currentNM()->mkSkolem( "w", n.getType(), "Skolem for wrongly applied selector." );
- d_uc_to_fresh_var[n] = k;
- ret = k;
- }else{
- ret = itu->second;
- }
- }else if( n.getNumChildren()>0 ){
- std::vector< Node > children;
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.push_back( n.getOperator() );
- }
- bool childChanged = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node nc = removeUninterpretedConstants( n[i], visited );
- childChanged = childChanged || nc!=n[i];
- children.push_back( nc );
- }
- if( childChanged ){
- ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
- }
- visited[n] = ret;
- return ret;
- }else{
- return it->second;
- }
-}
-
void TheoryDatatypes::collapseSelector( Node s, Node c ) {
Assert(c.getKind() == APPLY_CONSTRUCTOR);
Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl;
r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
}
if( !r.isNull() ){
- Node rr = Rewriter::rewrite( r );
- Node rrs = rr;
- if( wrong ){
- // we have inference S_i( C_j( t ) ) = t' for i != j, where t' is result of mkGroundTerm.
- // we must eliminate uninterpreted constants for datatypes that have uninterpreted sort subfields,
- // since uninterpreted constants should not appear in lemmas
- std::map< Node, Node > visited;
- rrs = removeUninterpretedConstants( rr, visited );
+ Node rrs;
+ if (wrong)
+ {
+ // Must use make ground term here instead of the rewriter, since we
+ // do not want to introduce arbitrary values. This is important so that
+ // we avoid constants for types that are not "closed enumerable", e.g.
+ // uninterpreted sorts and arrays, where the solver does not fully
+ // handle values of the sort. The call to mkGroundTerm does not introduce
+ // values for these sorts.
+ rrs = r.getType().mkGroundTerm();
+ Trace("datatypes-wrong-sel")
+ << "Bad apply " << r << " term = " << rrs
+ << ", value = " << r.getType().mkGroundValue() << std::endl;
+ }
+ else
+ {
+ rrs = Rewriter::rewrite(r);
}
if (s != rrs)
{
void merge( Node t1, Node t2 );
/** collapse selector, s is of the form sel( n ) where n = c */
void collapseSelector( Node s, Node c );
- /** remove uninterpreted constants */
- Node removeUninterpretedConstants( Node n, std::map< Node, Node >& visited );
/** for checking if cycles exist */
void checkCycles();
Node searchForCycle(TNode n,
<< d_datatype.isRecursiveSingleton(d_type);
Debug("dt-enum") << " " << d_datatype.isInterpretedFinite(d_type)
<< std::endl;
-
+ // 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. It is important that we
+ // start with this term, since it has the same shape as the one returned by
+ // TypeNode::mkGroundTerm for d_type, which avoids debug check model
+ // failures.
+ d_zeroTerm = d_datatype.mkGroundValue(d_type);
+ // Only use the zero term if it was successfully constructed. This may
+ // fail for codatatype types whose only values are infinite.
+ d_zeroTermActive = !d_zeroTerm.isNull();
if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype))
{
// start with uninterpreted constant
{
// find the "zero" term via mkGroundTerm
Debug("dt-enum-debug") << "make ground term..." << std::endl;
- // 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 = d_datatype.mkGroundValue(d_type);
- d_zeroTermActive = true;
Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl;
Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR);
d_has_debruijn = 0;
projects / cvc5.git / commitdiff