Module Yices

module Yices: sig .. end

type context 

type typ 

type expr 

type var_decl 

type model 

type assertion_id = int 

type lbool = 

type var_decl_iterator 

type unsat_core = assertion_id array 

val version : unit -> string

Return the Yices version number.

val set_verbosity : int -> unit

Set the verbosity level.

val enable_type_checker : bool -> unit

Force Yices to type check expressions when they are asserted (default = false).

val enable_log_file : string -> unit

Enable a log file that will store the assertions, checks, decls, etc.

If the log file is already open, then nothing happens.
Raises Failure if either:

• there's already a log file
• if the file cannot be opened for write (or some other file error)

val set_arith_only : bool -> unit

Inform yices that only arithmetic theory is going to be used.

This flag usually improves performance (default = false).

val set_max_num_conflicts_in_maxsat_iteration : int -> unit

Set the maximum number of conflicts that are allowed in a maxsat iteration.

If the maximum is reached, then "unknown" (i.e., Undef) is returned by maxsat.

val set_max_num_iterations_in_maxsat : int -> unit

Set the maximum number of iterations in the MaxSAT algorithm.

If the maximum is reached, then "unknown" (i.e., Undef) is returned by maxsat.

val set_maxsat_initial_cost : int64 -> unit

Set the initial cost for a maxsat problem.

val mk_context : unit -> context

mk_context () creates a logical context.

val del_context : context -> unit

del_context ctx deletes the given logical context.

See Yices.mk_context.

val reset : context -> unit

reset ctx resets the given logical context.

val dump_context : context -> unit

Display the internal representation of the given logical context on stderr.

This function is mostly for debugging.

val push : context -> unit

Create a backtracking point in the given logical context.

The logical context can be viewed as a stack of contexts. The scope level is the number of elements on this stack. The stack of contexts is simulated using trail (undo) stacks.

val pop : context -> unit

Backtrack.

Restores the context from the top of the stack, and pops it off the stack. Any changes to the logical context (by Yices.assert_simple or other functions) between the matching Yices.push and pop operators are flushed, and the context is completely restored to what it was right before the Yices.push.

See Yices.push.

val assert_simple : context -> expr -> unit

Assert a constraint in the logical context.

After one assertion, the logical context may become inconsistent. The method Yices.inconsistent may be used to check that.

val assert_weighted : context -> expr -> int64 -> assertion_id

Assert a constraint in the logical context with weight w.
Returns An id that can be used to retract the constraint.

See Yices.retract.

val assert_retractable : context -> expr -> assertion_id

Assert a constraint that can be later retracted.
Returns An id that can be used to retract the constraint.

This is similar to Yices.assert_weighted, but the weight is considered to be infinite.

See Yices.retract.

val retract : context -> assertion_id -> unit

Retract a retractable or weighted constraint.

See Yices.assert_weighted and Yices.assert_retractable.

val inconsistent : context -> int

Check whether the logical context is known to be inconsistent.

If the function returns true (i.e., a non-zero value) then the context is inconsistent. If it returns false (i.e., 0) then the context's status is unknown. To determine the status in this case, call Yices.check.

val check : context -> lbool

Check if the logical context is satisfiable.

• True means the context is satisfiable
• False means it is unsatisfiable
• Undef means it was not possible to decide due to an incompleteness.

If the context is satisfiable, then Yices.get_model can be used to obtain a model.

Warning! This method ignore the weights associated with the constraints.

val max_sat : context -> lbool

Compute the maximal satisfying assignment for the asserted weighted constraints.

• True means the maximal satisfying assignment was found
• False means it is unsatisfiable (this may happen if the context has unweighted constraints)
• Undef means it was not possible to decide due to an incompleteness.

If the result is True, then Yices.get_model can be used to obtain a model.

See Yices.assert_weighted

val max_sat_cost_leq : context -> int64 -> lbool

Similar to Yices.max_sat, but start looking for models with cost less than of equal to max_cost.
Returns False if such a model doesn't exist.

val find_weighted_model : context -> bool -> lbool

find_weighted_model ctx random searches for a model of the constraints asserted in ctx and compute its cost.

If random is true, then random search is used, otherwise, the default decision heuristic is used.

