On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package yices2
Context
module Config : sig ... endContext configuration
Options
var-elim: whether to eliminate variables by substitutionarith-elim: more variable elimination for arithmetic (Gaussian elimination)bvarith-elim: more variable elimination for bitvector arithmeticeager-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 variablex).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 equalitieskeep-ite: whether to eliminate term if-then-else or keep them as terms - this requires the context to include the egraphbreak-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 termtis defined as(ite c 10 (ite d 3 20)), then the context with include the assertion3 <= t <= 20.
val enable_option : context -> string -> unitEnable option
val disable_option : context -> string -> unitDisable option
Formula assertion
Assertion stack operations
val reset : context -> unitReset context, i.e. remove all assertions.
val push : context -> unitPush, i.e. mark a backtrack point.
val pop : context -> unitPop, i.e. remove all assertions up to last backtrack point.
module Params : sig ... endCheck parameters
val assert_blocking_clause : context -> unitAdd a blocking clause, i.e. a clause that ask for another model.
val stop_search : context -> unitInterrupt a search.
On This Page