======================================================================

 The Yices SMT Solver. Copyright 2014 SRI International.

 This program may only be used subject to the noncommercial end user
 license agreement which is downloadable along with this program.

======================================================================


YICES LANGUAGE

This is a summary of the commands and input language of the Yices 2 solver.


1) Lexical analysis
   ----------------

- comments start with ';' and extend to the end of the line ('\n' or EOF)

- tokens are ( ) :: <symbol> <string> <rational> <float> <binary bv> <hexa bv>

-  <strings> are similar to strings in C:

   - they are delimited by "
   - the characters \n, \t are replaced by newline and tab
   - '\' followed by at most 3 octal digits is replaced by the character
     whose ASCII code is the octal number
   - in all other cases, '\<char>' is replaced by <char> (including if <char> is newline)
   - newline cannot occur inside the string, unless preceded by '\'

- <rationals> are numbers in the format

        <optional_sign><digits>/<digits>
     or <optional_sign><digits>

- <floats> also denote numbers in a floating-point format

        <optional_sign> <digits> . <digits>
     or <optional_sign> <digits> <exp> <optional_sign> <digits>
     or <optional_sign> <digits> . <digits> <exp> <optional_sign> <digits>

   where <exp> is 'e' or 'E'


- <binary bvs> are bitvector constants in binary format 0b<binary-digits>

- <hexa bvs> are bitvector constants in hexadecimal format 0x<hexa-digits>


- <symbols>

    symbols start by anything that's not a digit, a space, or one of the
    characters ( ) ;  : "  if the first char is + or -, it must not be followed by a digit

    symbols end by a space of one of ( ) ; : "



  keywords
  --------

	bool	int	real	bitvector	scalar	tuple	->

	true	false	if	ite	=	/=	distinct
	or	and 	not	xor	<=>	=>	mk-tuple
	select	tuple-update	update 	forall	exists	lambda
	let

	+	-	*	/	^
	<	<=	>	>=

        abs     floor   ceil    div     mod     divides to-int

	mk-bv	bv-add	bv-sub	bv-mul	bv-neg  bv-pow
	bv-not	bv-and	bv-or	bv-xor	bv-nand	bv-nor	bv-xnor
	bv-shift-left0 	bv-shift-left1	bv-shift-right0	bv-shift-right1
	bv-ashift-right	bv-rotate-left	bv-rotate-right
	bv-extract	bv-concat	bv-repeat
	bv-sign-extend	bv-zero-extend	bv-ge 	bv-gt	bv-le	bv-lt
	bv-sge	bv-sgt	bv-sle	bv-slt  bv-shl  bv-lshr bv-ashr
	bv-div 	bv-rem  bv-sdiv bv-srem bv-smod
	bv-redor        bv-redand 	bv-comp
	bool-to-bv	bit

	define-type	define		assert	check	push	pop
	reset		dump-context	exit	echo	include
	show-model	eval		set-param	show-param
	show-params     show-stats      reset-stats     set-timeout
        help            ef-solve        export-to-dimacs
	show-implicant


