Index of values

Multiplication.

Addition.

Inverse of Multiplication.

x <<< y holds iff cmp x y <= 0.

a <<< b iff cmp a b <= 0.

abstract x a lamgda-abstracts a.

(g[a]; e; p) ==> (g[x]; e, x = a; p) with a a nonvariable term, , a an i-pure term, , and x fresh.

acc1 acc f b calls f b to obtain (c, a).

acc2 acc f b1 b2 calls f b1 b2 to obtain (c, a).

accb acc p b calls p b.

Folding over the members of a specific equivalence class.

add l activates the trace level l.

add d s adds a disequality d of the form x <> y to the disequality context s.

process s a extends the logical context s with an atom a.

Procedures f without parameters can be registered as exit procedures by add_to_exit f.

add_to_reset f registers f as a reset procedure

apply (x, b) a replaces uninterpreted occurrences of x in a with b, and returns a canonical form.

apply s x yields (b, rho) if x = b in s with justification rho; if x is not a dependent variable, Not_found is raised.

Test binary term relation r on f a and f b.

Test binary term relation r on f a and f b.

Test predicate p on f(a).

Test predicate p on f(a).

Replace a variable x by y in a flat term a.

apply (x, b) for uninterpreted occurrences of x in a with b, and normalizes.

apply (x, b) a occurrences of x in a with b, and normalizes.

Replacing a variable with a term.

sym_of a returns the argument list l of an application a of the form App(_,l, _).

Association lists for terms.

Retrieve the atom from an atom-index pair.

Unsigned interpretation of a bitvector constant.

(g; e; p) ==> (g, c1; e; p) | ... | (g, cn; e; p) with e, p |= c1 \/ ... \/ cn, not e, p |= ci

call l name arg pp outputs a function call trace message if l is currently active by first outputting name followed by printing arg using the pp printer.

replace s a substitutes dependent variables x in a with their right hand side b if x = b in s.

Given an equality set e and a partition p as obtained from processing, can (e, p) a returns a term b equivalent to a in (e, p) together with a justification rho.

If cheap is set, Combine.simplify only performs cheap simplifications for disequalities and inequalities.

check_sat s performs case-splitting and returns Some(splits', s') if there is a complete case-splitting path splits' yielding a satisfiable extension s' of s., None if all case-splittinig paths yield an inconsistent context.

choose s p x chooses a y which is congruent to x modulo s which satisfies p.

choose p a chooses a variable of a which satisfies predicate p.

choose p apply x chooses an x' such that apply x' does not raise Not_found.

choose s y returns equality e of the form x = a if x is dependent on y; otherwise, Not_found is raised.

cmp x y realizes a total ordering on variables.

cmp a b realizes a total ordering on terms.

cmp f g returns 0 iff eq f g holds, and cmp f g is positive iff cmp g f is negative.

cmp d e is 0 if eq d e holds, -1 if sub d e holds, 1 if sub e d holds. Otherwise the result is unspecified.

For a canonical variable x, cnstrnt s x returns the domain constraint associated with the equivalence class x.

cnstrnt s x returns a domain constraint on x, or raises Not_found if the interpretation of x is unconstrained.

cnstrnt_of x returns the domain constraint of variable x.

cnstrnt_of x returns the domain constraint associated with x.

Enable/Disable cone of influence.

Total variable ordering.

Total comparison on term which is designed to be fast.

If s (t) is the string associated to n (m), then compare n m equals 0 iff eq n m.

If g a = (b, rho) and f b = (c, tau) with rho |- a = b and tau |- b = c, then compose f g a returns (c, sigma) with sigma |- a = c.

compose3 f g h is defined as compose f (compose g h).

compose_partial1 f g a behaves like compose f g a when f does not throw an exception.

If a is of the form q + a', then constant_of a returns q.

Protect state against destructive updates.

copy p copies p to a partition which is observationally equal to p.

