Рекурсивная функция API Zcam Ocaml - PullRequest
Новая
       16

Рекурсивная функция API Zcam Ocaml

0 голосов
/ 12 мая 2018

Допустим, я хочу проверить, удовлетворяет ли формула x + y = z (x, y, z целые числа).Используя Z3, я мог бы ввести что-то вроде: 

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (= z (+ x y)))
(check-sat)

Я мог бы эквивалентно использовать API Ocaml и написать следующий код: 

let ctx=Z3.mk_context  [("model", "true"); ("proof", "false")] in 
let v1=(Z3.Arithmetic.Integer.mk_const_s ctx "x") in
let v2=(Z3.Arithmetic.Integer.mk_const_s ctx "y") in
let res=(Z3.Arithmetic.Integer.mk_const_s ctx "z") in
let sum=Z3.Arithmetic.mk_add ctx [ v1 ; v2] in 
let phi=Z3.Boolean.mk_eq ctx sum res in
let solver = (Z3.Solver.mk_solver ctx None) in
let _= Z3.Solver.add solver [phi] in
let is_sat=Z3.Solver.check solver [] in 
match is_sat with 
      | UNSATISFIABLE -> Printf.printf "unsat";
      | SATISFIABLE -> Printf.printf "sat";
      | UNKNOWN -> Printf.printf "unknown";

Я хотел бы использовать API ocaml z3 дляпроверьте выполнимость следующей факторной реализации, чтобы я получил значение для x (если оно существует). 

(declare-fun x () Int)
(define-fun-rec f ((x Int)) Int
                  (ite (> x 1)
                       (* (f (- x 1))
                            x)
                       1))
(assert (= x (f 10)))
(check-sat)
(get-model)

К сожалению, я не могу найти пример рекурсивных определений с использованием ml api z3.

...