simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 12:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fixed bug in smtlib translation

Browse source
This commit is contained in:
Guillaume Bury 2014-11-15 19:42:09 +01:00
parent 384bcb7270
commit c6dd201014
2 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
smt/smt.ml
View file

@ -52,7 +52,7 @@ module Fsmt = struct
let add_label _ _ = () let add_label _ _ = ()
let print fmt = function let print fmt = function
| Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") (abs i) | Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") ((abs i) / 2)
| Equal (a, b) -> Format.fprintf fmt "%s = %s" a b | Equal (a, b) -> Format.fprintf fmt "%s = %s" a b
| Distinct (a, b) -> Format.fprintf fmt "%s ≠ %s" a b | Distinct (a, b) -> Format.fprintf fmt "%s ≠ %s" a b

7
util/smtlib/smtlib.ml
View file

@ -46,9 +46,10 @@ let left_assoc s f = function
| x :: r -> List.fold_left f x r | x :: r -> List.fold_left f x r
| _ -> raise (Bad_arity s) | _ -> raise (Bad_arity s)
let right_assoc s f = function let rec right_assoc s f = function
| x :: r -> List.fold_right f r x | [] -> raise (Bad_arity s)
| _ -> raise (Bad_arity s) | [x] -> x
| x :: r -> f x (right_assoc s f r)
let translate_atom = function let translate_atom = function
| TermSpecConst(_, const) -> translate_const const | TermSpecConst(_, const) -> translate_const const