Module Astral_internal.Encoding_context_sig

type ('locs, 'heap) t = {
  1. phi : SL.t;
  2. vars : SL.Variable.t list;
  3. location_terms : SL.Term.t list;
  4. heap_sort : HeapSort.t;
  5. smt_vars : SMT.Variable.t list;
  6. sl_graph : SL_graph0.t;
  7. location_bounds : LocationBounds0.t;
  8. can_skolemise : bool;
  9. under_star : bool;
  10. polarity : bool;
  11. mutable quantifier_prefix : SMT.Variable.t list;
  12. loc_sort : Sort.t;
  13. fp_sort : Sort.t;
  14. locs : 'locs;
  15. heap : 'heap;
  16. global_footprint : SMT.t;
  17. block_begin : SMT.t;
  18. block_end : SMT.t;
  19. mutable footprints : SMT.t list;
  20. mutable heaps : SMT.t list;
}
module type ENCODING_CONTEXT = sig ... end