From 6479c8ef954f6ac5877bd3302bdd9feb5f389d17 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Thu, 9 Jan 2025 10:56:57 +1300 Subject: [PATCH] Fix parsing of array accesses A simple fix for #505, which was being caused by the parser not considering qualified names correctly. --- pkg/corset/parser.go | 8 +- pkg/test/valid_corset_test.go | 8 ++ testdata/perspective_26.accepts | 31 +++++ testdata/perspective_26.lisp | 19 +++ testdata/perspective_26.rejects | 21 +++ testdata/perspective_27.accepts | 219 ++++++++++++++++++++++++++++++++ testdata/perspective_27.lisp | 15 +++ testdata/perspective_27.rejects | 54 ++++++++ 8 files changed, 373 insertions(+), 2 deletions(-) create mode 100644 testdata/perspective_26.accepts create mode 100644 testdata/perspective_26.lisp create mode 100644 testdata/perspective_26.rejects create mode 100644 testdata/perspective_27.accepts create mode 100644 testdata/perspective_27.lisp create mode 100644 testdata/perspective_27.rejects diff --git a/pkg/corset/parser.go b/pkg/corset/parser.go index 5d1d9d2..5f47d69 100644 --- a/pkg/corset/parser.go +++ b/pkg/corset/parser.go @@ -1237,8 +1237,12 @@ func arrayAccessParserRule(name string, args []Expr) (Expr, error) { if len(args) != 1 { return nil, errors.New("malformed array access") } - // - path := util.NewRelativePath(name) + // Handle qualified accesses (where permitted) + // Attempt to split column name into module / column pair. + path, err := parseQualifiableName(name) + if err != nil { + return nil, err + } // return &ArrayAccess{path, args[0], nil}, nil } diff --git a/pkg/test/valid_corset_test.go b/pkg/test/valid_corset_test.go index f7d0eee..04be1aa 100644 --- a/pkg/test/valid_corset_test.go +++ b/pkg/test/valid_corset_test.go @@ -871,6 +871,14 @@ func Test_Perspective_24(t *testing.T) { // Check(t, false, "perspective_25") // } +func Test_Perspective_26(t *testing.T) { + Check(t, false, "perspective_26") +} + +func Test_Perspective_27(t *testing.T) { + Check(t, false, "perspective_27") +} + // =================================================================== // Complex Tests // =================================================================== diff --git a/testdata/perspective_26.accepts b/testdata/perspective_26.accepts new file mode 100644 index 0000000..91390f7 --- /dev/null +++ b/testdata/perspective_26.accepts @@ -0,0 +1,31 @@ +{ "A": [], "P": [], "Q": [], "B_xor_C": [] } +;; +{ "A": [0], "P": [0], "Q": [0], "B_xor_C": [0] } +{ "A": [0], "P": [0], "Q": [0], "B_xor_C": [1] } +{ "A": [0], "P": [0], "Q": [0], "B_xor_C": [2] } +{ "A": [0], "P": [0], "Q": [0], "B_xor_C": [3] } +{ "A": [1], "P": [0], "Q": [0], "B_xor_C": [0] } +{ "A": [1], "P": [0], "Q": [0], "B_xor_C": [1] } +{ "A": [1], "P": [0], "Q": [0], "B_xor_C": [2] } +{ "A": [1], "P": [0], "Q": [0], "B_xor_C": [3] } +{ "A": [2], "P": [0], "Q": [0], "B_xor_C": [0] } +{ "A": [2], "P": [0], "Q": [0], "B_xor_C": [1] } +{ "A": [2], "P": [0], "Q": [0], "B_xor_C": [2] } +{ "A": [2], "P": [0], "Q": [0], "B_xor_C": [3] } +{ "A": [3], "P": [0], "Q": [0], "B_xor_C": [0] } +{ "A": [3], "P": [0], "Q": [0], "B_xor_C": [1] } +{ "A": [3], "P": [0], "Q": [0], "B_xor_C": [2] } +{ "A": [3], "P": [0], "Q": [0], "B_xor_C": [3] } +;; perspective p1 +{ "A": [0], "P": [1], "Q": [0], "B_xor_C": [0] } +{ "A": [1], "P": [1], "Q": [0], "B_xor_C": [1] } +{ "A": [2], "P": [1], "Q": [0], "B_xor_C": [2] } +{ "A": [3], "P": [1], "Q": [0], "B_xor_C": [3] } +;; perspective p2 +{ "A": [0], "P": [0], "Q": [1], "B_xor_C": [0] } +{ "A": [0], "P": [0], "Q": [1], "B_xor_C": [1] } +{ "A": [0], "P": [0], "Q": [1], "B_xor_C": [2] } +{ "A": [0], "P": [0], "Q": [1], "B_xor_C": [3] } +{ "A": [1], "P": [0], "Q": [1], "B_xor_C": [0] } +{ "A": [2], "P": [0], "Q": [1], "B_xor_C": [0] } +{ "A": [3], "P": [0], "Q": [1], "B_xor_C": [0] } diff --git a/testdata/perspective_26.lisp b/testdata/perspective_26.lisp new file mode 100644 index 0000000..ccef803 --- /dev/null +++ b/testdata/perspective_26.lisp @@ -0,0 +1,19 @@ +(defpurefun ((vanishes! :@loob :force) e0) e0) +;; +(defcolumns + ;; Column (not in perspective) + A + ;; Selector column for perspective p1 + (P :binary@prove) + ;; Selector column for perspective p2 + (Q :binary@prove)) + +;; Section 1 +(defperspective p1 P ((B :binary))) +(defun (p1-B) p1/B) +(defconstraint c1 (:perspective p1) (vanishes! (- A (p1-B)))) + +;; Section 2 +(defperspective p2 Q ((C :binary))) +(defun (p2-C) p2/C) +(defconstraint c2 (:perspective p2) (vanishes! (* A (p2-C)))) diff --git a/testdata/perspective_26.rejects b/testdata/perspective_26.rejects new file mode 100644 index 0000000..f13e9de --- /dev/null +++ b/testdata/perspective_26.rejects @@ -0,0 +1,21 @@ +{ "A": [0], "P": [1], "Q": [0], "B_xor_C": [1] } +{ "A": [0], "P": [1], "Q": [0], "B_xor_C": [2] } +{ "A": [0], "P": [1], "Q": [0], "B_xor_C": [3] } +{ "A": [1], "P": [1], "Q": [0], "B_xor_C": [2] } +{ "A": [1], "P": [1], "Q": [0], "B_xor_C": [3] } +{ "A": [1], "P": [1], "Q": [0], "B_xor_C": [0] } +{ "A": [2], "P": [1], "Q": [0], "B_xor_C": [0] } +{ "A": [2], "P": [1], "Q": [0], "B_xor_C": [1] } +{ "A": [2], "P": [1], "Q": [0], "B_xor_C": [3] } +{ "A": [3], "P": [1], "Q": [0], "B_xor_C": [0] } +{ "A": [3], "P": [1], "Q": [0], "B_xor_C": [1] } +{ "A": [3], "P": [1], "Q": [0], "B_xor_C": [2] } +{ "A": [1], "P": [0], "Q": [1], "B_xor_C": [1] } +{ "A": [1], "P": [0], "Q": [1], "B_xor_C": [2] } +{ "A": [1], "P": [0], "Q": [1], "B_xor_C": [3] } +{ "A": [2], "P": [0], "Q": [1], "B_xor_C": [1] } +{ "A": [2], "P": [0], "Q": [1], "B_xor_C": [2] } +{ "A": [2], "P": [0], "Q": [1], "B_xor_C": [3] } +{ "A": [3], "P": [0], "Q": [1], "B_xor_C": [1] } +{ "A": [3], "P": [0], "Q": [1], "B_xor_C": [2] } +{ "A": [3], "P": [0], "Q": [1], "B_xor_C": [3] } diff --git a/testdata/perspective_27.accepts b/testdata/perspective_27.accepts new file mode 100644 index 0000000..22753f7 --- /dev/null +++ b/testdata/perspective_27.accepts @@ -0,0 +1,219 @@ +{ "P": [], "Q": [], "B_1_xor_C_1": [], "B_2_xor_C_2": [] } +;; +{ "P": [0], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [3], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [256], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [423], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [551], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [892], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [3], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [256], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [423], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [551], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [892], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [3], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [256], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [423], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [551], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [892], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [255] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [3], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [256], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [423], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [551], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [892], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [3], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [256], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [423], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [551], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [892], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [444] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [3], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [256], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [423], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [551], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [892], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [1023] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [3], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [256], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [423], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [551], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [892], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [16385] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [3], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [256], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [423], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [551], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [892], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [3], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [256], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [423], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [551], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [892], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [65536] } +{ "P": [0], "Q": [0], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [65536] } +;; perspective p1 +{ "P": [1], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [0] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [1], "B_2_xor_C_2": [1] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [2], "B_2_xor_C_2": [2] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [3], "B_2_xor_C_2": [3] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [256], "B_2_xor_C_2": [256] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [423], "B_2_xor_C_2": [423] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [551], "B_2_xor_C_2": [551] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [892], "B_2_xor_C_2": [892] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [1011] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [2022] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [4483] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [8919] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [10101] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [16868] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [32378] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [65534] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [65535] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [65536] } +;; perspective p2 +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [1], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [2], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [2] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [3], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [3] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [256], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [423], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [423] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [551], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [551] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [892], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [892] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [1011] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [2022] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [4483] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [8919] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [10101] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [16868] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [32378] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [65534] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [0] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [0], "B_2_xor_C_2": [65536] } diff --git a/testdata/perspective_27.lisp b/testdata/perspective_27.lisp new file mode 100644 index 0000000..b2119c0 --- /dev/null +++ b/testdata/perspective_27.lisp @@ -0,0 +1,15 @@ +(defpurefun ((vanishes! :@loob :force) e0) e0) +;; +(defcolumns + ;; Selector column for perspective p1 + (P :binary@prove) + ;; Selector column for perspective p2 + (Q :binary@prove)) + +;; Section 1 +(defperspective p1 P ((B :binary :array [2]))) +(defconstraint c1 (:perspective p1) (vanishes! (- [p1/B 1] [p1/B 2]))) + +;; Section 2 +(defperspective p2 Q ((C :binary :array [2]))) +(defconstraint c2 (:perspective p2) (vanishes! (* [p2/C 1] [p2/C 2]))) diff --git a/testdata/perspective_27.rejects b/testdata/perspective_27.rejects new file mode 100644 index 0000000..a85e160 --- /dev/null +++ b/testdata/perspective_27.rejects @@ -0,0 +1,54 @@ +;; perspective p1 +{ "P": [1], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [1] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [0], "B_2_xor_C_2": [1] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [1], "B_2_xor_C_2": [2] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [2], "B_2_xor_C_2": [3] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [226], "B_2_xor_C_2": [256] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [42], "B_2_xor_C_2": [423] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [5511], "B_2_xor_C_2": [551] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [8342], "B_2_xor_C_2": [892] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [1111], "B_2_xor_C_2": [1011] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [20222], "B_2_xor_C_2": [2022] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [448], "B_2_xor_C_2": [4483] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [89], "B_2_xor_C_2": [8919] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [11], "B_2_xor_C_2": [10101] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [1668], "B_2_xor_C_2": [16868] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [33378], "B_2_xor_C_2": [32378] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [63534], "B_2_xor_C_2": [65534] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [65435], "B_2_xor_C_2": [65535] } +{ "P": [1], "Q": [0], "B_1_xor_C_1": [65539], "B_2_xor_C_2": [65536] } +;; perspective p2 +{ "P": [0], "Q": [1], "B_1_xor_C_1": [1], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [2], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [2], "B_2_xor_C_2": [3] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [4], "B_2_xor_C_2": [2] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [3], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [2], "B_2_xor_C_2": [3] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [256], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [255], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [423], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [1], "B_2_xor_C_2": [423] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [551], "B_2_xor_C_2": [233] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [8192], "B_2_xor_C_2": [551] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [892], "B_2_xor_C_2": [12] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [9812], "B_2_xor_C_2": [892] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [1011], "B_2_xor_C_2": [10] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [901], "B_2_xor_C_2": [1011] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [2022], "B_2_xor_C_2": [121] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [2], "B_2_xor_C_2": [2022] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [4483], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [9999], "B_2_xor_C_2": [4483] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [8919], "B_2_xor_C_2": [12] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [897], "B_2_xor_C_2": [8919] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [10101], "B_2_xor_C_2": [123] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [98], "B_2_xor_C_2": [10101] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [16868], "B_2_xor_C_2": [9] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [1], "B_2_xor_C_2": [16868] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [32378], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [32378] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [65534], "B_2_xor_C_2": [3278] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [255], "B_2_xor_C_2": [65534] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [65535], "B_2_xor_C_2": [256] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [101], "B_2_xor_C_2": [65535] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [65536], "B_2_xor_C_2": [1] } +{ "P": [0], "Q": [1], "B_1_xor_C_1": [1], "B_2_xor_C_2": [65536] }