Module Term

Term representation

Terms are hashconsed for maximal sharing, comparison with physical equality and to store type information.

Terms are lambda trees, see Ltree, with symbols of type Symbol.t, free variables of type Var.t and types Type.t.

The type t is private and cannot be constructed outside this module in order to ensure that all equal subterms are physically equal for hashconsing.

Use the constructor functions like mk_true, mk_num etc. to construct terms. An exception will be raised if an incorrectly typed term is constructed.

author
Christoph Sticksel, Arjun Viswanathan

Types and hash-consing

module T : Ltree.S with type symbol = Symbol.t and type var = Var.t and type sort = Type.t
type t = T.t

Terms are hashconsed abstract syntax trees

type lambda = T.lambda

Terms are hashconsed abstract syntax trees

Hashtables, maps and sets

val compare : t -> t -> int

Comparison function on terms

val equal : t -> t -> bool

Equality function on terms

val hash : t -> int

Hashing function on terms

val tag : t -> int

Unique identifier for terms

module TermHashtbl : Stdlib.Hashtbl.S with type TermHashtbl.key = t

Hash table over terms

module TermSet : Stdlib.Set.S with type TermSet.elt = t

Set over terms

module TermMap : Stdlib.Map.S with type TermMap.key = t

Map over terms

Constructors

val mk_term : T.t_node -> t

Create a hashconsed term

val mk_lambda : Var.t list -> t -> lambda

Create a hashconsed lambda expression

val import : t -> t

Import a term from a different instance into this hashcons table

val import_lambda : lambda -> lambda

Import a term from a different instance into this hashcons table

val is_lambda_identity : lambda -> bool

Returns true if the lamda expression is the identity, i.e. lambda x.x

val mk_true : unit -> t

Create the propositional constant true

val mk_false : unit -> t

Create the propositional constant false

val mk_not : t -> t

Create an Boolean negation

Hint: consider using negate to avoid double negations

val mk_implies : t list -> t

Create a Boolean implication

val mk_and : t list -> t

Create an Boolean conjunction

val mk_or : t list -> t

Create an Boolean disjunction

val mk_xor : t list -> t

Create an Boolean exclusive disjunction

val mk_eq : t list -> t

Create an equality

val mk_distinct : t list -> t

Create an pairwise distinct predicate

val mk_ite : t -> t -> t -> t

Create an if-then-else term

val mk_num : Numeral.t -> t

Create an integer numeral

val mk_num_of_int : int -> t

Create an integer numeral

val mk_constr : string -> t

Create a constructor encoded as a numeral

val mk_dec : Decimal.t -> t

Create a floating point decimal

val mk_ubv : Bitvector.t -> t

Create a constant unsigned bitvector

val mk_bv : Bitvector.t -> t

Create a constant bitvector

val mk_bvadd : t list -> t

Create a signed bitvector sum

val mk_bvsub : t list -> t

Create a signed bitvector difference

val mk_bvmul : t list -> t

Create a bitvector produce

val mk_bvudiv : t list -> t

Create a bitvector division

val mk_bvsdiv : t list -> t

Create a signed bitvector division

val mk_bvurem : t list -> t

Create a bitvector modulus

val mk_bvsrem : t list -> t

Create a signed bitvector modulus

val mk_bvand : t list -> t

Create a bitvector conjunction

val mk_bvor : t list -> t

Create a bitvector disjunction

val mk_bvnot : t -> t

Create a bitwise negation

val mk_bvneg : t -> t
val mk_bvshl : t list -> t

Create a bitvector left shift

val mk_bvlshr : t list -> t

Create a bitvector logical right shift

val mk_bvashr : t list -> t

Create a bitvector arithmetic right shift

val mk_bvult : t list -> t

Create an unsigned bitvector less-than comparison

val mk_bvule : t list -> t

Create an unsigned bitvector less-than-or-equal-to comparison

val mk_bvugt : t list -> t

Create an unsigned bitvector greater-than comparison

val mk_bvuge : t list -> t

Create an unsigned bitvector greater-than-or-eqaul-to comparison

val mk_bvslt : t list -> t

Create a bitvector less-than comparison

val mk_bvsle : t list -> t

Create a bitvector less-than-or-equal-to comparison

val mk_bvsgt : t list -> t

Create a bitvector greater-than comparison

val mk_bvsge : t list -> t

Create a bitvector greater-than=or-eqaul-to comparison

val mk_minus : t list -> t

Create an integer or real difference

val mk_plus : t list -> t

Create an integer or real sum

val mk_times : t list -> t

Create an integer or real product

val mk_div : t list -> t

Create a real quotient

val mk_intdiv : t list -> t

Create an integer quotient

val mk_mod : t -> t -> t

Create an integer modulus

val mk_abs : t -> t

Create an absolute value

val mk_leq : t list -> t

Create a less-or-equal predicate

val mk_lt : t list -> t

Create a less-than predicate

val mk_geq : t list -> t

Create a greater-or-equal predicate

val mk_gt : t list -> t

Create a greater-than predicate