ctxt_of s returns the logical context of s as a list of atoms.

d_add a returns Some(bl) if a is a function application with symbol Sym.Add.

Accessor for bitvector constants.

Same as Acsym.TERM.

If a is of the form b*c, then d_interp a returns (b, c).

If a is of the form b*c, then d_interp a returns (b, c).

d_num a return q if a is a constant with function symbol Sym.Num(q), and raises Not_found otherwise.

Accessing the variable disequalities of a partititioning.

d_select a returns (b, i, x, j) if a is of the form a[i:=x][j].

For a term a such that is_uninterp a holds, d_uninterp a returns the uninterpreted function symbol and the argument list of a.

Level of debugging.

Decompose x*x*...*x*y*.... into (x, n) with n the multiplicity of x in a and y*....

Decompose x*x*...*x*y*.... into (x, n) with n the multiplicity of x in a and y*....

dep s y returns all x such that x = a in s, and the variable y occurs in a.

dep i s x returns a set ys of variables such that y in ys iff there is an x = a in s with y a subterm of a.

destruct a destructure an application a of the form App(f, l) into (f, l).

diff s1 s2 contains all variable equalities in s1 but not in s2.

diff p q contains all facts in p but not in q.

diff s1 s2 contains all equalities in s1 that are not in s2.

diff d1 d2 contains all disequalities in d1 not in d2.

Difference.

diff s1 s2 returns the equality set s such that an equality e is in s iff if it is in s1 but not in s2.

Propagate a disequalities x <> y.

diseqs s x returns the set of all variable y disequal to x as stored in the variable disequality part d of the partitioning s.

diseqs s x returns set of disequalites of the form x <> y such that x <> y is represented in s.

Disjunction.

disjoint d e holds iff the denotations of d and e are disjoint.

diseq d s adds a disequality of the form x <> y to s.

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

Divide a of the form x * ... y^m ... *z by y^n, where n <= m.

Procedures f registered by Tools.add_at_exit are called by do_at_exit().

do_at_reset().

tau lookup op al returns a constraint in Cnstrnt.t given a lookup function, which is applied to each noninterpreted term, and by propagation using abstract domain operations for the interpreted symbols.

dom p a returns a domain d for a term a together with a justification rho such that rho |- a in d.

dom_of x returns the domain of interpretation of variable x, and raises Not_found if this domain is "unrestricted".

dom_of x returns the domain restriction associated with x (see Var.dom_of).

Abstract constraint interpretation

The empty variable context.

The empty partition.

The empty equality set.

Empty set of inputs.

The empty disequality context.

The empty logical context

The empty equality configuration.

eq s t holds iff s and t are identical.

eq a b holds iff a and b are syntactically equal.

eq f g succeeds iff f and g represent the same function symbol.

eq s t holds if the respective equality, disequality, and constraint parts are identical, that is, stored in the same memory location.

eq n m holds if the strings associated with n and m are equal.

Test for identity of two solution sets.

Identity test for input facts.

Equality.

eq d e holds iff the denotation of d equals the denotation of e.

eq s t holds iff s and t are 'physically' equal.

Identity test on contexts.

Identity test for two equality sets.

eql al bl holds iff al and bl are of the form a1;...;an and b1;...;bn, respectively, and if eq ai bi holds for all i.

Equality on atoms.

equality s x yields an equality e of the form x = a with justification rho if x is a dependent variable.

Given two rational numbers p, q, euclid p q finds integers x, y, (p, q) satisfying p * x + q * y = (p, q), where (p, q) denotes the greatest common divisor of p, q.

exists s p x holds if p y holds for some y congruent to x modulo s.

exists p holds if predicate p i holds for some i.

exists s p y holds iff p e holds for all equalities x = a with x dependent on y.

exists f s checks if f e holds for all equalities e in s.

exists_but j p holds if predicate p i holds for some i <> j.

