Fix finiteness check for bounded fmf (#3589)

Recently, finite model finding via uninterpreted sorts was decoupled from finite bound inference techniques (the BoundedIntegers module in theory/quantifiers/fmf/). This module assumed that finite model finding was enabled in one place. This fixes the issue by adding an additional check. This fixes a model unsoundness issue where bounds on an uninterpreted sort were not being enforced.

This fixes #3587.

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index cfff64f1578fd033f7d303f056f7d2cef8fc9443..2bcb154a05551eda692729afc5e0daada929c55e 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -409,7 +409,7 @@ void BoundedIntegers::checkOwnership(Node f)
       for( unsigned i=0; i<f[0].getNumChildren(); i++) {
         if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
           TypeNode tn = f[0][i].getType();
-          if (tn.isSort()
+          if ((tn.isSort() && tn.isInterpretedFinite())
               || d_quantEngine->getTermEnumeration()->mayComplete(tn))
           {
             success = true;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e27cff94d3150cbde7de2523b5568ee19c22074b..b42d586c86688b08e906c4f1cdf2342f2cc02679 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1222,6 +1222,7 @@ set(regress_1_tests
   regress1/fmf/german169.smt2
   regress1/fmf/german73.smt2
   regress1/fmf/issue2034-preinit.smt2
+  regress1/fmf/issue3587.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/ko-bound-set.cvc

diff --git a/test/regress/regress1/fmf/issue3587.smt2 b/test/regress/regress1/fmf/issue3587.smt2
new file mode 100644 (file)
index 0000000..5ca5e4f
--- /dev/null
+++ b/test/regress/regress1/fmf/issue3587.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: unknown
+(set-logic ALL)
+(declare-sort a 0) 
+(declare-datatypes ((prod 0)) (((Pair (gx a) (gy a))))) 
+(declare-fun p () prod) 
+(assert (forall ((x a) (y a)) (not (= p (Pair x y))))) 
+; problem is unsat, currently unknown with fmf-bound
+(check-sat)  

diff --git a/test/regress/regress1/quantifiers/issue3537.smt2 b/test/regress/regress1/quantifiers/issue3537.smt2
index 08f929c4c3df8ef9db7bca429556e46904b3c653..2024153ad885383493099cf20ace5766e1e239ce 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3537.smt2
+++ b/test/regress/regress1/quantifiers/issue3537.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --no-check-models
+; COMMAND-LINE: --strings-exp --no-check-models --finite-model-find
 ; EXPECT: sat
 (set-logic ALL)
 (declare-datatypes ((UNIT 0)) (((Unit))