From 4604e6119a0a5e968e47cf23ce93b09c17a726b8 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 15 Feb 2017 11:26:56 -0600
Subject: Minimization modes for fmf bound.

---
 src/theory/quantifiers/bounded_integers.cpp | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

(limited to 'src/theory/quantifiers/bounded_integers.cpp')

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 09bb2dab3..c488e8c23 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -407,8 +407,10 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
               Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() );
               d_bounds[b][f][v] = bound_int_range_term[b][v];
             }
-            Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );
-            d_range[f][v] = Rewriter::rewrite( r );
+            if( options::fmfBoundMinMode()==FMF_BOUND_MIN_ALL || options::fmfBoundMinMode()==FMF_BOUND_MIN_INT_RANGE ){
+              Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );
+              d_range[f][v] = Rewriter::rewrite( r );
+            }
             Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
           }
         }else if( it->second==BOUND_SET_MEMBER ){
@@ -416,7 +418,9 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
           setBoundVar = true;
           d_setm_range[f][v] = bound_lit_map[2][v][1];
           d_setm_range_lit[f][v] = bound_lit_map[2][v];
-          d_range[f][v] = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] );
+          if( options::fmfBoundMinMode()==FMF_BOUND_MIN_ALL || options::fmfBoundMinMode()==FMF_BOUND_MIN_SET_CARD ){
+            d_range[f][v] = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] );
+          }
           Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[2][v] << std::endl;
         }else if( it->second==BOUND_FIXED_SET ){
           setBoundedVar( f, v, BOUND_FIXED_SET );
@@ -509,8 +513,9 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
     d_bound_quants.push_back( f );
     for( unsigned i=0; i<d_set[f].size(); i++) {
       Node v = d_set[f][i];
-      if( d_bound_type[f][v]==BOUND_INT_RANGE || d_bound_type[f][v]==BOUND_SET_MEMBER ){
-        Node r = d_range[f][v];
+      std::map< Node, Node >::iterator itr = d_range[f].find( v );
+      if( itr != d_range[f].end() ){
+        Node r = itr->second;
         Assert( !r.isNull() );
         bool isProxy = false;
         if( r.hasBoundVar() ){
-- 
cgit v1.2.3