diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-07 11:37:43 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-07 11:37:43 +0100 |
commit | 56a523d9c4dd04cedbd812570cd80e3bc94cce4c (patch) | |
tree | d53f96c61369f826ef38dbf07eea264d27f64c03 /src/theory | |
parent | e6a588264154bf4b93abd0aaac39dbf10c496e6f (diff) |
Properly distinguish which EQC to assign values in datatypes, use assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 23 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 2 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 5 |
6 files changed, 32 insertions, 12 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 22c0477d8..72d0c6b2b 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1183,8 +1183,10 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Node c = ei->d_constructor.get(); cons.push_back( c ); eqc_cons[ eqc ] = c; + m->assertRepresentative( c ); }else{ //if eqc contains a symbol known to datatypes (a selector), then we must assign +#if 0 bool shouldConsider = false; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ @@ -1196,9 +1198,10 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ } ++eqc_i; } -/* +#else + //should assign constructors to EQC if they have a selector or a tester bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc ); - */ +#endif if( shouldConsider ){ nodes.push_back( eqc ); } @@ -1217,6 +1220,8 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ bool addCons = false; const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); if( !d_equalityEngine.hasTerm( eqc ) ){ + Assert( false ); + /* if( !dt.isCodatatype() ){ Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl; Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; @@ -1263,6 +1268,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ neqc = *te; } } + */ }else{ Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; @@ -1280,12 +1286,12 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ //must try the infinite ones first if( pcons[i] && (r==1)==dt[ i ].isFinite() ){ neqc = DatatypesRewriter::getInstCons( eqc, dt, i ); - for( unsigned j=0; j<neqc.getNumChildren(); j++ ){ - //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){ - if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){ - nodes.push_back( neqc[j] ); - } - } + //for( unsigned j=0; j<neqc.getNumChildren(); j++ ){ + // //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){ + // if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){ + // nodes.push_back( neqc[j] ); + // } + //} break; } } @@ -1297,6 +1303,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Trace("dt-cmi") << "Assign : " << neqc << std::endl; m->assertEquality( eqc, neqc, true ); eqc_cons[ eqc ] = neqc; + m->assertRepresentative( neqc ); } //m->assertRepresentative( neqc ); if( addCons ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 5c7b31d33..ffe64beba 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -88,6 +88,9 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) { bool CegInstantiation::needsModel( Theory::Effort e ) { return true; } +bool CegInstantiation::needsFullModel( Theory::Effort e ) { + return false; +} void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 67125a8ad..235f2b01c 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -99,6 +99,7 @@ public: public: bool needsCheck( Theory::Effort e ); bool needsModel( Theory::Effort e ); + bool needsFullModel( Theory::Effort e ); /* Call during quantifier engine's check */ void check( Theory::Effort e, unsigned quant_e ); /* Called for new quantifiers */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 88b56b6bb..46995653f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -258,6 +258,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); bool needsCheck = false; bool needsModel = false; + bool needsFullModel = false; std::vector< QuantifiersModule* > qm; if( d_model->getNumAssertedQuantifiers()>0 ){ needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call @@ -267,6 +268,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ needsCheck = true; if( d_modules[i]->needsModel( e ) ){ needsModel = true; + if( d_modules[i]->needsFullModel( e ) ){ + needsFullModel = true; + } } } } @@ -328,9 +332,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ //build the model if any module requested it if( quant_e==QEFFORT_MODEL && needsModel ){ Assert( d_builder!=NULL ); - Trace("quant-engine-debug") << "Build model, fullModel = " << d_builder->optBuildAtFullModel() << "..." << std::endl; + Trace("quant-engine-debug") << "Build model, fullModel = " << ( needsFullModel || d_builder->optBuildAtFullModel() ) << "..." << std::endl; d_builder->d_addedLemmas = 0; - d_builder->buildModel( d_model, d_builder->optBuildAtFullModel() ); + d_builder->buildModel( d_model, needsFullModel || d_builder->optBuildAtFullModel() ); //we are done if model building was unsuccessful if( d_builder->d_addedLemmas>0 ){ success = false; @@ -349,7 +353,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_hasAddedLemma ){ break; //otherwise, complete the model generation if necessary - }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() && !d_builder->optBuildAtFullModel() ){ + }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() && !needsFullModel && !d_builder->optBuildAtFullModel() ){ Trace("quant-engine-debug") << "Build completed model..." << std::endl; d_builder->buildModel( d_model, true ); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 75b55ca4a..f56cd0d19 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -55,6 +55,8 @@ public: virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } /* whether this module needs a model built */ virtual bool needsModel( Theory::Effort e ) { return false; } + /* whether this module needs a model built */ + virtual bool needsFullModel( Theory::Effort e ) { return false; } /* reset at a round */ virtual void reset_round( Theory::Effort e ){} /* Call during quantifier engine's check */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 7e1129e7b..b67140db8 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -681,7 +681,10 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) continue; } TypeNode t = TypeSet::getType(it); - TypeNode tb = t.getBaseType(); + if(t.isTuple() || t.isRecord()) { + t = NodeManager::currentNM()->getDatatypeForTupleRecord(t); + } + TypeNode tb = t.getBaseType(); if (!assignOne) { set<Node>* repSet = typeRepSet.getSet(tb); if (repSet != NULL && !repSet->empty()) { |