exit l name arg pp outputs a function exit trace message if l is currently active by first outputting name followed by printing arg using the pp printer.

Return the value of the extension field.

fail l exc outputs a failure warining if l is curently active, and raises exception exc.

Retrieve modified equality set.

find s x returns the canonical representative of x of the equivalence class in s containing x together with a justification of the equality find s x = x.

find s x returns the canonical representative of the equivalence class in the partitioning s containing the variable x.

find s x yields (b, rho) if x is a dependent variable in s with x = b; otherwise, (x, refl) is returned with refl a justification of x = x.

find s th x is a if x = a is in the solution set for theory th in s; otherwise, the result is just x.

Floor function on rationals.

fold f s e applies f x (y, rho) for each x = y with justification rho in s and accumulates the result starting with e.

fold f e applies f i to each theory i and accumulates the result, starting with e, in an unspecified order.

Fold operator fold f a e on terms applies argument function f to all variables in a and accumulates the results starting with e.

fold s f y e accumulates, starting with e, applications of f to each equality x = a which x dependent on y.

fold f s acc applies f e for each equality e in s and accumulates the result starting with acc.

fold f a e applies f at uninterpreted positions of a and accumulates the results starting with e.

Folding over the non-constant monomials of an arithmetic term.

fold f a e applies f at uninterpreted positions of a and accumulates results starting with e.

If a is of the form x1^m1*(x2^m2*...*xn^mn), then fold f a e is f x1 m1 (f x2 m2 (... (f xn mn e)...)).

If a is of the form x1^m1*(x2^m2*...*xn^mn), then fold f a e is f x1 m1 (f x2 m2 (... (f xn mn e)...)).

for_all s p x holds if p y holds for all y congruent to x modulo s.

for_all p holds if predicate p i holds for all theories i.

forall p a holds if p x for all variables in a.

for_all s p y holds iff p e holds for all equalities x = a with x dependent on y.

for_all f s checks if f e holds for all equalities e in s.

for_all f holds iff f x holds for all top-level uninterpreted x in a.

for_all_but j p holds if predicate p i holds for all i <> j.

Chooses a "fresh" variable disequality.

Chooses a "fresh" variable equality.

func l name pp qq f provides a trace wrapper for function f for calling call before applying f and exit after applying f.

Global variables for current input facts g, current variable partitioning p.

Switch for enabling/disabling garbage collection of noncanonical, internal variables.

gc filter s removes variables x in removable s, if the test filter x succeeds.

gc p s removes all noncanonical, internal variables x with p x.

gc c garbage collects internal variables in configuration c as introduced by Combine.process.

get () returns the set of currently active trace levels as a list.

get f returns a theory-specific operator together with a tag for specifying the theory corresponding to f.

get g chooses a fact fct in g and returns this fact fct together with g where fct is removed.

get_clause g removes a clause cl in g or raise Not_found.

hash a returns a hash value such that Term.eqa b implies hash a = hash b.

Nonnegative hash value for function symbols.

Return hash values for names n.

id a returns (a, rho) such that rho |- a = a.

Retrieve the unique index from an atom-index pair.

infix p str q (a, b) prints a using printer p, then it prints str, and then b using printer b.

infixl pp op prints a list [a1;...;an] in the form a1 op ... op an.

Intitialize inference system with equality set.

inj i hashconses injection of theories i into Some(i).

inter u v evaluates to Some(w) if both is_sub w u and is_sub w v; otherwise None is returned.

inter d1 d2 returns d iff the denotation of d is the nonempty intersection of the denotations of d1 and d2.

inv s a yields (x, rho) if rho |- x = a is in s with justification rho.

Inverse of Addition.

inv s a is x if there is x = a in the solution set for theory th; otherwise Not_found is raised.

Test if certain trace level is active.

is_app a holds iff a is of the form App _.

is_can i holds if i is a canonizable theory.

