[SOLVED] Does Picat support Program Synthesis?

Does Picat support Program Synthesis?

Can I define a program synthesis task in Picat, similar to this definition in SyGuS format?

(set-logic LIA)

(synth-fun f ((color Int) (sortAsc Int) (sortDesc Int)) Int 
  ((I Int) (B Bool))
  ((I Int (color sortAsc sortDesc 0 1 2 3 4
           (ite B I I)))
   (B Bool ((<= I I) (= I I))))
)

(declare-var color Int)
(declare-var sortAsc Int)
(declare-var sortDesc Int)

(constraint (= (f 1 2 2) 0))
(constraint (= (f 1 4 0) 2))
(constraint (= (f 1 1 3) 0))
(constraint (= (f 1 3 1) 0))
(constraint (= (f 1 0 4) 3))

(constraint (= (f 1 2 1) 0))
(constraint (= (f 1 0 3) 3))
(constraint (= (f 1 3 0) 2))
(constraint (= (f 1 1 2) 0))

(check-synth)

Solution

Picat does not have any built-in support for program synthesis. It has support of constraint modelling using Constraint Logic Programming (CLP) with support for CP/SAT/MIP/SMT solvers, but the SMT solver is used as a constraint solver.

Perhaps related: I wrote an (experimental) symbolic regression program which might be used for similar tasks: http://hakank.org/picat/symbolic_regression.pi

Admittedly, I'm not sure exactly what operators are allowed in the presented SyGuS program, but given the data in the "constraints" section and with some given operators (if_then_else and if_less) and some constants (0..3), it finds some possible solutions such as the following for the input [1,2,3] (as [A,B,C]):

 if_less(0,B * C,0,if_less(B,A,3,2)) 
 if_less(0,C,if_less(B,A,3,0),2)

as well as a more complex variants, all giving 0 as the output.

The data file shows some of the different solutions from a single run of the program: http://hakank.org/picat/symbolic_regression_program_synthesis.pi

Note that the program is not deterministic and will yield different solutions each time it's run, though smaller solutions tends be selected more often.

Also, the solutions might not be proper Picat syntax, so one have to translate it to proper syntax. For example, the first solution if_less(0,B * C,0,if_less(B,A,3,2)) corresponds to this Picat program/snippet

if 0 < B * C then
   println(0)
elseif B < A then
   println(3)
else
   println(2)
end,

or - better - using cond/3:

cond(0 < B * C, 0, cond(B < A, 3, 2))

The program is tested in the test predicate of symbolic_regression_program_synthesis.pi And it generates all the expected outputs from the data:

[input = [1,2,2],expected = 0,out = 0,verdict = ok]
[input = [1,4,0],expected = 2,out = 2,verdict = ok]
[input = [1,1,3],expected = 0,out = 0,verdict = ok]
[input = [1,3,1],expected = 0,out = 0,verdict = ok]
[input = [1,0,4],expected = 3,out = 3,verdict = ok]
[input = [1,2,1],expected = 0,out = 0,verdict = ok]
[input = [1,0,3],expected = 3,out = 3,verdict = ok]
[input = [1,3,0],expected = 2,out = 2,verdict = ok]
[input = [1,1,2],expected = 0,out = 0,verdict = ok]

At my Picat page (http://hakank.org/picat/) there are quite a few other examples of using this (search for "symbolic regression"). I also wrote a short introduction of the program in the Picat group: https://groups.google.com/g/picat-lang/c/1CngmWD0_tw/m/m_9T_SViEAAJ