gillian » Gillian » Symbolic » FO_logic » FOSolver

Module FO_logic.FOSolver

val check_satisfiability_with_model :
  Gil_syntax.Expr.t list ->
  Type_env.t ->
  Symbolic.Subst.t option

check_satisfiability_with_model pfs gamma checks whether or not the pure formulae pfs are satisfiable under the typing environment gamma. If this is the case, the function returns the appropriate logical environment.

val check_satisfiability :
  ?matching:bool ->
  ?time:string ->
  ?relevant_info:
    (Utils.Containers.SS.t * Utils.Containers.SS.t * Utils.Containers.SS.t) ->
  Gil_syntax.Expr.t list ->
  Type_env.t ->
  bool

check_satisfiability ?matching pfs gamma checks whether or not the pure formulae pfs are satisfiable under the typing environment gamma. The matching flag should not be used by Gillian instantiation developers.

val sat :
  matching:bool ->
  pfs:Pure_context.t ->
  gamma:Type_env.t ->
  Gil_syntax.Expr.t ->
  bool

A different API for check_satisfiability better adapted for usage in memory models

val check_entailment :
  ?matching:bool ->
  Utils.Containers.SS.t ->
  Pure_context.t ->
  Gil_syntax.Expr.t list ->
  Type_env.t ->
  bool

check_entailment existentials lpfs rpfs gamma checks whether or not the entailment << ∃ existentials. lpfs => rpfs >> holds under the typing environment gamma.

val is_equal :
  ?matching:bool ->
  pfs:Pure_context.t ->
  gamma:Type_env.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  bool

is_equal e1 e2 pfs gamma checks whether or not << pfs, gamma |- e1 = e2 >>.

val is_different :
  pfs:Pure_context.t ->
  gamma:Type_env.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  bool

is_different e1 e2 pfs gamma checks whether or not << pfs, gamma |- e1 <> e2 >>.

val num_is_less_or_equal :
  pfs:Pure_context.t ->
  gamma:Type_env.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  bool

val resolve_loc_name :
  pfs:Pure_context.t ->
  gamma:Type_env.t ->
  Gil_syntax.Expr.t ->
  string option