structure Cvc.Sys.Candidate.Info {S : Symbols.Repr} (State : Symbols S) : Type

Basic candidate information.

• name : String

  Name of the candidate.

• pred : Symbols.StatePredicate

  State predicate of the candidate.

inductive Cvc.Sys.Candidate.Status {S : Symbols.Repr} (State : Symbols S) (α : Nat → Type) (length : Nat) : Type

Status of a candidate, only carries α-information when 0 < length.

• init {S : Symbols.Repr} {State : Symbols S} {α : Nat → Type} (info : Info State) : Status State α 0
• mk {S : Symbols.Repr} {State : Symbols S} {α : Nat → Type} {k : Nat} (info : Info State) (data : α k) : Status State α k.succ

def Cvc.Sys.Candidate.Status.info {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {α : Nat → Type} {len : Nat} : Status State α len → Info State

Candidate information.

Equations

• (Cvc.Sys.Candidate.Status.init info).info = info
• (Cvc.Sys.Candidate.Status.mk info data).info = info

def Cvc.Sys.Candidate.Status.decons {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {α : Nat → Type} {k : Nat} : Status State α k.succ → Info State × α k

Deconstructs a candidate status, only for Status _ (_ + 1).

Equations

• (Cvc.Sys.Candidate.Status.mk info data).decons = (info, data)

def Cvc.Sys.Candidate.Status.data {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {α : Nat → Type} {k : Nat} (status : Status State α k.succ) : α k

Data in a candidate status, only for State _ (_ + 1).

Equations

• status.data = status.decons.snd

def Cvc.Sys.Candidate.Status.name {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {α : Nat → Type} {length : Nat} (status : Status State α length) : String

Name of the candidate.

Equations

• status.name = status.info.name

def Cvc.Sys.Candidate.Status.pred {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {α : Nat → Type} {length : Nat} (status : Status State α length) : Symbols.StatePredicate

State predicate of the candidate.

Equations

• status.pred = status.info.pred

def Cvc.Sys.Candidate.Status.toString {α : Nat → Type} {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {length : Nat} [(k : Nat) → ToString (α k)] : Status State α length → String

String representation.

Equations

• (Cvc.Sys.Candidate.Status.init info).toString = toString "`" ++ toString info.name ++ toString "`: init"
• (Cvc.Sys.Candidate.Status.mk info data).toString = toString "`" ++ toString info.name ++ toString "`: " ++ toString data ++ toString ""

instance Cvc.Sys.Candidate.Status.instToString {α : Nat → Type} {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {length : Nat} [(k : Nat) → ToString (α k)] : ToString (Status State α length)

Equations

• Cvc.Sys.Candidate.Status.instToString = { toString := Cvc.Sys.Candidate.Status.toString }

structure Cvc.Sys.Candidate.Invariant.Data {S : Symbols.Repr} (State : Symbols S) (k : Nat) : Type

• provedAt : Nat
• posActlit : Actlit
• withCandidates : Array String
• withLemmas : Array Symbols.Predicate

def Cvc.Sys.Candidate.Invariant.Data.next {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (info : Info State) (nextState : Symbols.TermsAt k.succ) : Data State k → (activate : optParam Bool true) → Smt (Data State k.succ)

Equations

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

def Cvc.Sys.Candidate.Invariant.Data.toString {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (data : Data State k) : String

Equations

• data.toString = toString "" ++ toString data.provedAt ++ toString "-inductive"

instance Cvc.Sys.Candidate.Invariant.Data.instToString {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} : ToString (Data State k)

Equations

• Cvc.Sys.Candidate.Invariant.Data.instToString = { toString := Cvc.Sys.Candidate.Invariant.Data.toString }

@[reducible, inline]

abbrev Cvc.Sys.Candidate.Invariant {S : Symbols.Repr} (State : Symbols S) (length : Nat) : Type

Equations

• Cvc.Sys.Candidate.Invariant State = Cvc.Sys.Candidate.Status State (Cvc.Sys.Candidate.Invariant.Data State)

def Cvc.Sys.Candidate.Invariant.toString {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (inv : Invariant State depth) : String

Equations

• inv.toString = toString inv

def Cvc.Sys.Candidate.Invariant.provedAt {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (inv : Invariant State k.succ) : Nat

Equations

• inv.provedAt = (Cvc.Sys.Candidate.Status.data inv).provedAt

def Cvc.Sys.Candidate.Invariant.next {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (nextState : Symbols.TermsAt k.succ) : Invariant State k.succ → Smt (Invariant State k.succ.succ)

Equations

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

structure Cvc.Sys.Candidate.Falsified.Data {S : Symbols.Repr} (State : Symbols S) (k : Nat) : Type

• negActlit : Actlit
• falsifiedAt : Nat
• cex : State.ValueTrace self.falsifiedAt.succ

def Cvc.Sys.Candidate.Falsified.Data.next {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (info : Info State) (state : Symbols.TermsAt k.succ) : Data State k → Smt (Data State k.succ)

Equations

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

def Cvc.Sys.Candidate.Falsified.Data.toString {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (data : Data State k) : String

Equations

• data.toString = toString "falsified at " ++ toString data.falsifiedAt ++ toString ""

instance Cvc.Sys.Candidate.Falsified.Data.instToString {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} : ToString (Data State k)

Equations

• Cvc.Sys.Candidate.Falsified.Data.instToString = { toString := Cvc.Sys.Candidate.Falsified.Data.toString }

@[reducible, inline]

abbrev Cvc.Sys.Candidate.Falsified {S : Symbols.Repr} (State : Symbols S) (length : Nat) : Type

Equations

• Cvc.Sys.Candidate.Falsified State = Cvc.Sys.Candidate.Status State (Cvc.Sys.Candidate.Falsified.Data State)

def Cvc.Sys.Candidate.Falsified.toString {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (fls : Falsified State depth) : String

Equations

• fls.toString = toString fls

@[reducible, inline]

abbrev Cvc.Sys.Candidate.Falsified.falsifiedAt {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (fls : Falsified State k.succ) : Nat

Equations

• fls.falsifiedAt = (Cvc.Sys.Candidate.Status.data fls).falsifiedAt

def Cvc.Sys.Candidate.Falsified.cex {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (fls : Falsified State k.succ) : State.ValueTrace fls.falsifiedAt.succ

Equations

• fls.cex = (Cvc.Sys.Candidate.Status.data fls).cex

def Cvc.Sys.Candidate.Falsified.next {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (state : Symbols.TermsAt k.succ) : Falsified State k.succ → Smt (Falsified State k.succ.succ)

Equations

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

structure Cvc.Sys.Candidate.Unknown.Data {S : Symbols.Repr} (State : Symbols S) (k : Nat) : Type

• posActlit : Actlit
• currNegActlit : Actlit
• currPred : Formula
• baseValidUpTo : Option Nat
• stepInvalidUpTo : Option Nat
• stepValidAt : Option Nat

def Cvc.Sys.Candidate.Unknown.Data.isBaseValid {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (data : Data State k) : Bool

Equations

• data.isBaseValid = decide (data.baseValidUpTo = some k)

def Cvc.Sys.Candidate.Unknown.Data.isPrevBaseValid {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (data : Data State k) : Bool

Equations

• data.isPrevBaseValid = decide (k = 0 ∨ data.baseValidUpTo = some k.pred)

def Cvc.Sys.Candidate.Unknown.Data.isStepInvalid {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (data : Data State k) : Bool

Equations

• data.isStepInvalid = decide (k = 0 ∨ data.stepInvalidUpTo = some k)

def Cvc.Sys.Candidate.Unknown.Data.isPrevStepInvalid {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (data : Data State k) : Bool

Equations

• data.isPrevStepInvalid = decide (k = 0 ∨ data.stepInvalidUpTo = some k.pred)

def Cvc.Sys.Candidate.Unknown.Data.toString {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (data : Data State k) : String

Equations

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

instance Cvc.Sys.Candidate.Unknown.Data.instToString {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} : ToString (Data State k)

Equations

• Cvc.Sys.Candidate.Unknown.Data.instToString = { toString := Cvc.Sys.Candidate.Unknown.Data.toString }

def Cvc.Sys.Candidate.Unknown.Data.isInvariant? {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (data : Data State k) : Option Nat

Equations

• data.isInvariant? = do let baseK ← data.baseValidUpTo let stepK ← data.stepValidAt if stepK ≤ baseK.succ then pure stepK else none

def Cvc.Sys.Candidate.Unknown.Data.toInvariant? {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (data : Data State k) : Option (Invariant.Data State k)

Equations

• data.toInvariant? = do let invK ← data.isInvariant? pure { provedAt := invK, posActlit := data.posActlit, withCandidates := #[], withLemmas := #[] }

@[reducible, inline]

abbrev Cvc.Sys.Candidate.Unknown {S : Symbols.Repr} (State : Symbols S) (length : Nat) : Type

Equations

• Cvc.Sys.Candidate.Unknown State = Cvc.Sys.Candidate.Status State (Cvc.Sys.Candidate.Unknown.Data State)

def Cvc.Sys.Candidate.Unknown.toString {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (unk : Unknown State depth) : String

Equations

• unk.toString = toString unk

def Cvc.Sys.Candidate.Unknown.next {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (nextState : Symbols.TermsAt k) : Unknown State k → Smt (Unknown State k.succ)

Equations

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

def Cvc.Sys.Candidate.Unknown.baseValidUpTo? {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : Unknown State k.succ) : Option Nat

Equations

• unk.baseValidUpTo? = (Cvc.Sys.Candidate.Status.data unk).baseValidUpTo

def Cvc.Sys.Candidate.Unknown.isBaseValid {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : Unknown State k.succ) : Bool

Equations

• unk.isBaseValid = (Cvc.Sys.Candidate.Status.data unk).isBaseValid

def Cvc.Sys.Candidate.Unknown.isPrevBaseValid {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : Unknown State k.succ) : Bool

Equations

• unk.isPrevBaseValid = (Cvc.Sys.Candidate.Status.data unk).isPrevBaseValid

def Cvc.Sys.Candidate.Unknown.isStepInvalid {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : Unknown State k.succ) : Bool

Equations

• unk.isStepInvalid = (Cvc.Sys.Candidate.Status.data unk).isStepInvalid

def Cvc.Sys.Candidate.Unknown.isPrevStepInvalid {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : Unknown State k.succ) : Bool

Equations

• unk.isPrevStepInvalid = (Cvc.Sys.Candidate.Status.data unk).isPrevStepInvalid

def Cvc.Sys.Candidate.Unknown.isInvariant? {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : Unknown State k.succ) : Option Nat

Equations

• unk.isInvariant? = (Cvc.Sys.Candidate.Status.data unk).isInvariant?

def Cvc.Sys.Candidate.Unknown.toInvariant? {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : Unknown State k.succ) : Option (Invariant State k.succ)

Equations

• unk.toInvariant? = do let __do_lift ← (Cvc.Sys.Candidate.Status.data unk).toInvariant? pure (Cvc.Sys.Candidate.Status.mk (Cvc.Sys.Candidate.Status.info unk) __do_lift)

def Cvc.Sys.Candidate.Unknown.checkFalsified {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : Unknown State k.succ) : Smt.Sat Bool

Equations

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

def Cvc.Sys.Candidate.Unknown.confirmBase {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : Unknown State k.succ) : Res (Unknown State k.succ)

Equations

• unk.confirmBase = do let __do_lift ← Cvc.Sys.Candidate.Unknown.Data.confirmBase✝ (Cvc.Sys.Candidate.Status.data unk) pure (Cvc.Sys.Candidate.Status.updateData✝ __do_lift unk)

def Cvc.Sys.Candidate.Unknown.confirmStep {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : Unknown State k.succ.succ) : Res (Unknown State k.succ.succ)

Equations

• unk.confirmStep = do let __do_lift ← Cvc.Sys.Candidate.Unknown.Data.confirmStep✝ (Cvc.Sys.Candidate.Status.data unk) pure (Cvc.Sys.Candidate.Status.updateData✝ __do_lift unk)

def Cvc.Sys.Candidate.Unknown.invalidStep {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : Unknown State k.succ.succ) : Res (Unknown State k.succ.succ)

Equations

• unk.invalidStep = do let __do_lift ← Cvc.Sys.Candidate.Unknown.Data.invalidStep✝ (Cvc.Sys.Candidate.Status.data unk) pure (Cvc.Sys.Candidate.Status.updateData✝ __do_lift unk)

def Cvc.Sys.Candidate.mkUnknown {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} (name : String) (pred : Symbols.StatePredicate) : Unknown State 0

Equations

• Cvc.Sys.Candidate.mkUnknown name pred = Cvc.Sys.Candidate.Status.init { name := name, pred := fun {k : Nat} => pred }

inductive Cvc.Sys.Candidate {S : Symbols.Repr} (State : Symbols S) (k : Nat) : Type

• unknown {S : Symbols.Repr} {State : Symbols S} {k : Nat} : Unknown State k → Candidate State k
• invariant {S : Symbols.Repr} {State : Symbols S} {k : Nat} : Invariant State k → Candidate State k
• falsified {S : Symbols.Repr} {State : Symbols S} {k : Nat} : Falsified State k → Candidate State k

def Cvc.Sys.Candidate.map {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} {α : Sort u_1} (ifUnknown : Unknown State k → α) (ifInvariant : Invariant State k → α) (ifFalsified : Falsified State k → α) : Candidate State k → α

Equations

• Cvc.Sys.Candidate.map ifUnknown ifInvariant ifFalsified (Cvc.Sys.Candidate.unknown status) = ifUnknown status
• Cvc.Sys.Candidate.map ifUnknown ifInvariant ifFalsified (Cvc.Sys.Candidate.invariant status) = ifInvariant status
• Cvc.Sys.Candidate.map ifUnknown ifInvariant ifFalsified (Cvc.Sys.Candidate.falsified status) = ifFalsified status

def Cvc.Sys.Candidate.info {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (candidate : Candidate State k) : Info State

Equations

• candidate.info = Cvc.Sys.Candidate.map Cvc.Sys.Candidate.Status.info Cvc.Sys.Candidate.Status.info Cvc.Sys.Candidate.Status.info candidate

def Cvc.Sys.Candidate.name {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (c : Candidate State k) : String

Equations

• c.name = c.info.name

def Cvc.Sys.Candidate.pred {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (c : Candidate State k) : Symbols.StatePredicate

Equations

• c.pred = c.info.pred

def Cvc.Sys.Candidate.unknown? {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (candidate : Candidate State k) : Option (Unknown State k)

Equations

• candidate.unknown? = Cvc.Sys.Candidate.map some (Cvc.𝕂 none) (Cvc.𝕂 none) candidate

def Cvc.Sys.Candidate.invariant? {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (candidate : Candidate State k) : Option (Invariant State k)

Equations

• candidate.invariant? = Cvc.Sys.Candidate.map (Cvc.𝕂 none) some (Cvc.𝕂 none) candidate

def Cvc.Sys.Candidate.falsified? {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (candidate : Candidate State k) : Option (Falsified State k)

Equations

• candidate.falsified? = Cvc.Sys.Candidate.map (Cvc.𝕂 none) (Cvc.𝕂 none) some candidate

def Cvc.Sys.Candidate.isUnknown {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (candidate : Candidate State k) : Bool

Equations

• candidate.isUnknown = candidate.unknown?.isSome

def Cvc.Sys.Candidate.isInvariant {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (candidate : Candidate State k) : Bool

Equations

• candidate.isInvariant = candidate.invariant?.isSome

def Cvc.Sys.Candidate.isFalsified {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (candidate : Candidate State k) : Bool

Equations

• candidate.isFalsified = candidate.falsified?.isSome

@[reducible, inline]

abbrev Cvc.Sys.Candidate.Map (α : Type) : Type

Equations

• Cvc.Sys.Candidate.Map α = Cvc.RBMap String α

def Cvc.Sys.Candidate.Map.valsToLines {α : Type} [ToString α] (map : Map α) (desc : String) (pref : String := "") : Array String

Equations

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

@[reducible, inline]

abbrev Cvc.Sys.Candidate.UnknownMap {S : Symbols.Repr} (State : Symbols S) (depth : Nat) : Type

Equations

• Cvc.Sys.Candidate.UnknownMap State depth = Cvc.Sys.Candidate.Map (Cvc.Sys.Candidate.Unknown State depth)

def Cvc.Sys.Candidate.UnknownMap.toLines {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (unk : UnknownMap State depth) (pref : String := "") : Array String

Equations

• unk.toLines pref = Cvc.Sys.Candidate.Map.valsToLines unk "unknown" pref

def Cvc.Sys.Candidate.UnknownMap.addBaseActivators {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : UnknownMap State k.succ) (activators : Array Formula) : Term.Build (Array Formula)

Equations

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

def Cvc.Sys.Candidate.UnknownMap.addStepActivators {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : UnknownMap State k.succ) (activators : Array Formula) : Term.Build (Array Formula)

Equations

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

def Cvc.Sys.Candidate.UnknownMap.isNextBaseReady {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : UnknownMap State k.succ) : Bool

Equations

• unk.isNextBaseReady = Batteries.RBMap.all unk fun (x : String) (unk : Cvc.Sys.Candidate.Unknown State k.succ) => unk.isBaseValid

def Cvc.Sys.Candidate.UnknownMap.isNextStepReady {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (unk : UnknownMap State k.succ) : Bool

Equations

• unk.isNextStepReady = Batteries.RBMap.all unk fun (x : String) (unk : Cvc.Sys.Candidate.Unknown State k.succ) => unk.isStepInvalid

@[reducible, inline]

abbrev Cvc.Sys.Candidate.InvariantMap {S : Symbols.Repr} (State : Symbols S) (depth : Nat) : Type

Equations

• Cvc.Sys.Candidate.InvariantMap State depth = Cvc.Sys.Candidate.Map (Cvc.Sys.Candidate.Invariant State depth)

def Cvc.Sys.Candidate.InvariantMap.toLines {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (inv : InvariantMap State depth) (pref : String := "") : Array String

Equations

• inv.toLines pref = Cvc.Sys.Candidate.Map.valsToLines inv "invariant" pref

def Cvc.Sys.Candidate.InvariantMap.addActivators {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (inv : InvariantMap State k.succ) (activators : Array Formula) : Array Formula

Equations

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

@[reducible, inline]

abbrev Cvc.Sys.Candidate.FalsifiedMap {S : Symbols.Repr} (State : Symbols S) (depth : Nat) : Type

Equations

• Cvc.Sys.Candidate.FalsifiedMap State depth = Cvc.Sys.Candidate.Map (Cvc.Sys.Candidate.Falsified State depth)

def Cvc.Sys.Candidate.FalsifiedMap.toLines {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (fls : FalsifiedMap State depth) (pref : String := "") : Array String

Equations

• fls.toLines pref = Cvc.Sys.Candidate.Map.valsToLines fls "falsified" pref

inductive Cvc.Sys.Candidates {S : Symbols.Repr} (State : Symbols S) (depth : Nat) : Type

• init {S : Symbols.Repr} {State : Symbols S} (candidates : UnknownMap State 0 := RBMap.empty) : Candidates State 0
• mk {S : Symbols.Repr} {State : Symbols S} {k : Nat} (unknown : UnknownMap State k.succ) (invariant : InvariantMap State k.succ) (falsified : FalsifiedMap State k.succ) : Candidates State k.succ

def Cvc.Sys.Candidates.empty {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} : Candidates State 0

Equations

• Cvc.Sys.Candidates.empty = Cvc.Sys.Candidates.init

def Cvc.Sys.Candidates.toLines {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (pref : String := "") : Candidates State depth → Array String

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Sys.Candidates.toLines pref (Cvc.Sys.Candidates.init unk) = (#[pref ++ "candidates in init {"] ++ unk.toLines (pref ++ " ")).push (pref ++ "}")

def Cvc.Sys.Candidates.unknown {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} : Candidates State depth → UnknownMap State depth

Equations

• (Cvc.Sys.Candidates.init unk).unknown = unk
• (Cvc.Sys.Candidates.mk unk inv fls).unknown = unk

def Cvc.Sys.Candidates.isDone {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (cs : Candidates State depth) : Bool

Equations

• cs.isDone = Batteries.RBMap.isEmpty cs.unknown

@[reducible, inline]

abbrev Cvc.Sys.Candidates.isNextBaseReady {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (self : Candidates State depth) : Bool

Equations

• (Cvc.Sys.Candidates.init unk).isNextBaseReady = true
• (Cvc.Sys.Candidates.mk unk inv fls).isNextBaseReady = unk.isNextBaseReady

@[simp]

theorem Cvc.Sys.Candidates.isNextBaseReady_0 {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} (self : Candidates State 0) : self.isNextBaseReady = true

@[reducible, inline]

abbrev Cvc.Sys.Candidates.isNextStepReady {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (self : Candidates State depth) : Bool

Equations

• (Cvc.Sys.Candidates.init unk).isNextStepReady = true
• (Cvc.Sys.Candidates.mk unk inv fls).isNextStepReady = unk.isNextStepReady

@[simp]

theorem Cvc.Sys.Candidates.isNextStepReady_0 {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} (self : Candidates State 0) : self.isNextStepReady = true

def Cvc.Sys.Candidates.invariant {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} : Candidates State depth.succ → InvariantMap State depth.succ

Equations

• (Cvc.Sys.Candidates.mk unknown inv falsified).invariant = inv

def Cvc.Sys.Candidates.falsified {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} : Candidates State depth.succ → FalsifiedMap State depth.succ

Equations

• (Cvc.Sys.Candidates.mk unknown inv falsified).falsified = falsified

def Cvc.Sys.Candidates.insertFalsified {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (newFls : Falsified State k.succ) : Candidates State k.succ → Res (Candidates State k.succ)

Equations

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

def Cvc.Sys.Candidates.insertInvariant {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (newInv : Invariant State k.succ) : Candidates State k.succ → Res (Candidates State k.succ)

Equations

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

def Cvc.Sys.Candidates.insertUnknown {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (newUnk : Unknown State depth) : Candidates State depth → Res (Candidates State depth)

Equations

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

instance Cvc.Sys.Candidates.instForInCandidate {m : Type u_1 → Type u_2} {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} : ForIn m (Candidates State depth) (Candidate State depth)

Equations

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

def Cvc.Sys.Candidates.isEmpty {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} : Candidates State depth → Bool

Equations

• (Cvc.Sys.Candidates.init unk).isEmpty = Batteries.RBMap.isEmpty unk
• (Cvc.Sys.Candidates.mk unk inv fls).isEmpty = decide (Batteries.RBMap.isEmpty unk = true ∧ Batteries.RBMap.isEmpty inv = true ∧ Batteries.RBMap.isEmpty fls = true)

def Cvc.Sys.Candidates.unknownCount {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (cs : Candidates State depth.succ) : Nat

Equations

• cs.unknownCount = Batteries.RBMap.size cs.unknown

def Cvc.Sys.Candidates.invariantCount {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (cs : Candidates State depth.succ) : Nat

Equations

• cs.invariantCount = Batteries.RBMap.size cs.invariant

def Cvc.Sys.Candidates.falsifiedCount {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (cs : Candidates State depth.succ) : Nat

Equations

• cs.falsifiedCount = Batteries.RBMap.size cs.falsified

def Cvc.Sys.Candidates.addBaseActivators {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (cs : Candidates State depth.succ) : Array Formula → Term.Build (Array Formula)

Equations

• cs.addBaseActivators = cs.unknown.addBaseActivators

def Cvc.Sys.Candidates.addStepActivators {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {depth : Nat} (cs : Candidates State depth.succ) : Array Formula → Term.Build (Array Formula)

Equations

• cs.addStepActivators = cs.unknown.addStepActivators ∘ cs.invariant.addActivators

def Cvc.Sys.Candidates.next' {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (state : Symbols.TermsAt k) (candidates : Candidates State k) : Smt (Candidates State k.succ)

Equations

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

def Cvc.Sys.Candidates.next {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (state : Symbols.TermsAt k) (candidates : Candidates State k) (h : ¬candidates.isDone = true := by assumption) : Smt (Candidates State k.succ)

Equations

• Cvc.Sys.Candidates.next state candidates x = Cvc.Sys.Candidates.next' state candidates

def Cvc.Sys.Candidates.registerBaseCex {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (self : Candidates State k.succ) (cex : State.ValueTrace k.succ) : Smt.Sat (Candidates State k.succ)

Equations

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

def Cvc.Sys.Candidates.registerBaseUnsat {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (self : Candidates State k.succ) : Smt.Unsat (Candidates State k.succ)

Equations

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

def Cvc.Sys.Candidates.registerStepCex {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (self : Candidates State k.succ.succ) : Smt.Sat (Candidates State k.succ.succ)

Equations

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

def Cvc.Sys.Candidates.registerStepUnsat {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (self : Candidates State k.succ.succ) : Smt.Unsat (Candidates State k.succ.succ)

Equations

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