From 6f6703473ccc66b3d2bdefed688602f93d33cd8f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 28 Apr 2014 12:28:16 -0500 Subject: [PATCH] Preparation for models for co-inductive datatypes. Minor cleanup. --- src/theory/datatypes/theory_datatypes.cpp | 114 ++++++++++++------ src/theory/datatypes/theory_datatypes.h | 2 + .../quantifiers/inst_match_generator.cpp | 7 +- src/theory/quantifiers/rewrite_engine.cpp | 1 + src/theory/quantifiers_engine.cpp | 6 - 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 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( indexareEqual( 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() || indexareEqual( 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; iassertEquality( 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 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; imkNode( 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 */ -- 2.30.2