Skip to content

Commit

Permalink
Support :guard attribute
Browse files Browse the repository at this point in the history 
This implements the `:guard` attribute on vanishing constraints.  This
is a relatively straightforward extension of the status quo.
  • Loading branch information
@DavePearce
DavePearce committed Oct 24, 2024
1 parent 266c677 commit d6b5d9d
Show file tree
Hide file tree
Showing 17 changed files with 474 additions and 10 deletions.
27 changes: 17 additions & 10 deletions pkg/hir/parser.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -435,7 +435,7 @@ func (p *hirParser) parseConstraintDeclaration(elements []sexp.SExp) error {
// Vanishing constraints do not have global scope, hence qualified column
// accesses are not permitted.
p.global = false
attributes, err := p.parseConstraintAttributes(elements[2])
domain, guard, err := p.parseConstraintAttributes(elements[2])
// Check for error
if err != nil {
return err
Expand All @@ -444,6 +444,9 @@ func (p *hirParser) parseConstraintDeclaration(elements []sexp.SExp) error {
expr, err := p.translator.Translate(elements[3])
if err != nil {
return err
} else if guard != nil {
// if guard != 0 then expr
expr = &IfZero{guard, nil, expr}
}
// Determine evaluation context of expression.
ctx := expr.Context(p.env.schema)
Expand All @@ -454,16 +457,15 @@ func (p *hirParser) parseConstraintDeclaration(elements []sexp.SExp) error {
return p.translator.SyntaxError(elements[3], "empty evaluation context")
}

p.env.schema.AddVanishingConstraint(handle, ctx, attributes, expr)
p.env.schema.AddVanishingConstraint(handle, ctx, domain, expr)

return nil
}

func (p *hirParser) parseConstraintAttributes(attributes sexp.SExp) (domain *int, err error) {
var res *int = nil
func (p *hirParser) parseConstraintAttributes(attributes sexp.SExp) (domain *int, guard Expr, err error) {
// Check attribute list is a list
if attributes.AsList() == nil {
return nil, p.translator.SyntaxError(attributes, "expected attribute list")
return nil, nil, p.translator.SyntaxError(attributes, "expected attribute list")
}
// Deconstruct as list
attrs := attributes.AsList()
Expand All @@ -472,21 +474,26 @@ func (p *hirParser) parseConstraintAttributes(attributes sexp.SExp) (domain *int
ith := attrs.Get(i)
// Check start of attribute
if ith.AsSymbol() == nil {
return nil, p.translator.SyntaxError(ith, "malformed attribute")
return nil, nil, p.translator.SyntaxError(ith, "malformed attribute")
}
// Check what we've got
switch ith.AsSymbol().Value {
case ":domain":
i++
if res, err = p.parseDomainAttribute(attrs.Get(i)); err != nil {
return nil, err
if domain, err = p.parseDomainAttribute(attrs.Get(i)); err != nil {
return nil, nil, err
}
case ":guard":
i++
if guard, err = p.translator.Translate(attrs.Get(i)); err != nil {
return nil, nil, err
}
default:
return nil, p.translator.SyntaxError(ith, "unknown attribute")
return nil, nil, p.translator.SyntaxError(ith, "unknown attribute")
}
}
// Done
return res, nil
return domain, guard, nil
}

func (p *hirParser) parseDomainAttribute(attribute sexp.SExp) (domain *int, err error) {
Expand Down
24 changes: 24 additions & 0 deletions pkg/test/ir_test.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -248,6 +248,30 @@ func Test_If_09(t *testing.T) {
Check(t, "if_09")
}

// ===================================================================
// Guards
// ===================================================================

func Test_Guard_01(t *testing.T) {
Check(t, "guard_01")
}

func Test_Guard_02(t *testing.T) {
Check(t, "guard_02")
}

func Test_Guard_03(t *testing.T) {
Check(t, "guard_03")
}

func Test_Guard_04(t *testing.T) {
Check(t, "guard_04")
}

func Test_Guard_05(t *testing.T) {
Check(t, "guard_05")
}

// ===================================================================
// Column Types
// ===================================================================
Expand Down
22 changes: 22 additions & 0 deletions testdata/guard_01.accepts
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
{ "STAMP": [], "X": [] }
{ "STAMP": [0], "X": [0] }
{ "STAMP": [0], "X": [1] }
{ "STAMP": [0], "X": [2] }
{ "STAMP": [0], "X": [3] }
{ "STAMP": [1], "X": [1] }
{ "STAMP": [1], "X": [2] }
;;
{ "STAMP": [0,0], "X": [0,0] }
{ "STAMP": [0,1], "X": [0,1] }
{ "STAMP": [0,1], "X": [0,2] }
{ "STAMP": [0,2], "X": [0,1] }
{ "STAMP": [0,2], "X": [0,2] }
{ "STAMP": [1,0], "X": [1,0] }
{ "STAMP": [1,0], "X": [2,0] }
{ "STAMP": [2,0], "X": [1,0] }
{ "STAMP": [2,0], "X": [2,0] }
{ "STAMP": [1,0], "X": [1,0] }
{ "STAMP": [1,1], "X": [1,1] }
{ "STAMP": [1,1], "X": [1,2] }
{ "STAMP": [1,2], "X": [1,1] }
{ "STAMP": [1,2], "X": [1,2] }
3 changes: 3 additions & 0 deletions testdata/guard_01.lisp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
(defcolumns STAMP X)
;; STAMP == 0 || X == 1 || X == 2
(defconstraint c1 (:guard STAMP) (* (- X 1) (- X 2)))
8 changes: 8 additions & 0 deletions testdata/guard_01.rejects
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
{ "STAMP": [1], "X": [0] }
{ "STAMP": [1], "X": [3] }
{ "STAMP": [2], "X": [0] }
{ "STAMP": [2], "X": [3] }
{ "STAMP": [1,0], "X": [0,0] }
{ "STAMP": [1,1], "X": [0,1] }
{ "STAMP": [1,1], "X": [0,2] }
{ "STAMP": [1,2], "X": [0,1] }
36 changes: 36 additions & 0 deletions testdata/guard_02.accepts
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
{ "ST": [], "A": [], "B": [] }
{ "ST": [0], "A": [-2], "B": [123] }
{ "ST": [0], "A": [-1], "B": [123] }
{ "ST": [0], "A": [0], "B": [0] }
{ "ST": [0], "A": [1], "B": [123] }
{ "ST": [0], "A": [2], "B": [123] }
{ "ST": [0], "A": [0], "B": [-1] }
{ "ST": [0], "A": [0], "B": [1] }
{ "ST": [0], "A": [0], "B": [2] }
{ "ST": [0,0], "A": [1,0], "B": [-1,-1] }
{ "ST": [0,0], "A": [1,0], "B": [1,1] }
{ "ST": [0,0], "A": [1,0], "B": [2,2] }
{ "ST": [0,0], "A": [0,0], "B": [0,0] }
{ "ST": [0,0], "A": [1,0], "B": [123,0] }
{ "ST": [0,0], "A": [0,1], "B": [0,123] }
{ "ST": [0,0], "A": [1,1], "B": [123,234] }
;;
{ "ST": [], "A": [], "B": [] }
{ "ST": [1], "A": [-2], "B": [123] }
{ "ST": [1], "A": [-1], "B": [123] }
{ "ST": [1], "A": [0], "B": [0] }
{ "ST": [1], "A": [1], "B": [123] }
{ "ST": [1], "A": [2], "B": [123] }
{ "ST": [0,1], "A": [0,0], "B": [0,0] }
{ "ST": [0,1], "A": [1,0], "B": [123,0] }
{ "ST": [0,1], "A": [0,1], "B": [0,123] }
{ "ST": [0,1], "A": [1,1], "B": [123,234] }
{ "ST": [1,0], "A": [0,0], "B": [0,0] }
{ "ST": [1,0], "A": [1,0], "B": [123,0] }
{ "ST": [1,0], "A": [0,1], "B": [0,123] }
{ "ST": [1,0], "A": [1,1], "B": [123,234] }
{ "ST": [1,1], "A": [0,0], "B": [0,0] }
{ "ST": [1,1], "A": [1,0], "B": [123,0] }
{ "ST": [1,1], "A": [0,1], "B": [0,123] }
{ "ST": [1,1], "A": [1,1], "B": [123,234] }
;;
3 changes: 3 additions & 0 deletions testdata/guard_02.lisp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
(defcolumns ST A B)
;; STAMP == 0 || X == 1 || X == 2
(defconstraint c1 (:guard ST) (if A B))
9 changes: 9 additions & 0 deletions testdata/guard_02.rejects
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
{ "ST": [1], "A": [0], "B": [-1] }
{ "ST": [1], "A": [0], "B": [1] }
{ "ST": [1], "A": [0], "B": [2] }
{ "ST": [0,1], "A": [1,0], "B": [-1,-1] }
{ "ST": [0,1], "A": [1,0], "B": [1,1] }
{ "ST": [0,1], "A": [1,0], "B": [2,2] }
{ "ST": [1,1], "A": [1,0], "B": [-1,-1] }
{ "ST": [1,1], "A": [1,0], "B": [1,1] }
{ "ST": [1,1], "A": [1,0], "B": [2,2] }
29 changes: 29 additions & 0 deletions testdata/guard_03.accepts
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
{ "ST": [], "A": [], "B": [] }
{ "ST": [0], "A": [0], "B": [-1] }
{ "ST": [0], "A": [0], "B": [1] }
{ "ST": [0], "A": [0], "B": [2] }
{ "ST": [1], "A": [0], "B": [-1] }
{ "ST": [1], "A": [0], "B": [1] }
{ "ST": [1], "A": [0], "B": [2] }
{ "ST": [0,0], "A": [1,0], "B": [0,-1] }
{ "ST": [0,0], "A": [1,0], "B": [0,1] }
{ "ST": [0,0], "A": [1,0], "B": [0,2] }
{ "ST": [1,0], "A": [1,0], "B": [0,-1] }
{ "ST": [1,0], "A": [1,0], "B": [0,1] }
{ "ST": [1,0], "A": [1,0], "B": [0,2] }
{ "ST": [0,1], "A": [1,0], "B": [0,-1] }
{ "ST": [0,1], "A": [1,0], "B": [0,1] }
{ "ST": [0,1], "A": [1,0], "B": [0,2] }
{ "ST": [1,1], "A": [1,0], "B": [0,-1] }
{ "ST": [1,1], "A": [1,0], "B": [0,1] }
{ "ST": [1,1], "A": [1,0], "B": [0,2] }
;;
{ "ST": [0], "A": [-2], "B": [123] }
{ "ST": [0], "A": [-1], "B": [123] }
{ "ST": [0], "A": [1], "B": [1] }
{ "ST": [0], "A": [1], "B": [123] }
{ "ST": [0], "A": [2], "B": [123] }
{ "ST": [0,0], "A": [0,1], "B": [0,1] }
{ "ST": [0,0], "A": [1,0], "B": [123,0] }
{ "ST": [0,0], "A": [0,1], "B": [0,123] }
{ "ST": [0,0], "A": [1,1], "B": [123,234] }
2 changes: 2 additions & 0 deletions testdata/guard_03.lisp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
(defcolumns ST A B)
(defconstraint c1 (:guard ST) (ifnot A B))
9 changes: 9 additions & 0 deletions testdata/guard_03.rejects
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
{ "ST": [1], "A": [-2], "B": [123] }
{ "ST": [1], "A": [-1], "B": [123] }
{ "ST": [1], "A": [1], "B": [1] }
{ "ST": [1], "A": [1], "B": [123] }
{ "ST": [1], "A": [2], "B": [123] }
{ "ST": [1,1], "A": [0,1], "B": [0,1] }
{ "ST": [1,1], "A": [1,0], "B": [123,0] }
{ "ST": [1,1], "A": [0,1], "B": [0,123] }
{ "ST": [1,1], "A": [1,1], "B": [123,234] }
46 changes: 46 additions & 0 deletions testdata/guard_04.accepts
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
{ "ST": [], "A": [], "B": [], "C": [] }
{ "ST": [0], "A": [-2], "B": [234], "C": [0] }
{ "ST": [0], "A": [-1], "B": [123], "C": [0] }
{ "ST": [0], "A": [0], "B": [0], "C": [123] }
{ "ST": [0], "A": [0], "B": [0], "C": [234] }
{ "ST": [0], "A": [1], "B": [123], "C": [0] }
{ "ST": [0], "A": [2], "B": [234], "C": [0] }
;;
{ "ST": [1], "A": [-2], "B": [234], "C": [0] }
{ "ST": [1], "A": [-1], "B": [123], "C": [0] }
{ "ST": [1], "A": [0], "B": [0], "C": [123] }
{ "ST": [1], "A": [0], "B": [0], "C": [234] }
{ "ST": [1], "A": [1], "B": [123], "C": [0] }
{ "ST": [1], "A": [2], "B": [234], "C": [0] }
;;
{ "ST": [0], "A": [0], "B": [-2], "C": [0] }
{ "ST": [0], "A": [0], "B": [-1], "C": [0] }
{ "ST": [0], "A": [0], "B": [1], "C": [0] }
{ "ST": [0], "A": [0], "B": [2], "C": [0] }
{ "ST": [0], "A": [0], "B": [-2], "C": [-1] }
{ "ST": [0], "A": [0], "B": [-1], "C": [1] }
{ "ST": [0], "A": [0], "B": [1], "C": [2] }
{ "ST": [0], "A": [0], "B": [2], "C": [-2] }
{ "ST": [0], "A": [1], "B": [0], "C": [-2] }
{ "ST": [0], "A": [1], "B": [0], "C": [-1] }
{ "ST": [0], "A": [1], "B": [0], "C": [1] }
{ "ST": [0], "A": [1], "B": [0], "C": [2] }
{ "ST": [0], "A": [1], "B": [-2], "C": [-2] }
{ "ST": [0], "A": [1], "B": [-1], "C": [-1] }
{ "ST": [0], "A": [1], "B": [1], "C": [1] }
{ "ST": [0], "A": [1], "B": [1], "C": [2] }
{ "ST": [0], "A": [2], "B": [0], "C": [-2] }
{ "ST": [0], "A": [2], "B": [0], "C": [-1] }
{ "ST": [0], "A": [2], "B": [0], "C": [1] }
{ "ST": [0], "A": [2], "B": [0], "C": [2] }
{ "ST": [0], "A": [2], "B": [-2], "C": [-2] }
{ "ST": [0], "A": [2], "B": [-1], "C": [-1] }
{ "ST": [0], "A": [2], "B": [1], "C": [1] }
{ "ST": [0], "A": [2], "B": [1], "C": [2] }
;;
{ "ST": [0,0,0,0,0], "A": [-2,-1,0,1,2], "B": [234,123,0,456,789], "C": [0,0,123,0,0]}
{ "ST": [1,0,0,0,0], "A": [-2,-1,0,1,2], "B": [234,123,0,456,789], "C": [0,0,123,0,0]}
{ "ST": [0,1,0,0,0], "A": [-2,-1,0,1,2], "B": [234,123,0,456,789], "C": [0,0,123,0,0]}
{ "ST": [0,0,1,0,0], "A": [-2,-1,0,1,2], "B": [234,123,0,456,789], "C": [0,0,123,0,0]}
{ "ST": [0,0,0,1,0], "A": [-2,-1,0,1,2], "B": [234,123,0,456,789], "C": [0,0,123,0,0]}
{ "ST": [0,0,0,0,1], "A": [-2,-1,0,1,2], "B": [234,123,0,456,789], "C": [0,0,123,0,0]}
2 changes: 2 additions & 0 deletions testdata/guard_04.lisp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
(defcolumns ST A B C)
(defconstraint c1 (:guard ST) (if A B C))
24 changes: 24 additions & 0 deletions testdata/guard_04.rejects
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
{ "ST": [1], "A": [0], "B": [-2], "C": [0] }
{ "ST": [1], "A": [0], "B": [-1], "C": [0] }
{ "ST": [1], "A": [0], "B": [1], "C": [0] }
{ "ST": [1], "A": [0], "B": [2], "C": [0] }
{ "ST": [1], "A": [0], "B": [-2], "C": [-1] }
{ "ST": [1], "A": [0], "B": [-1], "C": [1] }
{ "ST": [1], "A": [0], "B": [1], "C": [2] }
{ "ST": [1], "A": [0], "B": [2], "C": [-2] }
{ "ST": [1], "A": [1], "B": [0], "C": [-2] }
{ "ST": [1], "A": [1], "B": [0], "C": [-1] }
{ "ST": [1], "A": [1], "B": [0], "C": [1] }
{ "ST": [1], "A": [1], "B": [0], "C": [2] }
{ "ST": [1], "A": [1], "B": [-2], "C": [-2] }
{ "ST": [1], "A": [1], "B": [-1], "C": [-1] }
{ "ST": [1], "A": [1], "B": [1], "C": [1] }
{ "ST": [1], "A": [1], "B": [1], "C": [2] }
{ "ST": [1], "A": [2], "B": [0], "C": [-2] }
{ "ST": [1], "A": [2], "B": [0], "C": [-1] }
{ "ST": [1], "A": [2], "B": [0], "C": [1] }
{ "ST": [1], "A": [2], "B": [0], "C": [2] }
{ "ST": [1], "A": [2], "B": [-2], "C": [-2] }
{ "ST": [1], "A": [2], "B": [-1], "C": [-1] }
{ "ST": [1], "A": [2], "B": [1], "C": [1] }
{ "ST": [1], "A": [2], "B": [1], "C": [2] }
Loading

0 comments on commit d6b5d9d

Please sign in to comment.