summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp13
-rw-r--r--src/theory/theory_model.cpp27
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;
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback