This module provides a thin wrapper around CaDiCaL's C++ FFI, allowing it to interact with the CNF API from Std.Sat.CNF.

structure Lean.Cadical.State : Type

The IPASIR state of the solver.

• bits : UInt16

@[instance_reducible]

instance Lean.Cadical.instInhabitedState : Inhabited State

Equations

• Lean.Cadical.instInhabitedState = { default := Lean.Cadical.instInhabitedState.default }

def Lean.Cadical.instDecidableEqState.decEq (x✝ x✝¹ : State) : Decidable (x✝ = x✝¹)

Equations

• Lean.Cadical.instDecidableEqState.decEq { bits := a } { bits := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Lean.Cadical.instDecidableEqState : DecidableEq State

Equations

• Lean.Cadical.instDecidableEqState = Lean.Cadical.instDecidableEqState.decEq

@[instance_reducible]

instance Lean.Cadical.instHashableState : Hashable State

Equations

• Lean.Cadical.instHashableState = { hash := Lean.Cadical.instHashableState.hash }

def Lean.Cadical.instHashableState.hash : State → UInt64

Equations

• Lean.Cadical.instHashableState.hash { bits := a } = mixHash 0 (hash a)

@[inline]

def Lean.Cadical.State.initializing : State

Equations

• Lean.Cadical.State.initializing = { bits := 1 }

@[inline]

def Lean.Cadical.State.configuring : State

Equations

• Lean.Cadical.State.configuring = { bits := 2 }

@[inline]

def Lean.Cadical.State.steady : State

Equations

• Lean.Cadical.State.steady = { bits := 4 }

@[inline]

def Lean.Cadical.State.adding : State

Equations

• Lean.Cadical.State.adding = { bits := 8 }

@[inline]

def Lean.Cadical.State.solving : State

Equations

• Lean.Cadical.State.solving = { bits := 16 }

@[inline]

def Lean.Cadical.State.satisfied : State

Equations

• Lean.Cadical.State.satisfied = { bits := 32 }

@[inline]

def Lean.Cadical.State.unsatisfied : State

Equations

• Lean.Cadical.State.unsatisfied = { bits := 64 }

@[inline]

def Lean.Cadical.State.deleting : State

Equations

• Lean.Cadical.State.deleting = { bits := 128 }

@[inline]

def Lean.Cadical.State.inconclusive : State

Equations

• Lean.Cadical.State.inconclusive = { bits := 256 }

@[inline]

def Lean.Cadical.State.isReady (s : State) : Bool

Equations

• s.isReady = (s.bits &&& Lean.Cadical.State.ready✝.bits != { toBitVec := 0 })

@[inline]

def Lean.Cadical.State.isValid (s : State) : Bool

Equations

• s.isValid = (s.bits &&& Lean.Cadical.State.valid✝.bits != { toBitVec := 0 })

@[inline]

def Lean.Cadical.State.isInvalid (s : State) : Bool

Equations

• s.isInvalid = (s.bits &&& Lean.Cadical.State.invalid✝.bits != { toBitVec := 0 })

def Lean.Cadical.State.toString (s : State) : String

Equations

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

@[instance_reducible]

instance Lean.Cadical.State.instToString : ToString State

Equations

• Lean.Cadical.State.instToString = { toString := Lean.Cadical.State.toString }

inductive Lean.Cadical.Status : Type

• satisfiable : Status
• unsatisfiable : Status
• unknown : Status

@[instance_reducible]

instance Lean.Cadical.instInhabitedStatus : Inhabited Status

Equations

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

@[instance_reducible]

instance Lean.Cadical.instDecidableEqStatus : DecidableEq Status

Equations

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

@[instance_reducible]

instance Lean.Cadical.instHashableStatus : Hashable Status

Equations

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

def Lean.Cadical.instHashableStatus.hash : Status → UInt64

Equations

• Lean.Cadical.instHashableStatus.hash Lean.Cadical.Status.satisfiable = 0
• Lean.Cadical.instHashableStatus.hash Lean.Cadical.Status.unsatisfiable = 1
• Lean.Cadical.instHashableStatus.hash Lean.Cadical.Status.unknown = 2

def Lean.Cadical.instReprStatus.repr : Status → Nat → Format

Equations

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

@[instance_reducible]

instance Lean.Cadical.instReprStatus : Repr Status

Equations

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

def Lean.Cadical.Status.toInt32 : Status → Int32

Equations

• Lean.Cadical.Status.satisfiable.toInt32 = 10
• Lean.Cadical.Status.unsatisfiable.toInt32 = 20
• Lean.Cadical.Status.unknown.toInt32 = 0

def Lean.Cadical.Status.toString : Status → String

Equations

• Lean.Cadical.Status.satisfiable.toString = "SAT"
• Lean.Cadical.Status.unsatisfiable.toString = "UNSAT"
• Lean.Cadical.Status.unknown.toString = "UNKNOWN"

@[instance_reducible]

instance Lean.Cadical.Status.instToString : ToString Status

Equations

• Lean.Cadical.Status.instToString = { toString := Lean.Cadical.Status.toString }

structure Lean.Cadical.Solver : Type

An incremental SAT solver.

• ofNative :: (
• solver : Lean.Cadical.Internal.Solver
• )

instance Lean.Cadical.instNonemptySolver : Nonempty Solver

def Lean.Cadical.Solver.new : BaseIO Solver

Allocate a new SAT solver.

Equations

• Lean.Cadical.Solver.new = do let __do_lift ← Lean.Cadical.Internal.Solver.new pure { solver := __do_lift }

def Lean.Cadical.Solver.state (s : Solver) : BaseIO State

Get the current IPASIR state of the solver.

Equations

• s.state = do let __do_lift ← (Lean.Cadical.Solver.solver✝ s).state pure { bits := __do_lift }

def Lean.Cadical.Solver.clause (s : Solver) (clause : Std.Sat.CNF.Clause Nat) : IO Unit

Add a clause to the solver.

Equations

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

def Lean.Cadical.Solver.inconsistent (s : Solver) : BaseIO Bool

Check whether the formula is currently inconsistent (potentially under assumptions).

Equations

• s.inconsistent = (Lean.Cadical.Solver.solver✝ s).inconsistent

def Lean.Cadical.Solver.assume (s : Solver) (lit : Nat) (pol : Bool) : IO Unit

Add a new assumption literal to the solver, reset upon the next call to solve.

Equations

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

def Lean.Cadical.Solver.solve (s : Solver) : BaseIO Status

Run the SAT solver on current formula and assumptions.

Equations

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

def Lean.Cadical.Solver.val (s : Solver) (lit : Nat) : IO Bool

Obtain the value of a literal in the current model if it exists.

Equations

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

def Lean.Cadical.Solver.resetAssumptions (s : Solver) : BaseIO Unit

Reset assumptions made via assume explicitily.

Equations

• s.resetAssumptions = (Lean.Cadical.Solver.solver✝ s).resetAssumptions

def Lean.Cadical.Solver.status (s : Solver) : BaseIO Status

Query the current status (not to be confused with the IPASIR state) of the oslver.

Equations

• s.status = do let status ← (Lean.Cadical.Solver.solver✝ s).status pure (Lean.Cadical.Status.ofInternal✝ status)

def Lean.Cadical.Solver.isValidOption (opt : String) : Bool

Equations

• Lean.Cadical.Solver.isValidOption opt = Lean.Cadical.Internal.Solver.isValidOption opt

def Lean.Cadical.Solver.isPreprocessingOption (opt : String) : Bool

Equations

• Lean.Cadical.Solver.isPreprocessingOption opt = Lean.Cadical.Internal.Solver.isPreprocessingOption opt

def Lean.Cadical.Solver.isValidLongOption (opt : String) : Bool

Equations

• Lean.Cadical.Solver.isValidLongOption opt = Lean.Cadical.Internal.Solver.isValidLongOption opt

def Lean.Cadical.Solver.getOption (s : Solver) (opt : String) : BaseIO Int32

Equations

• s.getOption opt = (Lean.Cadical.Solver.solver✝ s).get opt

def Lean.Cadical.Solver.setOption (s : Solver) (opt : String) (val : Int32) : BaseIO Bool

Equations

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

def Lean.Cadical.Solver.setLongOption (s : Solver) (opt : String) : BaseIO Bool

Equations

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

def Lean.Cadical.Solver.isValidConfiguration (opt : String) : Bool

Equations

• Lean.Cadical.Solver.isValidConfiguration opt = Lean.Cadical.Internal.Solver.isValidConfiguration opt

def Lean.Cadical.Solver.configure (s : Solver) (opt : String) : BaseIO Bool

Equations

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

def Lean.Cadical.Solver.terminate (s : Solver) : BaseIO Unit

Equations

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

def Lean.Cadical.Solver.printConfigurations : IO Unit

Equations

• Lean.Cadical.Solver.printConfigurations = Lean.Cadical.Internal.Solver.configurations

def Lean.Cadical.Solver.printStatistics (s : Solver) : IO Unit

Equations

• s.printStatistics = (Lean.Cadical.Solver.solver✝ s).statistics

def Lean.Cadical.Solver.printResources (s : Solver) : IO Unit

Equations

• s.printResources = (Lean.Cadical.Solver.solver✝ s).resources