2) Syntax
   ------

   <command>  ::=
 	      ( define-type <symbol> )
            | ( define-type <symbol> <typedef> )
            | ( define <symbol> :: <type> )
            | ( define <symbol> :: <type> <expression> )
            | ( assert <expression> )
            | ( exit )
            | ( check )
            | ( push )
            | ( pop )
            | ( reset )
            | ( show-model )
            | ( eval <expression> )
            | ( echo <string> )
            | ( include <string> )
            | ( set-param <symbol> <immediate-value> )
	    | ( show-param <symbol> )
	    | ( show-params )
	    | ( show-stats )
            | ( reset-stats )
	    | ( set-timeout <number> )
            | ( show-timeout )
            | ( dump-context )
	    | ( help )
            | ( help <symbol> )
            | ( help <string> )
	    | ( ef-solve )
	    | ( export-to-dimacs <string> )
	    | ( show-implicant )
            | EOS


   <typedef> ::=
              <type>
            | ( scalar <symbol> ... <symbol> )


   <type> ::=
              <symbol>
            | ( tuple <type> ... <type> )
            | ( -> <type> ... <type> <type> )
            | ( bitvector <rational> )
            | int
            | bool
            | real


   <expression> ::=
	      true
	    | false
            | <symbol>
            | <rational>
            | <float>
            | <binary bv>
            | <hexa bv>
            | ( forall ( <var_decl> ... <var_decl> ) <expression> )
            | ( exists ( <var_decl> ... <var_decl> ) <expression> )
	    | ( lambda ( <var_decl> ... <var_decl> ) <expression> )
            | ( let ( <binding> ... <binding> ) <expression> )
            | ( update <expression> ( <expression> ... <expression> ) <expression> )
            | ( <function> <expression> ... <expression> )


   <function> ::=
              <function-keyword>
            | <expression>


   <var_decl> ::= <symbol> :: <type>


   <binding> ::= ( <symbol> <expression> )


   <immediate-value> ::=
              true
            | false
            | <number>
            | <symbol>

   <number> ::=
              <rational>
            | <float>


3) Types
   -----

3.1) The primitive types are: bool, int, real, and (bitvector k) where k is
     a positive integer.


3.2) A new uninterpreted type T can be declared using

         (define-type T)

     provided T is a fresh name (i.e., not already mapped to a type).


3.3) A new scalar type (i.e., a finite enumeration) can de defined using:

         (define-type <name> (scalar <elem1> ... <elem_n>))

     <name> must be a fresh type name

     <elem1> ... <elem_n> must all be fresh term names and they must be distinct.

     There must be at list one element in the enumeration (i.e., n must be >= 1).

     This declaration introduces <name> as a new type of n elements
     and also introduces n new constant <elem_1> ... <elem_n>, all of type <name>.


3.4) A tuple type is written (tuple tau_1 ... tau_n) where tau_i's are types


3.5) A function type is written (-> tau_1 ... tau_n sigma) where the tau_i's
     and sigma are types. This is the type of functions of domain
     tau_1 x ... x tau_n and range sigma.

     There's no distinct array type constructor. Arrays are functions.




4) Built-in constants and functions
   --------------------------------

4.1) ite is the if-then-else construct.
     if is a synonym for ite

     distinct takes are least 2 arguments.

     =, /= are strictly binary (unlike in SMT-LIB 1, where = can take more than two arguments).


4.2) true, false, or, and, not, xor, <=>, => are the usual boolean constants and
     functions.

     or, and, xor can take any number of arguments (provided there's at least one).

     <=> and => are binary operators.


4.3) the usual arithmetic operators are available. For example the
     linear expression 3x + y + 2 can be written (+ (* 3 x) y 2).

     The +, *, - operators can take any number of arguments (at least one),

     For the minus sign, Yices 2 (unlike Yices 1) follows the usual
     convention:

       (- x) means opposite of x

       (- x y z)  means x - y - z, and could be written equivalently
       as (- x (+ y z))


     Yices also includes division and exponentiation operators. Only
     division by constants is supported (provided the divisor is nonzero).

       (/ x 3) is fine
       (/ x 0) is an error
       (/ 1 x) is an error

     Exponentiation is written

       (^ <term> <exponent>)

     the <exponent> must be a non-negative integer constant.

     Arithmetic constraints include the usual inequality operators:

          <=   <   >=   >

     (and the generic = and /= operations).


4.4) More arithmetic operations:

       (abs x)        absolute value of x
 
       (floor x)      largest integer less than or equal to x
       (ceil x)       smallest integer more than or equal to x

       (div x k)      integer division by a constant k
       (mod x k)      modulo operation

       (divides k x)  divisibility test
       (is-int x)     integrality test


      Floor and ceiling satisfy the following constraints:

          (floor x) <= x < (floor x) + 1

       (ceil x) - 1 <= x < (ceil x)


      For the division and modulo operations, the divider k must be
      a non-zero arithmetic constant. The division and remainder are
      defined as follows:

        (div x k) is an integer

        x = (div x k) * k  + (mod x k)

        0 <= (mod x k) < (abs k)

      Another way to look at this is:

        (div x k) = (floor (/ x k))   if k > 0
        (div x k) =  (ceil (/ x k))   if k < 0

      This follows the SMT-LIB convention for the theory Ints, except
      that the Yices versions are not restricted to integers. Both div
      and mod are defined for any real x and non-zero constant k. 
      For example,  (div 1/3 1/6)  is  2.
     

      The atom (divides k x) is true if x is an integer multiple of k,
      that is, we have:

          (divides k x)  iff  (exists (n::int) x = k * n)

      The divider k must be a constant (but it can be zero). If k is zero,
      (divides k x) is true iff x is zero. As in the div/mod operations,
      both k and x can be any real, not only integer.

      The atom (is-int x) it true if x is an integer. It can be defined
      using any of the following equivalences:

          (is-int x)   iff  (divides 1 x)
          (is-int x)   iff  (= x (floor x))
          (is-int x)   iff  (= x (ceil x)) 



4.5) tuple constructor: (mk-tuple <term_1> ... <term_n>) with n>=1

     projection: (select <tuple> i) is the i-th component of the term <tuple>.

          <tuple> must have type (tuple tau_1 ... tau_n)

     and i must be between 1 and n

     tuple update: (tuple-update <tuple> i <term>) is <tuple> with
     the i-th component replaced by <term>


4.6) function update: (update <function> (<arg_1> ... <arg_n>) <new_value>)