If there are no weighted constaints in ctx, then this function is the same as Yices.check.

Otherwise, it searches for a model that satisfies all the non-weighted constraints but not necessarily the weighted constraints. The function returns True if such a model is found, and the model can be obtained using Yices.get_model. The cost of this model is the sum of the weights of the unsatisfied weighted constraints.

The function returns False if it cannot find such a model.

The function may also return Undef, if the context contains formulas for which yices is incomplete (e.g., quantifiers). Do not use the model in this case.

val get_unsat_core : context -> unsat_core

Get the unsat core as an array.

Each element is the id of a retractable assertion.

See Yices.assert_retractable.

val get_model : context -> model

Return a model for a satisfiable logical context.

Warning!

• The should be only called if Yices.check or Yices.max_sat returned True or Undef.
• Calls to functions which modify the context invalidate the model.

Raises Failure if the model is not available

val get_value : model -> var_decl -> lbool

get_value m v returns the assignment for the variable v.

The result is Undef if the value of v is a "don't care".

Warning! v must be the declaration of a boolean variable.

See Yices.get_int_value, Yices.get_arith_value and Yices.get_double_value.

val get_int_value : model -> var_decl -> int32

get_int_value m v returns the integer value assigned to variable v in model m
Raises Failure if one of the following errors occurs:

• v is not a proper declaration or not the declaration of a numerical variable
• v has no value assigned in model m (typically, this means that v does not occur in the asserted constraints)
• v has a value that cannot be converted to long, because it is rational or too big

See Yices.get_value, Yices.get_arith_value and Yices.get_double_value.

val get_arith_value : model -> var_decl -> int32 * int32

get_arith_value m v returns the rational value as a pair (numerator, denominator)
Raises Failure if one of the following errors occurs:

• v is not a proper declaration or not the declaration of a numerical variable
• v has no value assigned in model m (typically, this means that v does not occur in the asserted constraints)
• v has a value that cannot be converted to long/long, because the numerator or the denominator is too big

See Yices.get_value, Yices.get_int_value and Yices.get_double_value.

val get_double_value : model -> var_decl -> float

get_double_value m v converts the value assigned to variable v in model m to a floating point number and returns it.
Raises Failure if one of the following errors occurs:

• v is not a proper declaration or not the declaration of a numerical variable
• v has no value assigned in model m (typically, this means that v does not occur in the asserted constraints)

See Yices.get_value, Yices.get_int_value and Yices.get_arith_value.

val get_arith_value_as_string : model -> var_decl -> string

get_arith_value_as_string m d converts the value assigned to a variable, given its variable declaration d in model m to a character string.

val get_ratio_value : model -> var_decl -> Ratio.ratio

val get_big_int_value : model -> var_decl -> Big_int.big_int

val get_bitvector_value : model -> var_decl -> int -> bool array

get_bitvector_value m v n gets the bitvector constant assigned to a variable v in model m.

It returns an array of n booleans: bv.(0) is the low-order bit and bv.(n - 1) is the high-order bit.

n should be the size of the bitvector variable v. Otherwise:

• If n is smaller than v's size, the n lower-order bits of v are returned.
• If n is larger than v's size, then the extra high-order bits are set to 0.

Raises Failure if one of the following errors occurs:

• v is not a proper declaration or not the declaration of a bitvector variable
• v has no value assigned in model m (typically, this means that v does not occur in the asserted constraints)

val get_bv_value : model -> var_decl -> int -> bool array

Alias of Yices.get_bitvector_value.

val get_scalar_value : model -> var_decl -> int

get_scalar_value m d gets the value assigned to a variable of scalar type in model m as an integer index.

If d is a variable declaration of a scalar type tau, then tau must have been defined as (define-type tau (scalar e_0 ... e_(n-1))) for some n>0.

This function returns the value of variable d in model m as an index between 0 and n-1 (i.e., if the function returns i then the value of d is e_i).
Raises Failure if one of the following error occurs:

• d is not the declaration of a scalar variable
• d is not assigned a value in model m

val get_scalar_value_name : model -> var_decl -> string

get_scalar_value_name m d gets the value assigned to a variable of scalar type in model m as a string.

