module Bitvector: sig end
Creating fresh bitvector variables for solver.
The index variable are always reset to the current value
when solver is called.
val const : Bitv.t -> Sym.t
val conc : int -> int -> Sym.t
val sub : int -> int -> int -> Sym.t
val bitwise : int -> Sym.t
val is_bvsym : Sym.t -> bool
val d_bvsym : Sym.t -> Sym.bv option
val is_interp : Term.t -> bool
val d_interp : Term.t -> (Sym.bv * Term.t list) option
val mk_const : Bitv.t -> Term.t
val is_const : Term.t -> bool
val mk_eps : Term.t
val is_eps : Term.t -> bool
val mk_zero : int -> Term.t
val is_zero : Term.t -> bool
val mk_one : int -> Term.t
val is_one : Term.t -> bool
Creating fresh bitvector variables for solver.
The index variable are always reset to the current value
when solver is called.
val mk_fresh : int -> Term.t
Bitvector symbols
val width : Term.t -> int option
val iter : (Term.t -> unit) -> Term.t -> unit
Fold functional.
val fold : (Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
val is_bitwise : Term.t -> bool
val d_bitwise : Term.t -> (int * Term.t * Term.t * Term.t) option
val d_conc : Term.t -> (int * int * Term.t * Term.t) option
val d_const : Term.t -> Bitv.t option
val d_sub : Term.t -> (int * int * int * Term.t) option
Building up Bitvector BDDs
val is_bvbdd : Term.t -> bool
val cofactors : Term.t -> Term.t -> Term.t * Term.t
val topvar : Term.t -> Term.t -> Term.t -> Term.t
module H3: sig end
val ht : Term.t H3.t
val build : int -> H3.key -> Term.t
val build_fun : int -> H3.key -> Term.t
| Parameters: |
|
n |
: |
int
|
|
(s1,s2,s3) |
: |
H3.key
|
|
Term constructors.
val mk_sub : int -> int -> int -> Term.t -> Term.t
| Parameters: |
|
n |
: |
int
|
|
i |
: |
int
|
|
j |
: |
int
|
|
a |
: |
Term.t
|
|
val mk_conc : int -> int -> Term.t -> Term.t -> Term.t
val merge : int -> int -> Term.t -> Term.t -> Term.t option
val mk_conc3 : int -> int -> int -> Term.t -> Term.t -> Term.t -> Term.t
val mk_bitwise : int -> Term.t -> Term.t -> Term.t -> Term.t
val lift : int -> Term.t -> Term.t
val drop : Term.t -> Term.t
val cut : int -> int -> Term.t -> Term.t * Term.t
Derived bitwise constructors.
val mk_bwconj : int -> Term.t -> Term.t -> Term.t
val mk_bwdisj : int -> Term.t -> Term.t -> Term.t
val mk_bwneg : int -> Term.t -> Term.t
val mk_bwimp : int -> Term.t -> Term.t -> Term.t
val mk_bwiff : int -> Term.t -> Term.t -> Term.t
Mapping over bitvector terms.
val map : (Term.t -> Term.t) -> Term.t -> Term.t
Does term a occur interpreted in b.
val occurs : Term.t -> Term.t -> bool
Sigmatizing an expression.
val sigma : Sym.bv -> Term.t list -> Term.t
val mk_iterate : int -> Term.t -> int -> Term.t
val decompose : Term.t * Term.t -> (Term.t * Term.t) list
Solving is based on the equation
ite(x,p,n) = (p or n) and exists delta. x = (p and (n => delta))
val solve_bitwise : int -> Term.t * Term.t -> (Term.t * Term.t) list
Adding a solved pair a |-> b to the list of solved forms sl,
and propagating this new binding to the unsolved equalities el and
the rhs of sl. It also makes sure that fresh variables a are never
added to sl but only propagated.
val add : Term.t ->
Term.t ->
(Term.t * Term.t) list * (Term.t * Term.t) list ->
(Term.t * Term.t) list * (Term.t * Term.t) list
val is_fresh_bv_var : Term.t -> bool
val inste : (Term.t * Term.t) list -> Term.t -> Term.t -> (Term.t * Term.t) list
val insts : (Term.t * Term.t) list -> Term.t -> Term.t -> (Term.t * Term.t) list
val inconsistent : Term.t -> Term.t -> bool
val apply1 : Term.t -> Term.t -> Term.t -> Term.t
Toplevel solver.
val solve : Fact.equal -> Fact.equal list
val solvel : (Term.t * Term.t) list * (Term.t * Term.t) list -> (Term.t * Term.t) list
val solve_sub_sub : Term.t -> int -> int -> int -> int -> int -> Term.t * Term.t
| Parameters: |
|
x |
: |
Term.t
|
|
n |
: |
int
|
|
i |
: |
int
|
|
j |
: |
int
|
|
k |
: |
int
|
|
l |
: |
int
|
|