From: ajreynol Date: Sat, 1 Nov 2014 12:01:31 +0000 (+0100) Subject: Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemmas being... X-Git-Tag: cvc5-1.0.0~6532 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6b652f7239aaf7ef1793eb115a6e7371a3ec54eb;p=cvc5.git Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemmas being rewritten). Minor improvement to dt care graph. Reenable regressions. --- diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 77cab86a2..2b5e52415 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1096,7 +1096,10 @@ void TheoryDatatypes::computeCareGraph(){ Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl; if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){ EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y); - if( eqStatus!=EQUALITY_UNKNOWN ){ + if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_UNKNOWN ){ + somePairIsDisequal = true; + break; + }else{ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES); TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES); Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl; @@ -1433,10 +1436,19 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, return it->second; }else{ //add constructor to equivalence class - Node n_ic = DatatypesRewriter::getInstCons( n, dt, index ); + Node k = n; + if( n.getKind()==APPLY_CONSTRUCTOR ){ + //must construct variable to refer to n, add lemma immediately + k = NodeManager::currentNM()->mkSkolem( "k", n.getType(), "for dt instantiation" ); + Node eq = k.eqNode( n ); + Trace("datatypes-infer") << "DtInfer : instantiation ref : " << eq << std::endl; + d_out->lemma( eq ); + } + Node n_ic = DatatypesRewriter::getInstCons( k, dt, index ); if( isActive ){ for( unsigned i = 0; i