4.7) bitvector functions:

     a) bitvector constant from an integer

        (mk-bv <size> <value>)

        Note: value must be a non-negative integer and
        size must be a positive integer.


     b) bitvector arithmetic

        bv-add, bv-sub, bv-mul take one or more arguments, all arguments must
	have the same size

        (bv-neg x) = opposite of x in 2's complement arithmetic

        (bv-pow x k) = exponentiation (k must be a non-negative integer constant)


     c) bitwise logical operators

        (bv-not x) = bitwise negation of x

        bv-and, bv-or, bv-xor, bv-nand, bv-nor, bv-xnor: bitwise operators,
        all take one or more arguments of the same size

        note: (bv-xnor x y) is the same as (bv-not (bv-xor x y)).


     d) shift/rotate by a fixed constant

        (bv-shift-left0 x k):  shift x by k bits to the left, padding with 0
        (bv-shift-left1 x k):  shift x by k bits to the left, padding with 1
        (bv-shift-right0 x k): shift x by k bits to the right, padding with 0
        (bv-shift-right1 x k): shift x by k bits to the right, padding with 1

        (bv-ashift-right x k): arithmetic shift by k bits
        (bv-rotate-left x k):  rotate x by k bits to the left
        (bv-rotate-right x k): rotate x by k bits to the right

        In all these shift/rotate operations, k must an integer be between 0
	and the size of x.


       shift by a varying amount: in the following operations,
       x and y must be bitvectors of the same size (n bits)

        (bv-shl x y): shift x by k bits to the left, padding with 0
                      where k = value of bitvector y

        (bv-lshr x y): logical shift: shift x by k bits to the right
                       (padding with 0) where k = value of bitvector y

        (bv-ashr x y): arithmetic shift: shift x by k bits to the right,
		       padding with x's sign bit, where k = value of
                       bitvector y.

     e) subvector extraction:

        (bv-extract i j x): extract  bits j, j+1, .. i of x

        Requires 0 <= j <= i <= (size of x) - 1.


     f) bv-concat takes one or more arguments.

        Example: (bv-concat 0b000 0b111 0b00001) is the same as 0b00011100001
 

     g) (bv-repeat x n) is n copies of x concatenated together. n must be > 0.


     h) (bv-sign-extend x n): add n times the sign bit to the left of x (n must be >= 0)
        (bv-zero-extend x n): add n times '0' to the left of x (n must be >= 0)


     i) unsigned bit-vector comparisons:

        (bv-ge x y): x >= y
        (bv-gt x y): x > y
        (bv-le x y): x <= y
        (bv-lt x y): x < y

        x and y are interpreted as non-negative integers (both must have the same size)


     j) signed bit-vector comparisons

        (bv-sge x y): x >= y
        (bv-sgt x y): x > y
        (bv-sle x y): x <= y
        (bv-slt x y): x < y

        x and y are interpreted as signed integers (in 2's complement representation)
        they must have the same size


     k) (bv-div x y):  quotient in the unsigned division of x by y
        (bv-rem x y):  remainder in the unsigned division of x by y

         x and y must have the same size (n bits)

         if y = 0, Yices uses the following convention:

           (bv-rem x 0) = x
           (bv-div x 0) = largest integer representable using n bits (i.e. 0b1111...1)


        (bv-sdiv x y):  quotient in the signed division of x by y, with rounding to 0
        (bv-srem x y):  remainder in the signed division of x by y (also rounding to 0).

         x and y must have the same size

         if y = 0, Yices uses the following convention:

           (bv-srem x 0) = x

           (bv-sdiv x 0) = 0b00000...01 if x < 0
           (bv-sdiv x 0) = 0b11111...11 if x >= 0


        (bv-smod x y):  remainder in the signed division of x by y, with rounding to minus
                        infinity

         if y = 0, (bv-smod x 0) = x.


      l) (bv-redor x):  this is the 1-bit vector [(or b_0 ... b_{n-1})] where b_i is bit i of x
         (bv-redand x): same thing for and

         (bv-comp x y): compute a 1-bit vector u such that u = 0b1 if x and y are equal
                                                           u = 0b0 otherwise

          x and y must have the same size.


      m)  Conversion between Boolean and bitvector terms

          (bool-to-bv b_1 ... b_n): build a bitvector from n Boolean terms
          the result is a bitvector of n bits equal to [b_1 .... b_n]:
          - b_1 = high-order bit
          - b_n = low-order bit

          (bit u i): extract the i-th bit of bitvector u (as a Boolean term)
	  - if u has type (bitvector n) then i must be an integer constant
            such that 0 <= i <= n-1
          - (bit u 0) = low-order bit of u
          - (bit u n-1) = high-order bit of u

          Examples:

            (bool-to-bv true false false) is 0b100
            (bit 0b100 0) is false
            (bit 0b100 1) is false
            (bit 0b100 2) is true
          

5) Commands
   --------

   (define-type name):  create a new uninterpreted type called 'name'

   (define-type name <type-definition>) : create a new type called 'name' equal
                                          to the <type-definition>

   (define name :: <type>): create a new uninterpreted constant (i.e., global variable) of the
                            given <type> called <name>

   (define name :: <type> <expr>):  create a new term called 'name' equal to <expr>
                            After this definition, every occurrence of 'name' in any expression is
                            replaced by <expr>.

   (assert <formula>):  add an assertion to the context

   (check):  check whether the context is satisfiable

   (push):  start a new assertion scope

   (pop):  remove all assertions added after the matching (push)
   	   Note: this does not remove declarations.

   (reset):  clears the context (all assertions are removed, all 'push's are undone)
             the current model is also deleted (if any))

   (show-model): display the current model (if any)
                 a model is available after (check) provided (check) return sat or unknown
                 it is deleted on the next call to (assert) or (push) or (reset) or (pop)

   (eval <term>): show the value of <term> in the current model

   (echo <string>):  prints <string> on stdout

   (include <string>):  <string> must be the name of a file that contains Yices commands
   	    		this reads and executes all the commands in that file

   (set-param <parameter-name> <parameter-value>):
                 assign a value to one parameter (parameters control simplification
                 and search heuristics)

   (show-param <parameter-name>): show the current value of a parameter

   (show-params): show all parameters and their values

   (show-stats): show statistics (on the search).

   (reset-stats): reset all statistics to zero

   (set-timeout <value>): give a timeout in seconds. This timeout value
          will limit the search time on the subsequent call to (check)
          If <value> is 0 then the timeout is cleared (i.e., no timeout).
	  The timeout is reset (to 0) after every call to (check).

   (show-timeout): print the current timeout. The value displayed
          will be used as timeout in the next call to (check).

   (help): print a summary of the main commands

   (help <topic>): print help on a particular topic. <topic> can be given
       as a symbol as in (help syntax) or as a string as in (help "syntax").


   (ef-solve): solve an exists/forall problem.

   (export-to-dimacs <string>): convert the current set of assertions to
       the DIMACS CNF format. <string> is a file name where the result is
       written.

   (show-implicant): show an implicant built from the model.
       The implicant is a list of literals that are true in the current model,
       and the conjunction of these literals implies the assertions.


