Skip to content

Commit

Permalink
working
Browse files Browse the repository at this point in the history
  • Loading branch information
@tnelson
tnelson committed Mar 17, 2024
1 parent 2790b49 commit da233ff
Show file tree
Hide file tree
Showing 5 changed files with 128 additions and 87 deletions.
24 changes: 17 additions & 7 deletions forge/lang/ast.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -500,7 +500,7 @@
; these are shown to an end-user)
(define (raise-set-comp-quantifier-error e)
(raise-forge-error
#:msg (format "Set-comprehension variable domain expected a singleton or relational expression: ~a" (deparse e))
#:msg (format "Set-comprehension variable domain expected a singleton or relational expression of arity 1: ~a" (deparse e))
#:context e))
(define (comprehension info decls formula)
(for ([e (map cdr decls)])
Expand Down Expand Up @@ -531,12 +531,18 @@
([r0 e0 m0:opt-mult-class] ...)
pred)
(quasisyntax/loc stx
(begin
(unless (node/expr? e0)
(raise-set-comp-quantifier-error e0))
...
(let* ([r0 (node/expr/quantifier-var (nodeinfo #,(build-source-location stx) check-lang.check-lang) (node/expr-arity e0) (gensym (format "~a_set" 'r0)) 'r0)] ... )
(set/func #:info (nodeinfo #,(build-source-location stx) check-lang.check-lang) (list (cons r0 e0) ...) pred))))]))
(let* ([r0 (node/expr/quantifier-var
(nodeinfo #,(build-source-location stx) check-lang.check-lang)
1 (gensym (format "~a_set" 'r0)) 'r0)] ... )
; We need to check these only inside the let*, to allow for later decls to use earlier ones.
;(unless (node/expr? e0)
; (raise-set-comp-quantifier-error e0))
;;...
;(unless (equal? 1 (node/expr-arity e0))
; (raise-set-comp-quantifier-error e0))
;...
(set/func #:info (nodeinfo #,(build-source-location stx) check-lang.check-lang)
(list (cons r0 e0) ...) pred)))]))

;; -- relations ----------------------------------------------------------------

Expand Down Expand Up @@ -703,6 +709,10 @@
(define hash2-proc (make-robust-node-hash-syntax node/int/sum-quant 3))])

(define (sum-quant/func decls raw-int-expr #:info [node-info empty-nodeinfo])
(when (@> (length decls) 1)
(raise-forge-error
#:msg (format "sum aggregator only supports a single variable; if you wish to sum over multiple domains, please use nested sum aggregators.")
#:context node-info))
(for ([e (map cdr decls)])
(unless (node/expr? e)
(raise-forge-error
Expand Down
63 changes: 39 additions & 24 deletions forge/last-checker.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -461,28 +461,40 @@
checker-hash
; For rationale here, see the quantified-formula case. This differs slightly
; because a comprehension is an expression, and thus needs to report its type.
(cons (let ([child-values
(map (lambda (decl)
(let ([var (car decl)]
[domain (cdr decl)])
; CHECK: shadowed variables
(when (ormap (lambda (qvd)
(equal?
(node/expr/quantifier-var-name var)
(node/expr/quantifier-var-name (first qvd)))) quantvars)
(raise-forge-error
#:msg (format "Nested re-use of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var)
#:context info))
; CHECK: recur into domain(s)
(checkExpression run-or-state domain quantvars checker-hash)))
decls)]
; Extend domain environment
[new-quantvars (append (map assocify decls) quantvars)])
; CHECK: recur into subformula
(checkFormula run-or-state subform new-quantvars checker-hash)
; Return type constructed from decls above
(map flatten (map append (apply cartesian-product child-values))))
#f))]

(begin
(printf "comp: ~a ~n" decls)
(let ([new-decls-and-child-values
(foldl (lambda (decl acc)
(let ([var (car decl)]
[domain (cdr decl)]
[expanded-quantvars (first acc)]
[child-types (second acc)])
; CHECK: shadowed variables
(when (ormap (lambda (qvd)
(equal?
(node/expr/quantifier-var-name var)
(node/expr/quantifier-var-name (first qvd)))) quantvars)
(raise-forge-error
#:msg (format "Nested re-use of variable ~a detected. Check for something like \"some x: A | some x : B | ...\"." var)
#:context info))
; CHECK: recur into domain(s), aware of prior variables
(printf "checking in comp. ~a : ~a; ~a -- ~a~n" var domain expanded-quantvars child-types)
(let ([next-child-type
(checkExpression run-or-state domain expanded-quantvars checker-hash)])
; Accumulator: add current decl, add type (to end)
(list (cons (assocify decl) expanded-quantvars)
(reverse (cons next-child-type (reverse child-types)))))))
; Acc has the form: (quantvars-so-far child-values-in-order)
(list quantvars '())
decls)])
; CHECK: recur into subformula
(define new-quantvars (first new-decls-and-child-values))
(define child-values (second new-decls-and-child-values))
(checkFormula run-or-state subform new-quantvars checker-hash)
; Return type constructed from decls above
(cons (map flatten (map append (apply cartesian-product child-values)))
#f))))]

[else (error (format "no matching case in checkExpression for ~a" (deparse expr)))]))

Expand Down Expand Up @@ -711,10 +723,13 @@
(define decls (node/int/sum-quant-decls expr))
(let ([new-quantvars (append (map assocify decls) quantvars)])
(checkInt run-or-state (node/int/sum-quant-int-expr expr) new-quantvars checker-hash))
(for ([decl decls])
(for/fold ([new-quantvars quantvars])
([decl decls])
(define var (car decl))
(define domain (cdr decl))
(checkExpression run-or-state domain quantvars checker-hash))]))
; Check and throw away result
(checkExpression run-or-state domain new-quantvars checker-hash)
(cons (list var domain) quantvars))]))

; Is this integer literal safe under the current bitwidth?
(define/contract (check-int-literal run-or-state expr)
Expand Down
73 changes: 38 additions & 35 deletions forge/send-to-kodkod.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@
[(and (unbox server-state) ((Server-ports-is-running? (unbox server-state))))
(define sstate (unbox server-state))
(when (@> (get-verbosity) VERBOSITY_LOW)
(printf "Pardinus solver process already running. Starting new run with id ~a.~n" run-name))
(printf "Pardinus solver process already running. Preparing to start new run with id ~a.~n" run-name))
(values (Server-ports-stdin sstate) (Server-ports-stdout sstate)
(Server-ports-stderr sstate) (Server-ports-shutdown sstate)
(Server-ports-is-running? sstate))]
Expand Down Expand Up @@ -190,7 +190,43 @@

; Print configure and declare univ size
; Note that target mode is passed separately, nearer to the (solve) invocation
(define bitwidth (get-bitwidth run-spec))
(define bitwidth (get-bitwidth run-spec))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Generate top-level constraint for this run, execute last-checker
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (maybe-alwaysify fmla)
(if (equal? 'temporal (get-option run-spec 'problem_type))
(always/info (node-info fmla) fmla)
fmla))

; If in temporal mode, need to always-ify the auto-generated constraints but not the
; predicates that come from users
(define raw-implicit-constraints
(append (get-sig-size-preds run-spec sig-to-bound #:error raise-run-error)
(get-relation-preds run-spec)
(get-extender-preds run-spec)
relation-constraints
break-preds))
(define conjuncts-implicit-constraints
(apply append (map maybe-and->list raw-implicit-constraints)))
(define implicit-constraints
(map maybe-alwaysify conjuncts-implicit-constraints))
(define explicit-constraints
(apply append (map maybe-and->list (Run-spec-preds run-spec))))
(define run-constraints
(append explicit-constraints implicit-constraints))

; Run last-minute checks for errors
(for-each (lambda (c)
(checkFormula run-spec c '() (get-checker-hash)))
run-constraints)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Beginning to send to Pardinus. All type-checking must be complete _before_ this point.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(pardinus-print (pardinus:print-cmd (format "(with ~a" run-name)))
(pardinus-print
(pardinus:configure (format ":bitwidth ~a :solver ~a :max-solutions 1 :verbosity ~a :skolem-depth ~a :sb ~a :core-gran ~a :core-minimization ~a :log-trans ~a ~a ~a"
Expand Down Expand Up @@ -247,39 +283,6 @@

; Declare assertions
(define all-rels (get-all-rels run-spec))

(define (maybe-alwaysify fmla)
(if (equal? 'temporal (get-option run-spec 'problem_type))
(always/info (node-info fmla) fmla)
fmla))

; Get and print predicates
; If in temporal mode, need to always-ify the auto-generated constraints but not the
; predicates that come from users
; !!!
(define raw-implicit-constraints
(append (get-sig-size-preds run-spec sig-to-bound #:error raise-run-error)
(get-relation-preds run-spec)
(get-extender-preds run-spec)
relation-constraints
break-preds))
(define conjuncts-implicit-constraints
(apply append (map maybe-and->list raw-implicit-constraints)))
(define implicit-constraints
(map maybe-alwaysify conjuncts-implicit-constraints))
(define explicit-constraints
(apply append (map maybe-and->list (Run-spec-preds run-spec))))

(define run-constraints
(append explicit-constraints implicit-constraints))

; Run last-minute checks for errors
(for-each (lambda (c)
;(printf "deparse-constraint: ~a~n" (deparse c))
(checkFormula run-spec c '() (get-checker-hash)))
run-constraints)
;(when (@>= (get-verbosity) VERBOSITY_LOW)
; (printf " Last-checker finished. Beginning to send problem.~n"))

; Keep track of which formula corresponds to which CLI assert
; for highlighting unsat cores. TODO: map back from CLI output
Expand Down
4 changes: 3 additions & 1 deletion forge/sigs.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -658,7 +658,9 @@
#:msg (format "Failed test ~a. No Forge error was produced." 'name)
#:context loc
#:run run-reference
#:sterling #f))]
#:sterling #f))
(when (member 'name (hash-keys (State-runmap curr-state)))
(printf "Warning: successful `is forge_error` test run left in state environment: ~a.~n" 'name))]

[(member 'expected '(sat unsat))
#,(syntax/loc stx (run name args ...))
Expand Down
51 changes: 31 additions & 20 deletions forge/tests/forge/other/ast-errors.frg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,44 +28,42 @@ test expect {
sum_aggregator_decl_domain: {(sum x : (Person = Person) | x.age) = 1} is forge_error
-- test for bad arity in sum-aggregator sub-expression
sum_aggregator_decl_fmla: {(sum x : Person | age) = 1} is forge_error


-- test that the sum aggregator gives an error when multiple variables are declared
sum_aggregator_multiple_decls: {(sum x: Person, y: Person | min[x.age + y.age]) = 1} is forge_error
-- but that nesting is OK
sum_aggregator_multiple_decls_nested_ok: {(sum x: Person | sum y: Person | min[x.age + y.age]) = 1} is sat

----- quantification -----
-- Should be similar structure for each quantifier. Labeling the "some" cases for reference.



-- SOME
-- test for bad decl arity in quantification
quantifier_some_decl_arity: {some x : age | some x} is forge_error
-- test for bad syntax-type in quantifier decl
quantifier_some_decl_syntax_type: {some x : (Person = Person) | some x} is forge_error
-- test for bad syntax-type in quantifier decl
quantifier_some_decl_syntax_type: {some x : (Person = Person) | some x} is forge_error
-- test for bad type in quantified-formula subformula
quantifier_some_subformula_type: {some x : Person | x} is forge_error
-- test for non-variable in quantifier variable position
quantifier_some_decl_var: {some Person : Person | some Person} is forge_error

-- ALL
quantifier_all_decl_arity: {all x : age | some x} is forge_error
quantifier_all_decl_syntax_type: {all x : (Person = Person) | some x} is forge_error
quantifier_all_subformula_type: {all x : Person | x} is forge_error
quantifier_all_decl_var: {all Person : Person | some Person} is forge_error

-- LONE
quantifier_lone_decl_arity: {lone x : age | some x} is forge_error
quantifier_lone_decl_syntax_type: {lone x : (Person = Person) | some x} is forge_error
quantifier_lone_subformula_type: {lone x : Person | x} is forge_error
quantifier_lone_decl_var: {lone Person : Person | some Person} is forge_error

-- ONE
quantifier_one_decl_arity: {one x : age | some x} is forge_error
quantifier_one_decl_syntax_type: {one x : (Person = Person) | some x} is forge_error
quantifier_one_subformula_type: {one x : Person | x} is forge_error
quantifier_one_decl_var: {one Person : Person | some Person} is forge_error


-- NO
quantifier_no_decl_arity: {no x : age | some x} is forge_error
quantifier_no_decl_syntax_type: {no x : (Person = Person) | some x} is forge_error
quantifier_no_subformula_type: {no x : Person | x} is forge_error
quantifier_no_decl_var: {no Person : Person | some Person} is forge_error

-- Formula operators mis-used
and_given_expr_1: {some Person and Person} is forge_error
Expand Down Expand Up @@ -95,12 +93,10 @@ test expect {
tc_given_formula: {some ^(some Person)} is forge_error
rtc_given_formula: {some *(some Person)} is forge_error
transpose_given_formula: {some ~(some Person)} is forge_error


-- Set comprehension mis-used
comprehension_used_quantifier: { some {all x: Person | some x.age}} is forge_error
comprehension_bad_decl_arity: { some {x: age | some x.age}} is forge_error
comprehension_bad_decl_var: { some {Person: Person | some Person.age}} is forge_error
comprehension_bad_decl_type: { some {x: (Person = Person) | some x.age}} is forge_error

-- Cardinality mis-used
Expand Down Expand Up @@ -129,6 +125,8 @@ test expect {
-- 0-ary join result
zero_arity_join_result: {some Nim.Nim} is forge_error



-- Variable-name shadowing: this is an ergonomic issue. In basic examples, the need for
-- an error is "obvious". But even the Forge developers re-use variable names in helper
-- predicates, and so a very strict shadowing check would be annoying at best. We're
Expand All @@ -149,16 +147,29 @@ test expect {
set_minus_rhs_empty_join: { some Person - (age.Nim) } is forge_error

-- Minus operator: check RHS for validity, allow chaining
set_minus_rhs_quant: {all x: Person, y: Person - x | x != y} is theorem -- should be OK
set_minus_rhs_comp: {some {x: Person, y: Person - x | x != y}} is theorem -- should be OK

-- (Does not apply to sum aggregator, since that requires only one decl)
set_minus_rhs_quant_all: {all x: Person, y: Person - x | x != y} is theorem -- should be OK
set_minus_rhs_quant_no: {no x: Person, y: Person - x | x != y} is sat -- should be OK
set_minus_rhs_quant_some: {some x: Person, y: Person - x | x != y} is sat -- should be OK
set_minus_rhs_quant_lone: {lone x: Person, y: Person - x | x != y} is sat -- should be OK
set_minus_rhs_quant_one: {one x: Person, y: Person - x | x != y} is unsat -- should be OK
set_minus_rhs_comp: {some {x: Person, y: Person - x | x != y}} is sat -- should be OK

-- TODO --
-- Regression test: shadowing within a single comprehension or quantifier would cause Pardinus to crash.
internal_comp_variable_name_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat -- s/b FORGE error
internal_quant_variable_name_shadowing: {some x: Person, x: Person | x.age = x.age} is sat


//internal_quant_variable_name_shadowing: {some x: Person, x: Person | x.age = x.age} is sat
//internal_comp_variable_name_shadowing: {some {x: Person, x: Person | x.age = x.age}} is sat -- s/b FORGE error

-- test for non-variable in quantifier variable position
quantifier_some_decl_var: {some Person : Person | some Person} is forge_error
quantifier_all_decl_var: {all Person : Person | some Person} is forge_error
quantifier_lone_decl_var: {lone Person : Person | some Person} is forge_error
quantifier_one_decl_var: {one Person : Person | some Person} is forge_error
quantifier_no_decl_var: {no Person : Person | some Person} is forge_error
comprehension_bad_decl_var: { some {Person: Person | some Person.age}} is forge_error
-- regression test: the above "sig name as variable" forms could cause the below to crash:
all_multiple_vars_ok: {all x: Person, y: Person | x != y} is unsat -- should be OK
}


Expand Down

0 comments on commit da233ff

Please sign in to comment.