If d is a variable declaration of a scalar type tau, then tau must have been defined as (define-type tau (scalar e_0 ... e_(n-1))) for some n>0.

This function returns the value of variable d in model m as one of the strings e_i.
Raises Failure if one of the following error occurs:

• d is not the declaration of a scalar variable
• d is not assigned a value in model m

val get_assertion_value : model -> assertion_id -> bool

Return true (false) if the assertion of the given assertion id is satisfied (not satisfied) in the model.

This function is only useful for assertion ids obtained using Yices.assert_weighted, and if Yices.max_sat was used to build the model. That is the only scenario where an assertion may not be satisfied in a model produced by yices.

val evaluate_in_model : model -> expr -> lbool

Evaluate a formula in a model.

Model can be obtained via Yices.get_model, after a call to Yices.check, Yices.max_sat, or Yices.find_weighted_model

• True means the formula is true in the model
• False means the formula is false in the model
• Undef means the model does not have enough information. typically this is due to a function application, e.g., the model defines (f 1) and (f 2), but the formula references (f 3)

val display_model : model -> unit

Display the given model in the standard output.

val get_cost : model -> int64

Return the cost of model m.

The cost is the sum of the weights of unsatisfied constraints.

Warning! The model cost is computed automatically by Yices.max_sat but not by Yices.check. If Yices.check returns True (or Undef), you can to call compute_model_cost to compute the cost explicitly. But this function does not seem to exist yet... MD

val get_cost_as_double : model -> float

Return the cost of the model m, converted to a double-precision floating point number.

val iter_bool_var_decl : (var_decl -> unit) -> context -> unit

(OCaml-specific) Applies a function to each boolean variable declarations of a given context.

val parse_expression : context -> string -> expr

parse_expression ctx s parses string s as a Yices expression and return the expression. The string must use the Yices input language (not SMT-LIB).

val parse_type : context -> string -> typ

parse_type ctx s parses string s as a Yices type and return the type. The string must uses the Yices input language (not SMT-LIB).

val parse_command : context -> string -> unit

parse_command ctx s parses and executes the command in string s. s must use the Yices input language.

val mk_type : context -> string -> typ

mk_type ctx name returns the type associated with the given name. If the type does not exist, a new uninterpreted type is created.

Remark: number, real, int, nat, bool, any are builtin types.

val number_type_name : string

val real_type_name : string

val int_type_name : string

val nat_type_name : string

val bool_type_name : string

val any_type_name : string

val mk_bitvector_type : context -> int -> typ

mk_bitvector_typ ctx size returns the bitvector type of the given size (bv size).

The size must be positive.

val mk_bv_type : context -> int -> typ

Alias of Yices.mk_bv_type

val mk_function_type : context -> typ array -> typ -> typ

mk_function_type ctx d r returns a function type (-> d1 ... dn r).

val mk_tuple_type : context -> typ array -> typ

mk_tuple_type ctx a constructs the tuple type (a0, ..., an).

val mk_bool_var_decl : context -> string -> var_decl

mk_bool_var_decl ctx name returns a new boolean variable declaration.
Raises Failure if a variable already exists with the same name.

Remark: Short for mk_var_decl ctx name (mk_type ctx "bool").

val mk_var_decl : context -> string -> typ -> var_decl

mk_var_decl ctx name type returns a new (global) variable declaration. It is an error to create two variables with the same name.

val get_var_decl_from_name : context -> string -> var_decl

get_var_decl_from_name ctx name returns a variable declaration associated with the given name.
Raises Failure if there is no variable declaration associated with the given name.

val get_var_decl : expr -> var_decl

get_var_decl e returns the variable declaration object associated with the given name expression.

Warning! e must be a name expression created using methods such as: Yices.mk_bool_var, Yices.mk_fresh_bool_var, or Yices.mk_bool_var_from_decl.

val get_var_decl_name : var_decl -> string

get_var_decl_name d returns a name of a variable declaration.

val mk_var_from_decl : context -> var_decl -> expr

mk_var_from_decl ctx d returns a name expression (instance) using the given variable declaration.

val mk_bool_var_from_decl : context -> var_decl -> expr

