From: Andrew Reynolds Date: Mon, 14 Apr 2014 20:36:28 +0000 (-0500) Subject: Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). Improve... X-Git-Tag: cvc5-1.0.0~6966 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1138911e0af7c15a7b41a5d02ff3edab2c837449;p=cvc5.git Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). Improve datatypes rewrite, make option for previous dt semantics. --- diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 8cb3fb4a2..99245ef69 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -138,26 +138,25 @@ public: << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); }else{ - if( options::dtRewriteErrorSel() ){ - Node gt; - if( in.getType().isSort() ){ - TypeEnumerator te(in.getType()); - gt = *te; - }else{ - gt = in.getType().mkGroundTerm(); - } - TypeNode gtt = gt.getType(); - //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); - if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){ - gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); - } - Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " - << "Rewrite trivial selector " << in - << " to distinguished ground term " - << in.getType().mkGroundTerm() << std::endl; - return RewriteResponse(REWRITE_DONE,gt ); + //typically should not be called + Node gt; + if( in.getType().isSort() ){ + TypeEnumerator te(in.getType()); + gt = *te; + }else{ + gt = in.getType().mkGroundTerm(); } + TypeNode gtt = gt.getType(); + //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); + if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){ + gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); + } + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + << "Rewrite trivial selector " << in + << " to distinguished ground term " + << in.getType().mkGroundTerm() << std::endl; + return RewriteResponse(REWRITE_DONE,gt ); } } if(in.getKind() == kind::TUPLE_SELECT && @@ -204,11 +203,18 @@ public: return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } - if(in.getKind() == kind::EQUAL && - checkClash(in[0], in[1])) { - Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; - return RewriteResponse(REWRITE_DONE, - NodeManager::currentNM()->mkConst(false)); + if(in.getKind() == kind::EQUAL ) { + std::vector< Node > rew; + if( checkClash(in[0], in[1], rew) ){ + Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(false)); + }else if( rew.size()!=1 || rew[0]!=in ){ + Node nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) : + ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); + Trace("datatypes-rewrite") << "Rewrite equality to " << nn << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, nn ); + } } return RewriteResponse(REWRITE_DONE, in); @@ -222,7 +228,7 @@ public: static inline void init() {} static inline void shutdown() {} - static bool checkClash( Node n1, Node n2 ) { + static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) { if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) || (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) || (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) { @@ -231,18 +237,14 @@ public: } else { Assert( n1.getNumChildren() == n2.getNumChildren() ); for( int i=0; i<(int)n1.getNumChildren(); i++ ) { - if( checkClash( n1[i], n2[i] ) ) { + if( checkClash( n1[i], n2[i], rew ) ) { return true; } } } - }else if( !isTermDatatype( n1 ) ){ - //also check for clashes between non-datatypes + }else{ Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); - eq = Rewriter::rewrite( eq ); - if( eq==NodeManager::currentNM()->mkConst(false) ){ - return true; - } + rew.push_back( eq ); } return false; } diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options index 1daa30981..fcf36648d 100644 --- a/src/theory/datatypes/options +++ b/src/theory/datatypes/options @@ -9,8 +9,8 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory # then we do not rewrite such a selector term to an arbitrary ground term. # For example, by default cvc4 considers cdr( nil ) = nil. If this option is set, then # cdr( nil ) has no set value. -expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true - disable rewriting incorrectly applied selectors to arbitrary ground term +expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false + rewrite incorrectly applied selectors to arbitrary ground term option dtForceAssignment /--dt-force-assignment bool :default false :read-write force the datatypes solver to give specific values to all datatypes terms before answering sat diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index fc37c5417..4858d99db 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -327,15 +327,18 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { switch( n.getKind() ){ case kind::APPLY_SELECTOR: { - Node selector = n.getOperator(); - Expr selectorExpr = selector.toExpr(); + Node selector = n.getOperator(); + Expr selectorExpr = selector.toExpr(); + Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] ); + if( options::dtRewriteErrorSel() ){ + return sel; + }else{ size_t selectorIndex = Datatype::cindexOf(selectorExpr); const Datatype& dt = Datatype::datatypeOf(selectorExpr); const DatatypeConstructor& c = dt[selectorIndex]; Expr tester = c.getTester(); Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] ); tst = Rewriter::rewrite( tst ); - Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] ); Node n_ret; if( tst==NodeManager::currentNM()->mkConst( true ) ){ n_ret = sel; @@ -357,6 +360,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl; return n_ret; } + } break; default: return n; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 54be11b44..d5c2b0e9d 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -648,7 +648,18 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); Node curr; for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { - Node v = getRepresentative( d_models[op]->d_value[i] ); + Node v = d_models[op]->d_value[i]; + if( !hasTerm( v ) ){ + //can happen when the model basis term does not exist in ground assignment + TypeNode tn = v.getType(); + if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){ + //see full_model_check.cpp line 366 + v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ]; + }else{ + Assert( false ); + } + } + v = getRepresentative( v ); if( curr.isNull() ){ curr = v; }else{ @@ -664,7 +675,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { if( !isStar(cond[j][1]) ){ children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) ); } - }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground representatives of this type... + }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground eqc of this type d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){ Node c = getUsedRepresentative( cond[j] ); children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 6c889781d..126b30b81 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -937,7 +937,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n void FullModelChecker::doNegate( Def & dc ) { for (unsigned i=0; i