Lean.Cadical.Internal

This module provides CaDiCaL's C++ FFI in Lean. See https://github.com/arminbiere/cadical/blob/rel-2.2.1/src/cadical.hpp for precise usage information and invariants.

source

inductive Lean.Cadical.Internal.Status :

Type

satisfiable : Status
unsatisfiable : Status
unknown : Status

Instances For

source

@[instance_reducible]

instance Lean.Cadical.Internal.instInhabitedStatus :

Inhabited Status

Equations

Lean.Cadical.Internal.instInhabitedStatus = { default := Lean.Cadical.Internal.instInhabitedStatus.default }

source

@[instance_reducible]

instance Lean.Cadical.Internal.instDecidableEqStatus :

DecidableEq Status

Equations

Lean.Cadical.Internal.instDecidableEqStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[instance_reducible]

instance Lean.Cadical.Internal.instHashableStatus :

Hashable Status

Equations

Lean.Cadical.Internal.instHashableStatus = { hash := Lean.Cadical.Internal.instHashableStatus.hash }

source

def Lean.Cadical.Internal.instHashableStatus.hash :

Status → UInt64

Equations

Instances For

source

@[instance_reducible]

instance Lean.Cadical.Internal.instReprStatus :

Repr Status

Equations

Lean.Cadical.Internal.instReprStatus = { reprPrec := Lean.Cadical.Internal.instReprStatus.repr }

source

def Lean.Cadical.Internal.instReprStatus.repr :

Status → Nat → Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lean.Cadical.Internal.Status.toInt32 :

Status → Int32

Equations

Instances For

source

def Lean.Cadical.Internal.signature :

String

Equations

Lean.Cadical.Internal.signature = Lean.Cadical.Internal.getSignature✝ ()

Instances For

source

def Lean.Cadical.Internal.Solver :

Type

Equations

Lean.Cadical.Internal.Solver = Lean.Cadical.Internal.SolverImpl✝.type

Instances For

source

instance Lean.Cadical.Internal.instNonemptySolver :

Nonempty Solver

source

@[extern lean_cadical_solver_new]

opaque Lean.Cadical.Internal.Solver.new :

BaseIO Solver

source

@[extern lean_cadical_solver_add]

opaque Lean.Cadical.Internal.Solver.add (s : Solver) (lit : Int32) :

BaseIO Unit

source

@[extern lean_cadical_solver_clause]

opaque Lean.Cadical.Internal.Solver.clause (s : Solver) (lits : Array Int32) :

BaseIO Unit

source

@[extern lean_cadical_solver_inconsistent]

opaque Lean.Cadical.Internal.Solver.inconsistent (s : Solver) :

BaseIO Bool

source

@[extern lean_cadical_solver_assume]

opaque Lean.Cadical.Internal.Solver.assume (s : Solver) (lit : Int32) :

BaseIO Unit

source

@[extern lean_cadical_solver_solve]

opaque Lean.Cadical.Internal.Solver.solve (s : Solver) :

BaseIO Status

source

@[extern lean_cadical_solver_val]

opaque Lean.Cadical.Internal.Solver.val (s : Solver) (lit : Int32) :

BaseIO Int32

source

@[extern lean_cadical_solver_flip]

opaque Lean.Cadical.Internal.Solver.flip (s : Solver) (lit : Int32) :

BaseIO Bool

source

@[extern lean_cadical_solver_flippable]

opaque Lean.Cadical.Internal.Solver.flippable (s : Solver) (lit : Int32) :

BaseIO Bool

source

@[extern lean_cadical_solver_failed]

opaque Lean.Cadical.Internal.Solver.failed (s : Solver) (lit : Int32) :

BaseIO Bool

source

@[extern lean_cadical_solver_constrain]

opaque Lean.Cadical.Internal.Solver.constrain (s : Solver) (lit : Int32) :

BaseIO Unit

source

@[extern lean_cadical_solver_constraint_failed]

opaque Lean.Cadical.Internal.Solver.constraintFailed (s : Solver) :

BaseIO Bool

source

@[extern lean_cadical_solver_lookahead]

opaque Lean.Cadical.Internal.Solver.lookahead (s : Solver) :

BaseIO Int32

source

@[extern lean_cadical_solver_reset_assumptions]

opaque Lean.Cadical.Internal.Solver.resetAssumptions (s : Solver) :

BaseIO Unit

source

@[extern lean_cadical_solver_reset_constraint]

opaque Lean.Cadical.Internal.Solver.resetConstraint (s : Solver) :

BaseIO Unit

source

@[extern lean_cadical_solver_status]

opaque Lean.Cadical.Internal.Solver.status (s : Solver) :

BaseIO Status

source

@[extern lean_cadical_solver_vars]

opaque Lean.Cadical.Internal.Solver.vars (s : Solver) :

