diff options
Diffstat (limited to 'test/regress/regress1/rels/addr_book_1.cvc')
-rw-r--r-- | test/regress/regress1/rels/addr_book_1.cvc | 45 |
1 files changed, 0 insertions, 45 deletions
diff --git a/test/regress/regress1/rels/addr_book_1.cvc b/test/regress/regress1/rels/addr_book_1.cvc deleted file mode 100644 index 8e7cdbd9d..000000000 --- a/test/regress/regress1/rels/addr_book_1.cvc +++ /dev/null @@ -1,45 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -Atom : TYPE; -AtomTup : TYPE = [Atom]; -AtomBinTup : TYPE = [Atom, Atom]; -AtomTerTup : TYPE = [Atom, Atom, Atom]; -Target: SET OF AtomTup; - -Name: SET OF AtomTup; -Addr: SET OF AtomTup; -Book: SET OF AtomTup; -names: SET OF AtomBinTup; -addr: SET OF AtomTerTup; - -b1: Atom; -b1_tup : AtomTup; -ASSERT b1_tup = TUPLE(b1); -ASSERT b1_tup IS_IN Book; - -b2: Atom; -b2_tup : AtomTup; -ASSERT b2_tup = TUPLE(b2); -ASSERT b2_tup IS_IN Book; - -b3: Atom; -b3_tup : AtomTup; -ASSERT b3_tup = TUPLE(b3); -ASSERT b3_tup IS_IN Book; - -m: Atom; -m_tup : AtomTup; -ASSERT m_tup = TUPLE(m); -ASSERT m_tup IS_IN Name; - -t: Atom; -t_tup : AtomTup; -ASSERT t_tup = TUPLE(t); -ASSERT t_tup IS_IN Target; - -ASSERT ({m_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup; -ASSERT ({b2_tup} JOIN addr) = ({b1_tup} JOIN addr) | {(m,t)}; -ASSERT ({b3_tup} JOIN addr) = ({b2_tup} JOIN addr) - {(m,t)}; -ASSERT NOT (({b1_tup} JOIN addr) = ({b3_tup} JOIN addr)); - -CHECKSAT;
\ No newline at end of file |