structure Cvc.Symbols.Unroller {Struct : Symbols.Repr} (State : Symbols Struct) (length : Nat) : Type

Unroller for a trace of length states.

• mk' :: (
• idents : Idents

  State identifiers.

• init : StatePred

  Init predicate.

• step : StateRel

  Step predicate.

• trace : State.TermTrace length

  Trace of symbol-terms.

• )

def Cvc.Symbols.Unroller.mk {Struct : Symbols.Repr} [State : Symbols Struct] (idents : Idents) (init : StatePred) (step : StateRel) : State.Unroller 0

Constructs an unroller for 0 states.

Equations

• Cvc.Symbols.Unroller.mk idents init step = { idents := idents, init := fun {k : Nat} => init, step := fun {k : Nat} => step, trace := Cvc.Symbols.Trace.empty }

@[reducible, inline]

abbrev Cvc.Symbols.Unroller.length {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {length : Nat} : State.Unroller length → Nat

Number of states in an unroller's trace.

Equations

• Cvc.Symbols.Unroller.length = Cvc.𝕂 length

@[reducible, inline]

abbrev Cvc.Symbols.Unroller.Idx {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {length : Nat} : State.Unroller length → Type

Type of legal state indices in an unroller.

Equations

• Cvc.Symbols.Unroller.Idx = Cvc.𝕂 (Fin length)

@[reducible, inline]

abbrev Cvc.Symbols.Unroller.CexTrace {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {length : Nat} (sys : State.Unroller length) : Type

Alias for a trace of symbol-values.

Equations

• sys.CexTrace = State.ValueTrace sys.length

def Cvc.Symbols.Unroller.getTermsAt {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {length : Nat} (sys : State.Unroller length) (i : sys.Idx) : TermsAt ↑i

Retrieves the symbol-terms at some index.

Equations

• sys.getTermsAt i = Cvc.Symbols.Trace.get sys.trace ↑i ⋯

def Cvc.Symbols.Unroller.extractCex {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {length : Nat} (sys : State.Unroller length) : Smt.Sat sys.CexTrace

Extracts a trace of state-values in a sat context.

Equations

• sys.extractCex = Cvc.Symbols.Trace.mapM sys.trace fun (x : Fin length) (terms : Cvc.Symbols.TermsAt ↑x) => terms.getValues

@[reducible, inline]

abbrev Cvc.Symbols.Unroller.idx0 {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (sys : State.Unroller k.succ) : sys.Idx

Index 0 as a legal index for a non-empty unroller.

Equations

• sys.idx0 = ⟨0, ⋯⟩

@[reducible, inline]

abbrev Cvc.Symbols.Unroller.idxLast {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (sys : State.Unroller k.succ) : sys.Idx

Last index of a non-empty unroller.

Equations

• sys.idxLast = ⟨k, ⋯⟩

@[reducible, inline]

abbrev Cvc.Symbols.Unroller.getTerms0 {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (sys : State.Unroller k.succ) : TermsAt 0

Retrieves the symbol-terms at index 0 in a non-empty unroller.

Equations

• sys.getTerms0 = sys.getTermsAt sys.idx0

@[reducible, inline]

abbrev Cvc.Symbols.Unroller.getTermsLast {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (sys : State.Unroller k.succ) : TermsAt k

Retrieves the symbol-terms at the highest index in a non-empty unroller.

Equations

• sys.getTermsLast = sys.getTermsAt sys.idxLast

def Cvc.Symbols.Unroller.checkSatAnd {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {m : Type → Type} {α : Type} {k : Nat} (sys : State.Unroller k.succ) [Monad m] (init : Bool) (assuming : Array Formula := #[]) (ifSat : Smt.SatT m α := Smt.Sat.unexpected) (ifUnsat : Smt.UnsatT m α := Smt.Unsat.unexpected) (ifUnknown : Smt.UnknownT m α := Smt.Unknown.unexpected) : SmtT m α

Smt.checkSatAnd with the init flag (de)activating that state 0 is initial.

Equations

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

def Cvc.Symbols.Unroller.checkSatBaseAnd {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {m : Type → Type} {α : Type} {k : Nat} (sys : State.Unroller k.succ) [Monad m] (assuming : Array Formula := #[]) (ifSat : Smt.SatT m α := Smt.Sat.unexpected) (ifUnsat : Smt.UnsatT m α := Smt.Unsat.unexpected) (ifUnknown : Smt.UnknownT m α := Smt.Unknown.unexpected) : SmtT m α

Performs a base check, i.e. state 0 is initial.

Equations

• sys.checkSatBaseAnd assuming ifSat ifUnsat ifUnknown = sys.checkSatAnd true assuming ifSat ifUnsat ifUnknown

def Cvc.Symbols.Unroller.checkSatStepAnd {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {m : Type → Type} {α : Type} {k : Nat} (sys : State.Unroller k.succ) [Monad m] (assuming : Array Formula := #[]) (ifSat : Smt.SatT m α := Smt.Sat.unexpected) (ifUnsat : Smt.UnsatT m α := Smt.Unsat.unexpected) (ifUnknown : Smt.UnknownT m α := Smt.Unknown.unexpected) : SmtT m α

Performs a step check, i.e. state 0 is not initial.

Equations

• sys.checkSatStepAnd assuming ifSat ifUnsat ifUnknown = sys.checkSatAnd false assuming ifSat ifUnsat ifUnknown

def Cvc.Symbols.Unroller.findCex? {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {k : Nat} (sys : State.Unroller k.succ) (init : Bool) (assuming : Array Formula := #[]) : Smt (Option sys.CexTrace)

Performs a Unroller.checkSatAnd and extracts a cex trace if sat.

• init: controls whether state 0 must be an initial state.

Equations

• sys.findCex? init assuming = sys.checkSatAnd init assuming (some <$> sys.extractCex) (pure none)

def Cvc.Symbols.Unroller.unroll {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {length : Nat} (sys : State.Unroller length) : Smt (TermsAt length × State.Unroller length.succ)

Unrolls one state further.

Equations

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

def Cvc.Symbols.Unroller.unroll' {Struct✝ : Symbols.Repr} {State : Symbols Struct✝} {length : Nat} (sys : State.Unroller length) : Smt (State.Unroller length.succ)

Unrolls one state further.

Equations

• sys.unroll' = Prod.snd <$> sys.unroll