6) Parameters
   ----------

The following parameters can be set using (set-param ...) and examined using (show-param ...).


6.1) Parameters controlling preprocessing and simplifications


   Parameter	 Type		Description
   Name

   var-elim      Boolean        If var-elim is true then variable elimination is enabled.

                                Example: assertion (and (= x (g a)) (P y (f x))) is simplified
				to (P y (f (g a)))

   arith-elim    Boolean        If arith-elim is true then arithmetic variables are eliminated
                                using Gaussian elimination.

   bvarith-elim  Boolean        Similar to arith-elim, for bitvector constraints.

   flatten       Boolean        If flatten is true then nested 'or' and 'and' are flattened:

   				Example: (or a b (or b c d))  is rewritten to (or a b c d).

   learn-eq      Boolean        If learn-eq is true, then a heuristic that attempts to learn
   				equalities across disjunction is enabled.
                                Example: from assertion
                                  (or (and (= a b) (= b c) (= c d)) (and (= d e) (= e a)))
				yices can learn (= a d) because it's implied by both disjunct.

   keep-ite      Boolean        If keep-ite is true, then terms of the from (ite c a b) are
     				represented as is in the E-graph. Otherwise, they are eliminated
				using the rule

                                   t = (ite c a b)   iff  c => (t = a)  AND  NOT c => (t = b)

                                This parameter is relevant only for the QF_UF logic
                                (uninterpreted functions) and for logics that combine UF
                                with other theories.



6.2) SAT Solver Parameters

   Yices uses a CDCL SAT solver, similar to Minisat and Picosat. The following parameters
   affect heuristics used by this SAT solver.


6.2.1) Restart Heuristics


   Parameter	 Type
   Name

   fast-restart  Boolean       If true, Yices will use a fast restart heuristics.

   c-threshold	 Integer       Number of conflict before the first restart

   c-factor	 Float	       Increase factor for c-threshold after every restart (must be >= 1.0)

   d-threshold	 Integer       Secondary threshold used only if fast-restart is true

   d-factor	 Float	       Increase factor for d-threshold (must be >= 1.0)



   If fast-restart is false, the following procedure is used
   (restart with a geometric progression):

      c := c-threshold
      while not solved
         dpll search
	 when number of conflicts == c:
	    restart the search
	    c := c-factor * c

   If fast-restart is true, the following procedure is used
   (Picosat-like restart)

     d := d-threshold
     c := c-threshold
     while not solved
        dpll search
	when number of conflicts == c:
	   restart the search
	   c := c_factor * c
	   if c >= d then
             c := c_threshold
	     d := d_factor * d




