Module Term

module Term: sig .. end
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 Term.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 Term.mk_true, Term.mk_num etc. to construct terms. An exception will be raised if an incorrectly typed term is constructed.
Author(s): Christoph Sticksel



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: Hashtbl.S  with type key = t
Hash table over terms
module TermSet: Set.S  with type elt = t
Set over terms
module TermMap: Map.S  with type 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 Term.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_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_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 Term.mk_named, which will create a unique name.

The namespace "t" will be rejected, because this is the namespace used by Term.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 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 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 : 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 : 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 (NoneNone) 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