Simplify fmc model construction, add regression. Improve FMF debug assertions.

5 files changed, 54 insertions, 6 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 018a0c3e0..aa2a43fbf 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -669,6 +669,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
     Node v = d_models[op]->d_value[i];
     Trace("fmc-model-func") << "Value is : " << v << std::endl;
+    Assert( v.isConst() );
+    /*
     if( !hasTerm( v ) ){
       //can happen when the model basis term does not exist in ground assignment
       TypeNode tn = v.getType();
@@ -685,6 +687,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       }
     }
     v = getRepresentative( v );
+    */
     if( curr.isNull() ){
       Trace("fmc-model-func") << "base : " << v << std::endl;
       curr = v;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 56f966426..6dfd4c737 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1605,10 +1605,10 @@ bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
 }
 
 bool TermDb::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ) {
-  if( std::find( t.begin(), t.end(), n )!=t.end() ){
-    return true;
-  }else{
-    if( visited.find( n )==visited.end() ){
+  if( visited.find( n )==visited.end() ){
+    if( std::find( t.begin(), t.end(), n )!=t.end() ){
+      return true;
+    }else{
       visited[n] = true;
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
         if( containsTerms2( n[i], t, visited ) ){
@@ -1616,8 +1616,22 @@ bool TermDb::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, boo
         }
       }
     }
-    return false;
   }
+  return false;
+}
+
+bool TermDb::containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited ) {
+  if( n.getKind()==UNINTERPRETED_CONSTANT ){
+    return true;
+  }else if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( containsUninterpretedConstant2( n[i], visited ) ){
+        return true;
+      }
+    }
+  }
+  return false;
 }
 
 bool TermDb::containsTerm( Node n, Node t ) {
@@ -1634,6 +1648,11 @@ bool TermDb::containsTerms( Node n, std::vector< Node >& t ) {
   }
 }
 
+bool TermDb::containsUninterpretedConstant( Node n ) {
+  std::map< Node, bool > visited;
+  return containsUninterpretedConstant2( n, visited );
+}
+
 Node TermDb::simpleNegate( Node n ){
   if( n.getKind()==OR || n.getKind()==AND ){
     std::vector< Node > children;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 86b0efbf3..0c4e94517 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -397,12 +397,15 @@ private:
   //helper for contains term
   static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );
   static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited );
+  static bool containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited );
 //general utilities
 public:
   /** simple check for whether n contains t as subterm */
   static bool containsTerm( Node n, Node t );
   /** simple check for contains term, true if contains at least one term in t */
   static bool containsTerms( Node n, std::vector< Node >& t );
+  /** contains uninterpreted constant */
+  static bool containsUninterpretedConstant( Node n );
   /** simple negate */
   static Node simpleNegate( Node n );
   /** is assoc */
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 8b7202906..370096a1e 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -48,7 +48,8 @@ TESTS =	\
 	tail_rec.smt2 \
 	jasmin-cdt-crash.smt2 \
 	loopy_coda.smt2 \
-	fmc_unsound_model.smt2
+	fmc_unsound_model.smt2 \
+	am-bad-model.cvc
 
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/fmf/am-bad-model.cvc b/test/regress/regress0/fmf/am-bad-model.cvc
new file mode 100644
index 000000000..e30b5e04a
--- /dev/null
+++ b/test/regress/regress0/fmf/am-bad-model.cvc
@@ -0,0 +1,22 @@
+% EXPECT: sat
+OPTION "produce-models";
+OPTION "finite-model-find";
+
+f     : (BITVECTOR(2),BITVECTOR(2)) ->ARRAY INT OF INT;
+f0    : BITVECTOR(2) -> ARRAY INT OF INT;
+
+td,td1,td2: ARRAY INT OF INT;
+ASSERT td1 = td WITH[0]:= 1;
+ASSERT td2 = td WITH[0]:= 2;
+ASSERT f(0bin01,0bin00)=td1;
+ASSERT f(0bin10,0bin00)=td2;
+%ASSERT FORALL(i:BITVECTOR(2)) : f0(i)=f(0bin00,i) ;
+%Artificial bypass of quantifier for f0 definition
+ASSERT f0(0bin00) = f(0bin00,0bin00);
+ASSERT f0(0bin01) = f(0bin00,0bin01);
+ASSERT f0(0bin10) = f(0bin00,0bin10);
+ASSERT f0(0bin11) = f(0bin00,0bin11);
+ASSERT FORALL(i:BITVECTOR(2)) : f0(i)=td2 ;
+
+CHECKSAT;
+