Skip to content

Commit

Permalink
Fix parsing of array accesses
Browse files Browse the repository at this point in the history
A simple fix for #505, which was being caused by the parser not
considering qualified names correctly.
  • Loading branch information
DavePearce committed Jan 8, 2025
1 parent 0e49cad commit 6479c8e
Show file tree
Hide file tree
Showing 8 changed files with 373 additions and 2 deletions.
8 changes: 6 additions & 2 deletions pkg/corset/parser.go
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
Expand Down
8 changes: 8 additions & 0 deletions pkg/test/valid_corset_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -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
// ===================================================================
Expand Down
31 changes: 31 additions & 0 deletions testdata/perspective_26.accepts
Original file line number Diff line number Diff line change
@@ -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] }
19 changes: 19 additions & 0 deletions testdata/perspective_26.lisp
Original file line number Diff line number Diff line change
@@ -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))))
21 changes: 21 additions & 0 deletions testdata/perspective_26.rejects
Original file line number Diff line number Diff line change
@@ -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] }
219 changes: 219 additions & 0 deletions testdata/perspective_27.accepts
Original file line number Diff line number Diff line change
@@ -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] }
15 changes: 15 additions & 0 deletions testdata/perspective_27.lisp
Original file line number Diff line number Diff line change
@@ -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])))
Loading

0 comments on commit 6479c8e

Please sign in to comment.