From 42e970e822ec3d0adaacbff40e0aee02a32372cc Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 28 Sep 2017 07:23:33 -0500
Subject: Improve finite model finding for recursive predicates (#1150)

* Optimization for model finding for recursive functions involving branching positions. Update documentation, add regressions.

* Simplifications, update comments.
---
 test/regress/regress0/fmf/Makefile.am          |  4 ++-
 test/regress/regress0/fmf/issue916-fmf-or.smt2 | 48 ++++++++++++++++++++++++++
 test/regress/regress0/fmf/pow2-bool.smt2       | 17 +++++++++
 3 files changed, 68 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/fmf/issue916-fmf-or.smt2
 create mode 100644 test/regress/regress0/fmf/pow2-bool.smt2

(limited to 'test')

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 4f81d79aa..b2ed657d0 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -76,7 +76,9 @@ TESTS =	\
 	fmf-fun-no-elim-ext-arith.smt2 \
 	fmf-fun-no-elim-ext-arith2.smt2 \
 	cruanes-no-minimal-unk.smt2 \
-	no-minimal-sat.smt2
+	no-minimal-sat.smt2 \
+	issue916-fmf-or.smt2 \
+	pow2-bool.smt2 
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/issue916-fmf-or.smt2 b/test/regress/regress0/fmf/issue916-fmf-or.smt2
new file mode 100644
index 000000000..0c51e39af
--- /dev/null
+++ b/test/regress/regress0/fmf/issue916-fmf-or.smt2
@@ -0,0 +1,48 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+
+(set-logic UFDTLIA)
+(set-info :smt-lib-version 2.5)
+
+(define-funs-rec
+  (
+    (validIdValue ((x Int)(v Int)) Bool)
+  )
+  (
+    (or 
+        (and (= x 0) (< (- 10) v 10) )
+        (and (= x 1) (<= (- 100) v (- 10)) )
+        (and (= x 2) (<= 10 v 100) )
+        (and (= x 3) (< (- 1000) v (- 100)) )
+        (and (= x 4) (< 100 v 1000) )
+        (and (= x 5) (<= (- 1000) v) )
+        (and (= x 6) (<= v 1000) )
+            (validIdValue (- x 7) v)
+    )
+  )
+)
+
+(declare-datatypes (T) ( (List (Nil) (Cstr (head T) (tail List) ) ) ) )
+(declare-datatypes (T S) ( (Pair (Pair (first T) (second S)) ) ) )
+
+(define-funs-rec
+  (
+    (validList ((l (List (Pair Int Int)))) Bool)
+  )
+  (
+    (ite (= l (as Nil (List (Pair Int Int))) )
+        true
+        (let ((hd (head l))) (and (>= (first hd) 0) 
+                                  (validIdValue (first hd) (second hd)) 
+                                  (validList (tail l))
+                              )
+        )
+    )
+  )
+)
+
+
+(declare-const myList (List (Pair Int Int)))
+(assert (distinct myList (as Nil (List (Pair Int Int)))))
+(assert (validList myList))
+(check-sat)
diff --git a/test/regress/regress0/fmf/pow2-bool.smt2 b/test/regress/regress0/fmf/pow2-bool.smt2
new file mode 100644
index 000000000..4943c646c
--- /dev/null
+++ b/test/regress/regress0/fmf/pow2-bool.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+
+(define-fun-rec pow2 ((n Int) (p Int)) Bool (
+	or
+	(and (= n 0) (= p 1))
+	(and (> n 0) (> p 1) (= 0 (mod p 2)) (pow2 (- n 1) (div p 2)))
+))
+
+(declare-const n Int)
+(declare-const p Int)
+
+(assert (= n 10))
+(assert (pow2 n p))
+
+(check-sat)
-- 
cgit v1.2.3