diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-27 22:24:52 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-27 22:25:00 +0200 |
| commit | 384cafab1e362a5083836e478b58ba55e0d3d377 (patch) | |
| tree | 843d2fdfd3d2ce4064b6194beac0c350a61f4ee7 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
| parent | 525e7328cad1ac8afbc60ed8103e06665cf5b163 (diff) | |
Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
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; |