Skip to content

Commit

Permalink
Format
Browse files Browse the repository at this point in the history
  • Loading branch information
filipeom committed Sep 14, 2024
1 parent 1c358ef commit 801e36e
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 6 deletions.
5 changes: 4 additions & 1 deletion src/ast/ast.mli
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,10 @@
type t =
| Assert of Expr.t
| Check_sat of Expr.t list
| Declare_const of { id : Symbol.t; sort : Symbol.t }
| Declare_const of
{ id : Symbol.t
; sort : Symbol.t
}
| Echo of string
| Exit
| Get_assertions
Expand Down
2 changes: 1 addition & 1 deletion src/mappings.nop.ml
Original file line number Diff line number Diff line change
Expand Up @@ -370,7 +370,7 @@ module Nop = struct
end

module Smtlib = struct
let pp ?name:_ ?logic:_ ?status:_ _fmt _ = die ()
let pp ?name:_ ?logic:_ ?status:_ _fmt _ = die ()
end
end

Expand Down
8 changes: 4 additions & 4 deletions src/solvers/solver_intf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -37,10 +37,10 @@ module type S = sig
[?params] is of type {!type:Params.t} and is used to modify/set parameters
inside the solver.
[?logic] is of type {!type:Ty.logic} and is used to set the
theory of the assertions used. When knowing what the underlying theory is
going to be, setting this parameter can help the SMT solver be more
performant. The default logic is {e unknown_theory}. *)
[?logic] is of type {!type:Ty.logic} and is used to set the theory of the
assertions used. When knowing what the underlying theory is going to be,
setting this parameter can help the SMT solver be more performant. The
default logic is {e unknown_theory}. *)
val create : ?params:Params.t -> ?logic:Ty.logic -> unit -> t

(** Interrupt solver. *)
Expand Down

0 comments on commit 801e36e

Please sign in to comment.