module Prop: sig end
Translations to/from ICSAT propositions
|
type t =
val pp : t Pretty.printer
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
?? |
: |
t
|
|
val occurs : Name.t -> t -> bool
val mk_true : t
val mk_false : t
val mk_var : Name.t -> t
val mk_poslit : Atom.t -> t
val mk_neglit : Atom.t -> t
val mk_disj : t list -> t
val mk_iff : t -> t -> t
val mk_ite : t -> t -> t -> t
val mk_neg : t -> t
val mk_conj : t list -> t
val mk_let : Name.t -> t -> t -> t
val apply : (Name.t * t) list -> t -> t
Translations to/from ICSAT propositions
|
type prop = int
val icsat_initialize : unit -> unit
val icsat_finalize : unit -> unit
val icsat_mk_true : unit -> prop
val icsat_mk_false : unit -> prop
val icsat_mk_var : string -> prop
val icsat_mk_atom : int -> int -> prop
val icsat_mk_or : prop list -> prop
val icsat_mk_and : prop list -> prop
val icsat_mk_iff : prop -> prop -> prop
val icsat_mk_implies : prop -> prop -> prop
val icsat_mk_xor : prop -> prop -> prop
val icsat_mk_not : prop -> prop
val icsat_mk_ite : prop -> prop -> prop -> prop
val icsat_is_true : prop -> bool
val icsat_is_false : prop -> bool
val icsat_is_not : prop -> bool
val icsat_is_or : prop -> bool
val icsat_is_iff : prop -> bool
val icsat_is_ite : prop -> bool
val icsat_is_var : prop -> bool
val icsat_is_atom : prop -> bool
val icsat_d_var : prop -> string
val icsat_d_atom : prop -> int
val icsat_d_not : prop -> prop
val icsat_num_arguments : prop -> int
val icsat_get_argument : prop -> int -> prop
val icsat_get_assignment : int -> int
val icsat_print_statistics : unit -> unit
Parameter settings for SAT solver
val set_verbose : bool -> unit
val set_remove_subsumed_clauses : bool -> unit
val set_validate_counter_example : bool -> unit
val set_polarity_optimization : bool -> unit
val set_clause_relevance : int -> unit
val set_cleanup_period : int -> unit
val set_num_refinements : int -> unit
Translating to and from propositions
module Atomtbl: sig end
module Inttbl: sig end
module Nametbl: sig end
val id : Inttbl.key Pervasives.ref
val atomtbl : Inttbl.key Atomtbl.t
val inttbl : Atomtbl.key Inttbl.t
val idtbl : prop Atomtbl.t
val vartbl : prop Nametbl.t
val atom_to_id : Atomtbl.key -> Inttbl.key
val id_to_atom : Inttbl.key -> Atomtbl.key
val atom_to_icsat_id : Atomtbl.key -> prop
val var_to_icsat_id : Nametbl.key -> prop
val to_prop : t -> prop
val of_prop : prop -> t
val d_disj : prop -> prop list
val is_nil : 'a list -> bool
val head : 'a list -> 'a
val tail : 'a list -> 'a list
val length : 'a list -> int
val is_connected : Inttbl.key -> Inttbl.key -> bool
| Parameters: |
|
i |
: |
Inttbl.key
|
|
j |
: |
Inttbl.key
|
|
val atom_pp : Inttbl.key -> unit
val stack : (Context.t * Atomtbl.key list) Stack.t
val initial : (Context.t * Atomtbl.key list) Pervasives.ref
val stack_reset : unit -> unit
val dup : unit -> unit
val push : Context.t * Atomtbl.key list -> unit
val pop : unit -> unit
val top : unit -> Context.t
val stackpp : unit -> unit
val add : Inttbl.key -> int
Scratch state
val scratch : Context.t Pervasives.ref
val reset_scratch_context : unit -> unit
val add_scratch_context : Inttbl.key -> int
Calling external SAT solver
val icsat_sat : prop -> bool
val init : Context.t -> unit
val finalize : unit -> unit
val statistics : bool Pervasives.ref
module Assignment: sig end
val sat : Context.t -> t -> (Assignment.t * Context.t) option
val debug : unit -> unit
val assignment : unit -> Assignment.t