From e8c09abb9165278b13491c83bdcbe17ae535126e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 7 Dec 2016 12:43:15 -0600 Subject: 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. --- test/regress/regress0/fmf/Makefile.am | 7 ++- test/regress/regress0/fmf/bounded_sets.smt2 | 18 ++++++++ test/regress/regress0/fmf/fmf-bound-2dim.smt2 | 15 +++++++ .../regress/regress0/fmf/fmf-strange-bounds-2.smt2 | 24 ++++++++++ test/regress/regress0/fmf/fmf-strange-bounds.smt2 | 35 +++++++++++++++ .../regress/regress0/fmf/memory_model-R_cpp-dd.cvc | 52 ++++++++++++++++++++++ 6 files changed, 150 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/fmf/bounded_sets.smt2 create mode 100644 test/regress/regress0/fmf/fmf-bound-2dim.smt2 create mode 100644 test/regress/regress0/fmf/fmf-strange-bounds-2.smt2 create mode 100644 test/regress/regress0/fmf/fmf-strange-bounds.smt2 create mode 100644 test/regress/regress0/fmf/memory_model-R_cpp-dd.cvc (limited to 'test') 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; -- cgit v1.2.3