mk_bool_var_from_decl ctx d returns a name expression (instance) using the given variable declaration.

val mk_bool_var : context -> string -> expr

mk_bool_var ctx name returns a name expression for the given variable name.

mk_bool_var ctx n1 = mk_bool_var ctx n2 when n1 = n2.

See Yices.mk_bool_var_decl, Yices.mk_fresh_bool_var, Yices.mk_bool_var_from_decl.

val mk_fresh_bool_var : context -> expr

mk_fresh_bool_var ctx returns a fresh boolean variable.

val mk_true : context -> expr

mk_true ctx returns an expression representing true.

val mk_false : context -> expr

mk_false ctx returns an expression representing false.

val mk_or : context -> expr array -> expr

mk_or ctx args returns an expression representing the disjunction or of the given arguments (as an array).

Warning! the length of the array must be greater than 0.

val mk_and : context -> expr array -> expr

mk_and ctx args returns an expression representing the conjunction and of the given arguments (as an array).

Warning! the length of the array must be greater than 0.

val mk_not : context -> expr -> expr

mk_not ctx a returns an expression representing (not a).

val mk_eq : context -> expr -> expr -> expr

mk_eq ctx a1 a2 returns an expression representing a1 = a2.

val mk_diseq : context -> expr -> expr -> expr

mk_eq ctx a1 a2 returns an expression representing a1 /= a2.

val mk_ite : context -> expr -> expr -> expr -> expr

mk_ite ctx c t e returns an expression representing (if c t e) (if condition then then-value else else-value).

val mk_app : context -> expr -> expr array -> expr

mk_app ctx f a returns a function application term (f a1 ... an).

The type of f must be a function type, and its arity must be equal to the number of arguments, that is the size of the array a.

val mk_function_update : context -> expr -> expr array -> expr -> expr

mk_function_update ctx f a v returns a function update term (update f (a1 ... an) v).

The type of f must be a function type, and its arity must be equal to the number of arguments, that is the size of the array a.

val mk_tuple_literal : context -> expr array -> expr

mk_tuple_literal ctx a Build the tuple term (tuple a1 ... an).

val mk_num : context -> int -> expr

mk_num ctx n returns an expression representing the given integer.

val mk_num_from_string : context -> string -> expr

mk_num_from_string ctx n returns an expression representing the number provided in ASCII format.

val mk_sum : context -> expr array -> expr

mk_sum ctx arr returns an expression representing arr.(0) + ... + arr.(n).

Warning! Array.length arr must be greater than zero.

val mk_sub : context -> expr array -> expr

mk_sub ctx arr returns an expression representing arr.(0) - ... - arr.(n).

Warning! Array.length arr must be greater than zero.

val mk_mul : context -> expr array -> expr

mk_mul ctx arr returns an expression representing arr.(0) * ... * arr.(n).

Warning! Array.length arr must be greater than zero.

val mk_lt : context -> expr -> expr -> expr

mk_lt ctx a1 a2 returns an expression representing a1 < a2.

val mk_le : context -> expr -> expr -> expr

mk_le ctx a1 a2 returns an expression representing a1 <= a2.

val mk_gt : context -> expr -> expr -> expr

mk_gt ctx a1 a2 returns an expression representing a1 > a2.

val mk_ge : context -> expr -> expr -> expr

mk_ge ctx a1 a2 returns an expression representing a1 >= a2.

val mk_bv_constant : context -> int -> int32 -> expr

mk_bv_constant ctx size value creates a bit vector constant of size bits and from the given value.

size must be positive.

val mk_bv_constant_from_array : context -> bool array -> expr

mk_bv_constant ctx size bv creates a bit vector constant from an array of booleans bv.

Bit i of the bitvector is set to 0 if bv.(i) is false and to 1 if bv.(i) is true.

val mk_bv_add : context -> expr -> expr -> expr

mk_bv_add ctx a1 a2 Bitvector addition

a1 and a2 must be bitvector expression of same size.

val mk_bv_sub : context -> expr -> expr -> expr

mk_bv_sub ctx a1 a2 Bitvector subtraction

a1 and a2 must be bitvector expression of same size.

val mk_bv_mul : context -> expr -> expr -> expr

