package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type
type rule =
  1. | NoChange
  2. | Change of int * smt_exp
  3. | Reconstruct of int * SimpSet.t * smt_exp * smt_exp -> smt_exp
val change : smt_exp -> rule
type strategy =
  1. | Skip
  2. | Rule of string * SimpSet.t -> smt_exp -> rule
  3. | Repeat of strategy
  4. | Then of strategy list
val mk_simple_rule : string -> (smt_exp -> rule) -> strategy
val mk_rule : string -> (SimpSet.t -> smt_exp -> rule) -> strategy
val run_strategy : SimpSet.t -> smt_exp -> strategy -> rule
val append_to_or : smt_exp -> smt_exp -> smt_exp
val append_to_and : smt_exp -> smt_exp -> smt_exp
val rule_squash_ite : strategy
val rule_chain_right_ite : strategy
val rule_same_ite : strategy
val rule_ite_literal : strategy
val remove_duplicates : smt_exp list -> smt_exp list
val rule_and_duplicates : strategy
val rule_or_duplicates : strategy
val rule_bit_bool_inequality : strategy
val rule_and_inequalities : strategy
val rule_or_equalities : strategy
val rule_or_ite : strategy
val rule_ite_lit : strategy
val rule_concat_literal_eq : strategy
val rule_flatten_and : strategy
val rule_flatten_or : strategy
val rule_false_and : strategy
val rule_true_and : strategy
val rule_true_or : strategy
val rule_false_or : strategy
val rule_order_and : strategy
val rule_order_or : strategy
val add_to_and : smt_exp -> smt_exp -> smt_exp
val rule_and_assume : strategy
val rule_ite_assume : strategy
val is_equality : smt_exp -> (smt_exp * smt_exp) option
val apply_equality : (smt_exp * smt_exp) -> smt_exp -> smt_exp
val rule_distribute_or_equality_in_and : strategy
val add_to_or : smt_exp -> smt_exp -> smt_exp
val rule_or_assume : strategy
val rule_var : strategy
val rule_tester : strategy
val rule_access_ite : strategy
val rule_inequality : strategy
val rule_not_not : strategy
val rule_not_push : strategy
val is_bvfunction : string -> bool
val rule_bvfunction_literal : strategy
val rule_extend_literal : strategy
val rule_extract_shift : strategy
val rule_extract : strategy
val rule_simp_eq : strategy
val rule_do_nothing : strategy
val apply : SimpSet.t -> (SimpSet.t -> smt_exp -> rule) -> smt_exp -> int * smt_exp
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct