Minor fix for explanations for co-datatypes. Bug fix for explanations in FMF for...

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 544589306cfd0b56fd2400203ba7b1151c2a30a2..65d307a34dcccd0e647922d963ffcb134a021d80 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -570,7 +570,12 @@ void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){
   TNode atom = polarity ? literal : literal[0];
   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
     explainEquality( atom[0], atom[1], polarity, assumptions );
+  } else if( atom.getKind() == kind::AND && polarity ){
+    for( unsigned i=0; i<atom.getNumChildren(); i++ ){
+      explain( atom[i], assumptions );
+    }
   } else {
+    Assert( atom.getKind()!=kind::AND );
     explainPredicate( atom, polarity, assumptions );
   }
 }
@@ -670,7 +675,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             for( unsigned i=0; i<deq_cand.size(); i++ ){
               if( d_equalityEngine.areDisequal( deq_cand[i].first, deq_cand[i].second, true ) ){
                 conf = true;
-                Node eq = NodeManager::currentNM()->mkNode( deq_cand[i].first.getType().isBoolean() ? kind::IFF : kind::EQUAL, 
+                Node eq = NodeManager::currentNM()->mkNode( deq_cand[i].first.getType().isBoolean() ? kind::IFF : kind::EQUAL,
                                                             deq_cand[i].first, deq_cand[i].second );
                 exp.push_back( eq.negate() );
               }
@@ -1488,6 +1493,7 @@ void TheoryDatatypes::checkCycles() {
   }
   //process codatatypes
   if( cod_eqc.size()>1 ){
+    Trace("dt-cod-debug") << "Process " << cod_eqc.size() << " co-datatypes" << std::endl;
     std::vector< std::vector< Node > > part_out;
     std::vector< TNode > exp;
     std::map< Node, Node > cn;
@@ -1496,7 +1502,9 @@ void TheoryDatatypes::checkCycles() {
       cn[cod_eqc[i]] = cod_eqc[i];
     }
     separateBisimilar( cod_eqc, part_out, exp, cn, dni, 0, false );
+    Trace("dt-cod-debug") << "Done separate bisimilar." << std::endl;
     if( !part_out.empty() ){
+      Trace("dt-cod-debug") << "Process partition size " << part_out.size() << std::endl;
       for( unsigned i=0; i<part_out.size(); i++ ){
         std::vector< Node > part;
         part.push_back( part_out[i][0] );

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index d5ed5589bba6b5668694802bfae4f19db3939d10..c21859e87225ae06c27de6dc2fd379d5775bca09 100644 (file)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -871,7 +871,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       Trace("fmc-debug") << "Can't process base array " << r << std::endl;
       //can't process this array
       d.reset();
-      d.addEntry(fm, defC, Node::null());
+      d.addEntry(fm, mkCondDefault(fm, f), Node::null());
     }
   }
   else if( n.getNumChildren()==0 ){

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 9542725493f83ae94642cb8ddce0df3b4404baa6..5a9b92fa0692eb03a2a038b5bdf1651656c507ba 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -38,6 +38,7 @@ int RepSet::getNumRepresentatives( TypeNode tn ) const{
 }
 
 void RepSet::add( TypeNode tn, Node n ){
+  Assert( n.getType()==tn );
   d_tmap[ n ] = (int)d_type_reps[tn].size();
   Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
   d_type_reps[tn].push_back( n );