sketch doesn't work for me

[Mangpo Phitchaya Phothilimthana]

Hi Class,

I tried to verify my solution with sketch and it gave me this error "UNSATISFIABLE ASSERTION The spec and sketch can not be made to be equal". I thought I might got a wrong solution, so I ran the original code I got from the website (xpose3-QF_AUFLIA.rkt), but it still gave me the same error.

I attach 3 files here.
sol.out: output from z3
xpose.sk: what I put in sketch to solve. Note that I leave shuffle bits as ??, and it still give me unsat.
xpose.py: I just wrote a python script to check, and it seems that the solution is correct.

Please help! I don't know how to get sketch to work.

Mangpo

[Ras Bodik]

Hi Mangpo,

 

I tried to get to the root of the problem this morning but I failed. It’s quite possible that there is a bug in the SKETCH compiler.  It is a complex system and sometimes diagnosing it is difficult.  This is one reason why cs294 teaches you how to build a small, lightweight synthesizer.

 

Your Python-based verification is a good way to verify this particular program. 

 

Another approach for verifying your solution would be to create a verification formula, as explained in Lecture 2: translate the spec to a formula; translate the sketch to a formula; set holes to your solution; and ask the solver if there is an input on which the spec and the completed sketch disagree.

 

--Ras

 

--
 
 

[Emina Torlak]

Hi Mangpo,

Following up on Ras's response, I verified in Rosette that the QF_AUFLIA solution is correct for all 4x4 matrices.  But your Python verifier is also sufficient for this example, due to the lemma mentioned in L3:  if the code works on the input we gave you, it will work on all inputs.

We'll switch to using Rosette to verify your solutions, so it's no longer necessary to submit the completed xpose*.sk files.  We'll update HW2 to reflect this.

Thanks for letting us know about the problem.

Emina

--