How to get the “P_4” = 3 from m below
(match Z3.Solver.get_model solver with
| Some m -> (SAT, Some m)
| None -> assert false))
I got SAT status and a Model.model option solution, which can be printed as
SAT
(define-fun P_4 () Int
3)
(define-fun P_6 () Int
6)
(define-fun P_2 () Int
7)
(define-fun P_8 () Int
2)
(define-fun P_3 () Int
1)
(define-fun P_7 () Int
4)
(define-fun P_1 () Int
5)
(define-fun P_5 () Int
8)
New contributor
bftang is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.