For a term variable x, is_canonical s x holds iff find s x returns x.

is_connected atm1 atm2 holds iff vars_of atm1 and vars_of atm2 not disjoint.

is_const a holds iff a is of the form App(_,[], _).

is_const a holds iff a is a bitvector constant.

is_dependent s x holds iff there is an a such that x = a is in s.

is_diophantine a holds iff all variables in a are integer.

Apply the equality test on canonical variables.

Check if two terms are known to be disequal.

is_diseq a b iff a, b are disequal in the theory of COP.

Two bitvector terms a, b are disequal iff they disagree on at least one position.

is_disjoint u v holds iff the inter u v is None.

is_dom d x holds iff the domain e of x as obtained by Term.Var.dom_ofx is a subdomain of d (see also Dom.sub).

is_empty s holds iff s does not contain any equalities.

is_empty g holds iff g does not contain any inputs.

Check if the argument disequality context is empty.

Succeeds if all individual equality sets are empty.

For variables x, y[], is_equal s x y holds if and only if x and y are in the same equivalence class modulo s.

is_equal a b returns Three.Yes if Term.eqa b holds,, Three.No is a and b are two distinct constants in some theory th, and, Three.X if none of the above holds.

Apply the equality test on variables only.

Test for equality or disequality of canonical variables.

is_false atm holds iff atm represents the false atom.

is_fresh i x holds iff x is a fresh variable of theory i.

is_inconsistent s al is true iff the conjunction of atoms in al is inconsistent in s.

is_independent s x holds iff x is a variable in some a with y = a in s.

is_int x holds iff x is constraint over the integers.

is_int x holds if x is restricted to be interpreted over the integers.

Integer test of a rational.

is_internal x holds iff either is_rename x, is_slack x, or is_fresh x holds.

is_internal x holds iff x is either a renaming, a fresh, or a slack variable.

in_interp a holds if the top-level function symbol is in the signature of P.

in_interp a holds if the top-level function symbol is in the signature of COP.

