package yices2

  1. Overview
  2. Docs

Context

module Config : sig ... end

Context configuration

val create : ?config:config -> unit -> context

Create a context

val status : context -> status

Get status.

Options

  • var-elim: whether to eliminate variables by substitution
  • arith-elim: more variable elimination for arithmetic (Gaussian elimination)
  • bvarith-elim: more variable elimination for bitvector arithmetic
  • eager-arith-lemmas: if enabled and the simplex solver is used, the simplex solver will eagerly generate lemmas such as (x >= 1) => (x >= 0) (i.e., the lemmas that involve two inequalities on the same variable x).
  • flatten: whether to flatten nested (or ...). If this is enabled the term (or (or a b) (or c d) ) is flattened to (or a b c d).
  • learn-eq: enable/disable heuristics to learn implied equalities
  • keep-ite: whether to eliminate term if-then-else or keep them as terms - this requires the context to include the egraph
  • break-symmetries: attempt to detect symmetries and add constraints to remove them (this can be used only if the context is created for QF_UF)
  • assert-ite-bounds: try to determine upper and lower bound on if-then-else terms and assert these bounds. For example, if term t is defined as (ite c 10 (ite d 3 20)), then the context with include the assertion 3 <= t <= 20.
val enable_option : context -> string -> unit

Enable option

val disable_option : context -> string -> unit

Disable option

Formula assertion

val assert_formula : context -> term -> unit

Assert a single formula

val assert_formulas : context -> term array -> unit

Assert multiple formulae

Assertion stack operations

val reset : context -> unit

Reset context, i.e. remove all assertions.

val push : context -> unit

Push, i.e. mark a backtrack point.

val pop : context -> unit

Pop, i.e. remove all assertions up to last backtrack point.

module Params : sig ... end

Check parameters

val check : ?params:params -> context -> status

Check satisfiability.

val assert_blocking_clause : context -> unit

Add a blocking clause, i.e. a clause that ask for another model.

Interrupt a search.

val get_model : ?keepsubst:bool -> context -> model

Get model (should be called after check).

OCaml

Innovation. Community. Security.