mk_bv_mul ctx a1 a2 Bitvector multiplication

a1 and a2 must be bitvector expression of same size. The result is truncated to that size too, e.g., multiplication of two 8-bit vectors gives an 8-bit result.

val mk_bv_minus : context -> expr -> expr

mk_bv_minus ctx a1 Bitvector opposite

a1 must be bitvector expression. The result is (- a1).

val mk_bv_concat : context -> expr -> expr -> expr

mk_bv_concat ctx a1 a2 Bitvector concatenation

a1 and a2 must be two bitvector expressions. a1 is the left part of the result and a2 the right part.

Assuming a1 and a2 have n1 and n2 bits, respectively, then the result is a bitvector concat of size n1 + n2. Bit 0 of concat is bit 0 of a2 and bit n2 of concat is bit 0 of a1.

val mk_bv_and : context -> expr -> expr -> expr

mk_bv_and ctx a1 a2 Bitwise and

a1 and a2 must be bitvector expression of same size.

val mk_bv_or : context -> expr -> expr -> expr

mk_bv_or ctx a1 a2 Bitwise or

a1 and a2 must be bitvector expression of same size.

val mk_bv_xor : context -> expr -> expr -> expr

mk_bv_xor ctx a1 a2 Bitwise exclusive or

a1 and a2 must be bitvector expression of same size.

val mk_bv_not : context -> expr -> expr

mk_bv_not ctx a Bitwise negation

val mk_bv_extract : context -> int -> int -> expr -> expr

mk_bv_extract ctx end begin a extracts a subvector from the bitvector a.

a must a bitvector expression of size n with begin < end < n. The result is the subvector from a[begin] to a[end].

val mk_bv_sign_extend : context -> expr -> int -> expr

mk_bv_sign_extend ctx a n returns the sign extension of the bitvector a to n bits.

Append n times the most-significant bit of a to the left of a.

val mk_bv_shift_left0 : context -> expr -> int -> expr

mk_bv_shift_left0 ctx a n Left shift by n bits, padding with zeros.

val mk_bv_shift_left1 : context -> expr -> int -> expr

mk_bv_shift_left1 ctx a n Left shift by n bits, padding with ones.

val mk_bv_shift_right0 : context -> expr -> int -> expr

mk_bv_shift_right0 ctx a n Right shift by n bits, padding with zeros.

val mk_bv_shift_right1 : context -> expr -> int -> expr

mk_bv_shift_right1 ctx a n Right shift by n bits, padding with ones.

val mk_bv_lt : context -> expr -> expr -> expr

mk_bv_lt ctx a1 a2 Unsigned comparison: (a1 < a2)

a1 and a2 must be bitvector expression of same size.

val mk_bv_le : context -> expr -> expr -> expr

mk_bv_le ctx a1 a2 Unsigned comparison: (a1 <= a2)

a1 and a2 must be bitvector expression of same size.

val mk_bv_gt : context -> expr -> expr -> expr

mk_bv_gt ctx a1 a2 Unsigned comparison: (a1 > a2)

a1 and a2 must be bitvector expression of same size.

val mk_bv_ge : context -> expr -> expr -> expr

mk_bv_ge ctx a1 a2 Unsigned comparison: (a1 >= a2)

a1 and a2 must be bitvector expression of same size.

val mk_bv_slt : context -> expr -> expr -> expr

mk_bv_slt ctx a1 a2 Signed comparison: (a1 < a2)

a1 and a2 must be bitvector expression of same size.

val mk_bv_sle : context -> expr -> expr -> expr

mk_bv_sle ctx a1 a2 Signed comparison: (a1 <= a2)

a1 and a2 must be bitvector expression of same size.

val mk_bv_sgt : context -> expr -> expr -> expr

mk_bv_sgt ctx a1 a2 Signed comparison: (a1 > a2)

a1 and a2 must be bitvector expression of same size.

val mk_bv_sge : context -> expr -> expr -> expr

mk_bv_sge ctx a1 a2 Signed comparison: (a1 >= a2)

a1 and a2 must be bitvector expression of same size.

val pp_expr : expr -> unit

Pretty print the given expression in the standard output.

module Future: sig .. end

Untested and potentially harmful features