BaseIO Int32

source

@[extern lean_cadical_solver_resize]

opaque Lean.Cadical.Internal.Solver.resize (s : Solver) (minMaxVar : Int32) :

BaseIO Unit

source

@[extern lean_cadical_solver_is_valid_option]

opaque Lean.Cadical.Internal.Solver.isValidOption (opt : String) :

Bool

source

@[extern lean_cadical_solver_is_preprocessing_option]

opaque Lean.Cadical.Internal.Solver.isPreprocessingOption (opt : String) :

Bool

source

@[extern lean_cadical_solver_is_valid_long_option]

opaque Lean.Cadical.Internal.Solver.isValidLongOption (opt : String) :

Bool

source

@[extern lean_cadical_solver_get]

opaque Lean.Cadical.Internal.Solver.get (s : Solver) (opt : String) :

BaseIO Int32

source

@[extern lean_cadical_solver_set]

opaque Lean.Cadical.Internal.Solver.set (s : Solver) (opt : String) (val : Int32) :

BaseIO Bool

source

@[extern lean_cadical_solver_set_long_option]

opaque Lean.Cadical.Internal.Solver.setLongOption (s : Solver) (opt : String) :

BaseIO Bool

source

@[extern lean_cadical_solver_is_valid_configuration]

opaque Lean.Cadical.Internal.Solver.isValidConfiguration (opt : String) :

Bool

source

@[extern lean_cadical_solver_configure]

opaque Lean.Cadical.Internal.Solver.configure (s : Solver) (opt : String) :

BaseIO Bool

source

@[extern lean_cadical_solver_optimize]

opaque Lean.Cadical.Internal.Solver.optimize (s : Solver) (val : Int32) :

BaseIO Unit

source

@[extern lean_cadical_solver_limit]

opaque Lean.Cadical.Internal.Solver.limit (s : Solver) (limit : String) (val : Int32) :

BaseIO Bool

source

@[extern lean_cadical_solver_is_valid_limit]

opaque Lean.Cadical.Internal.Solver.isValidLimit (s : Solver) (limit : String) :

BaseIO Bool

source

@[extern lean_cadical_solver_active]

opaque Lean.Cadical.Internal.Solver.active (s : Solver) :

BaseIO Int32

source

@[extern lean_cadical_solver_redundant]

opaque Lean.Cadical.Internal.Solver.redundant (s : Solver) :

BaseIO Int64

source

@[extern lean_cadical_solver_irredundant]

opaque Lean.Cadical.Internal.Solver.irredundant (s : Solver) :

BaseIO Int64

source

@[extern lean_cadical_solver_simplify]

opaque Lean.Cadical.Internal.Solver.simplify (s : Solver) (rounds : Int32) :

BaseIO Status

source

@[extern lean_cadical_solver_terminate]

opaque Lean.Cadical.Internal.Solver.terminate (s : Solver) :

BaseIO Unit

source

@[extern lean_cadical_solver_frozen]

opaque Lean.Cadical.Internal.Solver.frozen (s : Solver) (lit : Int32) :

BaseIO Bool

source

@[extern lean_cadical_solver_freeze]

opaque Lean.Cadical.Internal.Solver.freeze (s : Solver) (lit : Int32) :

BaseIO Unit

source

@[extern lean_cadical_solver_melt]

opaque Lean.Cadical.Internal.Solver.melt (s : Solver) (lit : Int32) :

BaseIO Unit

source

@[extern lean_cadical_solver_fixed]

opaque Lean.Cadical.Internal.Solver.fixed (s : Solver) (lit : Int32) :

BaseIO Int32

source

@[extern lean_cadical_solver_phase]

opaque Lean.Cadical.Internal.Solver.phase (s : Solver) (lit : Int32) :

BaseIO Unit

source

@[extern lean_cadical_solver_unphase]

opaque Lean.Cadical.Internal.Solver.unphase (s : Solver) (lit : Int32) :

BaseIO Unit

source

@[extern lean_cadical_solver_conclude]

opaque Lean.Cadical.Internal.Solver.conclude (s : Solver) :

BaseIO Unit

source

@[extern lean_cadical_solver_usage]

opaque Lean.Cadical.Internal.Solver.usage :

IO Unit

source

@[extern lean_cadical_solver_configurations]

opaque Lean.Cadical.Internal.Solver.configurations :

IO Unit

source

@[extern lean_cadical_solver_statistics]

opaque Lean.Cadical.Internal.Solver.statistics (s : Solver) :

IO Unit

source

@[extern lean_cadical_solver_resources]

opaque Lean.Cadical.Internal.Solver.resources (s : Solver) :

IO Unit

source

@[extern lean_cadical_solver_state]

opaque Lean.Cadical.Internal.Solver.state (s : Solver) :

BaseIO UInt16