package yices2

Context configuration

         name    |    value            |      meaning
----------------------------------------------------------------------------------------
         "mode"  | "one-shot"          |  only one call to check is supported
                 |                     |
                 | "multi-checks"      |  several calls to assert and check are
                 |                     |  possible
                 |                     |
                 | "push-pop"          |  like multi-check and with support for
                 |                     |  retracting assertions (via push/pop)
                 |                     |
                 | "interactive"       |  like push-pop, but with automatic context clean
                 |                     |  up when search is interrupted.
----------------------------------------------------------------------------------------
 "uf-solver"     | "default"           |  the uf-solver is included (i.e., the egraph)
                 | "none"              |  no uf-solver
----------------------------------------------------------------------------------------
 "bv-solver"     | "default"           |  the bitvector solver is included
                 | "none"              |  no bitvector solver
----------------------------------------------------------------------------------------
 "array-solver"  | "default"           |  the array solver is included
                 | "none"              |  no array solver
----------------------------------------------------------------------------------------
 "arith-solver"  | "ifw"               |  solver for IDL, based on the Floyd-Warshall
                 |                     |  algorithm
                 |                     |
                 | "rfw"               |  solver for RDL, based on Floyd-Warshall
                 |                     |
                 | "simplex"           |  solver for linear arithmetic, based on Simplex
                 |                     |
                 | "default"           |  same as "simplex"
                 |                     |
                 | "auto"              |  same as "simplex" unless mode="one-shot" and
                 |                     |  logic is QF_IDL or QF_RDL, in which case the
                 |                     |  solver is determined after the first call to
                 |                     |  yices_assert_formula(s).
                 |                     |
                 | "none"              |  no arithmetic solver
----------------------------------------------------------------------------------------
"arith-fragment" | "IDL"               |  integer difference logic
                 | "RDL"               |  real difference logic
                 | "LIA"               |  linear integer arithmetic
                 | "LRA"               |  linear real arithmetic
                 | "LIRA"              |  mixed linear arithmetic (real + integer variables)