Previous  Up  Next

Module Context


module Context: sig  end

Decision procedure state



Decision procedure state



type t = {
   mutable ctxt : Atom.Set.t;
   mutable p : Partition.t;
   eqs : Solution.t Th.Array.arr;
   mutable upper : int;
   mutable diseqs : (int * Term.Set.t) Term.Map.t;
} 
val empty : t


Accessors 


val ctxt_of : t -> Atom.Set.t
Parameters:
s : t
 
val p_of : t -> Partition.t
Parameters:
s : t
 
val v_of : t -> V.t
Parameters:
s : t
 
val d_of : t -> D.t
Parameters:
s : t
 
val c_of : t -> C.t
Parameters:
s : t
 
val eqs_of : t -> Th.t -> Solution.t
Parameters:
s : t
 
val upper_of : t -> int
Parameters:
s : t
 
val eq : t -> t -> bool
Equality test. Do not take upper bounds into account.
Parameters:
s : t
t : t
 
val update : t -> Th.t -> Solution.t -> t
Destructive updates.
Parameters:
s : t
i : Th.t
eqs : Solution.t
 
val copy : t -> t
Shallow copying.
Parameters:
s : t

Canonical variables module s.

val v : t -> Term.t -> Term.t
Parameters:
s : t
x : Term.t
 
val d : t -> Term.t -> Term.t list
Parameters:
s : t
x : Term.t
 
val sign : (Term.t -> Sign.t) -> Term.t -> Sign.t
Parameters:
lookup : Term.t -> Sign.t
a : Term.t
 
val c : t -> Term.t -> Sign.t
Parameters:
s : t
a : Term.t
 