6.2.2) Clause deletion


   Parameter	    Type
   Name

   r-threshold      Integer	Clause-reduction initial threshold

   r-fraction       Float       Clause-reduction fraction (must be between 0.0 and 1.0)

   r-factor         Float       Increase factor for clause reduction (must be >= 1.0)

   clause-decay     Float	Clause activity decay (must be between 0.0 and 1.0)



   To control clause deletion, Yices uses the following strategy (same as Minisat
   and other SAT solvers).

   Clause activity:

   Each learned clause has an activity score that decays
   geometrically.  After each conflict, the activity of all clauses
   not involved in this conflict is reduced by a factor equal to
   clause-decay (by default it's 0.999).  A smaller clause-decay
   causes clauses activity do go down faster.

   To trigger clause deletion: the solver uses a threshold = reduction-bound

   Initially:

     reduction-bound = max(r-threshold, r-fraction * number of clauses in initial problem)

   During the search:

      when the number of learned clauses >= reduction bound
      delete low-activity clauses
      reduction-bound  := r-factor * reduction-bound



6.2.3) Decision heuristic

   When the SAT solver makes a decision, it picks an unassigned Boolean variable
   of highest activity or it picks a variable randomly.  Once this decision
   variable is picked, the solver assigns it to true or false depending
   on the branching mode.


   Parameter	  Type
   Name


   var-decay      Float         Variable activity decay factor (must be between 0 and 1.0)
   		  		Controls how fast variable activities go down.

   randomness     Float         Fraction of random decisions in branching (must be between 0 and 1.0)
   		  		(e.g., if randomness is 0.1, 10% of the decision are variables
				picked randomly).

   branching      see below




   Once a decision variable 'x' is selected, the branching mode
   determines whether 'x' is set to true or false. The following modes
   are defined:

   default:	default heuristic (as in RSAT)
   		This use a cache to remember the last value of each variable (i.e., true or false).
		When 'x' is picked as a decision variable, then it is assigned the cached value
		(i.e., the same value as what was last assigned to 'x')

   negative:    always set 'x' to false

   positive:	always set 'x' to true


   theory:	use the default if 'x' is a pure Boolean, delegate to the theory solver otherwise

   th-neg:      set 'x' to false if 'x' is a pure Boolean, delegate to the theory solver otherwise

   th-pos: 	set 'x' to true if 'x' is a pure Boolean, delegate to the theory solver otherwise



   Delegating to the theory solver, means asking the theory solver to evaluate the atom attached
   to 'x' in the theory solver's current model. Then branching accordingly. This is supported by
   the Egraph and by the Simplex solver.

   Example: if 'x' is attached to arithmetic atom (<= n 4),  then the Simplex solver
   examines the value of 'n' in its current variable assignment.  If this value
   is more than 4, branch 'x := false', otherwise, branch 'x := true'.




