@[reducible, inline]

abbrev Alphabet (arity : Type) [FinEnum arity] : Type

Equations

• Alphabet arity = BitVec (FinEnum.card arity + 1)

def finFunToBitVec {carry : Type u_1} (c : carry → Bool) [FinEnum carry] : BitVec (FinEnum.card carry)

Equations

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

def bitVecToFinFun {ar : Sort u_1} [FinEnum ar] (bv : BitVec (FinEnum.card ar)) : ar → Bool

Equations

• bitVecToFinFun bv c = bv[FinEnum.equiv.toFun c]

def NFA.ofFSM {arity : Type} [FinEnum arity] (p : AutoStructs.FSM arity) [FinEnum p.α] : NFA (Alphabet arity)

Transforms an FSM of arity k to an NFA of arity k+1. This correponds to transforming a function with k inputs and one output to a k+1-ary relation. By convention, the output is the MSB of the alphabet.

Equations

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

partial def NFA.ofFSM.go {arity : Type} [FinEnum arity] (p : AutoStructs.FSM arity) [FinEnum p.α] (st : fsm.State (FinEnum.card p.α)) : NFA (Alphabet arity)

def NFA.ofConst {w : ℕ} (bv : BitVec w) : NFA (BitVec 1)

Equations

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

def NFA.autEq : NFA (BitVec 2)

Equations

• NFA.autEq = match NFA.empty.newState with | (s, m) => let m := m.addInitial s; let m := m.addFinal s; let m := m.addTrans 0 s s; let m := m.addTrans 3 s s; m

def NFA.autSignedCmp (cmp : AutoStructs.RelationOrdering) : NFA (BitVec 2)

Equations

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

def NFA.autUnsignedCmp (cmp : AutoStructs.RelationOrdering) : NFA (BitVec 2)

Equations

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

def NFA.autMsbSet : NFA (BitVec 1)

Equations

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

def liftMaxSucc1 (n : ℕ) (m : ℕ) : Fin (n + 1) → Fin (max n m + 2)

Equations

• liftMaxSucc1 n m k = if x : k = ↑n then ↑↑(Fin.last (max n m)) else Fin.castLE ⋯ k

def liftMaxSucc2 (n : ℕ) (m : ℕ) : Fin (m + 1) → Fin (max n m + 2)

Equations

• liftMaxSucc2 n m k = if x : k = ↑m then Fin.last (max n m + 1) else Fin.castLE ⋯ k

def liftLast2 (n : ℕ) : Fin 2 → Fin (n + 2)

Equations

• liftLast2 n 0 = ↑n
• liftLast2 n 1 = ↑n + 1

def liftExcecpt2 (n : ℕ) : Fin n → Fin (n + 2)

Equations

• liftExcecpt2 n k = Fin.castLE ⋯ k

def liftMax1 (n : ℕ) (m : ℕ) : Fin n → Fin (max n m)

Equations

• liftMax1 n m k = Fin.castLE ⋯ k

def liftMax2 (n : ℕ) (m : ℕ) : Fin m → Fin (max n m)

Equations

• liftMax2 n m k = Fin.castLE ⋯ k

@[simp]

theorem finEnumCardFin (n : ℕ) : FinEnum.card (Fin n) = n

def AutoStructs.Relation.autOfRelation : AutoStructs.Relation → NFA (BitVec 2)

Equations

• AutoStructs.Relation.eq.autOfRelation = NFA.autEq
• (AutoStructs.Relation.signed ord).autOfRelation = NFA.autSignedCmp ord
• (AutoStructs.Relation.unsigned ord).autOfRelation = NFA.autUnsignedCmp ord

def unopNfa {A : Type} [BEq A] [FinEnum A] [Hashable A] (op : AutoStructs.Unop) (m : NFA A) : NFA A

Equations

• unopNfa AutoStructs.Unop.neg m = m.neg

def binopNfa {A : Type} [BEq A] [FinEnum A] [Hashable A] (op : AutoStructs.Binop) (m1 : NFA A) (m2 : NFA A) : NFA A

Equations

• binopNfa AutoStructs.Binop.and m1 m2 = m1.inter m2
• binopNfa AutoStructs.Binop.or m1 m2 = m1.union m2
• binopNfa AutoStructs.Binop.impl m1 m2 = m1.neg.union m2
• binopNfa AutoStructs.Binop.equiv m1 m2 = (m1.neg.union m2).inter (m2.neg.union m1)

def nfaOfFormula (φ : AutoStructs.Formula) : NFA (BitVec φ.arity)

Equations

• One or more equations did not get rendered due to their size.
• nfaOfFormula (AutoStructs.Formula.unop op φ_2) = unopNfa op (nfaOfFormula φ_2)
• nfaOfFormula (AutoStructs.Formula.binop op φ1 φ2) = binopNfa op ((nfaOfFormula φ1).lift (liftMax1 φ1.arity φ2.arity)) ((nfaOfFormula φ2).lift (liftMax2 φ1.arity φ2.arity))

def formulaIsUniversal (f : AutoStructs.Formula) : Bool

Equations

• formulaIsUniversal f = (nfaOfFormula f).isUniversal'

axiom decision_procedure_is_correct {w : ℕ} (φ : AutoStructs.Formula) (env : ℕ → BitVec w) : formulaIsUniversal φ = true → φ.sat' env