Module Arr.Infsys

module Infsys: sig  end

Inference system for the theory Th.arr of extensional arrays as defined in module Funarr.

A context consists of equalities of the form x = b with x a variable and b a flat array term with variables as arguments:

• create(a) for creating a constant array with 'elements' a
• a[i:=x] for updating array a at position i with x
• a[j] for selection the value of array a at position j

Right-hand sides of context equalities x = a are kept in canonical form. That is, if the variable equality y = z has been merged using Arr.merge, then the noncanonical y is not appearing on any right-hand side.

Forward chaining is used to keep configurations confluent.

• (1) u = a[i:=x] ==> x = u[i],
• (2) i<>j, u = a[i:=x] ==> u[j] = a[j],
• (3) i<>j, v = a[i:=x][j:=y] ==> v = a[j:=y][i:=x],
• (4) u = a[i:=y][i:=x] ==> u = a[i:=x],
• (5) u = create(a)[j] ==> u = a

Here, i<>j are the known disequalities in a variable partition (see Partition.t).

val current : unit -> e

val initialize : e -> unit

Intitialize inference system with equality set.

val finalize : unit -> e

Retrieve modified equality set.

val abstract : Term.t -> unit

(g[a]; e; p) ==> (g[x]; e, x = a; p) with

• a a nonvariable term,
• a an i-pure term,
• and x fresh.

val merge : Fact.Equal.t -> unit

(g, a = b; e; p) ==> (g; e'; p') with

• a, b i-pure,
• |= e', p' <=> |= e, a = b, p
• if e' |= x = y then p' |= x = y.

val propagate : Fact.Equal.t -> unit

(g, e; p) ==> (g; e'; p) with

• e |= x = y,
• notp |= x = y,
• |= e, p <=> |= e', p'

val dismerge : Fact.Diseq.t -> unit

(g, a <> a; e; p) ==> (g; e'; p') with a, b i-pure, |= e', p' <=> |= e, p, a <> b.

val propagate_diseq : Fact.Diseq.t -> unit

(g; e; p) ==> (g; e'; p') with

• p' |= x <> y
• |= e', p' <=> |= e, p.

val branch : unit -> unit

(g; e; p) ==> (g, c1; e; p) | ... | (g, cn; e; p) with

• e, p |= c1 \/ ... \/ cn
• not e, p |= ci

val normalize : unit -> unit

(g; e; p) ==> (g'; e'; p') where source and target configuration are equivalent.