6.3) Theory Lemmas

  Yices includes heuristics to build theory lemmas.  A theory lemma is
  a set of clauses that are true in a theory and get added to the
  clauses stored in the SAT solver. The heuristics attempt to discover
  useful theory lemmas and convert them into clauses.

  Examples
  --------

  1) Generic lemmas: Theory solvers communicate with the CDCL SAT
     solver by generating so-called theory explanations. By default,
     these theory explanations are temporary. Optionally, Yices can
     convert these theory explanations into clauses (thus making them
     permanent).


  2) Simplex lemmas; If the Simplex solver contains atoms (<= n 4) and
     (<= n 3) then a valid theory lemma is that (<= n 3) implies (<= n 4).

     So we can add the following clause:

       (or (not (<= n 3)) (<= n 4))


  3) Ackermann Lemmas: If the Egraph contains terms (F x y) and
     (F x z) then we can add the following lemma

         y = z  implies (F x y) = (F x z)

     This is a known as Ackermann's lemma for the terms (F x y) and (F x z).


     Yices uses a variant of this lemmas for predicates. If the Egraph
     contains (P x) and (P y) where P is an uninterpreted predicate
     (i.e., (P x) and (P y) are Boolean), then the corresponding Ackermann
     lemma is written as two clauses:

        x = y and (P x) implies (P y)
        x = y and (P y) implies (P x)


     Generating Ackermann lemmas may require creating new equality atoms.
     For example in

         y = z implies (F x y) = (F x z):

     Yices may have to create as many as two atoms: the atom (y = z) and
     the atom ((F x y) = (F x z)).  Too many of these can overwhelm the
     Egraph. So Yices provides parameters to control the number of
     new equality atoms generated by the Ackermann lemmas heuristics.



   Parameters that control theory lemma generation
   -----------------------------------------------

   cache-tclauses          Boolean         enables/disables the generation of generic lemmas

   tclause-size            Integer         bound on the size of generic lemmas.
   			   		   If cache-tclauses is true, then only small theory
 					   explanations (that contains no more than tclause-size
                                           literals) are converted to clauses.



   dyn-ack	           Boolean         enables/disable the generation of Ackermann lemmas
   			   		   for non-Boolean terms

   max-ack	           Integer 	   bound on the number of Ackermann lemmas generated

   dyn-ack-threshold       Integer         heuristic threshold: A lower value makes the heuristic
   			   		   more aggressive (i.e., more lemmas are generated).


   dyn-bool-ack            Boolean         enables/disable the generation of Ackermann lemmas
   			   		   for Boolean terms

   max-bool-ack	           Integer         bound on the number of Boolean Ackermann lemmas
   			   		   generated

   dyn-bool-ack-threshold  Integer	   heuristic threshold: as above. Lower values make
   			   		   lemma generation more aggressive.


   To bound the number of new equality atoms by the Ackermann and Boolean Ackermann heuristics,
   Yices uses two parameters:

   aux-eq-quota		   Integer
   aux-eq-ratio		   Float


   From these two parameters, Yices sets a limit on the number of new equality atoms to

       max(aux-eq-quota, num-terms * aux-eq-ratio)

   where num-terms is the the total number of terms in the Egraph.




6.4) Simplex Parameters

   eager-lemmas	      	   Boolean	   enable/disable the generation of lemmas in the Simplex
   			   		   solver. If this parameter is true, then the Simplex
					   solver will generate lemmas of the form

					   	  (x >= a) => (x >= b)

                                           where a and b are constants, and a > b.


   simplex-prop		   Boolean	   enable/disable theory propagation in the Simplex solver

   prop-threshold	   Integer	   bound on the number of variables in rows of the simplex
   			   		   tableau. If a row contains more than this number, it's
					   not considered during theory propagation.

   simplex-adjust	   Boolean 	   use a heuristic to adjust the simplex model

   bland-threhsold	   Integer	   number of pivoting steps before activation of Bland's
   			   		   pivoting rule

   icheck		   Boolean 	   enable periodic checking for integer feasibility
   			   		   If this flag is false, checking for integer feasibility
					   is done only at the end of the search.

   icheck-period           Integer	   if icheck is true, this parameter specifies how often the
   			   		   integer-feasibility check is called.



6.5) Array-solver Parameters

    max-update-conflicts   Integer	   Bound on the number of 'update axioms' instantiated per
    			   		   call to the array solver's final

    max-extensionality	   Integer         Bound on the number of extensionality axioms instantiated
    			   		   per call to the arrays solver's final check.


6.6) Model Reconciliation Parameters

     max-interface-eqs	   Integer	   Bound on the number of interface equalities created per
     			   		   call to the Egraph's final check.


     Final check is called when the search completes. In this state,
     all Boolean atoms are assigned a value and all solvers have a
     local model that assigns values to variables managed by each
     solver. A model-reconciliation procedure is then called to check
     whether these local models are compatible: if two variables
     x and y are shared between the Egraph and a theory solver, then
     both the egraph and the solver must agree on whether x and y are
     equal. If they are not, then Yices instantiates an interface
     lemma for 'x' and 'y', to force agreement. Semantically, such a
     lemmas encodes the rule

          'x == y' in the theory solver implies (eq x y) is true in the Egraph

     For example, if x and y are shared between the Egraph and the Simplex solver,
     Yices will generate the lemma

         ((eq x y) or (< x y) or (< y x))

     where (eq x y) is an Equality atom in the Egraph and (< x y) and
     (< y x) are arithmetic atoms in the Simplex solver.

     max-interface-eqs is a bound on the number of such reconciliation lemmas.
     At most max-interface-eqs lemmas are created for each call to the model
     reconciliation procedure.


