diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 13 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 27 |
2 files changed, 24 insertions, 16 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 35d82b2ae..d49974df2 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -190,6 +190,7 @@ void TheoryDatatypes::check(Effort e) { if( !hasLabel( eqc, n ) ){ Trace("datatypes-debug") << "No constructor..." << std::endl; const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isUFinite() << " " << dt.isRecursiveSingleton() << std::endl; bool continueProc = true; if( dt.isRecursiveSingleton() ){ Trace("datatypes-debug") << "Check recursive singleton..." << std::endl; @@ -1410,11 +1411,13 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ //until models are implemented for codatatypes //throw Exception("Models for codatatypes are not supported in this version."); //must proactive expand to avoid looping behavior in model builder - std::map< Node, int > vmap; - Node v = getCodatatypesValue( it->first, eqc_cons, vmap, 0 ); - Trace("dt-cmi") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl; - m->assertEquality( eqc, v, true ); - m->assertRepresentative( v ); + if( !it->second.isNull() ){ + std::map< Node, int > vmap; + Node v = getCodatatypesValue( it->first, eqc_cons, vmap, 0 ); + Trace("dt-cmi") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl; + m->assertEquality( eqc, v, true ); + m->assertRepresentative( v ); + } }else{ Trace("dt-cmi") << "Datatypes : assert representative " << it->second << " for " << it->first << std::endl; m->assertRepresentative( it->second ); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 2a8e21059..18ed6714d 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -467,17 +467,19 @@ void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map<Node } bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) { - Trace("model-builder-cdt") << "Is " << val << " and excluded codatatype value for " << eqc << "? " << std::endl; + Trace("model-builder-debug") << "Is " << val << " and excluded codatatype value for " << eqc << "? " << std::endl; for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i ) { Assert(assertedReps.find(*i) != assertedReps.end()); Node rep = assertedReps[*i]; - Trace("model-builder-cdt") << " Rep : " << rep << std::endl; + Trace("model-builder-debug") << " Rep : " << rep << std::endl; //check matching val to rep with eqc as a free variable Node eqc_m; if( isCdtValueMatch( val, rep, eqc, eqc_m ) ){ - Trace("model-builder-cdt") << " ...matches with " << eqc << " -> " << eqc_m << std::endl; - Trace("model-builder-cdt") << "*** " << val << " is excluded datatype for " << eqc << std::endl; - return true; + Trace("model-builder-debug") << " ...matches with " << eqc << " -> " << eqc_m << std::endl; + if( eqc_m.getKind()==kind::UNINTERPRETED_CONSTANT ){ + Trace("model-builder-debug") << "*** " << val << " is excluded datatype for " << eqc << std::endl; + return true; + } } } return false; @@ -528,11 +530,11 @@ bool TheoryEngineModelBuilder::isExcludedUSortValue( std::map< TypeNode, unsigne visited[v] = true; TypeNode tn = v.getType(); if( tn.isSort() ){ - Trace("exc-value-debug") << "Is excluded usort value : " << v << " " << tn << std::endl; + Trace("model-builder-debug") << "Is excluded usort value : " << v << " " << tn << std::endl; unsigned card = eqc_usort_count[tn]; - Trace("exc-value-debug") << " Cardinality is " << card << std::endl; + Trace("model-builder-debug") << " Cardinality is " << card << std::endl; unsigned index = v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt(); - Trace("exc-value-debug") << " Index is " << index << std::endl; + Trace("model-builder-debug") << " Index is " << index << std::endl; return index>0 && index>=card; } for( unsigned i=0; i<v.getNumChildren(); i++ ){ @@ -772,6 +774,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if(t.isTuple() || t.isRecord()) { t = NodeManager::currentNM()->getDatatypeForTupleRecord(t); } + //get properties of this type bool isCorecursive = false; bool isUSortFiniteRestricted = false; @@ -782,6 +785,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if( options::finiteModelFind() ){ isUSortFiniteRestricted = !t.isSort() && involvesUSort( t ); } + set<Node>* repSet = typeRepSet.getSet(t); TypeNode tb = t.getBaseType(); if (!assignOne) { @@ -810,6 +814,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) evaluable = true; } } + Trace("model-builder-debug") << " eqc " << *i2 << " is assignable=" << assignable << ", evaluable=" << evaluable << std::endl; if (assignable) { Assert(!evaluable || assignOne); Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF); @@ -821,7 +826,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) //--- AJR: this code checks whether n is a legal value Assert( !n.isNull() ); success = true; - Trace("exc-value-debug") << "Check if excluded : " << n << std::endl; + Trace("model-builder-debug") << "Check if excluded : " << n << std::endl; if( isUSortFiniteRestricted ){ #ifdef CVC4_ASSERTIONS //must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc) @@ -829,7 +834,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) std::map< Node, bool > visited; success = !isExcludedUSortValue( eqc_usort_count, n, visited ); if( !success ){ - Trace("exc-value") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl; + Trace("model-builder") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl; } Assert( success ); #endif @@ -840,7 +845,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // this will check whether n \not\in V^x_I from page 9 of Reynolds/Blanchette CADE 2015 success = !isExcludedCdtValue( n, repSet, assertedReps, *i2 ); if( !success ){ - Trace("exc-value") << "Excluded value : " << n << " due to alpha-equivalent codatatype expression." << std::endl; + Trace("model-builder") << "Excluded value : " << n << " due to alpha-equivalent codatatype expression." << std::endl; } } } |