Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict.

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 7015b772e4c222bd1cc42dd30e81ede7bc17bc20..f74384d59b70f10be39037752ca2724381f3c9da 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -142,7 +142,7 @@ void TheoryDatatypes::check(Effort e) {
     flushPendingFacts();
   }
 
-  if( e == EFFORT_FULL ) {
+  if( e == EFFORT_FULL && !d_conflict ) {
     //check for cycles
     bool addedFact;
     do {

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 5ef7e9efa8578d5aa726372e426711d7dea2c678..2b4ce9aef511d54d82c714b675fc7847113eae66 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -26,6 +26,8 @@ option prenexQuant /--disable-prenex-quant bool :default true
 #   forall y. P( c, y )
 option varElimQuant /--disable-var-elim-quant bool :default true
  disable simple variable elimination for quantified formulas
+option dtVarExpandQuant --dt-var-exp-quant bool :default false
+ expand datatype variables bound to one constructor in quantifiers
 
 option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
  disable simple ite lifting for quantified formulas

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 1a20693f903841e775458df3effb7dc04e9a4cb9..624856671e4d8987cd6a3ec7a6a2fa421e319e76 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -388,6 +388,14 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
         }
       }
     }
+    /*
+    else if( options::dtVarExpandQuant() && it->first.getKind()==APPLY_TESTER && it->first[0].getKind()==BOUND_VARIABLE ){
+      if( it->second ){
+        Trace("dt-var-expand") << "Expand datatype variable based on : " << it->first << std::endl;
+        std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] );
+      }
+    }
+    */
   }
   if( !vars.empty() ){
     Trace("var-elim-quant") << "VE " << vars.size() << "/" << args.size() << std::endl;

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 5a9b92fa0692eb03a2a038b5bdf1651656c507ba..ee14d6fc15b9da25c3a08f2cd92a661de5031fd6 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -38,9 +38,9 @@ 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;
+  Assert( n.getType().isSubtypeOf( tn ) );
+  d_tmap[ n ] = (int)d_type_reps[tn].size();
   d_type_reps[tn].push_back( n );
 }