Imandra encoding of UBS dark pool (Form ATS)

In this notebook, we model the order priority logic of the UBS ATS dark pool as described in UBS's June 1st 2015 Form ATS submission to the SEC and analyse it using Imandra.

We observe that as described, the order priority logic suffers from a fundamental flaw: the order ranking function is not transitive.

This type of subtle issue in matching logic strongly motivates the use of formal, machine reasonable disclosures.

Some relevant references:

UBS Future of Finance Challenge - First Place Winner

This analysis was part of Aesthetic Integration's entry in the 2015 UBS Future of Finance Challenge, for which we won first place (out of 620 companies from 52 countries!). This analysis is based purely on publicly available documents, and is based on our interpretation of the English prose written in the Form ATS.

An Imandra Formal Model of UBS ATS Order Priority Logic

We begin our model by defining a record type corresponding to the current NBB/O and relevant market data signals.

In [1]:
type mkt_data = {
  nbb : real;
  nbo : real;
  l_up : real;
  l_down : real;
}
Out[1]:
type mkt_data = { nbb : real; nbo : real; l_up : real; l_down : real; }

Let us now introduce some useful functions on mkt_data.

In [2]:
type mkt_cond = MKT_NORMAL | MKT_CROSSED | MKT_LOCKED

let which_mkt mkt =
  if mkt.nbo = mkt.nbb then MKT_LOCKED
  else if mkt.nbo <. mkt.nbb then MKT_CROSSED
  else MKT_NORMAL

let mid_point mkt = (mkt.nbb +. mkt.nbo) /. 2.0
Out[2]:
type mkt_cond = MKT_NORMAL | MKT_CROSSED | MKT_LOCKED
val which_mkt : mkt_data -> mkt_cond = <fun>
val mid_point : mkt_data -> real = <fun>

Because our model is executable, we can compute with various mkt_data values:

In [3]:
{nbb=42.11; nbo=42.10; l_up=3. ; l_down= 2.5}
Out[3]:
- : mkt_data = {nbb = 4211/100; nbo = 421/10; l_up = 3; l_down = 5/2}
In [4]:
which_mkt {nbb=42.11; nbo=42.10; l_up=3. ; l_down= 2.5}
Out[4]:
- : mkt_cond = MKT_CROSSED

Aside: Custom Document Printers

Imandra has a powerful structured document system for making custom views and interfaces for your algorithm analysis tasks.

To make our Imandra notebooks and analysis toolchains user-friendly, we can define and install our own custom Imandra document printer that will render our market data type in a table in our notebook.

For example, we can define a simple table-based document printer for our mkt_data type as follows.

We use the [@@program] attribute on our pretty-printer definition, to tell Imandra to only define this function in #program mode (not in #logic mode, i.e., not within our formal logic). Arbitrary OCaml functions can be defined in #program mode, the basis for much custom Imandra interfaces and proof automation:

In [5]:
let doc_of_mkt_data m =
  let module D = Document in
  D.indent "mkt_data" @@ D.record [
           "nbb", D.s @@ Real.to_string_approx m.nbb;
           "nbo", D.s @@ Real.to_string_approx m.nbo;
           "l_up", D.s @@ Real.to_string_approx m.l_up;
           "l_down", D.s @@ Real.to_string_approx m.l_down;
  ]
[@@program]

#install_doc doc_of_mkt_data
Out[5]:
val doc_of_mkt_data : mkt_data -> Document.t = <fun>

If we view the same mkt_data value as above, we'll now see it rendered with our custom pretty-printer:

In [6]:
{nbb=42.11; nbo=42.10; l_up=3. ; l_down= 2.5}
Out[6]:
- : mkt_data = <document>

mkt_data

nbb42.11
nbo42.1
l_up3.
l_down2.5

Time, Price and Static Data

We now define some types and functions for representing time, price and static_data. We use int for time and real for price, as it is sufficient for this analysis, but custom types (e.g., decs with price bands) can be easily defined.

In [7]:
type time = int
Out[7]:
type time = int
In [8]:
type price = real
Out[8]:
type price = real
In [9]:
type static_data = { round_lot : int;
                     tick_size : float }
Out[9]:
type static_data = { round_lot : time; tick_size : float; }

Order types

We now define the order types supported by the dark pool.

Section 2 of the Form ATS defines the order types as follows:

Order Types:

  • Pegged Orders (both Resident and IOC TimeInForce).
    Pegging can be to the near, midpoint, or far
    side of the NBBO. Pegged Orders may have a limit price.
  • Limit Orders (both Resident and IOC TimeInForce)
  • Market Orders (both Resident and IOC TimeInForce)

Conditional Indication Types:

  • Pegged Conditional Indications (Resident T)
  • Limit Conditional Indications (Resident TimeInForce only)
In [10]:
type order_side = BUY | SELL | SELL_SHORT

type order_peg = NEAR | MID | FAR | NO_PEG

type order_type =
    MARKET
  | LIMIT
  | PEGGED
  | PEGGED_CI
  | LIMIT_CI
  | FIRM_UP_PEGGED
  | FIRM_UP_LIMIT
Out[10]:
type order_side = BUY | SELL | SELL_SHORT
type order_peg = NEAR | MID | FAR | NO_PEG
type order_type =
    MARKET
  | LIMIT
  | PEGGED
  | PEGGED_CI
  | LIMIT_CI
  | FIRM_UP_PEGGED
  | FIRM_UP_LIMIT

Source Categories are defined in the Form ATS as follows:

  • Source Category 1: Retail orders routed by broker - dealer clients of the UBS Retail Market Making business.
  • Source Category 2: Certain orders received from UBS algorithms, where the underlying client is an institutional client of UBS.
  • Source Category 3: Orders received from Order Originators that are determined by UBS to exhibit lowto - neutral reversion.
  • Source Category 4: All other orders not originating from Source Categories 1, 2 or 3.
In [11]:
type order_attr = RESIDENT | IOC

type category = C_ONE | C_TWO | C_THREE | C_FOUR
Out[11]:
type order_attr = RESIDENT | IOC
type category = C_ONE | C_TWO | C_THREE | C_FOUR

Capacity, Eligibilities and Crossing Restrictions

In [12]:
type capacity = Principal | Agency

(* ID of the order source *)

type order_source = int

