<commit_before>(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 <NAME>
Copyright 2014 <NAME>
*)

module Make (E : Expr_intf.S)
    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) : sig
  (** Functor to create a  McSolver parametrised by the atomic formulas and a theory. *)

  exception Unsat

  module St : Mcsolver_types.S
    with type formula = E.Formula.t

  module Proof : Res.S
    with type atom = St.atom
     and type clause = St.clause
     and type lemma = Th.proof

  val solve : unit -> unit
  (** Try and solves the current set of assumptions.
      @return () if the current set of clauses is satisfiable
      @raise Unsat if a toplevel conflict is found *)

  val assume : E.Formula.t list list -> cnumber:int -> unit
  (** Add the list of clauses to the current set of assumptions.
      Modifies the sat solver state in place.
      @raise Unsat if a conflict is detect when adding the clauses *)

  val eval : E.Formula.t -> bool
  (** Returns the valuation of a formula in the current state
      of the sat solver. *)<commit_msg>Fixed an interface omission<commit_after>(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 <NAME>
Copyright 2014 <NAME>
*)

module Make (E : Expr_intf.S)
    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) : sig
  (** Functor to create a  McSolver parametrised by the atomic formulas and a theory. *)

  exception Unsat

  module St : Mcsolver_types.S
    with type term = E.Term.t
     and type formula = E.Formula.t

  module Proof : Res.S
    with type atom = St.atom
     and type clause = St.clause
     and type lemma = Th.proof

  val solve : unit -> unit
  (** Try and solves the current set of assumptions.
      @return () if the current set of clauses is satisfiable
      @raise Unsat if a toplevel conflict is found *)

  val assume : E.Formula.t list list -> cnumber:int -> unit
  (** Add the list of clauses to the current set of assumptions.
      Modifies the sat solver state in place.
      @raise Unsat if a conflict is detect when adding the clauses *)

  val eval : E.Formula.t -> bool
  (** Returns the valuation of a formula in the current state
      of the sat solver. *)
{'fraction_non_alphanumeric': 0.07769973661106233, 'fraction_numerical': 0.007023705004389816, 'mean_word_length': 2.8758503401360542, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '766552', 'n_tokens_mistral': 706, 'n_tokens_neox': 650, 'n_words': 313}