From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 17 Aug 2018 17:08:48 +0000 (-0500)
Subject:  Fix spurious warning in sort inference (#2331)
X-Git-Tag: cvc5-1.0.0~4764
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1f9d6858f2d9cc21e6869ad743d18d07e82b30e7;p=cvc5.git

 Fix spurious warning in sort inference (#2331)
---

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index b6e8f7553..c4c0a8b47 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -710,11 +710,13 @@ Node SortInference::simplifyNode(
         }
       }
       children[0] = d_symbol_map[op];
-      //make sure all children have been taken care of
-      for( size_t i=0; i<n.getNumChildren(); i++ ){
+      // make sure all children have been given proper types
+      for (size_t i = 0, size = n.getNumChildren(); i < size; i++)
+      {
         TypeNode tn = children[i+1].getType();
         TypeNode tna = getTypeForId( d_op_arg_types[op][i] );
-        if( tn!=tna ){
+        if (!tn.isSubtypeOf(tna))
+        {
           Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl;
           Assert( false );
         }
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index e43f6675d..9db34bca2 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -434,7 +434,6 @@ REG0_TESTS = \
 	regress0/fmf/quant_real_univ.cvc \
 	regress0/fmf/sat-logic.smt2 \
 	regress0/fmf/sc_bad_model_1221.smt2 \
-	regress0/fmf/sort-inf-int.smt2 \
 	regress0/fmf/syn002-si-real-int.smt2 \
 	regress0/fmf/tail_rec.smt2 \
 	regress0/fp/simple.smt2 \
@@ -1115,6 +1114,8 @@ REG1_TESTS = \
 	regress1/fmf/radu-quant-set.smt2 \
 	regress1/fmf/refcount24.cvc.smt2 \
 	regress1/fmf/sc-crash-052316.smt2 \
+	regress1/fmf/sort-inf-int.smt2 \
+	regress1/fmf/sort-inf-int-real.smt2 \
 	regress1/fmf/with-ind-104-core.smt2 \
 	regress1/gensys_brn001.smt2 \
 	regress1/ho/auth0068.smt2 \
diff --git a/test/regress/regress0/fmf/sort-inf-int.smt2 b/test/regress/regress0/fmf/sort-inf-int.smt2
deleted file mode 100644
index e4a8978d4..000000000
--- a/test/regress/regress0/fmf/sort-inf-int.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-; COMMAND-LINE: --finite-model-find --sort-inference --no-check-models
-; EXPECT: sat
-(set-logic UFLIRA)
-(set-info :status sat)
-(declare-fun f (Int) Int)
-(declare-fun g (Int) Int)
-(declare-fun h (Int) Int)
-(assert (forall ((x Int)) (or (= (f x) (h x)) (= (f x) (g x)))))
-(assert (not (= (f 3) (h 3))))
-(assert (not (= (f 5) (g 5))))
-(assert (= (f 4) (g 8)))
-
-(check-sat)
diff --git a/test/regress/regress1/fmf/sort-inf-int-real.smt2 b/test/regress/regress1/fmf/sort-inf-int-real.smt2
new file mode 100644
index 000000000..9944ee55c
--- /dev/null
+++ b/test/regress/regress1/fmf/sort-inf-int-real.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --finite-model-find --sort-inference --no-check-models
+; EXPECT: sat
+(set-logic UFLIRA)
+(set-info :status sat)
+(declare-fun f (Int) Int)
+(declare-fun g (Int) Real)
+(declare-fun h (Real) Int)
+(assert (forall ((x Int)) (or (= (f x) (h (to_real x))) (= (f x) (to_int (g x))))))
+(assert (not (= (f 3) (h 3.0))))
+(assert (not (= (f 5) (to_int (g 5)))))
+(assert (= (f 4) (g 8)))
+(assert (= (h 5.0) 0.0))
+; Sort inference fails to infer that x can be uninterpreted in this example,
+; however, fmf is able to reason that all instances are sat.
+(check-sat)
diff --git a/test/regress/regress1/fmf/sort-inf-int.smt2 b/test/regress/regress1/fmf/sort-inf-int.smt2
new file mode 100644
index 000000000..e4a8978d4
--- /dev/null
+++ b/test/regress/regress1/fmf/sort-inf-int.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --finite-model-find --sort-inference --no-check-models
+; EXPECT: sat
+(set-logic UFLIRA)
+(set-info :status sat)
+(declare-fun f (Int) Int)
+(declare-fun g (Int) Int)
+(declare-fun h (Int) Int)
+(assert (forall ((x Int)) (or (= (f x) (h x)) (= (f x) (g x)))))
+(assert (not (= (f 3) (h 3))))
+(assert (not (= (f 5) (g 5))))
+(assert (= (f 4) (g 8)))
+
+(check-sat)