diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 16:23:58 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 16:23:58 -0500 |
commit | 031722bee8682005bd4c8700ef78b5f893fc48fe (patch) | |
tree | 46a936a1bd20ea2cc588df0d3205cf7eb0fd4177 /test/regress/regress0/rels/bv1p-sat.cvc | |
parent | e79e64329ce7d6df0003cab28dadb9b8bcc6f9ca (diff) |
New implementation of sets+cardinality. Merge Paul Meng's relation solver as extension of sets solver, add regressions.
Diffstat (limited to 'test/regress/regress0/rels/bv1p-sat.cvc')
-rw-r--r-- | test/regress/regress0/rels/bv1p-sat.cvc | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/bv1p-sat.cvc b/test/regress/regress0/rels/bv1p-sat.cvc new file mode 100644 index 000000000..5eceb214c --- /dev/null +++ b/test/regress/regress0/rels/bv1p-sat.cvc @@ -0,0 +1,22 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)]; +x : SET OF BvPair; +y : SET OF BvPair; + +a : BvPair; +b : BvPair; +c : BvPair; +d : BvPair; + +ASSERT DISTINCT ( a, b ); +ASSERT DISTINCT ( c, d ); + +ASSERT a IS_IN x; +ASSERT b IS_IN x; +ASSERT a IS_IN y; +ASSERT b IS_IN y; +ASSERT NOT ( c IS_IN (x JOIN y)) AND NOT ( d IS_IN (x JOIN y)); + + +CHECKSAT; |