6.7) Parameters for the Exists/Forall Solver

     The following parameters are used by the exists/forall solver

       ef-flatten-iff        Boolean       Enable flattening of iff
   
       ef-flatten-ite        Boolean       Enable flattening of if-then-else terms

       ef-max-iters          Integer       Maximal number of iterations

       ef-gen-mode                         Generalization mode

       ef-max-samples        Integer       Maximal number of samples for learning
                                           initial constraints


     If ef-flatten-iff is true, then the following rewriting rules are
     applied to the assertions when (ef-solve) is called:

       In a disjunction, (iff p q) is converted to  (or (and p q) (and (not p) (not q)))

       In a conjunction, (iff p q) is converted to  (and (=> p q) (=> q p))


     If ef-flatten-ite is true, the following rules are applied

       In a disjunction, (ite p q r) is converted to (or (and p q) (and (not p) r))

       In a conjunction, (ite p q r) is converted to (and (=> p q) (=> (not p) r))


    An exists/forall problem is of the following form 

        Exists x. Forall y. P(x, y)

    where x and y represents lists of variables and P(x, y) is quantifier free.
    The generic algorithm for solving such problems is as follows:

         i := 0
         C_0(x) := learned initial constraints on x
         repeat
           find x_i that satisfies C_i(x)
           if no such x_i is found
              return unsat

           find y_i that satisfies 'not P(x_i, y)'
           if no such y_i is found
              then x_i is a solution 
              return sat

           generalize from y_i:
           compute a new constraint G_i(x) such that  
              1) G_i(x_i) is true
              2) G_i(x) => (Exist y. not P(x, y))

           prepare for the next iteration:
           C_i+1(x) := C_i(x) and not G_i(x)
           i := i+1

         end

     Parameter 'ex-max-iters' puts a limit on the number of times the
     'repeat' loop above is executed.  By default, the limit is 100.
     It can be increased to say 1000 as follows

         (set-param ef-max-iters 1000).

     If the limit is reached without a solution, then (ef-solve) 
     returns 'unknown'.


     Parameter 'ef-gen-mode' specifies the generalization algorithm
     for constructing G_i(x) in each iteration.

     Four modes are possible:

         none         --> no generalization
         substitution --> generalization by substitution
         projection   --> model-based quantifier elimination
         auto         --> either substitution or projection depending on
                          the type of the universal variables y.

     No generalization means that G_i(x) is just the constraint (x = x_i).

     In generalization by substitution G_i(x) is the constraint  (not P(x, y_i))

     In generalization by projection, we first compute an implicant of 
     (not P(x, y)) from the model defined by (x_i, y_i). This implicant is a
     conjunction of literals involving variables x and y. Then a cheap form of
     quantifier elimination is applied to these literals to eliminate the 
     variables y. G_i(x) is the result of this quantifier-elimination procedure.
         
     The default setting for 'ef-gen-mode' is 'auto'. In this mode, Yices uses
     model-based quantifier elimination if the universal variables y contain
     arithmetic variables. Otherwise, Yices uses generalization by substitution.


     Parameter 'ef-max-samples' is used by a heuristic to learn the initial
     constraints C_0(x)  on the existential variables. The heuristic is
     based on sampling (random) values for the universal variables y and
     substituting these values for y in P(x, y). Parameter ef-max-samples
     is an upper bound on the number of samples in this process.