Problem with choose*

[subhajitroy]

Hi,

I am trying out synthesizing some expressions in a small DSL (please see attached file). The numbers are wrapped in a "num" struct, which I plan to extend later to handle "special" values like infinity via some additional axioms.

I get a strange behavior where the synthesis fails, though there exists an expression (plus (num x) (num x)) that is a feasible solution for the sketch. Interestingly, if the sketch is changed to the following semantically equivalent definition, it succeeds.

(define sketch (plus (plus (num 0) (num 0)) (??expr (list x p q))))

Could there be some bug in the implementation of choose* that prohibits the earlier sketch?

Regards, Subhajit

bug_report.txt

[emina]

Hi Subhajit,

Rosette's match is much more limited than Racket's match. Specifically, when you're matching a struct, you may not put additional constraints on the fields. So, (plus a b) is okay, but (plus (num a1) (num b1)) is not. In other words, the fields can only be bound to variables; they cannot be deconstructed further.

Here is a small edit to your example that works as expected.

Cheers, Emina

#lang rosette/safe

(require rosette/lib/match)
(require rosette/lib/synthax)
(require rosette/lib/angelic)

(struct plus (left right) #:transparent)
(struct num (val) #:transparent)

(define (interpret p)
  (match p
    [(plus a b) (num (+ (num-val (interpret a)) (num-val (interpret b))))]
    [(num _) p]))

; check if interpreter works
(interpret (plus (num 0) (plus (num 2) (num 3))))

(define (??expr terminals)
  (define a (apply choose* terminals))
  (define b (apply choose* terminals))
  (choose* (plus (num a) (num b))
           (num a)
           (num 0)))

(define-symbolic p q x integer?)  ; get access to more constants
(define sketch
  (plus (num 0) (??expr (list x p q))))
;  (plus (plus (num 0) (num 0)) (??expr (list x p q))))

(define M
  (synthesize
    #:forall (list x)
    #:guarantee (assert (equal? (interpret sketch) (num (* 2 x))))))

(evaluate sketch M)

[subhajitroy]

Hi Emina,

Thanks a lot! It also looks like matching on lists is not possible (either that or I am exceeding some nesting depth for matching). Is there some document that discusses the restrictions on the lifted version of match?

The following does not work:

(define (eval op eop a b) (if (and (num? a) (num? b)) (match (list (num-typ a) (num-typ b)) [(list #t #t) a] [(list #t #f) a] [(list #f #t) b] [(list #f #f) (num #f (op (num-val a) (num-val b)))]) (interpret (eop (interpret a) (interpret b)))))

But rewriting as if-condition works:

(define (eval op eop a b) (if (and (num? a) (num? b)) (if (or (num-typ a) (num-typ b)) (num #t 0) (num #f (op (num-val a) (num-val b)))) (interpret (eop (interpret a) (interpret b)))))

Regards, Subhajit

infinity.txt

[emina]

Hi Subhajit,

The restriction on lists, structs, and all other data structures is the same: the only patterns that can appear inside of a data-structure match are variables or wildcards, such as _. So constants, other structures, predicates, etc., are disallowed. For your example, this means that lists can only be matched as (list x y).

Think of Rosette's match as just a convenient way to extract struct field values. That's the most common (and safe) use case.

Cheers, Emina

[subhajitroy]

Hi Emina,

Got it! Thank you so much.

Regards, Subhajit

[subhajitroy]

Hi Emina,

I was trying to implement CEGIS-style synthesis; the expression being synthesized is (lambda x: x + x). The struct (num a b) models arithmetic on naturals with "special" values like infinity and negative-infinity as well.

On a set of "bad" examples that make the problem under-constrained, Rosette fails to return a proper program in the DSL (possibly due to the model returned by Z3). For example, on providing "f(infinity)=infinity" as the only example, evaluating the function on the model returns a long long string (attached) but not a program in the DSL. However, providing a good example like "f(2)=4" gives back a nice program (plus x x).

Is there way of forcing Rosette to provide "any of " the feasible programs? I can understand that the problem is with Z3's model, but I am curious if you have figured some way around this. As CEGIS problems are typically under-constrained, it essentially breaks the loop. Is there any feature or trick around it?

I will also appreciate your feedback on the encoding in Rosette and any suggestions/pointers for a better encoding :)

Regards, Subhajit

ouput.txt cegis.txt

[emina]

Hi Subhajit,

The issue here is that (f (num #t 1) (num #t 1)) in the synthesis query evaluates to #t. So there is nothing to solve for. The model M is the empty model, because the assertion is always true.

Cheers, Emina