Config (astral.Astral_internal.Config)

exception CmdOptionError of string

val check : unit -> unit

val parse_cmdline : ?version:string -> unit -> string

val to_json : unit -> Yojson.Basic.t

module Interactive : sig ... end

module InputFile : sig ... end

Solver behaviour

module BenchmarkMode : Param_sig.BOOL

module DryRun : Param_sig.BOOL

module Unsafe : Param_sig.BOOL

module Preprocessing : Param_sig.BOOL

module ProduceModels : Param_sig.BOOL

module VerifyModels : Param_sig.BOOL

Output

module Profiling : Param_sig.BOOL

module Statistics : Param_sig.BOOL

module JsonOutput : Param_sig.STRING

module DebugDir : Param_sig.STRING

module DebugKey : Param_sig.STRING

Semantics of input

module UseBuiltins : Param_sig.BOOL

module StrongSeparation : Param_sig.BOOL

module ImprecisePureAtoms : Param_sig.BOOL

Backend solvers

module Backend : 
  Param_sig.ENUM
    with type t =
           [ `Auto
           | `Bitwuzla
           | `Bitwuzla_ext
           | `Boolector
           | `cvc5
           | `Yices2
           | `Z3
           | `Z3_ext ]

module BackendOptions : Param_sig.STRING

module BackendTimeout : Param_sig.INT

module IncrementalBackend : 
  Param_sig.ENUM with type t = [ `Auto | `Bitwuzla | `Z3 ]

module IncrementalTimeout : Param_sig.INT

Encoding

module LocationEncoding : 
  Param_sig.ENUM with type t = [ `Bitvectors | `Datatype | `Direct ]

module SetEncoding : Param_sig.ENUM with type t = [ `Bitvectors | `Direct ]

module QuantifierEncoding : Param_sig.ENUM with type t = [ `Direct | `Enum ]

module Encoding : Param_sig.ENUM with type t = [ `Bitvectors | `Sets ]

Translation

module FootprintLimit : Param_sig.INT

module IncrementalUnfolding : Param_sig.BOOL

module UnfoldingLookahead : Param_sig.BOOL

Solver strategies

module SolverStrategy : 
  Param_sig.ENUM with type t = [ `Auto | `SingleQuery | `MultiQuery ]

module Verbosity : Param_sig.INT

module Debug : Param_sig.BOOL