From 2b64e19e84787c7f510a2e7a536be563072e1c8e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 5 Nov 2014 19:57:24 +0100 Subject: [PATCH] Fix model bug in --mbqi=fmc. Minor cleanup in datatypes. --- src/theory/datatypes/theory_datatypes.cpp | 20 +++++++++++--------- src/theory/quantifiers/first_order_model.cpp | 18 +++++++++++++----- src/theory/rep_set.cpp | 9 +++++++++ src/theory/rep_set.h | 2 ++ src/theory/theory_model.cpp | 3 +++ 5 files changed, 38 insertions(+), 14 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 83d14149b..f3b8c1ec9 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -170,9 +170,9 @@ void TheoryDatatypes::check(Effort e) { TypeNode tn = n.getType(); if( DatatypesRewriter::isTypeDatatype( tn ) ){ Trace("datatypes-debug") << "Process equivalence class " << n << std::endl; - EqcInfo* eqc = getOrMakeEqcInfo( n, true ); + EqcInfo* eqc = getOrMakeEqcInfo( n ); //if there are more than 1 possible constructors for eqc - if( eqc->d_constructor.get().isNull() && !hasLabel( eqc, n ) ) { + if( !hasLabel( eqc, n ) ){ Trace("datatypes-debug") << "No constructor..." << std::endl; const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); @@ -191,7 +191,7 @@ void TheoryDatatypes::check(Effort e) { if( consIndex==-1 ){ consIndex = j; } - if( !dt[ j ].isFinite() && !eqc->d_selectors ) { + if( !dt[ j ].isFinite() && ( !eqc || !eqc->d_selectors ) ) { needSplit = false; } } @@ -832,7 +832,7 @@ d_inst( c, false ), d_constructor( c, Node::null() ), d_selectors( c, false ){ } bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){ - return !eqc->d_constructor.get().isNull() || !getLabel( n ).isNull(); + return ( eqc && !eqc->d_constructor.get().isNull() ) || !getLabel( n ).isNull(); } Node TheoryDatatypes::getLabel( Node n ) { @@ -847,7 +847,7 @@ Node TheoryDatatypes::getLabel( Node n ) { } int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){ - if( !eqc->d_constructor.get().isNull() ){ + if( eqc && !eqc->d_constructor.get().isNull() ){ return Datatype::indexOf( eqc->d_constructor.get().getOperator().toExpr() ); }else{ return Datatype::indexOf( getLabel( n ).getOperator().toExpr() ); @@ -1118,7 +1118,7 @@ void TheoryDatatypes::computeCareGraph(){ TNode x = f1[k]; TNode y = f2[k]; Assert(d_equalityEngine.hasTerm(x)); - Assert(d_equalityEngine.hasTerm(y)); + Assert(d_equalityEngine.hasTerm(y)); if( areDisequal(x, y) ){ somePairIsDisequal = true; break; @@ -1209,7 +1209,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ cons.push_back( c ); eqc_cons[ eqc ] = c; }else{ - //if eqc contains a symbol known to datatypes (a selector), then we must assign + //if eqc contains a symbol known to datatypes (a selector), then we must assign bool containsTSym = false; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ @@ -1815,7 +1815,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ addLemma = true; } } - + if( !addLemma ){ TypeNode tn = n[0].getType(); if( !DatatypesRewriter::isTypeDatatype( tn ) ){ @@ -1907,7 +1907,9 @@ void TheoryDatatypes::printModelDebug( const char* c ){ //add terms to model eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ - Trace( c ) << (*eqc_i) << " "; + if( (*eqc_i)!=eqc ){ + Trace( c ) << (*eqc_i) << " "; + } ++eqc_i; } Trace( c ) << "}" << std::endl; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 07fea3cca..1570ba306 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -677,18 +677,24 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { Node curr; for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { Node v = d_models[op]->d_value[i]; + Trace("fmc-model-func") << "Value is : " << v << std::endl; 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 ); + //check if it is a constant introduced as a representative not existing in the model's equality engine + if( !d_rep_set.hasRep( tn, v ) ){ + 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 ); + } + Trace("fmc-model-func") << "No term, assign " << v << std::endl; } } v = getRepresentative( v ); if( curr.isNull() ){ + Trace("fmc-model-func") << "base : " << v << std::endl; curr = v; }else{ //make the condition @@ -711,6 +717,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { } Assert( !children.empty() ); Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ); + + Trace("fmc-model-func") << "condition : " << cc << ", value : " << v << std::endl; curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr ); } } diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index ee14d6fc1..db0524034 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -28,6 +28,15 @@ void RepSet::clear(){ d_tmap.clear(); } +bool RepSet::hasRep( TypeNode tn, Node n ) { + std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.find( tn ); + if( it==d_type_reps.end() ){ + return false; + }else{ + return std::find( it->second.begin(), it->second.end(), n )!=it->second.end(); + } +} + int RepSet::getNumRepresentatives( TypeNode tn ) const{ std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn ); if( it!=d_type_reps.end() ){ diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 23db36ead..19bb6d3d3 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -37,6 +37,8 @@ public: void clear(); /** has type */ bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); } + /** has rep */ + bool hasRep( TypeNode tn, Node n ); /** get cardinality for type */ int getNumRepresentatives( TypeNode tn ) const; /** add representative for type */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 54a647d89..7e1129e7b 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -169,9 +169,11 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const if (n.getNumChildren() > 0 && n.getKind() != kind::BITVECTOR_ACKERMANIZE_UDIV && n.getKind() != kind::BITVECTOR_ACKERMANIZE_UREM) { + Debug("model-getvalue-debug") << "Get model value children " << n << std::endl; std::vector children; if (n.getKind() == APPLY_UF) { Node op = getModelValue(n.getOperator(), hasBoundVars); + Debug("model-getvalue-debug") << " operator : " << op << std::endl; children.push_back(op); } else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -180,6 +182,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const //evaluate the children for (unsigned i = 0; i < n.getNumChildren(); ++i) { ret = getModelValue(n[i], hasBoundVars); + Debug("model-getvalue-debug") << " " << n << "[" << i << "] is " << ret << std::endl; children.push_back(ret); } ret = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children)); -- 2.30.2