val fold : t -> (Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
Parameters:
s : t
f : Term.t -> 'a -> 'a
x : Term.t

Parameterized operations on solution sets.

val mem : Th.t -> t -> Term.t -> bool
Parameters:
i : Th.t
s : t
 
val use : Th.t -> t -> Term.t -> Term.Set.t
Parameters:
i : Th.t
s : t
 
val apply : Th.t -> t -> Term.t -> Term.t
Parameters:
i : Th.t
s : t
 
val find : Th.t -> t -> Term.t -> Term.t
Parameters:
i : Th.t
s : t
 
val replace : Th.t -> t -> Term.t -> Term.t
Parameters:
i : Th.t
s : t
 
val inv : Th.t -> t -> Term.t -> Term.t
Parameters:
i : Th.t
s : t
 
val is_empty : Th.t -> t -> bool
Parameters:
i : Th.t
s : t
 
val interp : Th.t -> t -> Term.t -> Term.t
Parameters:
i : Th.t
s : t

Array selection

val d_select : t -> (Term.t -> bool) * (Term.t -> bool) -> Term.t -> Term.t * Term.t
Parameters:
s : t
(p1,p2) : (Term.t -> bool) * (Term.t -> bool)
v : Term.t
 
val d_update : t ->
       (Term.t -> bool) * (Term.t -> bool) * (Term.t -> bool) ->
       Term.t -> Term.t * Term.t * Term.t
Parameters:
s : t
(p1,p2,p3) : (Term.t -> bool) * (Term.t -> bool) * (Term.t -> bool)
v : Term.t
 
val tt : 'a -> bool
Parameters:
() : 'a

Constraint of a in s.

val dom : t -> Term.t -> Dom.t
Parameters:
s : t
a : Term.t
 
val is_int : t -> Term.t -> bool
Parameters:
s : t
a : Term.t
 
val name : Th.t -> t * Term.t -> t * Term.t
Parameters:
i : Th.t
(s,b) : t * Term.t
 
val extend : Th.t -> Fact.equal -> t -> t
Parameters:
i : Th.t
e : Fact.equal
s : t

Pretty-printing.

val pp : Format.formatter -> t -> unit
Parameters:
fmt : Format.formatter
s : t
 
val equation : Th.t -> t -> Term.t -> Fact.equal
Parameters:
i : Th.t
s : t

Variable partitioning.

val is_equal : t -> Term.t -> Term.t -> Three.t
Parameters:
s : t
x : Term.t
y : Term.t
 
val is_eq : t -> Term.t -> Term.t -> bool
Parameters:
s : t
x : Term.t
y : Term.t
 
val is_diseq : t -> Term.t -> Term.t -> bool
Parameters:
s : t
x : Term.t
y : Term.t

Constraint of a term.

val cnstrnt : t -> Term.t -> Sign.t
Parameters:
s : t
 
val cnstrnt : t -> Term.t -> Sign.t
Parameters:
s : t
 
val cnstrnt : t -> Term.t -> Sign.t
Parameters:
s : t

Sigma normal forms.

val sigma : t -> Sym.t -> Term.t list -> Term.t
Parameters:
s : t
op : Sym.t
 
val lookup : t -> Term.t -> Term.t
Parameters:
s : t
a : Term.t

Search for largest match on rhs. For example, if a is of the form x * y and there is an equality u = x^2 * y, then inv_pprod s a returns u * x if there is no larger rhs which matches a.

val inv_pprod : t -> Term.t -> Term.t
Parameters:
s : t
a : Term.t


Canonization 


module Can: sig  end
val can : t -> Term.t -> Term.t


Abstraction 


module Abstract: sig  end
val equality : Fact.Equalset.elt -> t -> t
Processing an equality over pure terms.
Parameters:
e : Fact.Equalset.elt
s : t
 
val merge_v : Fact.Equalset.elt -> t -> t
Processing of a variable equality.
Parameters:
e : Fact.Equalset.elt
s : t
 
val merge_i : Th.t -> Fact.Equalset.elt -> t -> t
Processing of an interpreted equality.
Parameters:
i : Th.t
e : Fact.Equalset.elt
s : t
 
val fuse : Th.t -> Fact.Equalset.elt -> t -> t
Parameters:
i : Th.t
e : Fact.Equalset.elt
s : t
 
val compose : Th.t -> t -> Fact.equal list -> t
Parameters:
i : Th.t
s : t
r : Fact.equal list
 
val refine : Fact.cnstrnt -> t -> t
Parameters:
c : Fact.cnstrnt
s : t
 
val infer : Th.t -> Fact.equal -> t -> t
Infer new disequalities from equalities.
Parameters:
i : Th.t
e : Fact.equal
s : t
 
val infer_la : Fact.equal -> t -> t
If x = q and y = p with q, p numerical constraints, then deduce x <> y.
Parameters:
e : Fact.equal
s : t
 
val infer_bv : Fact.equal -> t -> t
Parameters:
e : Fact.equal
s : t
 
val infer_cop : Fact.equal -> t -> t
If x = a, y = b are in the coproduct solution set, and if a and b are diseq in this theory, then deduce x <> y.
Parameters:
e : Fact.equal
s : t
 
val deduce : Th.t -> Fact.equal -> t -> t
Deduce new constraints from an equality
Parameters:
i : Th.t
e : Fact.equal
s : t
 
val deduce_bvarith : Fact.equal -> t -> t
Parameters:
e : Fact.equal
s : t
 
val deduce_nonlin : Fact.equal -> t -> t
Parameters:
e : Fact.equal
s : t
 
val deduce_nonlin2 : Fact.equal -> t -> t
Parameters:
e : Fact.equal
s : t
 
val deduce_la : Fact.equal -> t -> t
Parameters:
e : Fact.equal
s : t
 
val deduce_la1 : Fact.equal -> t -> t
Parameters:
e : Fact.equal
s : t
 
val diseq : Fact.diseq -> t -> t
Merging variable equality/disequalities/constraints
Parameters:
d : Fact.diseq
s : t
 
val add : t -> Atom.t -> t Status.t
val close_i : Th.t -> Term.Set.t -> t -> t
Propagate changes in the variable partitioning.
Parameters:
i : Th.t
 
val nonlin_equal : Fact.equal -> t -> t
Parameters:
e : Fact.equal
s : t
 
val close_p : Partition.changed -> t -> t
Propagate changes in the variable partitioning.
Parameters:
ch : Partition.changed
s : t
 
val close_v : Term.Set.t -> t -> t
Parameters:
chv : Term.Set.t
 
val close_c : Term.Set.t -> t -> t
Parameters:
chc : Term.Set.t
 
val close_d : Term.Set.t -> t -> t
Parameters:
chd : Term.Set.t


Bitvector propagation 


val bv_diseq : Fact.diseq -> t -> t
Parameters:
d' : Fact.diseq
s : t


Array propagation



Forward chaining on the array properties 

val arrays_diseq : Fact.diseq -> t -> t
Parameters:
d : Fact.diseq
s : t
 
val arrays_diseq1 : Fact.diseq -> t -> t
i <> j implies a[i:=x][j] = a[j]. Thus, look for v = u[j] and u' = a[i := x] with u = u' in s using the use lists. Now, when w = a[j], then infer v = w.
Parameters:
d : Fact.diseq
s : t
 
val arrays_diseq2 : Fact.diseq -> t -> t
i <> j and i <> k implies a[j:=x][i] = a[k:=y][i]. Thus, for i <> j, select v = u[i] and u' = a[j:=x] with u = u' in s. Now, for all u'' = a[k:=y] with k <> i, add a[j:=x][i] = a[k:=y][i].
Parameters:
d : Fact.diseq
s : t
 
val arrays_diseq3 : Fact.diseq -> t -> t
a[j:=x] = b[k:=y], i <> j, i <> k implies a[i] = b[i]. We are propagating disequalities i <> j. If u = a[j := x], then look for all k disequal from i for v = b[k:=y]. Now, assert a[i] = b[i].
Parameters:
d' : Fact.diseq
s : t
 
val arrays_equal : Fact.Equalset.elt -> t -> t
Parameters:
e : Fact.Equalset.elt
s : t
 
val arrays_equal1 : Fact.Equalset.elt -> t -> t
i = j implies a[i:= x][j] = x. Since i and j are already merged on rhs, it suffices to look for v1 = v2'[i] and v2 = a[i := x] with v2 equal v2' in s. Now, v1 = x.
Parameters:
e : Fact.Equalset.elt
s : t
 
val arrays_equal2 : Fact.Equalset.elt -> t -> t
a[i:=x] = b[i := y] implies x = y. Thus, if v = u has been merged, then look for v = a[i:=x] and v' = b[i := y] with v = v' in s, now merge x = y.
Parameters:
e : Fact.Equalset.elt
s : t
 
val arrays_equal3 : Fact.Equalset.elt -> t -> t
a[j:=x] = b[k:=y], i <> j, i <> k implies a[i] = b[i]. Thus, for a merged v = u, look for v = a[j:= x] and v' = b[k := y] with v = v' in s. For all i such that i <> j and i <> k add w1 = w2 for w1 = a[i] and w2 = b[i], possibly extending the solution set.
Parameters:
e : Fact.Equalset.elt
s : t
 
val bvarith_equal : Fact.Equalset.elt -> t -> t
Parameters:
e : Fact.Equalset.elt
s : t

Garbage collection. Remove all variables x which are are scheduled for removal in the partitioning. Check also that this variable x does not occur in any of the solution sets. Since x is noncanonical, this check only needs to be done for the u part, since all other solution sets are kept in canonical form.

val compactify : bool Pervasives.ref
val normalize : t -> t
Parameters:
s : t
 
val gc : t -> t
Parameters:
s : t


Adding new atoms 


module Status: sig  end
module Process: sig  end
val add : t -> Atom.t -> t Status.t

List all constraints with finite extension.

val split : t -> Atom.Set.t
Parameters:
s : t
 
val split_cnstrnt : t -> Atom.Set.t
Parameters:
s : t
 
val split_arrays : t -> Atom.Set.t
Parameters:
s : t


Model construction 


val model : t -> Term.Map.key list -> Term.t Term.Map.t
Parameters:
s : t
xs : Term.Map.key list