Index of values

Assert a constraint that can be later retracted.

Assert a constraint in the logical context.

Assert a constraint in the logical context with weight w.

Check if the logical context is satisfiable.

del_context ctx deletes the given logical context.

Delete the given logical context.

Display the given model in the standard output.

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

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

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

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

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

Evaluate a formula in a model.

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

get_arith_value m v returns the rational value as a pair (numerator, denominator)

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.

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

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

Alias of Yices.get_bitvector_value.

Return the cost of model m.

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

get_double_value m v converts the value assigned to variable v in model m to a floating point number and returns it.

get_int_value m v returns the integer value assigned to variable v in model m

Get the Lite context out of a Full context.

Return a model for a satisfiable logical context.

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

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

Get the unsat core as an array.

get_value m v returns the assignment for the variable v.

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

get_var_decl_from_name ctx name returns a variable declaration associated with the given name.

get_var_decl_name d returns a name of a variable declaration.

Check whether the logical context is known to be inconsistent.

Return true if the given logical context is inconsistent.

Given on yices-help by Bruno Dutertre (2009-12-16)

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

Compute the maximal satisfying assignment for the asserted weighted constraints.

Similar to Yices.max_sat, but start looking for models with cost less than of equal to max_cost.

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

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

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

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

mk_bool_var_decl ctx name returns a new boolean variable declaration.

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

mk_bv_add ctx a1 a2 Bitvector addition

mk_bv_and ctx a1 a2 Bitwise and

mk_bv_concat ctx a1 a2 Bitvector concatenation

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

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

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

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

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

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

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

mk_bv_minus ctx a1 Bitvector opposite

mk_bv_mul ctx a1 a2 Bitvector multiplication

mk_bv_not ctx a Bitwise negation

mk_bv_or ctx a1 a2 Bitwise or

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

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

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

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

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

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

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

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

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

mk_bv_sub ctx a1 a2 Bitvector subtraction

Alias of Yices.mk_bv_type

mk_bv_xor ctx a1 a2 Bitwise exclusive or

mk_context () creates a logical context.

Create a logical context.

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

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

mk_false ctx returns an expression representing false.

mk_fresh_bool_var ctx returns a fresh boolean variable.

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

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

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

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

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

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

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

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

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

mk_num ctx n returns an expression representing the given integer.

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

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

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

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

mk_true ctx returns an expression representing true.

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

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

mk_type ctx name returns the type associated with the given name.

mk_var_decl ctx name type returns a new (global) variable declaration.

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

parse_command ctx s parses and executes the command in string s.

parse_expression ctx s parses string s as a Yices expression and return the expression.

parse_type ctx s parses string s as a Yices type and return the type.

Backtrack.

Pretty print the given expression in the standard output.

Create a backtracking point in the given logical context.

Process the given command in the given logical context.

reset ctx resets the given logical context.

Retract a retractable or weighted constraint.

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

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

Set the maximum number of iterations in the MaxSAT algorithm.

Set the initial cost for a maxsat problem.

Set the file that will store the output produced by yices (e.g., models).

Set the verbosity level.

Set the verbosity level

Return the Yices version number.

Return the yices version number