====================================================================== This file is part of the Yices SMT Solver. Copyright (C) 2017 SRI International. Yices is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. Yices is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with Yices. If not, see . ====================================================================== 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 ( ) :: - 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, '\' is replaced by (including if is newline) - newline cannot occur inside the string, unless preceded by '\' - are numbers in the format / or - also denote numbers in a floating-point format . or or . where is 'e' or 'E' - are bitvector constants in binary format 0b - are bitvector constants in hexadecimal format 0x - 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 ------ ::= ( define-type ) | ( define-type ) | ( define :: ) | ( define :: ) | ( assert ) | ( assert ) | ( exit ) | ( check ) | ( check-assuming * ) | ( ef-solve ) | ( push ) | ( pop ) | ( reset ) | ( show-model ) | ( show-reduced-model ) | ( show-implicant ) | ( show-unsat-core ) | ( show-unsat-assumptions ) | ( eval ) | ( echo ) | ( include ) | ( set-param

) | ( show-param ) | ( show-params ) | ( show-stats ) | ( reset-stats ) | ( set-timeout ) | ( show-timeout ) | ( export-to-dimacs ) | ( dump-context ) | ( help ) | ( help ) | ( help ) | EOS ::= | ( scalar ... ) ::= | ( tuple ... ) | ( -> ... ) | ( bitvector ) | int | bool | real ::= true | false | | | | | | ( forall ( ... ) ) | ( exists ( ... ) ) | ( lambda ( ... ) ) | ( let ( ... ) ) | ( update ( ... ) ) | ( ... ) ::= | ::= :: ::= ( ) ::= true | false | | ::= | ::= | ( not ) 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 (scalar ... )) must be a fresh type name ... 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 as a new type of n elements and also introduces n new constant ... , all of type . 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 (^ ) the 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 ... ) with n>=1 projection: (select i) is the i-th component of the term . must have type (tuple tau_1 ... tau_n) and i must be between 1 and n tuple update: (tuple-update i ) is with the i-th component replaced by 4.6) function update: (update ( ... ) ) 4.7) bitvector functions: a) bitvector constant from an integer (mk-bv ) 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 ) : create a new type called 'name' equal to the (define name :: ): create a new uninterpreted constant (i.e., global variable) of the given called (define name :: ): create a new term called 'name' equal to After this definition, every occurrence of 'name' in any expression is replaced by . (assert ): add an assertion to the context (assert ): add a labeled assertion (check): check whether the context is satisfiable (check-assuming * ): check with a set of assumptions (ef-solve): solve an exists/forall problem. (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) (show-reduced-model): show the model if any, but print only the value of variables that are relevant to satisfying the assertions. (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. (show-unsat-core): list of labeled assertions that form an unsat core. (show-unsat-assumptions): list of assumptions that form an unsat core. (eval ): show the value of in the current model (echo ): prints on stdout (include ): must be the name of a file that contains Yices commands this reads and executes all the commands in that file (set-param

): assign a value to one parameter (parameters control simplification and search heuristics) (show-param ): 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 ): give a timeout in seconds. This timeout value will limit the search time on the subsequent call to (check) If 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). (export-to-dimacs ): convert the current set of assertions to the DIMACS CNF format. is a file name where the result is written. (dump-context): print the full context state (for debugging only). (help): print a summary of the main commands (help ): print help on a particular topic. can be given as a symbol as in (help syntax) or as a string as in (help "syntax"). 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.