Module Astral_internal.Context

type expected_status = [
  1. | `Sat
  2. | `Unsat
  3. | `Unknown
]
type status = [
  1. | `Sat
  2. | `Unsat
  3. | `Unknown of string
]
val negate_status : [< `Sat | `Unknown of 'a | `Unsat ] -> [> `Sat | `Unknown of 'a | `Unsat ]
val status_is_unknown : [< `Sat | `Unknown of 'a | `Unsat ] -> bool
type t = {
  1. raw_input : ParserContext.t;
  2. sorts : Sort.t list;
  3. heap_sort : HeapSort.t;
  4. defs : MemoryModel.StructDef.t list;
  5. inductive_preds : Stdlib.String.t list;
  6. phi : SL.t;
  7. vars : SL.Variable.t list;
  8. model_adapter : ModelAdapter.t;
  9. expected_status : expected_status;
  10. sl_graph : SL_graph0.t;
  11. location_bounds : LocationBounds0.t;
  12. size : Stdlib.Int.t option;
  13. status : status option;
  14. model : StackHeapModel.t option;
  15. unsat_core : SL.t list option;
  16. solved_by : string option;
  17. quantifiers : string option;
}
val init : ParserContext.t -> t
val empty : t
val (let*) : (t -> t) -> t -> t
val add_metadata : t -> SL_graph0.t -> LocationBounds0.t -> t

Model adapter

val add_skolem_var : t -> SL.Variable.t -> t
val apply_model_adapter : t -> t

Setters

val set_preprocessed : t -> SL.t -> SL.Variable.t list -> t

TODO: keep normalised?

val set_size : t -> Stdlib.Int.t -> t
val set_result : status -> ?model:StackHeapModel.t -> ?unsat_core:SL.t list -> ?solved_by:string -> t -> t

Getters

val get_raw_input : t -> SL.t * SL.Variable.t list

Get input formula before any preprocessing.

val get_input : t -> SL.t * SL.Variable.t list
val transform_to_entl : t -> t

Transform satisfiability to validity of entailment

val show_status : t -> string
val show_expected_status : t -> string