is_interp a holds iff the top-level function symbol of a is interpreted in the theory of bitvectors (see also module Sym.

is_interp a holds iff the toplevel function symbol in a is a linear arithmetic function symbol.

is_interp a holds iff a is of the form b*c.

is_interp a holds iff a is of the form b*c.

is_negatable atm is always true.

Test if a >= 0.

is_nonneg_num a holds iff a represents a nonnegative number.

is_zero_slack x holds iff x is a nonnegative slack variable.

is_nonpos_num a holds iff a represents a nonpositive number.

is_one a holds iff all bits in a are 1.

is_one a holds iff a is equal to mk_one.

Test if a > 0.

is_pos_num a holds iff a represents a positive number.

is_pure i a holds iff all function symbols in a are of theory i (see Th.t).

is_pure a holds if every function symbol in a is in P; that is, only variables occur at uninterpreted positions.

is_pure a holds if every function symbol in a is in COP; that is, only variables occur at uninterpreted positions.

is_pure a holds iff a is a linear arithmetic term; that is, a is term equal to a numeral (constructed with Arith.mk_num), a linear multiplication (Arith.mk_multq), or an addition (Arith.mk_add).

is_q q a holds iff a is equal to the numeral mk_num q.

is_real x holds iff x is constraint over the reals.

is_real x holds if x is restricted to be interpreted over the reals.

is_rename x holds iff x is a rename variable.

Variables are partitioned into renaming, external, fresh, free, and slack variables, and the following recognizers can be used to test membership of a variable into a partition.

is_sat [c] applies applicable branching rules until it finds a satisfiable configuration d (with empty input) for which no branching rule is applicable; in this case Some(d) is returned.

is_shostak i holds if i is a Shostak theory.

is_cnstrnt x holds iff x is a slack variable.

is_sub u v holds if either u = v or u < v.

is_true atm holds iff atm represents the true atom.

is_uninterp a holds iff the function symbol of a is uninterpreted (see module Sym).

is_uninterpreted i holds iff i is the uninterpreted theory Th.u.

is_valid s al is true iff the conjunction of atoms in al is valid in s.

is_var x holds iff x is an external variable, that is, it has been returned by a call to mk_external.

is_var a holds iff a is of the form Var _.

is_zero a holds iff all bits in a are 0.

is_zero a holds iff a is equal to mk_zero.

is_zero_slack x holds iff x is a zero slack variable.

Slacks are subpartitioned into zero and nonnegative slacks.

isolate y (a, b) isolates y in an equality a = b; that is, if there is a b such that y = b iff a = b, then b is returned.

Iterate over the extension of an equivalence class.

fold f applies f i for each theory i in some unspecified order.

Iteration operator on terms.

iter s f y applies f to each equality e of the form x = a with justification rho such that x is dependent on y.

iter f s applies f e for each equality fact e in s.

iter f a applies f for all toplevel subterms of a which are not interpreted in the theory of bitvectors.

iter f a applies f at uninterpreted positions of a.

If a is of the form x1^m1*(x2^m2*...*xn^mn), then iter f a is f x1 m1; f x2 m2; ...; f xn mn.

If a is of the form x1^m1*(x2^m2*...*xn^mn), then iter f a is f x1 m1; f x2 m2; ...; f xn mn.

Iterate over the x's satisfying f in the equivalence class of y.

For n>=1, iterate a n iterates make a n-1 times.

For n>=1, iterate a n iterates make a n-1 times.

k is a global variable for generating names of internally generated variables.

Theory identifiers.

linenumber used by lexer and parser.

Printing lists in Ocaml syntax.

For canonical a, b, make a b returns a canonical term c with AC |= c = a * b.

For canonical a, b, make a b returns a canonical term c with AC |= c = a * b.

map f a applies f to all top-level uninterpreted subterms of a, and rebuilds the interpreted parts in order.

map f a applies f at uninterpreted positions of a an builds a canonical term from the results.

Printing of a list of pairs as a finite map.

Applying a term transformer at all uninterpreted positions map f (mk_select a j) equals mk_select (map f a) (map f j), map f (mk_update a i x) equals mk_select (map f a) (map f i) (map f x), Otherwise, map f x equals f x

map f a homomorphically applies f at uninterpreted positions of a and returns the corresponding canonical term.

map f a applies f to all top-level uninterpreted subterms of a, and rebuilds the interpreted parts in order.

Applying a term transformer f at uninterpreted positions.

map f a applies the term transformer f to each uninterpreted subterm of a and rebuilds the term a by using the simplifying constructors mk_apply and mk_abs.

map f a applies f at uninterpreted positions and recanonizes the result.

map f a applies f at uninterpreted positions and recanonizes the result.

mapargs app f a maps f op over the arguments al of an application a of the form op(al).

Mapping over list of terms.

maximize c a returns either (b, rho) such that b+ is empty and rho |- la => a = b, or, raises La.Unbounded if a is unbounded in the linear arithmetic la equality set of c.

mem i jl tests if i is in jl.

mem q d tests if the rational q is an element of the denotation of d.

Adding a variable equality x = y by destructively updating context s.

merge e s adds a new variable equality e of the form x = y into the partition s.

merge e s propagates an equality e of the form x = y into the disequality context by computing a new disequality context which is equal to s except that every x has been replaced by y.

(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.

Minimize is the dual of maximize.

mk_add a b constructs the normalized linear arithmetic term for the sum of a and b.

mk_addl iterates Arith.mk_add as follows: mk_addl [] is mk_zero, mk_addl [a] is a, mk_addl [a0;...;an] is mk_add a0 (mk_addl [a1;...;an])

mk_addq q a creates the normalized linear arithmetic term representing q + a.

mk_app f l constructs a function application of symbol f to a list l.

mk_apply c a al builds an application with range type c by applying term a to an argument term b.

Given a canonical term a, mk_car a constructs a canonical term for representing the first projection on a.

Given a canonical term a, mk_cdr a constructs a canonical term for representing the second projection on a.

mk_conc n m b1 b2 concatenates a bitvector b1 of width n and a bitvector b2 of width m.

Given canonical terms a, b, mk_cons a b constructs a canonical term for representing a pair of a and b.

mk_const c constructs a function application of symbol c to the empty argument list.

Construct hashconsed "constant" variables

mk_const c is the constructor for building constant bitvectors, in which all bits are known to be either 0 or 1.

Creating constant array.

mk_decr a creates the normalized linear arithmetic term representing a - 1.

The atom-index pair mk_diseq (a, b) represents the disequality a <> b.

mk_eps is the constant bitvector of length 0.

The atom-index pair mk_equal (a, b) represents the equality a = b.

mk_external n d creates an external variable with associated name n and optional domain constraint d.

Atom-index pair for representing the false atom.

mk_fresh th i d creates a fresh variable associated with theory i and optional domain d.

mk_fresh th None d creates a theory-specific fresh variable with optional domain restriction d, and mk_fresh th Some(i) d creates the theory-specific fresh variable of index i with optional domain restriction d.

mk_incr a creates the normalized linear arithmetic term representing a + 1.

Generalized injection of the form inr(inr(....(inr(x)))) with x uninterpreted or of the form inr(y).

For canonical a, mk_inl a constructs a canonical term for representing inl(a)

For canonical a, mk_inr a constructs a canonical term for representing inr(a)

Constructing BDDs for conditional set constructor.

Constructing a term for representing a * b.

mk_multq q a creates the normalized linear arithmetic term representing q * a.

mk_neg a creates the normalized linear arithmetic term representing -a.

The atom-index pair mk_nonneg a represents the nonnegativity constraint a >= 0.

mk_num q creates a constant mk_app (num q) []

mk_one n is the constant one bitvector of length n

mk_one is mk_num Mpa.Q.one

Generalized coinjection: mk_out 0 a = mk_outl a, mk_out 1 a = mk_outr a, mk_out i a = mk_outr (mk_out (i - 1) x) if i > 1, Otherwise, the value of mk_out is unspecified.

For canonical a, mk_outl a constructs a canonical term for representing outl(a)

For canonical a, mk_outr a constructs a canonical term for representing outr(a)

The atom-index pair mk_nonneg a represents the positivity constraint a > 0.

mk_proj i a projects the term ai in a tuple of the form (a1, ((a2, ...)...), an).

mk_rename n d constructs a rename variable with associated name "n!i" and optional domain constraint.

mk_rename n None constructs a fresh variable, where 'fresh' means that the index part of this fresh variable (see Module Term.Var) is larger than Term.Var.k; as a side-effect, Term.Var.k is incremented.

mk_select a j constructs a canonical term equivalent to App(select, [a; j]).

- mk_slack i Zero creates a zero slack variable with 0 as the only possible interpretation.

mk_slack None sl constructs a fresh slack variable, and mk_slack Some(i) sl construct a slack variable of index i.

mk_sub n i j x returns the representation of the bitvector for the contiguous extraction of the j-i+1 bits i through j in the bitvector x of length n.

mk_sub a b creates the normalized linear arithmetic term representing a - b.

Atom-index pair for representing the true atom.

For n > 0 canonical terms ai, 0 <= i <= n, mk_tuple [a1;a2;...;an] constructs a canonical representation of (a1, ((a2, ...)...), an).

mk_one is mk_num Mpa.Q.one

mk_update a x i constructs a canonical term equivalent to App(update, [a;x;i]).

mk_var n d constructs an external variable (see Var.mk_external) of name n and optional domain constraint d.

mk_zero n is just defined to be the constant zero bitvector of length n

mk_zero is mk_num Mpa.Q.zero

model (p, s) xs returns an assignment rho for the variables in xs with bindings x |-> q.

Model construction.

msg l name arg pp outputs a trace message if l is currently active by first outputting name followed by printing arg using the pp printer.

multiplicity x a counts the number of interpreted occurrences of x in a.

multiplicity x a counts the number of interpreted occurrences of x in a.

name_of x returns the name associated with a variable x.

name_of a returns the name n if a is a variable of the form Var(n); otherwise the result is undefined.

nat2bitv n i returns the a bitvector of length n representing the unsigned interpretation of the nonnegative integer i.

negate f atm ...

If a is of the form q + a1 + ... + an, then nonconstant_of a returns the list of monomials [a1; ...; an]

If a is of the form q + a', then nonconstant_of a returns a'

nonneg d constructs Nonneg(d).

(g, a >= 0; e; p) ==> (g; e'; p') with a pure, |= e', p' <=> |= e, a >= 0, p, if e' |= x = y then p' |= x = y.

Above is identical to Infsys.EQ.

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

occurs a b holds if term a occurs in b.

Construct an atom-index pair with unique index from an atom.

of_index n returns an atom-index pair of index n if such and atom-index pair has been created since the last Tools.do_at_reset.

of_q q returns Int if the rational q is an integer, and Real otherwise.

of_string n returns theory identifier i if to_string i equals to n; otherwise the result is undefined.

of_string s constructs a name with associated string s.

orient (a, b) is (b, a) if b is greater than a, and (a, b) otherwise.

Returns i if argument is of the form Some(i), and raises Not_found otherwise.

p_of s returns the partitioning associated with s.

(g, a > 0; e; p) ==> (g; e'; p') with a pure, |= e', p' <=> |= e, a > 0, p, if e' |= x = y then p' |= x = y.

Pretty-printer for variables.

Pretty-printing

Pretty-printing

Pretty-printing theories.

Pretty-printing of terms.

Pretty-printing applications of symbols to an argument list.

Pretty-printing a partitioning.

Pretty-printing of names.

Pretty-printing a solution set.

Print a partitioned version of s.

Pretty-printing configurations.

Pretty-printing input facts.

Pretty-printing the atom of a justification.

Pretty-printing.

Pretty-printing the context of a state.

Pretty-printing of combined equality set.

Pretty-printing an atom.

Pretty-printing of an individual equality set.

Fact.pp prints justification only if this flag is set to true.

proc l name pp f is just func l name pp Pretty.unit f.

Given a starting configuration ({fct}, e, p), process applies all rules of the combined inference system (except branching rules).

profile str f profiles function f, and registers an exit function which outputs the number of calls of this function, and the total time spent in this function; the argument str is usually just the name of the function.

(g, e; p) ==> (g; e'; p) with e |= x = y, , notp |= x = y, , |= e, p <=> |= e', p'

(g; e; p) ==> (g; e'; p') with p' |= x <> y, |= e', p' <=> |= e, p.

put fct g adds fact fct to g.

put_clause g adds a clause cl to g.

solve e solves the equation e of the form a = b over the rationals.

Set of removable variables.

remove l deactivates the trace level l.

replace e g with e of the form x = a replaces occurrences of a in g with x.

Reset the set of trace levels to the empty set, that is, all tracing is disabled.

restrict s x removes equalities of the form x = a in s.

might fail if already in use.

Printing of a list as a set.

Parameter settings for SAT solver

Canonizer.

sigma op l applies the function symbol op from the pair theory to the list l of argument terms to build a canonical term equal to op(l).

Array canonizer.

sigma op [a] applies mk_inl a if op is equal to the inl symbol.

Theory-specific canonizers.

Given a bitvector symbol f (see module Sym) and a list l of arguments, sigma f l returns a concatenation normal form (CNF) of the application 'f(l)'.

sigma op al applies the linear arithmetic function symbol to the list of arguments al such that the result is equal to App(op, al) in this theory and normalized if all terms in al are normalized.

Depending on the function symbol f, sigma f al uses the constructors Apply.mk_apply to compute the normal-form of applying f to the arguments al.

If f equals *, then sigma f [a1; a2] reduces to make a1 a2; otherwise the uninterpreted application f(a1, a2) is built.

If f equals *, then sigma f [a1; a2] reduces to make a1 a2; otherwise the uninterpreted application f(a1, a2) is built.

Simplification of atoms in a context (e, p) by canonizing component terms using Combine.can.

Solver

Given an equality a = b, the pair solver solve(a, b) raises the exception Exc.Inconsistent iff the equality a = b does not hold in P, or, returns a solved list of equalities x1 = a1;...;xn = an with xi variables in a or b, the xi are pairwise disjoint, and no xi occurs in any of the ai. The ai are all in canonical form, and they might contain newly generated variables (see Term.Var.mk_fresh).

solve [c1;...;cn] b yields a particular solution for a linear diophantine equation c0 * x0 + ... + cn * xn = b with nonzero, rational coefficients ci, for i = 1,...,n with n >= 1.

Given an equality a = b, solve(a, b) raises the exception Exc.Inconsistent iff the equality a = b does not hold in COP, or, returns a solved list of equalities x1 = a1;...;xn = an with xi variables in a or b, the xi are pairwise disjoint, and no xi occurs in any of the ai. The ai are all in canonical form, and they might contain newly generated variables (see Term.Var.mk_fresh).

Theory-specific solvers.

solve b either fails, in which case b is unsatisfiable in the given bitvector theory or it returns a list of equations [(x1,e1);...(xn,en)] such that xi is a non bitvector term, all the xi are pairwise disjoint, none of the xi occurs in any of the terms ej, and, viewed as a conjunction of equivalences, the result is equivalent (in the theory of bitvectors) with b.

Work in progress.

Statistics.

status a classifies term a into one of: variables, pure terms with all function symbols drawn from a single theory i, mixed terms. In this case, a maximal pure term is retured.

sub d e holds iff the denotation of d is a subset of the denotation of e.

subterm a b holds if a is a subterm of b.

sym_of a returns the function symbol f of an application a of the form App(f,_).

theory_of a returns the theory associated with the top-level function symbol of a, and raises Not_found otherwise.

theory_of f returns the theory of type Th.t associated with f.

to_list s builds up a list of equalities from the solved form s.

to_stderr pp transforms a printer to print on stdout.

to_stdout pp transforms a printer pp to print on stdout.

to_string i returns a name for theory i.

Pretty-printing a term to a string.

to_string pp transforms a printer to print on a string.

to_string n returns the string associated with n.

Pretty-printing an atom to a string.

to_three fcts p a accumulate facts in the result of p a in global variable fcts and returns a corresponding result of type Three.t.

Projections to individual equality sets.

union u v evaluates to w if both is_sub u w and is_sub v w holds.

union d1 d2 returns d iff the denotation d is the union of the denotations of d1 and d2.

update s e updates s with a new equality of the form, say, x = a.

upper s a returns either (b, rho) such that b+ is empty and rho |- a = b, or, raises Unbounded if a is unbounded in s.

upper_of s returns an upper bound on the indices of all fresh variables in s.

utime f a returns not only the result of applying f to a but also the time required to compute the function.

Accessing the variable equalities of a partitioning.

Return set of variables.

vars_of atm collects all variables in atm.

Version and build date of current ICS version.

Computes the width of a bitvector term, and returns None if the argument is not an application of a bitvector symbol

width_of x returns the length n of variable x with a bitvector interpretation, and raises Not_found otherwise.

with_of x returns the length of the bitvector interpretation of x, or raises Not_found.

Neutral element of addition.

Solution for a linear diophantine equation.