From: ajreynol Date: Sat, 18 Oct 2014 21:10:40 +0000 (+0200) Subject: Add dt lemma: zero size implies nullary constructor. X-Git-Tag: cvc5-1.0.0~6552 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7671fc17558dbb52df67838b3ad7166cb39d698a;p=cvc5.git Add dt lemma: zero size implies nullary constructor. --- diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 3a41510dd..8214f23e2 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -260,7 +260,7 @@ public: } }else if( n1!=n2 ){ if( n1.isConst() && n2.isConst() ){ - return true; + return true; }else{ Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); rew.push_back( eq ); @@ -319,6 +319,23 @@ public: } return false; } + static bool isNullaryApplyConstructor( Node n ){ + Assert( n.getKind()==APPLY_CONSTRUCTOR ); + for( unsigned i=0; i " << n[i] << " " << result << endl; - if( result && !d_hasSeenCycle.get() ){ - Debug("datatypes-cycles") << "FOUND CYCLE" << std::endl; - } - d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); - //Node r = getRepresentative( n[i] ); - //EqcInfo* eqc = getOrMakeEqcInfo( r, true ); - //eqc->d_selectors = true; - } - */ }else if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE ){ d_selTerms.push_back( n ); //we must also record which selectors exist @@ -1413,7 +1399,7 @@ void TheoryDatatypes::collectTerms( Node n ) { EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); //add it to the eqc info addSelector( n, eqc, rep ); - + if( n.getKind() == DT_SIZE ){ Node conc = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), n ); //must be non-negative @@ -1421,6 +1407,23 @@ void TheoryDatatypes::collectTerms( Node n ) { d_pending.push_back( conc ); d_pending_exp[ conc ] = d_true; d_infer.push_back( conc ); + + //add size = 0 lemma + Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) ); + std::vector< Node > children; + children.push_back( nn.negate() ); + const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); + for( unsigned i=0; imkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] ); + children.push_back( test ); + } + } + conc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + Trace("datatypes-infer") << "DtInfer : zero size : " << conc << std::endl; + d_pending.push_back( conc ); + d_pending_exp[ conc ] = d_true; + d_infer.push_back( conc ); } } } @@ -1776,6 +1779,8 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ addLemma = true; }else if( n.getKind()==LEQ ){ addLemma = true; + }else if( n.getKind()==OR ){ + addLemma = true; } if( addLemma ){ //check if we have already added this lemma