Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.

6 files changed, 150 insertions, 1 deletions

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 31fdb0a40..d734a6b95 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -57,7 +57,12 @@ TESTS =	\
 	LeftistHeap.scala-8-ncm.smt2 \
 	sc-crash-052316.smt2 \
 	bound-int-alt.smt2 \
-	bug723-irrelevant-funs.smt2
+	bug723-irrelevant-funs.smt2 \
+	bounded_sets.smt2 \
+	fmf-strange-bounds.smt2 \
+	fmf-strange-bounds-2.smt2 \
+	fmf-bound-2dim.smt2 \
+	memory_model-R_cpp-dd.cvc
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/bounded_sets.smt2 b/test/regress/regress0/fmf/bounded_sets.smt2
new file mode 100644
index 000000000..b06c3636f
--- /dev/null
+++ b/test/regress/regress0/fmf/bounded_sets.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+
+(declare-fun S () (Set Int))
+(declare-fun P (Int) Bool)
+(declare-fun a () Int)
+(assert (member a S))
+(assert (forall ((y Int)) (=> (member y S) (P y))))
+
+
+(declare-fun T () (Set Int))
+(declare-fun b () Int)
+(assert (member b T))
+(assert (forall ((y Int)) (=> (member y T) (not (P y)))))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/fmf-bound-2dim.smt2 b/test/regress/regress0/fmf/fmf-bound-2dim.smt2
new file mode 100644
index 000000000..5f5c22770
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-bound-2dim.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun P (Int Int) Bool)
+
+(declare-fun a () Int)
+(assert (> a 10))
+
+(assert (forall ((x Int) (y Int))
+(=> (and (<= a x) (<= x (+ a 5)) (<= 14 y) (<= y (+ 7 x)))
+(P x y))))
+(assert (not (P 15 4)))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2 b/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2
new file mode 100644
index 000000000..f1c53c4ef
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun P (Int U) Bool)
+
+(declare-fun S (U) (Set Int))
+
+(declare-fun f (U) U)
+
+(assert (forall ((x Int) (z U))
+(=> (member x (S (f z)))
+(P x z))))
+
+; need model of U size 2 to satisfy these
+(declare-fun a () U)
+(assert (member 77 (S a)))
+(assert (not (P 77 a)))
+
+; unsat
+(assert (forall ((x U) (y U)) (= x y)))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/fmf-strange-bounds.smt2 b/test/regress/regress0/fmf/fmf-strange-bounds.smt2
new file mode 100644
index 000000000..7812c2431
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-strange-bounds.smt2
@@ -0,0 +1,35 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun P (Int Int U) Bool)
+
+(declare-fun S () (Set Int))
+
+(declare-fun f (Int) U)
+(declare-fun g (Int) U)
+
+(declare-fun h (U) Int)
+
+(assert (member 77 S))
+(assert (>= (h (f 77)) 3))
+(assert (>= (h (g 77)) 2))
+(assert (not (= (g 77) (f 77))))
+
+(assert (forall ((x Int) (y Int) (z U)) (=> 
+(or (= z (f x)) (= z (g x)))
+(=> (member x S)
+(=> (and (<= 0 y) (<= y (h z)))
+(P x y z))))))
+
+
+(declare-fun Q (U Int) Bool)
+(declare-const a U)
+(declare-const b U)
+(declare-const c U)
+(assert (distinct a b c))
+(assert (forall ((x U) (y Int)) (=> (and (<= 3 y) (<= y 10) (or (= x c) (= x (f y)))) (Q x y))))
+(assert (not (Q b 6)))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/memory_model-R_cpp-dd.cvc b/test/regress/regress0/fmf/memory_model-R_cpp-dd.cvc
new file mode 100644
index 000000000..5d1289997
--- /dev/null
+++ b/test/regress/regress0/fmf/memory_model-R_cpp-dd.cvc
@@ -0,0 +1,52 @@
+% EXPECT: sat
+OPTION "produce-models";
+OPTION "fmf-bound";
+
+DATATYPE MOPERATION = R | W | M END;
+DATATYPE ORDER = I | SC | U END;
+DATATYPE ATOM = AT | NA END;
+
+DATATYPE BINT = I0 | I1 | I2 | I3 END;
+
+DATATYPE TEAR_TYPE = TEAR_TRUE | TEAR_FALSE END;
+SDBLOCK_TYPE: TYPE;
+VALUE_TYPE: TYPE;
+ADDRESS_TYPE: TYPE = SET OF BINT;
+
+MEM_OP_TYPE : TYPE = [# O:MOPERATION, T:TEAR_TYPE, R:ORDER, A:ATOM, B:SDBLOCK_TYPE, M:ADDRESS_TYPE, V:VALUE_TYPE #];
+EV_REL: TYPE = SET OF [MEM_OP_TYPE, MEM_OP_TYPE];
+THREAD_TYPE : TYPE = [# E:SET OF MEM_OP_TYPE, PO:EV_REL #];
+
+m1 : SDBLOCK_TYPE;
+
+ow1 : MEM_OP_TYPE;
+or2 : MEM_OP_TYPE;
+
+v1 : VALUE_TYPE;
+v2 : VALUE_TYPE;
+
+ASSERT (ow1.O = W) AND
+       (ow1.T = TEAR_FALSE) AND
+       (ow1.R = U) AND
+       (ow1.A = NA) AND
+       (ow1.B = m1) AND
+       (ow1.M = {I0}) AND
+       (ow1.V = v1);
+
+ASSERT (or2.O = R) AND
+       (or2.T = TEAR_FALSE) AND
+       (or2.R = U) AND
+       (or2.A = NA) AND
+       (or2.B = m1) AND
+       (or2.M = {I0}) AND
+       (or2.V = v2);
+
+ev_set : SET OF MEM_OP_TYPE;
+
+ASSERT ev_set = {ow1, or2};
+
+RF : EV_REL;
+
+ASSERT FORALL (r,w: MEM_OP_TYPE) : (((r IS_IN ev_set) AND (w IS_IN ev_set)) => (((r,w) IS_IN RF) <=> ((r.O = R) AND (w.O = W))));
+
+CHECKSAT;