From 384cafab1e362a5083836e478b58ba55e0d3d377 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 27 Aug 2014 22:24:52 +0200 Subject: [PATCH] Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict. --- src/theory/datatypes/theory_datatypes.cpp | 2 +- src/theory/quantifiers/options | 2 ++ src/theory/quantifiers/quantifiers_rewriter.cpp | 8 ++++++++ src/theory/rep_set.cpp | 4 ++-- 4 files changed, 13 insertions(+), 3 deletions(-) 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 ); } -- 2.30.2