Module opt 

Structs

ConstraintContext 🔒

Simple facts learned from the normalized conjunction currently being queried.

SmtCsePlan 🔒

SmtCseVisit 🔒

SmtCseWriter 🔒

WordInterval 🔒

Enums

SmtBinding 🔒

Functions

bool_structural_key 🔒

cmp_op_key 🔒

const_side_bound 🔒

constraints_are_directly_unsat 🔒

Returns whether normalized conjunctive constraints contain a direct contradiction.

expr_binop_key 🔒

expr_ternop_key 🔒

nonzero_bound 🔒

normalize_bool_for_solver 🔒

Normalizes one boolean expression into an equivalent, solver-friendlier form.

normalize_bool_node_for_solver 🔒

normalize_cmp_for_solver 🔒

normalize_constraint_batch 🔒

normalize_constraints_for_solver 🔒

Normalizes path constraints into an equivalent, solver-friendlier form.

normalize_expr_for_solver 🔒

Normalizes one word expression into an equivalent, solver-friendlier form.

normalize_expr_node_for_solver 🔒

normalize_ite_expr_for_solver 🔒

sort_dedup_bool_exprs 🔒

sorted_bool_exprs_are_subset 🔒

Returns whether every expression in subset appears in superset.

write_bool_structural_key 🔒

write_expr_structural_key 🔒

write_exprs_structural_key 🔒

write_smt_assertions 🔒