val mk_to_real : t -> t

Create a conversion to a real decimal

val mk_to_int : t -> t

Create a conversion to an integer numeral

val mk_to_uint8 : t -> t

Create a conversion to an unsigned integer8 numeral

val mk_to_uint16 : t -> t

Create a conversion to an unsigned integer16 numeral

val mk_to_uint32 : t -> t

Create a conversion to an unsigned integer32 numeral

val mk_to_uint64 : t -> t

Create a conversion to an unsigned integer64 numeral

val mk_to_int8 : t -> t

Create a conversion to an integer8 numeral

val mk_to_int16 : t -> t

Create a conversion to an integer16 numeral

val mk_to_int32 : t -> t

Create a conversion to an integer32 numeral

val mk_to_int64 : t -> t

Create a conversion to an integer64 numeral

val mk_bv2nat : t -> t

Create a bitvector to nat conversion

val mk_bvextract : Numeral.t -> Numeral.t -> t -> t

Create a BV extraction

val mk_bvconcat : t -> t -> t

Create a BV concatenation

val mk_bvsignext : Numeral.t -> t -> t

Create a BV sign extension

val mk_is_int : t -> t

Create a predicate for coincidence of a real with an integer

val mk_divisible : Numeral.t -> t -> t

Create a predicate for divisibility by a constant integer

val mk_select : t -> t -> t

Create select from an array at a particular index

val mk_store : t -> t -> t -> t

Functionnaly update an array at a given index

val mk_named : t -> int * t

Uniquely name a term with an integer and return a named term and its name

val mk_named_unsafe : t -> string -> int -> t

Name term with the given integer in a given namespace

This is a basic function, the caller has to generate the name, and ensure the name is used only once. Use with caution, or better only use mk_named, which will create a unique name.

The namespace "t" will be rejected, because this is the namespace used by mk_named.

val mk_uf : UfSymbol.t -> t list -> t

Create an uninterpreted constant or function

val mk_var : Var.t -> t

Create a symbol to be bound to a term

val mk_let : (Var.t * t) list -> t -> t

Create a binding of symbols to terms

val mk_exists : ?⁠fundef:bool -> Var.t list -> t -> t

Return a hashconsed existentially quantified term

val mk_forall : ?⁠fundef:bool -> Var.t list -> t -> t

Return a hashconsed universally quantified term

Constant terms

val t_true : t

The propositional constant true

val t_false : t

The propositional constant false

Prefix and infix operators for term construction

module Abbrev : sig ... end

Additional term constructors

val mk_bool : bool -> t

Create the propositional constant true or false

val mk_const_of_symbol_node : Symbol.symbol -> t

Create a constant

val mk_const : Symbol.t -> t

Create constant of a hashconsed symbol

val mk_app_of_symbol_node : Symbol.symbol -> t list -> t

Create a function application

val mk_app : Symbol.t -> t list -> t

Create a function application of a hashconsed symbol

val mk_succ : t -> t

Increment integer or real term by one

val mk_pred : t -> t

Decrement integer or real term by one

val negate : t -> t

Negate term, avoiding double negation

val mk_minus_simplify : t -> t
val negate_simplify : t -> t

Negates a term by modifying the top node if it is a not, true, false, or an arithmetic inequality.

val unnegate : t -> t

Remove top negation from term, otherwise return term unchanged

Accessor functions

val type_of_term : t -> Type.t

Return the type of the term

val node_of_term : t -> T.t_node

Return the node of the hashconsed term

val destruct : t -> T.flat

Flatten top node of term

val has_quantifier : t -> bool

Returns true if the term has quantifiers

val construct : T.flat -> t

Convert a flat term to a term

val is_atom : t -> bool

Return true if the term is a simple Boolean atom, that is, has type Boolean and does not contain subterms of type Boolean

val is_negated : t -> bool

Return true if the top symbol of the term is a negation

val is_free_var : t -> bool

Return true if the term is a free variable

val free_var_of_term : t -> Var.t

Return the variable of a free variable term

val is_bound_var : t -> bool

Return true if the term is a bound variable

val is_leaf : t -> bool

Return true if the term is a leaf symbol

val leaf_of_term : t -> Symbol.t

Return the symbol of a leaf term

val is_node : t -> bool

Return true if the term is a function application

val node_symbol_of_term : t -> Symbol.t

Return the symbol of a function application

val node_args_of_term : t -> t list

Return the arguments of a function application

val is_let : t -> bool

Return true if the term is a let binding

val is_exists : t -> bool

Return true if the term is an existential quantifier

val is_forall : t -> bool

Return true if the term is a universal quantifier

val is_named : t -> bool

Return true if the term is a named term

val term_of_named : t -> t

Return the term of a named term

val name_of_named : t -> int

Return the name of a named term

val is_numeral : t -> bool

Return true if the term is an integer constant

val numeral_of_term : t -> Numeral.t

Return integer constant of a term

val bitvector_of_term : t -> Bitvector.t

Return bitvector constant of a term (sign-agnostic)

val sbitvector_of_term : t -> Bitvector.t

Return signed bitvector constant of a term

val ubitvector_of_term : t -> Bitvector.t

Return unsigned bitvector constant of a term

val is_bitvector : t -> bool

Return true if the term is a (sign-agnostic) bitvector consant

val is_sbitvector : t -> bool

Return true if the term is a signed bitvector constant

val is_ubitvector : t -> bool

Return true if the term is an unsigned bitvector constant

val is_decimal : t -> bool

Return true if the term is a decimal constant

val decimal_of_term : t -> Decimal.t

Return decimal constant of a term

val is_bool : t -> bool

Return true if the term is a Boolean constant

val bool_of_term : t -> bool

Return Boolean constant of a term

val is_select : t -> bool

Return true if the term is an application of the select operator

val is_store : t -> bool

Return true if the term is an application of the store operator

val is_ite : t -> bool

Return true if the term is an application of the ite operator

val indexes_and_var_of_select : t -> Var.t * t list

Return the indexes and the array variable of the select operator

The array argument of a select is either another select operation or a variable. For the expression (select (select A j) k) return the pair A and [j; k].

val array_and_indexes_of_select : t -> t * t list
val var_of_select_store : t -> Var.t

Pretty-printing

val pp_print_term : Stdlib.Format.formatter -> t -> unit

Pretty-print a term

val print_term : t -> unit

Pretty-print a term to the standard formatter

val string_of_term : t -> string

Return a string representation of a term

val pp_print_lambda : Stdlib.Format.formatter -> lambda -> unit

Pretty-print a lambda abstraction

val print_lambda : lambda -> unit

Pretty-print a lambda abstraction to the standard formatter

val string_of_lambda : lambda -> string

Return a string representation of a lambda abstraction

Conversions

val eval_t : ?⁠fail_on_quantifiers:bool -> (T.flat -> 'a list -> 'a) -> t -> 'a

Evaluate the term bottom-up and right-to-left. The evaluation function is called at each node of the term with the the term being evaluated, and the list of values computed for the subterms. Let bindings are lazily unfolded.

val eval_lambda : lambda -> t list -> t

Beta-evaluate a lambda expression

val partial_eval_lambda : lambda -> t list -> lambda

Partialy Beta-evaluate a lambda expression

val map : (int -> T.t -> T.t) -> t -> t

Tail-recursive bottom-up right-to-left map on the term

Not every subterm is a proper term, since the de Bruijn indexes are shifted. Therefore, the function f is called with the number of let bindings the subterm is under as first argument, so that the indexes can be adjusted in the subterm if necessary.

val apply_subst : (Var.t * t) list -> t -> t

Apply a substitution variable -> term

val map_state_vars : (StateVar.t -> StateVar.t) -> t -> t

Return a new term with each state variable replaced

map_state_vars t f returns a new term of t with each occurring state variable s replaced by the result of the evaluation f s.

val map_vars : (Var.t -> Var.t) -> t -> t

Return a new term with each variable instance replaced

val mod_to_divisible : t -> t

Convert (= 0 (mod t n)) to (divisble n t)

The term n must be an integer numeral.

val divisible_to_mod : t -> t

Convert (divisble n t) to (= 0 (mod t n))

val nums_to_pos_nums : t -> t

Convert negative numerals and decimals to negations of their absolute value

val bump_state : Numeral.t -> t -> t

Add to offset of state variable instances

Negative values are allowed

val bump_and_apply_k : (t -> unit) -> Numeral.t -> t -> unit

Apply function to term for instants 0..k

val state_vars_of_term : t -> StateVar.StateVarSet.t

Return the state variables occurring in the term

val vars_of_term : t -> Var.VarSet.t

Return the variables occurring in the term

val state_vars_at_offset_of_term : Numeral.t -> t -> StateVar.StateVarSet.t

Return the state variables at given offset in term

val vars_at_offset_of_term : Numeral.t -> t -> Var.VarSet.t

Return the state variables at given offset in term

val var_offsets_of_term : t -> Numeral.t option * Numeral.t option

Return the minimal and maximal offset of state variable instances

Return (None, None) if there are no state variable instances in the term.

Arrays

val select_symbols_of_term : t -> Symbol.SymbolSet.t

Return the select symbols occurring in the term

val select_terms : t -> TermSet.t

Return the terms of the form (select ...) that appear in a term

val convert_select : t -> t

Convert terms of the form (select (select a i) j) to (select a i j) for multi-dimensional arrays

val partial_selects : t -> t * UfSymbol.t list

Use fresh function symbols to encode partial select applications and add constraint that forall i, fresh a i = select a i, returns the modified term and the list of new fresh symbols to declare. This is only useful when using the fun-rec option of CVC4, it does nothing otherwise.

val reinterpret_select : t -> t

Inverse transformation of !convert_select

val indexes_of_state_var : StateVar.t -> t -> t list list

Return (array) indexes of a state variable appearing in a term

Statistics

val stats : unit -> int * int * int * int * int * int

return statistics of hashconsing