Add new method for checking candidate models, --fmf-fmc. Add infrastructure for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp). Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model. Add option for relational triggers such as x = f(y), --relational-trigger.

4 files changed, 51 insertions, 19 deletions

diff --git a/src/theory/uf/options b/src/theory/uf/options
index 33d1255ef..bea11621a 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -30,5 +30,7 @@ option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
  always use simple clique lemmas for uf strong solver
 option ufssDiseqPropagation --uf-ss-deq-prop bool :default false
  eagerly propagate disequalities for uf strong solver
+option ufssMinimalModel /--disable-uf-ss-min-model bool :default true
+ disable finding a minimal model in uf strong solver
 
 endmodule
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 228cfd2c4..2c853a4fa 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -17,6 +17,7 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/options.h"
 
 #define RECONSIDER_FUNC_DEFAULT_VALUE
 #define USE_PARTIAL_DEFAULT_VALUES
@@ -309,19 +310,21 @@ void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground
     if( !ground ){
       int defSize = (int)d_defaults.size();
       for( int i=0; i<defSize; i++ ){
-        bool isGround;
         //for soundness, to allow variable order-independent function interpretations,
         //  we must ensure that the intersection of all default terms
         //  is also defined.
         //for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,
         //  then we must define f( b, a ).
-        Node ni = getIntersection( m, n, d_defaults[i], isGround );
-        if( !ni.isNull() ){
-          //if the intersection exists, and is not already defined
-          if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
-              d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
-            //use the current value
-            setValue( m, ni, v, isGround, false );
+        if (!options::fmfFullModelCheck()) {
+          bool isGround;
+          Node ni = getIntersection( m, n, d_defaults[i], isGround );
+          if( !ni.isNull() ){
+            //if the intersection exists, and is not already defined
+            if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
+                d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
+              //use the current value
+              setValue( m, ni, v, isGround, false );
+            }
           }
         }
       }
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 12c1cf244..9140806ec 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -153,9 +153,10 @@ public:
   static Node toIte( TypeNode type, Node fm_node, const char* argPrefix );
 };
 
+
 class UfModelTreeGenerator
 {
-private:
+public:
   //store for set values
   Node d_default_value;
   std::map< Node, Node > d_set_values[2][2];
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index d64f7df60..e868460f8 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -595,9 +595,11 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
           if( d_regions[i]->d_valid ){
             std::vector< Node > clique;
             if( d_regions[i]->check( level, d_cardinality, clique ) ){
-              //add clique lemma
-              addCliqueLemma( clique, out );
-              return;
+              if( options::ufssMinimalModel() ){
+                //add clique lemma
+                addCliqueLemma( clique, out );
+                return;
+              }
             }else{
               Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
             }
@@ -659,13 +661,17 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
               //naive strategy, force region combination involving the first valid region
               for( int i=0; i<(int)d_regions_index; i++ ){
                 if( d_regions[i]->d_valid ){
-                  forceCombineRegion( i, false );
-                  recheck = true;
-                  break;
+                  int fcr = forceCombineRegion( i, false );
+                  Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl;
+                  if( options::ufssMinimalModel() || fcr!=-1 ){
+                    recheck = true;
+                    break;
+                  }
                 }
               }
             }
             if( recheck ){
+              Trace("uf-ss-debug") << "Must recheck." << std::endl;
               check( level, out );
             }
           }
@@ -869,8 +875,10 @@ void StrongSolverTheoryUF::SortModel::checkRegion( int ri, bool checkCombine ){
     //now check if region is in conflict
     std::vector< Node > clique;
     if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
-      //explain clique
-      addCliqueLemma( clique, &d_thss->getOutputChannel() );
+      if( options::ufssMinimalModel() ){
+        //explain clique
+        addCliqueLemma( clique, &d_thss->getOutputChannel() );
+      }
     }
   }
 }
@@ -1013,8 +1021,8 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
 }
 
 bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
+  Node s;
   if( r->hasSplits() ){
-    Node s;
     if( !options::ufssSmartSplits() ){
       //take the first split you find
       for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
@@ -1038,8 +1046,26 @@ bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
         }
       }
     }
+    Assert( s!=Node::null() );
+  }else{
+    if( !options::ufssMinimalModel() ){
+      //since candidate clique is not reported, we may need to find splits manually
+      for ( std::map< Node, Region::RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){
+        if ( it->second->d_valid ){
+          for ( std::map< Node, Region::RegionNodeInfo* >::iterator it2 = r->d_nodes.begin(); it2 != r->d_nodes.end(); ++it2 ){
+            if ( it->second!=it2->second && it2->second->d_valid ){
+              if( !r->isDisequal( it->first, it2->first, 1 ) ){
+                s = NodeManager::currentNM()->mkNode( EQUAL, it->first, it2->first );
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  if (!s.isNull() ){
     //add lemma to output channel
-    Assert( s!=Node::null() && s.getKind()==EQUAL );
+    Assert( s.getKind()==EQUAL );
     s = Rewriter::rewrite( s );
     Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
     if( options::sortInference()) {