diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-28 12:28:16 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-28 12:33:56 -0500 |
commit | 6f6703473ccc66b3d2bdefed688602f93d33cd8f (patch) | |
tree | d55fa0d80256641339ed286715f145ff18a5a8db /src/theory | |
parent | 9b97c9144875e072da4098f102f8989be26e5cdf (diff) |
Preparation for models for co-inductive datatypes. Minor cleanup.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 114 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 8 |
6 files changed, 81 insertions, 57 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9316c3fe8..2715f8e75 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -675,10 +675,10 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ d_infer.push_back( eq ); d_infer_exp.push_back( unifEq ); } - } + } /* std::vector< Node > rew; - if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){ + if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){ Assert(false); }else{ for( unsigned i=0; i<rew.size(); i++ ){ @@ -1072,7 +1072,7 @@ void TheoryDatatypes::computeCareGraph(){ } } } - } + } if (!somePairIsDisequal) { for (unsigned c = 0; c < currentPairs.size(); ++ c) { Trace("dt-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl; @@ -1133,6 +1133,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); std::vector< Node > cons; std::vector< Node > nodes; + std::map< Node, Node > eqc_cons; while( !eqccs_i.isFinished() ){ Node eqc = (*eqccs_i); //for all equivalence classes that are datatypes @@ -1140,51 +1141,55 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); if( !ei->d_constructor.get().isNull() ){ cons.push_back( ei->d_constructor.get() ); + eqc_cons[ eqc ] = ei->d_constructor.get(); }else{ nodes.push_back( eqc ); } } ++eqccs_i; } - + unsigned orig_size = nodes.size(); unsigned index = 0; while( index<nodes.size() ){ Node eqc = nodes[index]; Node neqc; + const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); if( !d_equalityEngine.hasTerm( eqc ) ){ - Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl; - Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; - //can assign arbitrary term - TypeEnumerator te(eqc.getType()); - bool success; - do{ - success = true; - Assert( !te.isFinished() ); - neqc = *te; - Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl; - ++te; - //if it is infinite or we are assigning to terms known by datatypes, make sure it is fresh - if( eqc.getType().getCardinality().isInfinite() || index<orig_size ){ - for( unsigned i=0; i<cons.size(); i++ ){ - //check if it is modulo equality the same - if( cons[i].getOperator()==neqc.getOperator() ){ - bool diff = false; - for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){ - if( !m->areEqual( cons[i][j], neqc[j] ) ){ - diff = true; + if( !dt.isCodatatype() ){ + Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl; + Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; + //can assign arbitrary term + TypeEnumerator te(eqc.getType()); + bool success; + do{ + success = true; + Assert( !te.isFinished() ); + neqc = *te; + Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl; + ++te; + //if it is infinite or we are assigning to terms known by datatypes, make sure it is fresh + if( eqc.getType().getCardinality().isInfinite() || index<orig_size ){ + for( unsigned i=0; i<cons.size(); i++ ){ + //check if it is modulo equality the same + if( cons[i].getOperator()==neqc.getOperator() ){ + bool diff = false; + for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){ + if( !m->areEqual( cons[i][j], neqc[j] ) ){ + diff = true; + break; + } + } + if( !diff ){ + Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; + success = false; break; } } - if( !diff ){ - Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; - success = false; - break; - } } } - } - }while( !success ); + }while( !success ); + } }else{ Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; @@ -1212,8 +1217,6 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ } Trace("dt-cmi") << std::endl; */ - - const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); for( unsigned r=0; r<2; r++ ){ if( neqc.isNull() ){ for( unsigned i=0; i<pcons.size(); i++ ){ @@ -1232,9 +1235,11 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ } } } - Assert( !neqc.isNull() ); - Trace("dt-cmi") << "Assign : " << neqc << std::endl; - m->assertEquality( eqc, neqc, true ); + if( !neqc.isNull() ){ + Trace("dt-cmi") << "Assign : " << neqc << std::endl; + m->assertEquality( eqc, neqc, true ); + eqc_cons[ eqc ] = neqc; + } /* for( unsigned kk=0; kk<all_eqc.size(); kk++ ){ for( unsigned ll=(kk+1); ll<all_eqc.size(); ll++ ){ @@ -1258,9 +1263,44 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ ++index; } + //assign MU for each codatatype eqc + std::map< Node, Node > eqc_mu; + for( std::map< Node, Node >::iterator it = eqc_cons.begin(); it != eqc_cons.end(); ++it ){ + Node eqc = it->first; + const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); + if( dt.isCodatatype() ){ + std::map< Node, Node > vmap; + Node v = getCodatatypesValue( it->first, eqc_cons, eqc_mu, vmap ); + Trace("dt-cmi-cod") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << std::endl; + } + } } +Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap ){ + std::map< Node, Node >::iterator itv = vmap.find( n ); + if( itv!=vmap.end() ){ + return itv->second; + }else if( DatatypesRewriter::isTermDatatype( n ) ){ + Node nv = NodeManager::currentNM()->mkBoundVar( n.getType() ); + vmap[n] = nv; + Trace("dt-cmi-cod-debug") << " map " << n << " -> " << nv << std::endl; + Node nc = eqc_cons[n]; + Assert( nc.getKind()==APPLY_CONSTRUCTOR ); + std::vector< Node > children; + children.push_back( nc.getOperator() ); + for( unsigned i=0; i<nc.getNumChildren(); i++ ){ + Node r = getRepresentative( nc[i] ); + Node rv = getCodatatypesValue( r, eqc_cons, eqc_mu, vmap ); + children.push_back( rv ); + } + vmap.erase( n ); + return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + }else{ + return n; + } +} + void TheoryDatatypes::collectTerms( Node n ) { if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){ d_collectTermsCache[n] = true; @@ -1802,7 +1842,7 @@ bool TheoryDatatypes::checkClashModEq( Node n1, Node n2, std::vector< Node >& ex } }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 ); if( d_equalityEngine.areDisequal( n1, n2, true ) ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 1c21c63b4..fe87d4439 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -253,6 +253,8 @@ private: std::vector< TNode >& exp, std::map< Node, Node >& cn, std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ); + /** build model */ + Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap ); /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 13186c7cc..da0a3c4f6 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -155,9 +155,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl; Assert( !d_match_pattern.isNull() ); - if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){ - return true; - }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){ + if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){ return false; }else{ EqualityQuery* q = qe->getEqualityQuery(); @@ -324,9 +322,6 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif m.add( baseMatch ); if( qe->addInstantiation( f, m ) ){ addedLemmas++; - if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){ - return addedLemmas; - } } }else{ addedLemmas++; diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 59ba40ca7..75f54d7d9 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -39,6 +39,7 @@ struct PrioritySort { RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) { d_true = NodeManager::currentNM()->mkConst( true ); + d_needsSort = true; } double RewriteEngine::getPriority( Node f ) { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 1837a34f4..be011cdb6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -109,12 +109,6 @@ d_lemmas_produced_c(u){ } //options - d_optInstCheckDuplicate = true; - d_optInstMakeRepresentative = true; - d_optInstAddSplits = false; - d_optMatchIgnoreModelBasis = false; - d_optInstLimitActive = false; - d_optInstLimit = 0; d_total_inst_count_debug = 0; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index e7843ab95..eb9803592 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -254,14 +254,6 @@ public: ~Statistics(); };/* class QuantifiersEngine::Statistics */ Statistics d_statistics; -public: - /** options */ - bool d_optInstCheckDuplicate; - bool d_optInstMakeRepresentative; - bool d_optInstAddSplits; - bool d_optMatchIgnoreModelBasis; - bool d_optInstLimitActive; - int d_optInstLimit; };/* class QuantifiersEngine */ |