Enable bounded set membership with --fmf-bound. Map to term models for bounded set membership.

10 files changed, 81 insertions, 20 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 953150e42..85355c037 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -163,8 +163,10 @@ option fmfFmcSimple --fmf-fmc-simple bool :default true
  simple models in full model check for finite model finding
 option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write
  finite model finding on bounded integer quantification
-option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write
- enforce bounds for bounded integer quantification lazily via use of proxy variables
+option fmfBound fmf-bound --fmf-bound bool :default false :read-write
+ finite model finding on bounded quantification
+option fmfBoundLazy --fmf-bound-lazy bool :default false :read-write
+ enforce bounds for bounded quantification lazily via use of proxy variables
  
 ### conflict-based instantiation options 
  
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d7b7f9c3e..32c44d224 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1350,8 +1350,8 @@ void SmtEngine::setDefaults() {
       Trace("smt") << "turning on quantifier logic, for strings-exp"
                    << std::endl;
     }
-    if(! options::fmfBoundInt.wasSetByUser()) {
-      options::fmfBoundInt.set( true );
+    if(! options::fmfBound.wasSetByUser()) {
+      options::fmfBound.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
     if(! options::fmfInstEngine.wasSetByUser()) {
@@ -1753,12 +1753,13 @@ void SmtEngine::setDefaults() {
     options::cbqi.set(false);
   }
 
-  if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) {
-    options::fmfBoundInt.set( true );
+  if( ( options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy() ) || 
+      ( options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt() ) ) {
+    options::fmfBound.set( true );
   }
   //now have determined whether fmfBoundInt is on/off
   //apply fmfBoundInt options
-  if( options::fmfBoundInt() ){
+  if( options::fmfBound() ){
     //must have finite model finding on
     options::finiteModelFind.set( true );
     if( ! options::mbqiMode.wasSetByUser() ||
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 7184624da..54853ceaf 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/theory_engine.h"
 
 using namespace CVC4;
 using namespace std;
@@ -30,7 +31,7 @@ using namespace CVC4::kind;
 
 BoundedIntegers::IntRangeModel::IntRangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy) : d_bi(bi),
       d_range(r), d_curr_max(-1), d_lit_to_range(u), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1), d_ranges_proxied(u) { 
-  if( options::fmfBoundIntLazy() ){
+  if( options::fmfBoundLazy() ){
     d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() );
   }else{
     d_proxy_range = r;
@@ -232,14 +233,12 @@ void BoundedIntegers::processLiteral( Node q, Node lit, bool pol,
     }
   }else if( lit.getKind()==MEMBER ){
     //TODO: enable this when sets models are fixed
-    /*
     if( !pol && lit[0].getKind()==BOUND_VARIABLE && !isBound( q, lit[0] ) && !lit[1].hasBoundVar() ){
       Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is membership." << std::endl;
       bound_lit_type_map[lit[0]] = BOUND_SET_MEMBER;
       bound_lit_map[0][lit[0]] = lit;
       bound_lit_pol_map[0][lit[0]] = pol;
     }
-    */
   }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {
     Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;
   }
@@ -330,6 +329,7 @@ void BoundedIntegers::registerQuantifier( Node f ) {
           setBoundedVar( f, v, BOUND_SET_MEMBER );
           setBoundVar = true;
           d_setm_range[f][v] = bound_lit_map[0][v][1];
+          d_setm_range_lit[f][v] = bound_lit_map[0][v];
           Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[0][v] << std::endl;
         }
         if( setBoundVar ){
@@ -515,6 +515,63 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
     Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
     sr = d_quantEngine->getModel()->getCurrentModelValue( sr );
     Trace("bound-int-rsi") << "Value is " << sr << std::endl;
+    //map to term model
+    if( sr.getKind()!=EMPTYSET ){
+      std::map< Node, Node > val_to_term;
+      while( sr.getKind()==UNION ){
+        Assert( sr[1].getKind()==kind::SINGLETON );
+        val_to_term[ sr[1][0] ] = sr[1][0];
+        sr = sr[0];
+      }
+      Assert( sr.getKind()==kind::SINGLETON );
+      val_to_term[ sr[0] ] = sr[0];
+      //must look back at assertions, not term database (theory of sets introduces extraneous terms internally)
+      Theory* theory = d_quantEngine->getTheoryEngine()->theoryOf( THEORY_SETS );
+      if( theory ){
+        context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+        for( unsigned i = 0; it != it_end; ++ it, ++i ){
+          Node lit = (*it).assertion;
+          if( lit.getKind()==kind::MEMBER ){
+            Node vr = d_quantEngine->getModel()->getCurrentModelValue( lit[0] );
+            Trace("bound-int-rsi-debug") << "....membership for " << lit << " ==> " << vr << std::endl;
+            Trace("bound-int-rsi-debug") << "  " << (val_to_term.find( vr )!=val_to_term.end()) << " " << d_quantEngine->getEqualityQuery()->areEqual( d_setm_range_lit[q][v][1], lit[1] ) << std::endl;
+            if( val_to_term.find( vr )!=val_to_term.end() ){
+              if( d_quantEngine->getEqualityQuery()->areEqual( d_setm_range_lit[q][v][1], lit[1] ) ){
+                Trace("bound-int-rsi") << "  Map value to term : " << vr << " -> " << lit[0] << std::endl;
+                val_to_term[ vr ] = lit[0];
+              }
+            }
+          }
+        }
+      }
+      //rebuild value
+      Node nsr;
+      for( std::map< Node, Node >::iterator it = val_to_term.begin(); it != val_to_term.end(); ++it ){
+        Node nv = NodeManager::currentNM()->mkNode( kind::SINGLETON, it->second );
+        if( nsr.isNull() ){
+          nsr = nv;
+        }else{
+          nsr = NodeManager::currentNM()->mkNode( kind::UNION, nsr, nv );
+        }
+      }
+      Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl;
+      return nsr;
+      
+      /*
+      Node lit = d_setm_range_lit[q][v];
+      Trace("bound-int-rsi-debug") << "Bounded from lit " << lit << std::endl;
+      Node f = d_quantEngine->getTermDatabase()->getMatchOperator( lit );
+      TermArgTrie * ta = d_quantEngine->getTermDatabase()->getTermArgTrie( f );
+      if( ta ){
+        Trace("bound-int-rsi-debug") << "Got term index for " << f << std::endl;
+        for( std::map< TNode, TermArgTrie >::iterator it = ta->d_data.begin(); it != ta->d_data.end(); ++it ){
+
+        }
+
+      }
+      */
+    }
+    
   }
   return sr;
 }
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index ab4bcba96..c3fb05641 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -60,6 +60,7 @@ private:
   std::map< Node, std::map< Node, Node > > d_nground_range;
   //set membership range
   std::map< Node, std::map< Node, Node > > d_setm_range;
+  std::map< Node, std::map< Node, Node > > d_setm_range_lit;
   void hasFreeVar( Node f, Node n );
   void process( Node f, Node n, bool pol,
                 std::map< Node, unsigned >& bound_lit_type_map,
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index a0665cb7f..be608aeaa 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -668,7 +668,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
               }
             }
             if( addInst ){
-              if( options::fmfBoundInt() ){
+              if( options::fmfBound() ){
                 std::vector< Node > cond;
                 cond.push_back(d_quant_cond[f]);
                 cond.insert( cond.end(), inst.begin(), inst.end() );
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 10a5ae41b..7bbe06108 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -45,7 +45,7 @@ bool QModelBuilder::isQuantifierActive( Node f ) {
 
 
 bool QModelBuilder::optUseModel() {
-  return options::mbqiMode()!=MBQI_NONE || options::fmfBoundInt();
+  return options::mbqiMode()!=MBQI_NONE || options::fmfBound();
 }
 
 void QModelBuilder::debugModel( FirstOrderModel* fm ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 5d575969f..7658f2b6b 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -121,7 +121,7 @@ void ModelEngine::registerQuantifier( Node f ){
       if( !tn.isSort() ){
         if( !tn.getCardinality().isFinite() ){
           if( tn.isInteger() ){
-            if( !options::fmfBoundInt() ){
+            if( !options::fmfBound() ){
               canHandle = false;
             }
           }else{
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 75d177fdc..c08fee712 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -98,7 +98,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
 
   //the model object
   if( options::mbqiMode()==quantifiers::MBQI_FMC ||
-      options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ||
+      options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBound() ||
       options::mbqiMode()==quantifiers::MBQI_TRUST ){
     d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
   }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
@@ -233,7 +233,7 @@ void QuantifiersEngine::finishInit(){
   }  
   //finite model finding
   if( options::finiteModelFind() ){
-    if( options::fmfBoundInt() ){
+    if( options::fmfBound() ){
       d_bint = new quantifiers::BoundedIntegers( c, this );
       d_modules.push_back( d_bint );
     }
@@ -282,9 +282,9 @@ void QuantifiersEngine::finishInit(){
   }
 
   if( needsBuilder ){
-    Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
+    Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
     if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
-        options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBoundInt() ){
+        options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBound() ){
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
       d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
     }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
@@ -1241,7 +1241,7 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   if( e==Theory::EFFORT_LAST_CALL ){
     //with bounded integers, skip every other last call,
     // since matching loops may occur with infinite quantification
-    if( d_ierCounter_lc%2==0 && options::fmfBoundInt() ){
+    if( d_ierCounter_lc%2==0 && options::fmfBound() ){
       performCheck = false;
     }
   }
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 184553ba7..86bcb2cac 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -366,12 +366,12 @@ int RepSetIterator::resetIndex( int i, bool initial ) {
       d_domain[v].clear();
       d_setm_bounds[v].clear();
       if( srv.getKind()!=EMPTYSET ){
-        //TODO: need term model, not value model
         while( srv.getKind()==UNION ){
           Assert( srv[1].getKind()==kind::SINGLETON );
           d_setm_bounds[v].push_back( srv[1][0] );
           srv = srv[0];
         }
+        Assert( srv.getKind()==kind::SINGLETON );
         d_setm_bounds[v].push_back( srv[0] );
         d_domain[v].push_back( d_setm_bounds[v].size() );
       }else{
diff --git a/test/regress/regress0/quantifiers/bi-artm-s.smt2 b/test/regress/regress0/quantifiers/bi-artm-s.smt2
index 5fb7522e9..b97c339fc 100644
--- a/test/regress/regress0/quantifiers/bi-artm-s.smt2
+++ b/test/regress/regress0/quantifiers/bi-artm-s.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-bound-int-lazy
+; COMMAND-LINE: --fmf-bound-lazy
 ; EXPECT: unsat
 (set-option :incremental "false")
 (set-info :status unsat)