(* UBS's ID in the model *)

let ubs_id = 12

(* Category crossing constraints *)

type category_elig = {
  c_one_elig : bool;
  c_two_elig : bool;
  c_three_elig : bool;
  c_four_elig : bool;
}

let default_cat_elig = {
  c_one_elig = true;
  c_two_elig = true;
  c_three_elig = true;
  c_four_elig = true;
}

(* Type for crossing restrictions *)

type cross_restrict = {
  cr_self_cross : bool;
  cr_ubs_principal : bool;
  cr_round_lot_only : bool;
  cr_no_locked_nbbo : bool;
  cr_pegged_mid_point_mode : int;

  (* From the examples, we understand that: 0 - no constraint 1 - mid      *)
  (* constraint 2 - limit constraint                                       *)

  cr_enable_conditionals : bool;
  cr_min_qty : bool;
  cr_cat_elig : category_elig;
}

let default_cross_restrict = {
  cr_self_cross = false;
  cr_ubs_principal = false;
  cr_round_lot_only = false;
  cr_no_locked_nbbo = false;
  cr_pegged_mid_point_mode = 0;
  cr_enable_conditionals = false;
  cr_min_qty = false;
  cr_cat_elig = default_cat_elig;
}
Out[12]:
type capacity = Principal | Agency
type order_source = time
val ubs_id : order_source = 12
type category_elig = {
  c_one_elig : bool;
  c_two_elig : bool;
  c_three_elig : bool;
  c_four_elig : bool;
}
val default_cat_elig : category_elig =
  {c_one_elig = true; c_two_elig = true; c_three_elig = true;
   c_four_elig = true}
type cross_restrict = {
  cr_self_cross : bool;
  cr_ubs_principal : bool;
  cr_round_lot_only : bool;
  cr_no_locked_nbbo : bool;
  cr_pegged_mid_point_mode : order_source;
  cr_enable_conditionals : bool;
  cr_min_qty : bool;
  cr_cat_elig : category_elig;
}
val default_cross_restrict : cross_restrict =
  {cr_self_cross = false; cr_ubs_principal = false;
   cr_round_lot_only = false; cr_no_locked_nbbo = false;
   cr_pegged_mid_point_mode = 0; cr_enable_conditionals = false;
   cr_min_qty = false;
   cr_cat_elig =
    {c_one_elig = true; c_two_elig = true; c_three_elig = true;
     c_four_elig = true}}

Orders

We now define the type order, representing all data associated with a given order.

In [13]:
(* Note: there's both the quantity of the order and the current filled quantity. *)

type order =
    { id : int;                        (* Order ID *)
      peg : order_peg;                 (* Near, Mid, Far or NoPeg *)
      client_id : int;                 (* Client ID *)
      order_type : order_type;         (* Market, Limit or Pegged order + Conditional Indications *)
      qty : int;                       (* Original quantity of the order (updated after cancel/replace) *)
      min_qty : int;                   (* Minimum acceptible quantity to trade *)
      leaves_qty : int;                (* Remaining quantity of the order *)
      price : price;                   (* Limit price (Not used if the order *)
      time : time;                     (* time of order entry (reset on update)) *)
      src : order_source;              (* ID of the order source *)
      order_attr : order_attr;         (* Resident or Immediate Or Cancel (IOC) *)
      capacity : capacity;             (* Principal or agency *)
      category : category;             (* Client category *)
      cross_restrict : cross_restrict; (* Crossing restrictions *)
      locate_found : bool;             (* A sell-short order without a locate would be rejected *)
      expiry_time : int;               (* When will the order expire? *)
    }
Out[13]:
type order = {
  id : order_source;
  peg : order_peg;
  client_id : order_source;
  order_type : order_type;
  qty : order_source;
  min_qty : order_source;
  leaves_qty : order_source;
  price : price;
  time : order_source;
  src : order_source;
  order_attr : order_attr;
  capacity : capacity;
  category : category;
  cross_restrict : cross_restrict;
  locate_found : bool;
  expiry_time : order_source;
}

Determining how much and at what price two orders may trade

In [14]:
(** Uses two orders' timestamps to determin the older price of the two *)
let older_price (o1, o2) =
  if o1.time > o2.time then o2.price else o1.price

type fill_price =
  | Known of price
  | Unknown
  | TOP of price

(* Functions for categorisations  *)

let cat_priority (o1, o2) =
  if o1.category = C_ONE then false
  else if o1.category = C_TWO &&
            (o2.category = C_THREE || o2.category = C_FOUR)
  then false
  else if o1.category = C_THREE && (o2.category = C_FOUR) then false
  else true

let eff_min_qty (o) = min o.min_qty o.leaves_qty

let effective_size (o, should_round, round_lot) =
  if should_round = true then
    ( if round_lot > 0 then ( (o.leaves_qty / round_lot) * round_lot )
      else o.leaves_qty )
  else
    o.leaves_qty

(* The pricing functions *)

let lessAggressive (side, lim_price, far_price) =
  if lim_price <. 0.0 then far_price else
    (if side = BUY then Real.min lim_price far_price
     else Real.max lim_price far_price)

(** This function is used to calculate the priority price *)
let priority_price (side, o, mkt) =
  let calc_pegged_price =
    ( match o.peg with
      | FAR -> lessAggressive(side, o.price,
                              (if side = BUY then mkt.nbo else mkt.nbb))
      | MID -> lessAggressive(side, o.price, (mid_point mkt))
      | NEAR -> lessAggressive(side, o.price,
                               (if side = BUY then mkt.nbb else mkt.nbo))
      | NO_PEG -> o.price )
  in
  let calc_nbbo_capped_limit =
    ( if side = BUY then lessAggressive (BUY, o.price, mkt.nbo)
      else lessAggressive (SELL, o.price, mkt.nbb ) )
  in
  match o.order_type with
  | LIMIT -> calc_nbbo_capped_limit
  | MARKET -> if side = BUY then mkt.nbo else mkt.nbb
  | PEGGED -> calc_pegged_price
  | PEGGED_CI -> calc_pegged_price
  | LIMIT_CI -> calc_nbbo_capped_limit
  | FIRM_UP_PEGGED -> calc_pegged_price
  | FIRM_UP_LIMIT -> calc_nbbo_capped_limit

(** This is used to calculate the actual price at which the order would trade   *)
let exec_price (side, o, mkt) =
  priority_price (side, o, mkt)
Out[14]:
val older_price : order * order -> price = <fun>
type fill_price = Known of price | Unknown | TOP of price
val cat_priority : order * order -> bool = <fun>
val eff_min_qty : order -> order_source = <fun>
val effective_size : order * bool * order_source -> order_source = <fun>
val lessAggressive : order_side * price * price -> price = <fun>
val priority_price : order_side * order * mkt_data -> price = <fun>
val exec_price : order_side * order * mkt_data -> price = <fun>

Crossing Restrictions

The UBS ATS allows all Order Originators to use the following optional crossing restrictions, on a per - order or configured basis:

  • No Self Cross: To prevent crossing against 'own orders' (orders sent with the same client ID).
  • No UBS Principal: To prevent crossing against UBS BD Principal Orders, or UBS affiliate Principal orders.
  • Round Lot Only: To prevent crossing in other than round lot orders.
  • No Locked: To prevent crossing on a pegged order when the NBBO is locked. (Bid = Offer)
  • PeggedMidPointMode: To prevent a Mid - point Pegged Order from being executed at its limit price if (i) in the case of a buy order, its limit price is less than the mid - point of the spread between the NBB and NBO and (ii) in the case of a sell order, its limit price is greater than the mid - point of the spread between the NBB and NBO. In the event this restriction is not elected, a Mid - Point Pegged Order with a specified limit price may be executed at the limit price even if the price is not equal to the mid - point of the spread between the NBB and the NBBO.
  • Enable Conditionals: To enable a Resident Order to interact with Conditional Indicators.
  • Minimum Quantity: Orders may be routed to the UBS ATS with a minimum quantity value specified. UBS ATS will only cross where at least this number of shares is available from a single eligible contra side order.
In [15]:
(* Note that these are order-level constraints. There are members of this  *)
(* structure, like cr_min_qty and cr_round_lot_only that are used in       *)
(* calculating the effective minimum price.                                *)

let get_cat_eligibility (cat_elig, c) =
  match c with
  | C_ONE -> cat_elig.c_one_elig
  | C_TWO -> cat_elig.c_two_elig
  | C_THREE -> cat_elig.c_three_elig
  | C_FOUR -> cat_elig.c_four_elig

let can_orders_cross (o1, o2) =
  let o1_cr = o1.cross_restrict in
  let o2_cr = o2.cross_restrict in
  if (o1_cr.cr_self_cross || o2_cr.cr_self_cross) && (o1.client_id = o2.client_id)
  then false
  else if (o1_cr.cr_ubs_principal || o2_cr.cr_ubs_principal) &&
            (o1.client_id = ubs_id || o2.client_id = ubs_id) then false
  else if (o1_cr.cr_enable_conditionals || o2_cr.cr_enable_conditionals) &&
            (o1.order_type = LIMIT_CI || o1.order_type = PEGGED_CI) then false
  else true
Out[15]:
val get_cat_eligibility : category_elig * category -> bool = <fun>
val can_orders_cross : order * order -> bool = <fun>

Order Book

The Order Book is used to match buy orders against sell orders.

In [16]:
type order_book = {
  buys  : order list;
  sells : order list;
}

let empty_book = { buys = []; sells = [] }

type fill = { order_buy : order;
              order_sell : order;
              fill_qty : int;
              fill_price : fill_price;
              fill_time : time;
            }
Out[16]:
type order_book = { buys : order list; sells : order list; }
val empty_book : order_book = {buys = []; sells = []}
type fill = {
  order_buy : order;
  order_sell : order;
  fill_qty : order_source;
  fill_price : fill_price;
  fill_time : order_source;
}

Ranking functions for orders

From Section 4.1 of UBS's June, 2015 Form ATS:

Eligible Resident Orders and IOC Orders are given priority
based first on price and second on the time of their receipt by the UBS ATS.
Eligibility is determined based on the crossing restrictions associated with
the orders on both sides of the potential cross.

Invites are sent to the Order Originators of Conditional Indications on a
priority based first on price, second on the quantity and third on the time of
receipt by UBS ATS. For orders with the same price and time, priority is given
to Resident and IOC Orders over Conditional Indications.

All marketable limit orders (i.e., buy orders with limit prices at or above the
NBO or sell orders with limit prices at or below the NBB) will be treated as
though they are at equivalent prices for priority purposes. As such, they will
be handled based strictly on time priority, as if they were market orders. If a
marketable limit order becomes non - marketable before execution, it will be treated
as a limit order and will receive price / time priority, with time based upon the
original time of receipt of the order by the UBS ATS.

Let us formalise this logic below.

In [17]:
let non_ci (ot) = not(ot = PEGGED_CI || ot = LIMIT_CI);;

let order_higher_ranked (side, o1, o2, mkt) =
  let ot1 = o1.order_type in
  let ot2 = o2.order_type in

  let p_price1 = priority_price (side, o1, mkt) in
  let p_price2 = priority_price (side, o2, mkt) in

  let wins_price = (
    if side = BUY then
      ( if p_price1 >. p_price2 then 1
        else if p_price1 = p_price2 then 0
        else -1)
    else
      ( if p_price1 <. p_price2 then 1
        else if p_price1 = p_price2 then 0
        else -1) ) in

  let wins_time = (
    if o1.time < o2.time then 1
    else if o1.time = o2.time then 0
    else -1
  ) in

  (* Note that the CI priority is price, quantity and then time *)
  if wins_price = 1 then true
  else if wins_price = -1 then false
  else (
    (* Same price level - first check to see whether we're comparing two   *)
    (* CI orders here                                                      *)
    if not (non_ci (ot1)) && not (non_ci (ot2)) then
      o1.leaves_qty > o2.leaves_qty
    else ( if wins_time = 1 then true
           else if wins_time = -1 then false
           else (
             if non_ci(ot1) then true
             else if (not(non_ci(ot1)) && non_ci(ot2)) then false
             else
               o1.leaves_qty > o2.leaves_qty)
         )
  )
Out[17]:
val non_ci : order_type -> bool = <fun>
val order_higher_ranked : order_side * order * order * mkt_data -> bool =
  <fun>

The property we're interested in is whether this ranking predicate is transitive (a necessary condition for being a proper ordering relation that can be used for sorting, e.g., orders in the book):

In [18]:
let rank_transitivity side o1 o2 o3 mkt =
    order_higher_ranked(side,o1,o2,mkt) &&
    order_higher_ranked(side,o2,o3,mkt)
    ==>
    order_higher_ranked(side,o1,o3,mkt)
Out[18]:
val rank_transitivity :
  order_side -> order -> order -> order -> mkt_data -> bool = <fun>

Now we can check whether this property of being transitive holds:

In [19]:
verify (fun side o1 o2 o3 mkt -> rank_transitivity side o1 o2 o3 mkt)
Out[19]:
- : order_side -> order -> order -> order -> mkt_data -> bool = <fun>
module CX :
  sig
    val side : order_side
    val o1 : order
    val o2 : order
    val o3 : order
    val mkt : mkt_data
  end
Counterexample (after 0 steps, 0.070s):
 let (side : order_side) = SELL
 let (o1 : order) =
  {id = 11; peg = MID; client_id = 12; order_type = FIRM_UP_PEGGED; qty = 13;
   min_qty = 14; leaves_qty = 20163; price = (Real.mk_of_string "91653/2");
   time = 1; src = 15; order_attr = RESIDENT; capacity = Principal;
   category = C_ONE;
   cross_restrict =
    {cr_self_cross = false; cr_ubs_principal = false;
     cr_round_lot_only = false; cr_no_locked_nbbo = false;
     cr_pegged_mid_point_mode = 10; cr_enable_conditionals = false;
     cr_min_qty = false;
     cr_cat_elig =
      {c_one_elig = false; c_two_elig = false; c_three_elig = false;
       c_four_elig = false}};
   locate_found = false; expiry_time = 16}
 let (o2 : order) =
  {id = 19; peg = NEAR; client_id = 20; order_type = PEGGED_CI; qty = 21;
   min_qty = 22; leaves_qty = 20162; price = (Real.mk_of_string "91653/2");
   time = 2; src = 23; order_attr = RESIDENT; capacity = Principal;
   category = C_ONE;
   cross_restrict =
    {cr_self_cross = false; cr_ubs_principal = false;
     cr_round_lot_only = false; cr_no_locked_nbbo = false;
     cr_pegged_mid_point_mode = 18; cr_enable_conditionals = false;
     cr_min_qty = false;
     cr_cat_elig =
      {c_one_elig = false; c_two_elig = false; c_three_elig = false;
       c_four_elig = false}};
   locate_found = false; expiry_time = 24}
 let (o3 : order) =
  {id = 4; peg = MID; client_id = 5; order_type = LIMIT_CI; qty = 6;
   min_qty = 7; leaves_qty = 20161; price = (Real.mk_of_string "91653/2");
   time = 0; src = 8; order_attr = RESIDENT; capacity = Principal;
   category = C_ONE;
   cross_restrict =
    {cr_self_cross = false; cr_ubs_principal = false;
     cr_round_lot_only = false; cr_no_locked_nbbo = false;
     cr_pegged_mid_point_mode = 3; cr_enable_conditionals = false;
     cr_min_qty = false;
     cr_cat_elig =
      {c_one_elig = false; c_two_elig = false; c_three_elig = false;
       c_four_elig = false}};
   locate_found = false; expiry_time = 9}
 let (mkt : mkt_data) =
  {nbb = 45826.0; nbo = (Real.mk_of_string "183305/4"); l_up = 2.0;
   l_down = 3.0}
Refuted
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.070s
details
Expand
smt_stats
num checks1
arith-assume-eqs7
arith-make-feasible210
arith-max-columns60
arith-conflicts8
rlimit count79077
arith-cheap-eqs239
mk clause868
datatype occurs check63
mk bool var1175
arith-lower239
arith-diseq185
datatype splits199
decisions2701
arith-propagations75
propagations3280
interface eqs6
arith-bound-propagations-cheap75
arith-max-rows39
conflicts70
datatype accessor ax138
minimized lits9
arith-bound-propagations-lp54
datatype constructor ax439
num allocs4901122
final checks8
added eqs3846
del clause210
arith eq adapter104
arith-upper195
time0.047000
memory11.690000
max memory12.860000
Expand
  • start[0.070s]
      let (_x_0 : int) = ( :var_1: ).time in
      let (_x_1 : int) = ( :var_2: ).time in
      let (_x_2 : int) = ( :var_1: ).leaves_qty in
      let (_x_3 : int) = ( :var_2: ).leaves_qty in
      let (_x_4 : order_type) = ( :var_1: ).order_type in
      let (_x_5 : bool) = _x_4 = PEGGED_CI || _x_4 = LIMIT_CI in
      let (_x_6 : order_type) = ( :var_2: ).order_type in
      let (_x_7 : bool) = _x_6 = PEGGED_CI || _x_6 = LIMIT_CI in
      let (_x_8 : order_type) = ….order_type in
      let (_x_9 : bool) = Is_a(LIMIT, _x_8) in
      let (_x_10 : real) = if ….0 = BUY then … else … in
      let (_x_11 : bool) = Is_a(MARKET, _x_8) in
      let (_x_12 : order_type) = ….1.order_type in
      let (_x_13 : bool) = Is_a(LIMIT, _x_12) in
      let (_x_14 : bool) = ….0 = BUY in
      let (_x_15 : real) = if _x_14 then ….nbo else ….nbb in
      let (_x_16 : bool) = Is_a(MARKET, _x_12) in
      let (_x_17 : int)
          = if (if _x_11 then _x_10 else if _x_9 then … else …) =
               (if _x_16 then _x_15 else if _x_13 then … else …)
            then 0 else -1
      in
      let (_x_18 : order_type) = ….1.order_type in
      let (_x_19 : bool) = Is_a(PEGGED, _x_18) in
      let (_x_20 : bool) = ….0 = BUY in
      let (_x_21 : bool) = Is_a(LIMIT, _x_18) in
      let (_x_22 : real) = if _x_20 then ….nbo else ….nbb in
      let (_x_23 : bool) = Is_a(MARKET, _x_18) in
      let (_x_24 : int)
          = if (if _x_23 then _x_22
                else
                if _x_21 then if _x_20 then … else …
                else if _x_19 then … else …)
               <.
               (if _x_16 then _x_15
                else
                if _x_13 then if _x_14 then … else …
                else if Is_a(PEGGED, _x_12) then … else …)
            then 1 else _x_17
      in
      let (_x_25 : bool) = ( :var_0: ) = BUY in
      let (_x_26 : order_type) = ….1.order_type in
      let (_x_27 : bool) = Is_a(LIMIT, _x_26) in
      let (_x_28 : bool) = ….0 = BUY in
      let (_x_29 : real) = if _x_28 then ….nbo else ….nbb in
      let (_x_30 : bool) = Is_a(MARKET, _x_26) in
      let (_x_31 : int) = ( :var_4: ).time in
      let (_x_32 : int) = ( :var_4: ).leaves_qty in
      let (_x_33 : order_type) = ( :var_4: ).order_type in
      let (_x_34 : bool) = _x_33 = PEGGED_CI || _x_33 = LIMIT_CI in
      let (_x_35 : order_type) = ….1.order_type in
      let (_x_36 : bool) = Is_a(LIMIT, _x_35) in
      let (_x_37 : bool) = ….0 = BUY in
      let (_x_38 : real) = if _x_37 then ….nbo else ….nbb in
      let (_x_39 : bool) = Is_a(MARKET, _x_35) in
      let (_x_40 : order_type) = ….1.order_type in
      let (_x_41 : bool) = Is_a(LIMIT, _x_40) in
      let (_x_42 : bool) = ….0 = BUY in
      let (_x_43 : real) = if _x_42 then ….nbo else ….nbb in
      let (_x_44 : bool) = Is_a(MARKET, _x_40) in
      let (_x_45 : int)
          = if (if _x_39 then _x_38 else if _x_36 then … else …) =
               (if _x_44 then _x_43 else if _x_41 then … else …)
            then 0 else -1
      in
      let (_x_46 : bool) = Is_a(PEGGED, _x_35) in
      let (_x_47 : bool) = Is_a(PEGGED, _x_40) in
      let (_x_48 : int)
          = if _x_25
            then
              if (if _x_39 then _x_38
                  else
                  if _x_36 then if _x_37 then … else …
                  else if _x_46 then … else …)
                 >.
                 (if _x_44 then _x_43
                  else
                  if _x_41 then if _x_42 then … else …
                  else if _x_47 then … else …)
              then 1 else _x_45
            else
            if (if _x_39 then _x_38
                else
                if _x_36 then if _x_37 then … else …
                else if _x_46 then … else …)
               <.
               (if _x_44 then _x_43
                else
                if _x_41 then if _x_42 then … else …
                else if _x_47 then … else …)
            then 1 else _x_45
      in
      let (_x_49 : order_type) = ….1.order_type in
      let (_x_50 : bool) = Is_a(LIMIT, _x_49) in
      let (_x_51 : bool) = ….0 = BUY in
      let (_x_52 : real) = if _x_51 then ….nbo else ….nbb in
      let (_x_53 : bool) = Is_a(MARKET, _x_49) in
      let (_x_54 : order_type) = ….1.order_type in
      let (_x_55 : bool) = Is_a(LIMIT, _x_54) in
      let (_x_56 : bool) = ….0 = BUY in
      let (_x_57 : real) = if _x_56 then ….nbo else ….nbb in
      let (_x_58 : bool) = Is_a(MARKET, _x_54) in
      let (_x_59 : int)
          = if (if _x_53 then _x_52 else if _x_50 then … else …) =
               (if _x_58 then _x_57 else if _x_55 then … else …)
            then 0 else -1
      in
      let (_x_60 : bool) = Is_a(PEGGED, _x_49) in
      let (_x_61 : bool) = Is_a(PEGGED, _x_54) in
      let (_x_62 : int)
          = if _x_25
            then
              if (if _x_53 then _x_52
                  else
                  if _x_50 then if _x_51 then … else …
                  else if _x_60 then … else …)
                 >.
                 (if _x_58 then _x_57
                  else
                  if _x_55 then if _x_56 then … else …
                  else if _x_61 then … else …)
              then 1 else _x_59
            else
            if (if _x_53 then _x_52
                else
                if _x_50 then if _x_51 then … else …
                else if _x_60 then … else …)
               <.
               (if _x_58 then _x_57
                else
                if _x_55 then if _x_56 then … else …
                else if _x_61 then … else …)
            then 1 else _x_59
      in
      (if (if _x_25
           then
             if (if _x_23 then _x_22
                 else
                 if _x_21 then if _x_20 then … else …
                 else if _x_19 then … else …)
                >.
                (if _x_30 then _x_29
                 else
                 if _x_27 then if _x_28 then … else …
                 else if Is_a(PEGGED, _x_26) then … else …)
             then 1
             else
             if (if _x_23 then _x_22 else if _x_21 then … else …) =
                (if _x_30 then _x_29 else if _x_27 then … else …)
             then 0 else -1
           else _x_24)
          = 1
       then true
       else
       if (if _x_25
           then
             if (if _x_11 then _x_10 else if _x_9 then … else …) >.
                (if _x_16 then _x_15 else if _x_13 then … else …)
             then 1 else _x_17
           else _x_24)
          = -1
       then false
       else
       if _x_5 && _x_7 then _x_2 > _x_3
       else if (if _x_0 < _x_1 then 1 else …) = 1 then true else …)
      && (if _x_48 = 1 then true
          else
          if _x_48 = -1 then false
          else
          if _x_7 && _x_34 then _x_3 > _x_32
          else if (if _x_1 < _x_31 then 1 else …) = 1 then true else …)
      ==> (if _x_62 = 1 then true
           else
           if _x_62 = -1 then false
           else
           if _x_5 && _x_34 then _x_2 > _x_32
           else if (if _x_0 < _x_31 then 1 else …) = 1 then true else …)
  • simplify

    into
    let (_x_0 : order_type) = ( :var_1: ).order_type in
    let (_x_1 : bool) = Is_a(LIMIT, _x_0) in
    let (_x_2 : bool) = ( :var_0: ) = BUY in
    let (_x_3 : real) = if _x_2 then ( :var_3: ).nbo else ( :var_3: ).nbb in
    let (_x_4 : bool) = Is_a(MARKET, _x_0) in
    let (_x_5 : order_type) = ( :var_4: ).order_type in
    let (_x_6 : bool) = Is_a(LIMIT, _x_5) in
    let (_x_7 : bool) = Is_a(MARKET, _x_5) in
    let (_x_8 : int)
        = if (if _x_4 then _x_3 else if _x_1 then … else …) =
             (if _x_7 then _x_3 else if _x_6 then … else …)
          then 0 else -1
    in
    let (_x_9 : bool) = Is_a(PEGGED, _x_5) || Is_a(PEGGED_CI, _x_5) in
    let (_x_10 : bool) = Is_a(PEGGED, _x_0) || Is_a(PEGGED_CI, _x_0) in
    let (_x_11 : int)
        = if _x_2
          then
            if (if _x_4 then _x_3
                else
                if _x_1 then if _x_2 then … else …
                else if _x_10 then … else …)
               <=.
               (if _x_7 then _x_3
                else
                if _x_6 then if _x_2 then … else …
                else if _x_9 then … else …)
            then _x_8 else 1
          else
          if (if _x_7 then _x_3
              else
              if _x_6 then if _x_2 then … else …
              else if _x_9 then … else …)
             <=.
             (if _x_4 then _x_3
              else
              if _x_1 then if _x_2 then … else …
              else if _x_10 then … else …)
          then _x_8 else 1
    in
    let (_x_12 : int) = ( :var_4: ).time in
    let (_x_13 : int) = ( :var_1: ).time in
    let (_x_14 : bool) = _x_12 <= _x_13 in
    let (_x_15 : bool) = _x_0 = LIMIT_CI || _x_0 = PEGGED_CI in
    let (_x_16 : bool) = not _x_15 in
    let (_x_17 : bool) = _x_5 = PEGGED_CI || _x_5 = LIMIT_CI in
    let (_x_18 : bool) = not _x_17 in
    let (_x_19 : int) = ( :var_1: ).leaves_qty in
    let (_x_20 : int) = ( :var_4: ).leaves_qty in
    let (_x_21 : bool) = not (_x_19 <= _x_20) in
    let (_x_22 : order_type) = ( :var_2: ).order_type in
    let (_x_23 : bool) = Is_a(LIMIT, _x_22) in
    let (_x_24 : bool) = Is_a(MARKET, _x_22) in
    let (_x_25 : int)
        = if (if _x_4 then _x_3 else if _x_1 then … else …) =
             (if _x_24 then _x_3 else if _x_23 then … else …)
          then 0 else -1
    in
    let (_x_26 : bool) = Is_a(PEGGED, _x_22) || Is_a(PEGGED_CI, _x_22) in
    let (_x_27 : int)
        = if _x_2
          then
            if (if _x_4 then _x_3
                else
                if _x_1 then if _x_2 then … else …
                else if _x_10 then … else …)
               <=.
               (if _x_24 then _x_3
                else
                if _x_23 then if _x_2 then … else …
                else if _x_26 then … else …)
            then _x_25 else 1
          else
          if (if _x_24 then _x_3
              else
              if _x_23 then if _x_2 then … else …
              else if _x_26 then … else …)
             <=.
             (if _x_4 then _x_3
              else
              if _x_1 then if _x_2 then … else …
              else if _x_10 then … else …)
          then _x_25 else 1
    in
    let (_x_28 : int) = ( :var_2: ).time in
    let (_x_29 : bool) = _x_28 <= _x_13 in
    let (_x_30 : bool) = _x_22 = LIMIT_CI || _x_22 = PEGGED_CI in
    let (_x_31 : bool) = not _x_30 in
    let (_x_32 : int) = ( :var_2: ).leaves_qty in
    let (_x_33 : bool) = not (_x_19 <= _x_32) in
    let (_x_34 : int)
        = if (if _x_24 then _x_3 else if _x_23 then … else …) =
             (if _x_7 then _x_3 else if _x_6 then … else …)
          then 0 else -1
    in
    let (_x_35 : int)
        = if (if _x_24 then _x_3 else if _x_23 then … else …) =
             (if _x_7 then _x_3 else if _x_6 then … else …)
          then 0 else -1
    in
    let (_x_36 : bool) = _x_12 <= _x_28 in
    let (_x_37 : bool) = not (_x_32 <= _x_20) in
    (_x_11 = 1
     || not (_x_11 = -1)
        && (if _x_15 && _x_17 then _x_21
            else
              (not _x_14
               || not (_x_14 && not (_x_13 = _x_12))
                  && (_x_16 || not (_x_15 && _x_18) && _x_21))))
    || not
       ((_x_27 = 1
         || not (_x_27 = -1)
            && (if _x_15 && _x_30 then _x_33
                else
                  (not _x_29
                   || not (_x_29 && not (_x_13 = _x_28))
                      && (_x_16 || not (_x_15 && _x_31) && _x_33))))
        && ((if _x_2
             then
               if (if _x_24 then _x_3
                   else
                   if _x_23 then if _x_2 then … else …
                   else if _x_26 then … else …)
                  <=.
                  (if _x_7 then _x_3
                   else
                   if _x_6 then if _x_2 then … else …
                   else if _x_9 then … else …)
               then _x_34 else 1
             else
             if (if _x_7 then _x_3
                 else
                 if _x_6 then if _x_2 then … else …
                 else if _x_9 then … else …)
                <=.
                (if _x_24 then _x_3
                 else
                 if _x_23 then if _x_2 then … else …
                 else if _x_26 then … else …)
             then _x_34 else 1)
            = 1
            || not
               ((if _x_2
                 then
                   if (if _x_24 then _x_3
                       else
                       if _x_23 then if _x_2 then … else …
                       else if _x_26 then … else …)
                      <=.
                      (if _x_7 then _x_3
                       else
                       if _x_6 then if _x_2 then … else …
                       else if _x_9 then … else …)
                   then _x_35 else 1
                 else
                 if (if _x_7 then _x_3
                     else
                     if _x_6 then if _x_2 then … else …
                     else if _x_9 then … else …)
                    <=.
                    (if _x_24 then _x_3
                     else
                     if _x_23 then if _x_2 then … else …
                     else if _x_26 then … else …)
                 then _x_35 else 1)
                = -1)
               && (if _x_30 && _x_17 then _x_37
                   else
                     (not _x_36
                      || not (_x_36 && not (_x_28 = _x_12))
                         && (_x_31 || not (_x_30 && _x_18) && _x_37)))))
    expansions
    []
    rewrite_steps
      forward_chaining
      • Sat (Some let (side : order_side) = SELL let (o1 : order) = {id = 11; peg = MID; client_id = 12; order_type = FIRM_UP_PEGGED; qty = 13; min_qty = 14; leaves_qty = 20163; price = (Real.mk_of_string "91653/2"); time = 1; src = 15; order_attr = RESIDENT; capacity = Principal; category = C_ONE; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 10; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 16} let (o2 : order) = {id = 19; peg = NEAR; client_id = 20; order_type = PEGGED_CI; qty = 21; min_qty = 22; leaves_qty = 20162; price = (Real.mk_of_string "91653/2"); time = 2; src = 23; order_attr = RESIDENT; capacity = Principal; category = C_ONE; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 18; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 24} let (o3 : order) = {id = 4; peg = MID; client_id = 5; order_type = LIMIT_CI; qty = 6; min_qty = 7; leaves_qty = 20161; price = (Real.mk_of_string "91653/2"); time = 0; src = 8; order_attr = RESIDENT; capacity = Principal; category = C_ONE; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 3; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 9} let (mkt : mkt_data) = {nbb = 45826.0; nbo = (Real.mk_of_string "183305/4"); l_up = 2.0; l_down = 3.0} )

      We just showed that the ranking function is not transitive! As always, the components of the counterexample are automatically reflected into a module called CX and can be computed with, just as any other value in our runtime:

      In [20]:
      CX.o1
      
      Out[20]:
      - : order =
      {id = 11; peg = MID; client_id = 12; order_type = FIRM_UP_PEGGED; qty = 13;
       min_qty = 14; leaves_qty = 20163; price = 91653/2; time = 1; src = 15;
       order_attr = RESIDENT; capacity = Principal; category = C_ONE;
       cross_restrict =
        {cr_self_cross = false; cr_ubs_principal = false;
         cr_round_lot_only = false; cr_no_locked_nbbo = false;
         cr_pegged_mid_point_mode = 10; cr_enable_conditionals = false;
         cr_min_qty = false;
         cr_cat_elig =
          {c_one_elig = false; c_two_elig = false; c_three_elig = false;
           c_four_elig = false}};
       locate_found = false; expiry_time = 16}
      

      Let's verify this counterexample to transitivity by computation!

      In [21]:
      order_higher_ranked CX.(side, o1, o2, mkt)
      
      Out[21]:
      - : bool = true
      
      In [22]:
      order_higher_ranked CX.(side, o2, o3, mkt)
      
      Out[22]:
      - : bool = true
      
      In [23]:
      order_higher_ranked CX.(side, o1, o3, mkt)
      
      Out[23]:
      - : bool = false
      

      Let us add some additional constraints to help make our counterexample "pretty":

      In [24]:
      let pretty mkt o1 o2 o3 =
          o1.leaves_qty <= o1.qty &&
          o2.leaves_qty <= o2.qty &&
          o3.leaves_qty <= o3.qty &&
          o1.time >= 0 &&
          o2.time >= 0 &&
          o3.time >= 0 &&
          o1.price >. 0.0 &&
          o2.price >. 0.0 &&
          o3.price >. 0.0 &&
          o1.qty > 0 &&
          o2.qty > 0 &&
          o3.qty > 0 &&
          o1.leaves_qty >= 0 &&
          o2.leaves_qty >= 0 &&
          o3.leaves_qty >= 0 &&
          mkt.l_down >. 0.0 &&
          mkt.nbb >. mkt.l_down &&
          mkt.nbo >. mkt.nbb &&
          mkt.l_up >. mkt.nbo
      
      Out[24]:
      val pretty : mkt_data -> order -> order -> order -> bool = <fun>
      
      In [25]:
      verify (fun side o1 o2 o3 mkt -> pretty mkt o1 o2 o3 ==> rank_transitivity side o1 o2 o3 mkt)
      
      Out[25]:
      - : order_side -> order -> order -> order -> mkt_data -> bool = <fun>
      module CX :
        sig
          val side : order_side
          val o1 : order
          val o2 : order
          val o3 : order
          val mkt : mkt_data
        end
      
      Counterexample (after 0 steps, 0.074s):
       let (side : order_side) = BUY
       let (o1 : order) =
        {id = 4; peg = MID; client_id = 5; order_type = FIRM_UP_PEGGED;
         qty = 14801; min_qty = 6; leaves_qty = 3004;
         price = (Real.mk_of_string "61341/2"); time = 1; src = 7;
         order_attr = RESIDENT; capacity = Principal; category = C_ONE;
         cross_restrict =
          {cr_self_cross = false; cr_ubs_principal = false;
           cr_round_lot_only = false; cr_no_locked_nbbo = false;
           cr_pegged_mid_point_mode = 3; cr_enable_conditionals = false;
           cr_min_qty = false;
           cr_cat_elig =
            {c_one_elig = false; c_two_elig = false; c_three_elig = false;
             c_four_elig = false}};
         locate_found = false; expiry_time = 8}
       let (o2 : order) =
        {id = 18; peg = MID; client_id = 19; order_type = PEGGED_CI; qty = 8366;
         min_qty = 20; leaves_qty = 3003; price = (Real.mk_of_string "245363/8");
         time = 8857; src = 21; order_attr = RESIDENT; capacity = Principal;
         category = C_ONE;
         cross_restrict =
          {cr_self_cross = false; cr_ubs_principal = false;
           cr_round_lot_only = false; cr_no_locked_nbbo = false;
           cr_pegged_mid_point_mode = 17; cr_enable_conditionals = false;
           cr_min_qty = false;
           cr_cat_elig =
            {c_one_elig = false; c_two_elig = false; c_three_elig = false;
             c_four_elig = false}};
         locate_found = false; expiry_time = 22}
       let (o3 : order) =
        {id = 10; peg = NO_PEG; client_id = 11; order_type = PEGGED_CI;
         qty = 32286; min_qty = 12; leaves_qty = 3002;
         price = (Real.mk_of_string "245361/8"); time = 0; src = 13;
         order_attr = RESIDENT; capacity = Principal; category = C_ONE;
         cross_restrict =
          {cr_self_cross = false; cr_ubs_principal = false;
           cr_round_lot_only = false; cr_no_locked_nbbo = false;
           cr_pegged_mid_point_mode = 9; cr_enable_conditionals = false;
           cr_min_qty = false;
           cr_cat_elig =
            {c_one_elig = false; c_two_elig = false; c_three_elig = false;
             c_four_elig = false}};
         locate_found = false; expiry_time = 14}
       let (mkt : mkt_data) =
        {nbb = 30670.0; nbo = (Real.mk_of_string "122681/4");
         l_up = (Real.mk_of_string "247611/8"); l_down = (Real.mk_of_string "1/8")}
      
      Refuted
      proof attempt
      ground_instances0
      definitions0
      inductions0
      search_time
      0.074s
      details
      Expand
      smt_stats
      num checks1
      arith-assume-eqs6
      arith-make-feasible187
      arith-max-columns67
      arith-conflicts14
      rlimit count72402
      arith-cheap-eqs196
      mk clause892
      datatype occurs check54
      mk bool var1096
      arith-lower144
      arith-diseq132
      datatype splits285
      decisions1967
      arith-propagations75
      propagations3166
      interface eqs6
      arith-bound-propagations-cheap75
      arith-max-rows41
      conflicts86
      datatype accessor ax139
      minimized lits16
      arith-bound-propagations-lp61
      datatype constructor ax324
      num allocs12186222
      final checks7
      added eqs3405
      del clause239
      arith eq adapter101
      arith-upper233
      time0.043000
      memory15.300000
      max memory16.520000
      Expand
      • start[0.074s]
          let (_x_0 : int) = ( :var_0: ).leaves_qty in
          let (_x_1 : int) = ( :var_0: ).qty in
          let (_x_2 : int) = ( :var_1: ).leaves_qty in
          let (_x_3 : int) = ( :var_1: ).qty in
          let (_x_4 : int) = ( :var_2: ).leaves_qty in
          let (_x_5 : int) = ( :var_2: ).qty in
          let (_x_6 : int) = ( :var_0: ).time in
          let (_x_7 : int) = ( :var_1: ).time in
          let (_x_8 : int) = ( :var_2: ).time in
          let (_x_9 : real) = ( :var_3: ).l_down in
          let (_x_10 : real) = ( :var_3: ).nbb in
          let (_x_11 : real) = ( :var_3: ).nbo in
          let (_x_12 : order_type) = ( :var_0: ).order_type in
          let (_x_13 : order_type) = ( :var_1: ).order_type in
          let (_x_14 : bool) = _x_13 = PEGGED_CI || _x_13 = LIMIT_CI in
          let (_x_15 : order_type) = ….1.order_type in
          let (_x_16 : bool) = Is_a(LIMIT, _x_15) in
          let (_x_17 : bool) = ….0 = BUY in
          let (_x_18 : real) = if _x_17 then ….nbo else ….nbb in
          let (_x_19 : bool) = Is_a(MARKET, _x_15) in
          let (_x_20 : order_type) = ….1.order_type in
          let (_x_21 : bool) = Is_a(LIMIT, _x_20) in
          let (_x_22 : bool) = ….0 = BUY in
          let (_x_23 : real) = if _x_22 then ….nbo else ….nbb in
          let (_x_24 : bool) = Is_a(MARKET, _x_20) in
          let (_x_25 : int)
              = if (if _x_19 then _x_18 else if _x_16 then … else …) =
                   (if _x_24 then _x_23 else if _x_21 then … else …)
                then 0 else -1
          in
          let (_x_26 : bool) = Is_a(PEGGED, _x_15) in
          let (_x_27 : bool) = Is_a(PEGGED, _x_20) in
          let (_x_28 : bool) = ( :var_4: ) = BUY in
          let (_x_29 : int)
              = if _x_28
                then
                  if (if _x_19 then _x_18
                      else
                      if _x_16 then if _x_17 then … else …
                      else if _x_26 then … else …)
                     >.
                     (if _x_24 then _x_23
                      else
                      if _x_21 then if _x_22 then … else …
                      else if _x_27 then … else …)
                  then 1 else _x_25
                else
                if (if _x_19 then _x_18
                    else
                    if _x_16 then if _x_17 then … else …
                    else if _x_26 then … else …)
                   <.
                   (if _x_24 then _x_23
                    else
                    if _x_21 then if _x_22 then … else …
                    else if _x_27 then … else …)
                then 1 else _x_25
          in
          let (_x_30 : order_type) = ( :var_2: ).order_type in
          let (_x_31 : order_type) = ….1.order_type in
          let (_x_32 : bool) = Is_a(LIMIT, _x_31) in
          let (_x_33 : bool) = ….0 = BUY in
          let (_x_34 : real) = if _x_33 then ….nbo else ….nbb in
          let (_x_35 : bool) = Is_a(MARKET, _x_31) in
          let (_x_36 : order_type) = ….1.order_type in
          let (_x_37 : bool) = Is_a(LIMIT, _x_36) in
          let (_x_38 : bool) = ….0 = BUY in
          let (_x_39 : real) = if _x_38 then ….nbo else ….nbb in
          let (_x_40 : bool) = Is_a(MARKET, _x_36) in
          let (_x_41 : int)
              = if (if _x_35 then _x_34 else if _x_32 then … else …) =
                   (if _x_40 then _x_39 else if _x_37 then … else …)
                then 0 else -1
          in
          let (_x_42 : bool) = Is_a(PEGGED, _x_31) in
          let (_x_43 : bool) = Is_a(PEGGED, _x_36) in
          let (_x_44 : int)
              = if _x_28
                then
                  if (if _x_35 then _x_34
                      else
                      if _x_32 then if _x_33 then … else …
                      else if _x_42 then … else …)
                     >.
                     (if _x_40 then _x_39
                      else
                      if _x_37 then if _x_38 then … else …
                      else if _x_43 then … else …)
                  then 1 else _x_41
                else
                if (if _x_35 then _x_34
                    else
                    if _x_32 then if _x_33 then … else …
                    else if _x_42 then … else …)
                   <.
                   (if _x_40 then _x_39
                    else
                    if _x_37 then if _x_38 then … else …
                    else if _x_43 then … else …)
                then 1 else _x_41
          in
          let (_x_45 : order) = ….1 in
          let (_x_46 : order) = ….2 in
          let (_x_47 : order_type) = _x_45.order_type in
          let (_x_48 : order_type) = _x_46.order_type in
          let (_x_49 : order_type) = ….1.order_type in
          let (_x_50 : bool) = Is_a(LIMIT, _x_49) in
          let (_x_51 : bool) = ….0 = BUY in
          let (_x_52 : real) = if _x_51 then ….nbo else ….nbb in
          let (_x_53 : bool) = Is_a(MARKET, _x_49) in
          let (_x_54 : order_type) = ….1.order_type in
          let (_x_55 : bool) = Is_a(LIMIT, _x_54) in
          let (_x_56 : bool) = ….0 = BUY in
          let (_x_57 : real) = if _x_56 then ….nbo else ….nbb in
          let (_x_58 : bool) = Is_a(MARKET, _x_54) in
          let (_x_59 : int)
              = if (if _x_53 then _x_52 else if _x_50 then … else …) =
                   (if _x_58 then _x_57 else if _x_55 then … else …)
                then 0 else -1
          in
          let (_x_60 : bool) = Is_a(PEGGED, _x_49) in
          let (_x_61 : bool) = Is_a(PEGGED, _x_54) in
          let (_x_62 : int)
              = if _x_28
                then
                  if (if _x_53 then _x_52
                      else
                      if _x_50 then if _x_51 then … else …
                      else if _x_60 then … else …)
                     >.
                     (if _x_58 then _x_57
                      else
                      if _x_55 then if _x_56 then … else …
                      else if _x_61 then … else …)
                  then 1 else _x_59
                else
                if (if _x_53 then _x_52
                    else
                    if _x_50 then if _x_51 then … else …
                    else if _x_60 then … else …)
                   <.
                   (if _x_58 then _x_57
                    else
                    if _x_55 then if _x_56 then … else …
                    else if _x_61 then … else …)
                then 1 else _x_59
          in
          _x_0 <= _x_1
          && _x_2 <= _x_3
             && _x_4 <= _x_5
                && _x_6 >= 0
                   && _x_7 >= 0
                      && _x_8 >= 0
                         && ( :var_0: ).price >. 0
                            && ( :var_1: ).price >. 0
                               && ( :var_2: ).price >. 0
                                  && _x_1 > 0
                                     && _x_3 > 0
                                        && _x_5 > 0
                                           && _x_0 >= 0
                                              && _x_2 >= 0
                                                 && _x_4 >= 0
                                                    && _x_9 >. 0
                                                       && _x_10 >. _x_9
                                                          && _x_11 >. _x_10
                                                             && ( :var_3: ).l_up >.
                                                                _x_11
          ==> (if _x_29 = 1 then true
               else
               if _x_29 = -1 then false
               else
               if (_x_12 = PEGGED_CI || _x_12 = LIMIT_CI) && _x_14 then _x_0 > _x_2
               else if (if _x_6 < _x_7 then 1 else …) = 1 then true else …)
              && (if _x_44 = 1 then true
                  else
                  if _x_44 = -1 then false
                  else
                  if _x_14 && (_x_30 = PEGGED_CI || _x_30 = LIMIT_CI)
                  then _x_2 > _x_4
                  else if (if _x_7 < _x_8 then 1 else …) = 1 then true else …)
              ==> (if _x_62 = 1 then true
                   else
                   if _x_62 = -1 then false
                   else
                   if (_x_47 = PEGGED_CI || _x_47 = LIMIT_CI)
                      && (_x_48 = PEGGED_CI || _x_48 = LIMIT_CI)
                   then _x_45.leaves_qty > _x_46.leaves_qty
                   else
                   if (if _x_45.time < _x_46.time then 1 else …) = 1 then true
                   else …)
      • simplify

        into
        let (_x_0 : order_type) = ( :var_0: ).order_type in
        let (_x_1 : bool) = Is_a(LIMIT, _x_0) in
        let (_x_2 : real) = ( :var_3: ).nbb in
        let (_x_3 : real) = ( :var_3: ).nbo in
        let (_x_4 : bool) = ( :var_4: ) = BUY in
        let (_x_5 : real) = if _x_4 then _x_3 else _x_2 in
        let (_x_6 : bool) = Is_a(MARKET, _x_0) in
        let (_x_7 : order_type) = ( :var_2: ).order_type in
        let (_x_8 : bool) = Is_a(LIMIT, _x_7) in
        let (_x_9 : bool) = Is_a(MARKET, _x_7) in
        let (_x_10 : int)
            = if (if _x_6 then _x_5 else if _x_1 then … else …) =
                 (if _x_9 then _x_5 else if _x_8 then … else …)
              then 0 else -1
        in
        let (_x_11 : bool) = Is_a(PEGGED, _x_7) || Is_a(PEGGED_CI, _x_7) in
        let (_x_12 : bool) = Is_a(PEGGED, _x_0) || Is_a(PEGGED_CI, _x_0) in
        let (_x_13 : int)
            = if _x_4
              then
                if (if _x_6 then _x_5
                    else
                    if _x_1 then if _x_4 then … else …
                    else if _x_12 then … else …)
                   <=.
                   (if _x_9 then _x_5
                    else
                    if _x_8 then if _x_4 then … else …
                    else if _x_11 then … else …)
                then _x_10 else 1
              else
              if (if _x_9 then _x_5
                  else
                  if _x_8 then if _x_4 then … else …
                  else if _x_11 then … else …)
                 <=.
                 (if _x_6 then _x_5
                  else
                  if _x_1 then if _x_4 then … else …
                  else if _x_12 then … else …)
              then _x_10 else 1
        in
        let (_x_14 : int) = ( :var_2: ).time in
        let (_x_15 : int) = ( :var_0: ).time in
        let (_x_16 : bool) = _x_14 <= _x_15 in
        let (_x_17 : bool) = _x_0 = LIMIT_CI || _x_0 = PEGGED_CI in
        let (_x_18 : bool) = not _x_17 in
        let (_x_19 : bool) = _x_7 = PEGGED_CI || _x_7 = LIMIT_CI in
        let (_x_20 : bool) = not _x_19 in
        let (_x_21 : int) = ( :var_0: ).leaves_qty in
        let (_x_22 : int) = ( :var_2: ).leaves_qty in
        let (_x_23 : bool) = not (_x_21 <= _x_22) in
        let (_x_24 : order_type) = ( :var_1: ).order_type in
        let (_x_25 : bool) = Is_a(LIMIT, _x_24) in
        let (_x_26 : bool) = Is_a(MARKET, _x_24) in
        let (_x_27 : int)
            = if (if _x_6 then _x_5 else if _x_1 then … else …) =
                 (if _x_26 then _x_5 else if _x_25 then … else …)
              then 0 else -1
        in
        let (_x_28 : bool) = Is_a(PEGGED, _x_24) || Is_a(PEGGED_CI, _x_24) in
        let (_x_29 : int)
            = if _x_4
              then
                if (if _x_6 then _x_5
                    else
                    if _x_1 then if _x_4 then … else …
                    else if _x_12 then … else …)
                   <=.
                   (if _x_26 then _x_5
                    else
                    if _x_25 then if _x_4 then … else …
                    else if _x_28 then … else …)
                then _x_27 else 1
              else
              if (if _x_26 then _x_5
                  else
                  if _x_25 then if _x_4 then … else …
                  else if _x_28 then … else …)
                 <=.
                 (if _x_6 then _x_5
                  else
                  if _x_1 then if _x_4 then … else …
                  else if _x_12 then … else …)
              then _x_27 else 1
        in
        let (_x_30 : int) = ( :var_1: ).time in
        let (_x_31 : bool) = _x_30 <= _x_15 in
        let (_x_32 : bool) = _x_24 = LIMIT_CI || _x_24 = PEGGED_CI in
        let (_x_33 : bool) = not _x_32 in
        let (_x_34 : int) = ( :var_1: ).leaves_qty in
        let (_x_35 : bool) = not (_x_21 <= _x_34) in
        let (_x_36 : int)
            = if (if _x_26 then _x_5 else if _x_25 then … else …) =
                 (if _x_9 then _x_5 else if _x_8 then … else …)
              then 0 else -1
        in
        let (_x_37 : int)
            = if _x_4
              then
                if (if _x_26 then _x_5
                    else
                    if _x_25 then if _x_4 then … else …
                    else if _x_28 then … else …)
                   <=.
                   (if _x_9 then _x_5
                    else
                    if _x_8 then if _x_4 then … else …
                    else if _x_11 then … else …)
                then _x_36 else 1
              else
              if (if _x_9 then _x_5
                  else
                  if _x_8 then if _x_4 then … else …
                  else if _x_11 then … else …)
                 <=.
                 (if _x_26 then _x_5
                  else
                  if _x_25 then if _x_4 then … else …
                  else if _x_28 then … else …)
              then _x_36 else 1
        in
        let (_x_38 : bool) = _x_14 <= _x_30 in
        let (_x_39 : bool) = not (_x_34 <= _x_22) in
        let (_x_40 : int) = ( :var_0: ).qty in
        let (_x_41 : int) = ( :var_1: ).qty in
        let (_x_42 : int) = ( :var_2: ).qty in
        let (_x_43 : real) = ( :var_3: ).l_down in
        ((_x_13 = 1
          || not (_x_13 = -1)
             && (if _x_17 && _x_19 then _x_23
                 else
                   (not _x_16
                    || not (_x_16 && not (_x_15 = _x_14))
                       && (_x_18 || not (_x_17 && _x_20) && _x_23))))
         || not
            ((_x_29 = 1
              || not (_x_29 = -1)
                 && (if _x_17 && _x_32 then _x_35
                     else
                       (not _x_31
                        || not (_x_31 && not (_x_15 = _x_30))
                           && (_x_18 || not (_x_17 && _x_33) && _x_35))))
             && (_x_37 = 1
                 || not (_x_37 = -1)
                    && (if _x_32 && _x_19 then _x_39
                        else
                          (not _x_38
                           || not (_x_38 && not (_x_30 = _x_14))
                              && (_x_33 || not (_x_32 && _x_20) && _x_39))))))
        || not
           ((((((((((((((((((_x_21 <= _x_40 && _x_34 <= _x_41) && _x_22 <= _x_42)
                           && _x_15 >= 0)
                          && _x_30 >= 0)
                         && _x_14 >= 0)
                        && not (( :var_0: ).price <=. 0))
                       && not (( :var_1: ).price <=. 0))
                      && not (( :var_2: ).price <=. 0))
                     && not (_x_40 <= 0))
                    && not (_x_41 <= 0))
                   && not (_x_42 <= 0))
                  && _x_21 >= 0)
                 && _x_34 >= 0)
                && _x_22 >= 0)
               && not (_x_43 <=. 0))
              && not (_x_2 <=. _x_43))
             && not (_x_3 <=. _x_2))
            && not (( :var_3: ).l_up <=. _x_3))
        expansions
        []
        rewrite_steps
          forward_chaining
          • Sat (Some let (side : order_side) = BUY let (o1 : order) = {id = 4; peg = MID; client_id = 5; order_type = FIRM_UP_PEGGED; qty = 14801; min_qty = 6; leaves_qty = 3004; price = (Real.mk_of_string "61341/2"); time = 1; src = 7; order_attr = RESIDENT; capacity = Principal; category = C_ONE; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 3; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 8} let (o2 : order) = {id = 18; peg = MID; client_id = 19; order_type = PEGGED_CI; qty = 8366; min_qty = 20; leaves_qty = 3003; price = (Real.mk_of_string "245363/8"); time = 8857; src = 21; order_attr = RESIDENT; capacity = Principal; category = C_ONE; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 17; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 22} let (o3 : order) = {id = 10; peg = NO_PEG; client_id = 11; order_type = PEGGED_CI; qty = 32286; min_qty = 12; leaves_qty = 3002; price = (Real.mk_of_string "245361/8"); time = 0; src = 13; order_attr = RESIDENT; capacity = Principal; category = C_ONE; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 9; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 14} let (mkt : mkt_data) = {nbb = 30670.0; nbo = (Real.mk_of_string "122681/4"); l_up = (Real.mk_of_string "247611/8"); l_down = (Real.mk_of_string "1/8")} )

          Extending the model with Document printers

          Let's define a few more custom document printers to make these (complex!) counterexamples easier to understand.

          In [26]:
          (* We can generate string printers for our types automatically using the pp plugin *)
          Imandra.add_plugin_pp ();;
          
          let doc_of_order_type o =
            Document.s @@ CCFormat.to_string pp_order_type o
          [@@program];;
          
          #install_doc doc_of_order_type;;
          
          let doc_of_order o =
            let module D = Document in
            D.indent "order" @@ D.record [
                "id", D.bigint o.id;
                "peg", D.s @@ CCFormat.to_string pp_order_peg o.peg;
                "client_id", D.bigint o.client_id;
                "order_type", D.s @@ CCFormat.to_string pp_order_type o.order_type;
                "qty", D.bigint o.qty;
                "min_qty", D.bigint o.min_qty;
                "leaves_qty", D.bigint o.leaves_qty;
                "price", D.s @@ Real.to_string_approx o.price;
                "time", D.s @@ CCFormat.to_string pp_time o.time;
                "src", D.s @@ CCFormat.to_string pp_order_source o.src;
                "order_attr", D.s @@ CCFormat.to_string pp_order_attr o.order_attr;
                "capacity", D.s @@ CCFormat.to_string pp_capacity o.capacity;
                "category", D.s @@ CCFormat.to_string pp_category o.category;
                (* "cross_restrict", D.s @@ CCFormat.to_string pp_cross_restrict o.cross_restrict; *)
                "locate_found", D.s_f "%B" o.locate_found;
                "expiry_time", D.bigint o.expiry_time;
            ]
          [@@program];;
          
          #install_doc doc_of_order;;
          
          let doc_of_side side = Document.s @@ CCFormat.to_string pp_order_side side
          [@@program];;
          
          #install_doc doc_of_side;;
          
          let doc_of_mkt mkt =
            let module D = Document in
            D.indent "mkt" @@ D.record [
                "nbb", D.s @@ Real.to_string_approx mkt.nbb;
                "nbo", D.s @@ Real.to_string_approx mkt.nbo;
                "l_up", D.s @@ Real.to_string_approx mkt.l_up;
                "l_down", D.s @@ Real.to_string_approx mkt.l_down;
            ]
          [@@program];;
          
          let pp_rank (side, o1, o2, o3, mkt) =
            Document.(tbl ~headers:["side";"order1";"order2";"order3";"mkt"]
              @@ [[doc_of_side side; doc_of_order o1; doc_of_order o2; doc_of_order o3; doc_of_mkt mkt]])
           [@@program];;
          
          #install_doc pp_rank
          
          Out[26]:
          - : unit = ()
          val doc_of_order_type : order_type -> Document.t = <fun>
          val doc_of_order : order -> Document.t = <fun>
          val doc_of_side : order_side -> Document.t = <fun>
          val doc_of_mkt : mkt_data -> Document.t = <fun>
          val pp_rank : order_side * order * order * order * mkt_data -> Document.t =
            <fun>
          

          Now, let's view our latest counterexample again:

          In [27]:
          CX.(side, o1, o2, o3, mkt)
          
          Out[27]:
          - : order_side * order * order * order * mkt_data = <document>
          
          sideorder1order2order3mkt
          BUY
          order
          id4
          pegMID
          client_id5
          order_typeFIRM_UP_PEGGED
          qty14801
          min_qty6
          leaves_qty3004
          price30670.5
          time1
          src7
          order_attrRESIDENT
          capacityPrincipal
          categoryC_ONE
          locate_foundfalse
          expiry_time8
          order
          id18
          pegMID
          client_id19
          order_typePEGGED_CI
          qty8366
          min_qty20
          leaves_qty3003
          price30670.375
          time8857
          src21
          order_attrRESIDENT
          capacityPrincipal
          categoryC_ONE
          locate_foundfalse
          expiry_time22
          order
          id10
          pegNO_PEG
          client_id11
          order_typePEGGED_CI
          qty32286
          min_qty12
          leaves_qty3002
          price30670.125
          time0
          src13
          order_attrRESIDENT
          capacityPrincipal
          categoryC_ONE
          locate_foundfalse
          expiry_time14
          mkt
          nbb30670.
          nbo30670.25
          l_up30951.375
          l_down0.125