package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Smt_exp.SimplifierSource

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