From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 27 Aug 2014 20:24:52 +0000 (+0200)
Subject: Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict.
X-Git-Tag: cvc5-1.0.0~6642
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=384cafab1e362a5083836e478b58ba55e0d3d377;p=cvc5.git

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 7015b772e..f74384d59 100644
--- 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 5ef7e9efa..2b4ce9aef 100644
--- 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 1a20693f9..624856671 100644
--- 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 5a9b92fa0..ee14d6fc1 100644
--- 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 );
 }