let rec pp_print_symbol_node ?arity ppf = function | `TRUE -> Format.pp_print_string ppf "true" | `FALSE -> Format.pp_print_string ppf "false" | `NOT -> Format.pp_print_string ppf "not" | `IMPLIES -> Format.pp_print_string ppf "=>" | `AND -> Format.pp_print_string ppf "and" | `OR -> Format.pp_print_string ppf "or" | `XOR -> Format.pp_print_string ppf "xor" | `EQ -> Format.pp_print_string ppf "=" | `DISTINCT -> failwith "distinct not implemented for yices" | `ITE -> Format.pp_print_string ppf "ite" | `NUMERAL i -> Numeral.pp_print_numeral ppf i | `DECIMAL f -> Decimal.pp_print_decimal ppf f (* | `BV b -> pp_yices_print_bitvector_b ppf b *) (* Special case for unary minus : print -a as (- 0 a) *) | `MINUS when arity = Some 1 -> Format.pp_print_string ppf "- 0" | `MINUS -> Format.pp_print_string ppf "-" | `PLUS -> Format.pp_print_string ppf "+" | `TIMES -> Format.pp_print_string ppf "*" | `DIV -> Format.pp_print_string ppf "/" | `INTDIV -> Format.pp_print_string ppf "div" | `MOD -> Format.pp_print_string ppf "mod" | `ABS -> failwith "abs not implemented for yices" | `LEQ -> Format.pp_print_string ppf "<=" | `LT -> Format.pp_print_string ppf "<" | `GEQ -> Format.pp_print_string ppf ">=" | `GT -> Format.pp_print_string ppf ">" | `TO_REAL -> Format.pp_print_string ppf "to_real" | `TO_INT -> Format.pp_print_string ppf "to_int" | `IS_INT -> failwith "is_int not implemented for yices" | `DIVISIBLE n -> failwith "divisible not implemented for yices" (* | `CONCAT -> Format.pp_print_string ppf "bv-concat" | `EXTRACT (i, j) -> Format.fprintf ppf "bv-extract %a %a" Numeral.pp_print_numeral j Numeral.pp_print_numeral i | `BVNOT -> Format.pp_print_string ppf "bv-not" | `BVNEG -> Format.pp_print_string ppf "bv-neg" | `BVAND -> Format.pp_print_string ppf "bv-and" | `BVOR -> Format.pp_print_string ppf "bv-or" | `BVADD -> Format.pp_print_string ppf "bv-add" | `BVMUL -> Format.pp_print_string ppf "bv-mul" | `BVDIV -> Format.pp_print_string ppf "bv-div" | `BVUREM -> Format.pp_print_string ppf "bvurem" | `BVSHL -> Format.pp_print_string ppf "bv-shift-left0" | `BVLSHR -> Format.pp_print_string ppf "bv-shift-right0" | `BVULT -> Format.pp_print_string ppf "bv-lt" *) | `SELECT _ -> Format.pp_print_string ppf "" | `STORE -> Format.pp_print_string ppf "update" | `UF u -> UfSymbol.pp_print_uf_symbol ppf u (* Pretty-print a hashconsed symbol *) and pp_print_symbol ?arity ppf s = pp_print_symbol_node ?arity ppf (Symbol.node_of_symbol s)