From 2f716d8e5eaf4a75c2cf2e431b96ac1f3c9b8a5f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 7 Oct 2013 10:02:57 -0500 Subject: Multiple fixes for datatypes theory solver: add support for parametric datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup. --- src/smt/smt_engine.cpp | 4 + src/theory/datatypes/datatypes_rewriter.h | 8 +- src/theory/datatypes/theory_datatypes.cpp | 230 ++++++++++++++++++++++++------ src/theory/datatypes/theory_datatypes.h | 2 + src/theory/datatypes/type_enumerator.h | 46 +++++- src/theory/quantifiers/model_engine.cpp | 7 +- src/theory/quantifiers/options | 2 +- src/theory/quantifiers_engine.cpp | 112 +++++++++++---- src/theory/quantifiers_engine.h | 8 +- 9 files changed, 329 insertions(+), 90 deletions(-) (limited to 'src') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 85a245a09..be6acd09c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1031,6 +1031,10 @@ void SmtEngine::setLogicInternal() throw() { options::fmfInstGen.set( false ); } } + if ( options::fmfBoundInt() ){ + //if bounded integers are set, must use full model check for MBQI + options::fmfFullModelCheck.set( true ); + } if( options::ufssSymBreak() ){ options::sortInference.set( true ); } diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 186444e0a..0bbef1601 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -32,7 +32,7 @@ class DatatypesRewriter { public: static RewriteResponse postRewrite(TNode in) { - Trace("datatypes-rewrite") << "post-rewriting " << in << std::endl; + Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl; if(in.getKind() == kind::APPLY_CONSTRUCTOR ){ Type t = in.getType().toType(); @@ -41,7 +41,7 @@ public: // to ensure a normal form, all parameteric datatype constructors must have a type ascription if( dt.isParametric() ){ if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){ - Trace("datatypes-rewrite") << "Ascribing type to parametric datatype constructor " << in << std::endl; + Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl; Node op = in.getOperator(); //get the constructor object const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())]; @@ -53,7 +53,7 @@ public: children.push_back( op_new ); children.insert( children.end(), in.begin(), in.end() ); Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); - Trace("datatypes-rewrite") << "Created " << inr << std::endl; + Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl; return RewriteResponse(REWRITE_DONE, inr); } } @@ -214,7 +214,7 @@ public: } static RewriteResponse preRewrite(TNode in) { - Trace("datatypes-rewrite") << "pre-rewriting " << in << std::endl; + Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl; return RewriteResponse(REWRITE_DONE, in); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index a0651efb4..c827a8f07 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -26,6 +26,8 @@ #include "smt/options.h" #include "smt/boolean_terms.h" #include "theory/quantifiers/options.h" +#include "theory/datatypes/options.h" +#include "theory/type_enumerator.h" #include @@ -158,15 +160,18 @@ void TheoryDatatypes::check(Effort e) { } } if( !needSplit && mustSpecifyAssignment() ){ + // && //for the sake of termination, we must choose the constructor of a ground term //NEED GUARENTEE: groundTerm should not contain any subterms of the same type //** TODO: this is probably not good enough, actually need fair enumeration strategy + /* Node groundTerm = n.getType().mkGroundTerm(); int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); if( pcons[index] ){ consIndex = index; } needSplit = true; + */ } if( needSplit && consIndex!=-1 ) { Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n ); @@ -179,7 +184,7 @@ void TheoryDatatypes::check(Effort e) { d_out->requirePhase( test, true ); return; }else{ - Trace("dt-split") << "Do not split constructor for " << n << std::endl; + Trace("dt-split-debug") << "Do not split constructor for " << n << std::endl; } } }else{ @@ -503,6 +508,9 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ trep2 = eqc2->d_constructor.get(); } EqcInfo* eqc1 = getOrMakeEqcInfo( t1 ); + + + if( eqc1 ){ if( !eqc1->d_constructor.get().isNull() ){ trep1 = eqc1->d_constructor.get(); @@ -538,6 +546,29 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ eqc1->d_inst = true; } if( cons1.isNull() && !cons2.isNull() ){ + Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl; + NodeListMap::iterator lbl_i = d_labels.find( t1 ); + if( lbl_i != d_labels.end() ){ + size_t constructorIndex = Datatype::indexOf(cons2.getOperator().toExpr()); + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + if( (*i).getKind()==NOT ){ + if( Datatype::indexOf( (*i)[0].getOperator().toExpr() )==constructorIndex ){ + Node n = *i; + std::vector< TNode > assumptions; + explain( *i, assumptions ); + explain( cons2.eqNode( (*i)[0][0] ), assumptions ); + d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); + Debug("datatypes-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; + Debug("datatypes-conflict-temp") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; + return; + } + } + } + } + checkInst = true; eqc1->d_constructor.set( eqc2->d_constructor ); } @@ -548,14 +579,18 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ eqc1->d_inst.set( eqc2->d_inst ); eqc1->d_constructor.set( eqc2->d_constructor ); } + + + //merge labels - Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl; NodeListMap::iterator lbl_i = d_labels.find( t2 ); if( lbl_i != d_labels.end() ){ + Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl; NodeList* lbl = (*lbl_i).second; for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){ addTester( *j, eqc1, t1 ); if( d_conflict ){ + Debug("datatypes-debug") << "Conflict!" << std::endl; return; } } @@ -643,7 +678,7 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool > void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ if( !d_conflict ){ - Debug("datatypes-labels") << "Add tester " << t << " " << eqc << std::endl; + Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl; bool tpolarity = t.getKind()!=NOT; Node tt = ( t.getKind() == NOT ) ? t[0] : t; int ttindex = Datatype::indexOf( tt.getOperator().toExpr() ); @@ -768,6 +803,28 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Trace("dt-model") << std::endl; printModelDebug( "dt-model" ); m->assertEqualityEngine( &d_equalityEngine ); + + std::vector< TypeEnumerator > vec; + std::map< TypeNode, int > tes; + Trace("dt-cmi") << "Datatypes : Collect model info " << std::endl; + + //get all constructors + eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); + std::vector< Node > cons; + while( !eqccs_i.isFinished() ){ + Node eqc = (*eqccs_i); + //for all equivalence classes that are datatypes + if( DatatypesRewriter::isTermDatatype( eqc ) ){ + EqcInfo* ei = getOrMakeEqcInfo( eqc ); + if( ei ){ + if( !ei->d_constructor.get().isNull() ){ + cons.push_back( ei->d_constructor.get() ); + } + } + } + ++eqccs_i; + } + //must choose proper representatives eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ @@ -778,10 +835,63 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ if( ei ){ if( !ei->d_constructor.get().isNull() ){ //specify that we should use the constructor as the representative - m->assertRepresentative( ei->d_constructor.get() ); + //m->assertRepresentative( ei->d_constructor.get() ); }else{ - Trace("model-warn") << "WARNING: Datatypes: no constructor in equivalence class " << eqc << std::endl; - Trace("model-warn") << " Type : " << eqc.getType() << std::endl; + Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; + Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; + + std::vector< bool > pcons; + getPossibleCons( ei, eqc, pcons ); + Trace("dt-cmi") << "Possible constructors : "; + for( unsigned i=0; iareEqual( cons[i][j], n[j] ) ){ + diff = true; + break; + } + } + if( !diff ){ + Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; + success = false; + break; + } + } + } + }else{ + Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl; + success = false; + } + }while( !success ); + Trace("dt-cmi") << "Assign : " << n << std::endl; + //m->assertRepresentative( n ); + m->assertEquality( eqc, n, true ); + } }else{ Trace("model-warn") << "WARNING: Datatypes: no equivalence class info for " << eqc << std::endl; @@ -871,7 +981,38 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index return n_ic; //} } - +/* +Node TheoryDatatypes::applyTypeAscriptions( Node n, TypeNode tn ){ + Debug("dt-ta-debug") << "Apply type ascriptions " << n << " " << tn << std::endl; + if( n.getKind()==APPLY_CONSTRUCTOR ){ + //add type ascription for ambiguous constructor types + if(!n.getType().isComparableTo(tn)) { + size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr()); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( dt.isParametric() ); + Debug("dt-ta-debug") << "Ambiguous type for " << n << ", ascribe to " << tn << std::endl; + Debug("dt-ta-debug") << "Constructor is " << dt[constructorIndex] << std::endl; + Type tspec = dt[constructorIndex].getSpecializedConstructorType(tn.toType()); + Debug("dt-ta-debug") << "Type specification is " << tspec << std::endl; + Node op = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(tspec)), n.getOperator() ); + std::vector< Node > children; + children.push_back( op ); + for( unsigned i=0; imkNode( APPLY_CONSTRUCTOR, children ) ); + Assert( n.getType()==tn ); + return n; + } + }else{ + if( n.getType()!=tn ){ + Debug("dt-ta-debug") << "Bad type : " << n.getType() << std::endl; + } + } + return n; +} +*/ void TheoryDatatypes::collapseSelectors(){ //must check incorrect applications of selectors for( BoolMap::iterator it = d_selector_apps.begin(); it != d_selector_apps.end(); ++it ){ @@ -918,7 +1059,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ int index = getLabelIndex( eqc, n ); const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype(); //must be finite or have a selector - if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){ + //if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){ //instantiate this equivalence class eqc->d_inst = true; Node tt_cons = getInstantiateCons( tt, dt, index ); @@ -933,7 +1074,10 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ d_infer.push_back( eq ); d_infer_exp.push_back( exp ); } - } + //} + //else{ + // Debug("datatypes-inst") << "Do not instantiate" << std::endl; + //} } } @@ -1094,43 +1238,45 @@ void TheoryDatatypes::printModelDebug( const char* c ){ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); - if( DatatypesRewriter::isTermDatatype( eqc ) ){ - Trace( c ) << "DATATYPE : "; - } - Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl; - Trace( c ) << " { "; - //add terms to model - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - Trace( c ) << (*eqc_i) << " "; - ++eqc_i; - } - Trace( c ) << "}" << std::endl; - if( DatatypesRewriter::isTermDatatype( eqc ) ){ - EqcInfo* ei = getOrMakeEqcInfo( eqc ); - if( ei ){ - Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl; - if( ei->d_constructor.get().isNull() ){ - Trace("model-warn") << eqc << " has no constructor in equivalence class!" << std::endl; - Trace("model-warn") << " Type : " << eqc.getType() << std::endl; - Trace( c ) << " Constructor : " << std::endl; - Trace( c ) << " Labels : "; - if( hasLabel( ei, eqc ) ){ - Trace( c ) << getLabel( eqc ); - }else{ - NodeListMap::iterator lbl_i = d_labels.find( eqc ); - if( lbl_i != d_labels.end() ){ - NodeList* lbl = (*lbl_i).second; - for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){ - Trace( c ) << *j << " "; + if( !eqc.getType().isBoolean() ){ + if( DatatypesRewriter::isTermDatatype( eqc ) ){ + Trace( c ) << "DATATYPE : "; + } + Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl; + Trace( c ) << " { "; + //add terms to model + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Trace( c ) << (*eqc_i) << " "; + ++eqc_i; + } + Trace( c ) << "}" << std::endl; + if( DatatypesRewriter::isTermDatatype( eqc ) ){ + EqcInfo* ei = getOrMakeEqcInfo( eqc ); + if( ei ){ + Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl; + if( ei->d_constructor.get().isNull() ){ + Trace("debug-model-warn") << eqc << " has no constructor in equivalence class!" << std::endl; + Trace("debug-model-warn") << " Type : " << eqc.getType() << std::endl; + Trace( c ) << " Constructor : " << std::endl; + Trace( c ) << " Labels : "; + if( hasLabel( ei, eqc ) ){ + Trace( c ) << getLabel( eqc ); + }else{ + NodeListMap::iterator lbl_i = d_labels.find( eqc ); + if( lbl_i != d_labels.end() ){ + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){ + Trace( c ) << *j << " "; + } } } + Trace( c ) << std::endl; + }else{ + Trace( c ) << " Constructor : " << ei->d_constructor.get() << std::endl; } - Trace( c ) << std::endl; - }else{ - Trace( c ) << " Constructor : " << ei->d_constructor.get() << std::endl; + Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl; } - Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl; } } ++eqcs_i; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index e38c522c5..203782a79 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -226,6 +226,8 @@ private: void collectTerms( Node n ); /** get instantiate cons */ Node getInstantiateCons( Node n, const Datatype& dt, int index ); + /** apply type ascriptions */ + //Node applyTypeAscriptions( Node n, TypeNode tn ); /** process new term that was created internally */ void processNewTerm( Node n ); /** check instantiate */ diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 778304f32..cec1dccfc 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -37,6 +37,8 @@ class DatatypesEnumerator : public TypeEnumeratorBase { size_t d_zeroCtor; /** Delegate enumerators for the arguments of the current constructor */ TypeEnumerator** d_argEnumerators; + /** type */ + TypeNode d_type; /** Allocate and initialize the delegate enumerators */ void newEnumerators() { @@ -65,7 +67,8 @@ public: d_datatype(DatatypeType(type.toType()).getDatatype()), d_ctor(0), d_zeroCtor(0), - d_argEnumerators(NULL) { + d_argEnumerators(NULL), + d_type(type) { //Assert(type.isDatatype()); Debug("te") << "datatype is datatype? " << type.isDatatype() << std::endl; @@ -76,8 +79,21 @@ public: /* FIXME: this isn't sufficient for mutually-recursive datatypes! */ while(d_zeroCtor < d_datatype.getNumConstructors()) { bool recursive = false; - for(size_t a = 0; a < d_datatype[d_zeroCtor].getNumArgs() && !recursive; ++a) { - recursive = (Node::fromExpr(d_datatype[d_zeroCtor][a].getSelector()).getType()[1] == type); + if( d_datatype.isParametric() ){ + TypeNode tn = TypeNode::fromType( d_datatype[d_zeroCtor].getSpecializedConstructorType(d_type.toType()) ); + for( unsigned i=0; i b(kind::APPLY_CONSTRUCTOR); - b << ctor.getConstructor(); + Type typ; + if( d_datatype.isParametric() ){ + typ = d_datatype[d_ctor].getSpecializedConstructorType(d_type.toType()); + b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) ); + }else{ + b << ctor.getConstructor(); + } try { for(size_t a = 0; a < d_datatype[d_ctor].getNumArgs(); ++a) { if(d_argEnumerators[a] == NULL) { - d_argEnumerators[a] = new TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a].getSelector()).getType()[1]); + if( d_datatype.isParametric() ){ + d_argEnumerators[a] = new TypeEnumerator(TypeNode::fromType( typ )[a]); + }else{ + d_argEnumerators[a] = new TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a].getSelector()).getType()[1]); + } } b << **d_argEnumerators[a]; } } catch(NoMoreValuesException&) { InternalError(); } - return Node(b); + Node nnn = Node(b); + //if( nnn.getType()!=d_type || !nnn.getType().isComparableTo(d_type) ){ + // Debug("dt-warn") << "WARNING : Enum : " << nnn << " bad type : " << nnn.getType() << " " << d_type << std::endl; + //} + return nnn; } else { throw NoMoreValuesException(getType()); } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index cb8cb8154..b1a0c4ed4 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -139,6 +139,11 @@ bool ModelEngine::optOneQuantPerRound(){ int ModelEngine::checkModel(){ FirstOrderModel* fm = d_quantEngine->getModel(); + + //flatten the representatives + //Trace("model-engine-debug") << "Flattening representatives...." << std::endl; + //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps ); + //for debugging if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); @@ -149,7 +154,7 @@ int ModelEngine::checkModel(){ Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); for( size_t i=0; isecond.size(); i++ ){ //Trace("model-engine-debug") << it->second[i] << " "; - Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] ); + Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 57211ade7..fd114df04 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -98,7 +98,7 @@ option finiteModelFind --finite-model-find bool :default false option fmfModelBasedInst /--disable-fmf-mbqi bool :default true disable model-based quantifier instantiation for finite model finding -option fmfFullModelCheck --fmf-fmc bool :default false +option fmfFullModelCheck --fmf-fmc bool :default false :read-write enable full model check for finite model finding option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2ae5edb39..c14ee01ce 100755 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -102,7 +102,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_eq_query; } -EqualityQuery* QuantifiersEngine::getEqualityQuery() { +EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() { return d_eq_query; } @@ -594,8 +594,9 @@ Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){ eq::EqualityEngine* ee = getEngine(); if( ee->hasTerm( a ) ){ return ee->getRepresentative( a ); + }else{ + return a; } - return a; } bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ @@ -631,14 +632,10 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, if( !options::internalReps() ){ return r; }else{ - int sortId = 0; - if( optInternalRepSortInference() && !f.isNull() ){ - sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] ); - } - if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){ + if( d_int_rep.find( r )==d_int_rep.end() ){ //find best selection for representative Node r_best; - if( options::fmfRelevantDomain() ){ + if( options::fmfRelevantDomain() && !f.isNull() ){ Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl; r_best = d_qe->getModelEngine()->getRelevantDomain()->getRelevantTerm( f, index, r ); Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl; @@ -656,13 +653,6 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, //if cbqi is active, do not choose instantiation constant terms if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){ int score = getRepScore( eqc[i], f, index ); - //base it on sort information as well - if( sortId!=0 ){ - int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i] ); - if( score>=0 && e_sortId!=sortId ){ - score += 100; - } - } //score prefers earliest use of this term as a representative if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || scoregetTermDatabase()->getInstantiationConstant( f, index ); - r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); + if( !f.isNull() ){ + Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index ); + r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); + }else{ + r_best = a; + } } //now, make sure that no other member of the class is an instance - if( !optInternalRepSortInference() ){ - r_best = getInstance( r_best, eqc ); - } + r_best = getInstance( r_best, eqc ); //store that this representative was chosen at this point if( d_rep_score.find( r_best )==d_rep_score.end() ){ d_rep_score[ r_best ] = d_reset_count; } Trace("internal-rep-select") << "...Choose " << r_best << std::endl; } - d_int_rep[sortId][r] = r_best; + d_int_rep[r] = r_best; if( r_best!=a ){ Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl; Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl; } - if( optInternalRepSortInference() ){ - int sortIdBest = d_qe->getTheoryEngine()->getSortInference()->getSortId( r_best ); - if( sortId!=sortIdBest ){ - Trace("sort-inf-rep") << "Choosing representative with bad type " << r_best << " " << sortId << " " << sortIdBest << std::endl; - } - } return r_best; }else{ - return d_int_rep[sortId][r]; + return d_int_rep[r]; } } } +void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) { + //make sure internal representatives currently exist + for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){ + if( it->first.isSort() ){ + for( unsigned i=0; isecond.size(); i++ ){ + Node r = getInternalRepresentative( it->second[i], Node::null(), 0 ); + } + } + } + Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl; + for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ + Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl; + } + //store representatives for newly created terms + std::map< Node, Node > temp_rep_map; + + bool success; + do { + success = false; + for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ + if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){ + Node ni = it->second; + std::vector< Node > cc; + cc.push_back( it->second.getOperator() ); + bool changed = false; + for( unsigned j=0; jsecond << " to subterm " << ni[j] << std::endl; + d_int_rep[it->first] = ni[j]; + changed = false; + success = true; + break; + }else{ + Node ir = d_int_rep[r]; + cc.push_back( ir ); + if( ni[j]!=ir ){ + changed = true; + } + } + }else{ + changed = false; + break; + } + } + if( changed ){ + Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc ); + Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl; + success = true; + d_int_rep[it->first] = n; + temp_rep_map[n] = it->first; + } + } + } + }while( success ); + Trace("internal-rep-flatten") << "---After flattening : " << std::endl; + for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ + Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl; + } +} + eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ return d_qe->getMasterEqualityEngine(); } @@ -758,6 +811,3 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){ //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth } -bool EqualityQueryQuantifiersEngine::optInternalRepSortInference() { - return false; //shown to be not effective -} diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index b075f7be8..8f645afe7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -142,7 +142,7 @@ public: TheoryEngine* getTheoryEngine() { return d_te; } /** get equality query object for the given type. The default is the generic one */ - EqualityQuery* getEqualityQuery(); + EqualityQueryQuantifiersEngine* getEqualityQuery(); /** get instantiation engine */ quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } /** get model engine */ @@ -277,7 +277,7 @@ private: /** pointer to theory engine */ QuantifiersEngine* d_qe; /** internal representatives */ - std::map< int, std::map< Node, Node > > d_int_rep; + std::map< Node, Node > d_int_rep; /** rep score */ std::map< Node, int > d_rep_score; /** reset count */ @@ -289,8 +289,6 @@ private: Node getInstance( Node n, std::vector< Node >& eqc ); /** get score */ int getRepScore( Node n, Node f, int index ); - /** choose rep based on sort inference */ - bool optInternalRepSortInference(); public: EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){} ~EqualityQueryQuantifiersEngine(){} @@ -308,6 +306,8 @@ public: not contain instantiation constants, if such a term exists. */ Node getInternalRepresentative( Node a, Node f, int index ); + /** flatten representatives */ + void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ); void setLiberal( bool l ) { d_liberal = l; } }; /* EqualityQueryQuantifiersEngine */ -- cgit v1.2.3