def Auto.IR.SMT.isSimpleSymbol (s : String) : Bool

Equations

• Auto.IR.SMT.isSimpleSymbol s = (s.length != 0 && (s.front.isAlpha || "~!@$%^&*_-+=<>.?/".contains s.front) && s.all fun (c : Char) => c.isAlphanum || "~!@$%^&*_-+=<>.?/".contains c)

inductive Auto.IR.SMT.SIdent : Type

• symb : String → SIdent
• indexed : String → Array (String ⊕ Nat) → SIdent

instance Auto.IR.SMT.instBEqSIdent : BEq SIdent

Equations

• Auto.IR.SMT.instBEqSIdent = { beq := Auto.IR.SMT.beqSIdent✝ }

instance Auto.IR.SMT.instHashableSIdent : Hashable SIdent

Equations

• Auto.IR.SMT.instHashableSIdent = { hash := Auto.IR.SMT.hashSIdent✝ }

instance Auto.IR.SMT.instInhabitedSIdent : Inhabited SIdent

Equations

• Auto.IR.SMT.instInhabitedSIdent = { default := Auto.IR.SMT.SIdent.symb default }

def Auto.IR.SMT.SIdent.toString : SIdent → String

Equations

• One or more equations did not get rendered due to their size.
• (Auto.IR.SMT.SIdent.symb a).toString = if Auto.IR.SMT.isSimpleSymbol a = true then a else "|" ++ a ++ "|"

instance Auto.IR.SMT.instToStringSIdent : ToString SIdent

Equations

• Auto.IR.SMT.instToStringSIdent = { toString := Auto.IR.SMT.SIdent.toString }

inductive Auto.IR.SMT.SSort : Type

• bvar : Nat → SSort
• app : SIdent → Array SSort → SSort

instance Auto.IR.SMT.instBEqSSort : BEq SSort

Equations

• Auto.IR.SMT.instBEqSSort = { beq := Auto.IR.SMT.beqSSort✝ }

instance Auto.IR.SMT.instHashableSSort : Hashable SSort

Equations

• Auto.IR.SMT.instHashableSSort = { hash := Auto.IR.SMT.hashSSort✝ }

instance Auto.IR.SMT.instInhabitedSSort : Inhabited SSort

Equations

• Auto.IR.SMT.instInhabitedSSort = { default := Auto.IR.SMT.SSort.bvar default }

def Auto.IR.SMT.SSort.toString (s : SSort) (binders : Array SIdent) : String

Equations

• s.toString binders = Auto.IR.SMT.SSort.toStringAux✝ s binders.toList

instance Auto.IR.SMT.instToStringSSort : ToString SSort

Caution : Do not use this in define-sort, because sort there might contain bvars

Equations

• Auto.IR.SMT.instToStringSSort = { toString := fun (s : Auto.IR.SMT.SSort) => s.toString #[] }

inductive Auto.IR.SMT.QualIdent : Type

〈qual_identifier〉 ::= 〈identifier〉 | ( as 〈identifier〉 〈sort〉 )

• ident : SIdent → QualIdent
• qualed : SIdent → SSort → QualIdent

instance Auto.IR.SMT.instBEqQualIdent : BEq QualIdent

Equations

• Auto.IR.SMT.instBEqQualIdent = { beq := Auto.IR.SMT.beqQualIdent✝ }

instance Auto.IR.SMT.instHashableQualIdent : Hashable QualIdent

Equations

• Auto.IR.SMT.instHashableQualIdent = { hash := Auto.IR.SMT.hashQualIdent✝ }

instance Auto.IR.SMT.instInhabitedQualIdent : Inhabited QualIdent

Equations

• Auto.IR.SMT.instInhabitedQualIdent = { default := Auto.IR.SMT.QualIdent.ident default }

def Auto.IR.SMT.QualIdent.ofString (s : String) : QualIdent

Equations

• Auto.IR.SMT.QualIdent.ofString s = Auto.IR.SMT.QualIdent.ident (Auto.IR.SMT.SIdent.symb s)

instance Auto.IR.SMT.instToStringQualIdent : ToString QualIdent

Equations

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

structure Auto.IR.SMT.MatchCase (α : Sort u) : Sort (max 1 u)

• constr : String
• args : Array String
• body : α

inductive Auto.IR.SMT.SpecConst : Type

• str : String → SpecConst
• binary : List Bool → SpecConst
• num : Nat → SpecConst

def Auto.IR.SMT.SpecConst.toString : SpecConst → String

Equations

• (Auto.IR.SMT.SpecConst.str s).toString = "\"" ++ String.join (List.map Auto.IR.SMT.SpecConst.toString.specCharRepr s.toList) ++ "\""
• (Auto.IR.SMT.SpecConst.binary bs).toString = List.foldl (fun (acc : String) (b : Bool) => acc.push (if b = true then '1' else '0')) "#b" bs
• (Auto.IR.SMT.SpecConst.num n).toString = toString (repr n)

def Auto.IR.SMT.SpecConst.toString.specCharRepr (c : Char) : String

Equations

• Auto.IR.SMT.SpecConst.toString.specCharRepr c = "\\u{" ++ { data := Nat.toDigits 16 c.toNat } ++ "}"

inductive Auto.IR.SMT.STerm : Type

• sConst : SpecConst → STerm
• bvar : Nat → STerm
• qIdApp : QualIdent → Array STerm → STerm
• testerApp : String → STerm → STerm
• letE (name : String) (binding body : STerm) : STerm
• forallE (name : String) (binderType : SSort) (body : STerm) : STerm
• existE (name : String) (binderType : SSort) (body : STerm) : STerm
• matchE (matchTerm : STerm) : Array (MatchCase STerm) → STerm
• attr : STerm → Array Attribute → STerm

inductive Auto.IR.SMT.Attribute : Type

〈attribute_value〉 ::= 〈spec_constant〉 | 〈symbol〉 | (〈s_expr〉∗ ) 〈attribute〉 ::= 〈keyword〉 | 〈keyword〉〈attribute_value〉

• none : String → Attribute
• spec : String → SpecConst → Attribute
• symb : String → String → Attribute
• sexpr : String → Array STerm → Attribute

def Auto.IR.SMT.STerm.qStrApp (s : String) (arr : Array STerm) : STerm

Equations

• Auto.IR.SMT.STerm.qStrApp s arr = Auto.IR.SMT.STerm.qIdApp (Auto.IR.SMT.QualIdent.ofString s) arr

def Auto.IR.SMT.STerm.attrApp (name : String) (attrTerm term : STerm) : STerm

Equations

• Auto.IR.SMT.STerm.attrApp name attrTerm (term'.attr attrs') = term'.attr (#[Auto.IR.SMT.STerm.attrApp.attr name attrTerm] ++ attrs')
• Auto.IR.SMT.STerm.attrApp name attrTerm term = term.attr #[Auto.IR.SMT.STerm.attrApp.attr name attrTerm]

def Auto.IR.SMT.STerm.attrApp.attr (name : String) (attrTerm : STerm) : Attribute

Equations

• Auto.IR.SMT.STerm.attrApp.attr name (Auto.IR.SMT.STerm.sConst (Auto.IR.SMT.SpecConst.str "")) = Auto.IR.SMT.Attribute.none name
• Auto.IR.SMT.STerm.attrApp.attr name (Auto.IR.SMT.STerm.sConst (Auto.IR.SMT.SpecConst.str sym)) = Auto.IR.SMT.Attribute.symb name sym
• Auto.IR.SMT.STerm.attrApp.attr name (Auto.IR.SMT.STerm.sConst c) = Auto.IR.SMT.Attribute.spec name c
• Auto.IR.SMT.STerm.attrApp.attr name attrTerm = Auto.IR.SMT.Attribute.sexpr name #[attrTerm]

def Auto.IR.SMT.STerm.toString (t : STerm) (binders : Array SIdent) : String

Equations

• t.toString binders = Auto.IR.SMT.STerm.toStringAux✝ t binders.toList

instance Auto.IR.SMT.instToStringSTerm : ToString STerm

Equations

• Auto.IR.SMT.instToStringSTerm = { toString := fun (t : Auto.IR.SMT.STerm) => t.toString #[] }

def Auto.IR.SMT.Attribute.toString (attr : Attribute) (binders : Array SIdent) : String

Equations

• attr.toString binders = Auto.IR.SMT.STerm.toStringAux.attrToStringAux✝ attr binders.toList

instance Auto.IR.SMT.instToStringAttribute : ToString Attribute

Equations

• Auto.IR.SMT.instToStringAttribute = { toString := fun (attr : Auto.IR.SMT.Attribute) => attr.toString #[] }

structure Auto.IR.SMT.ConstrDecl : Type

〈selector_dec〉 ::= ( 〈symbol〉 〈sort〉 ) 〈constructor_dec〉 ::= ( 〈symbol〉 〈selector_dec〉∗ )

• name : String
• selDecls : Array (String × SSort)

def Auto.IR.SMT.ConstrDecl.toString : ConstrDecl → Array SIdent → String

Equations

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

structure Auto.IR.SMT.DatatypeDecl : Type

〈datatype_dec〉 ::= ( 〈constructor_dec〉+ ) | ( par ( 〈symbol 〉+ ) ( 〈constructor_dec〉+ ) )

• params : Array String
• cstrDecls : Array ConstrDecl

def Auto.IR.SMT.DatatypeDecl.toString : DatatypeDecl → String

Equations

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

inductive Auto.IR.SMT.SMTOption : Type

• diagnosticOC : String → SMTOption
• globalDecl : Bool → SMTOption
• interactiveMode : Bool → SMTOption
• printSuccess : Bool → SMTOption
• produceAssertions : Bool → SMTOption
• produceAssignments : Bool → SMTOption
• produceModels : Bool → SMTOption
• produceProofs : Bool → SMTOption
• produceUnsatAssumptions : Bool → SMTOption
• produceUnsatCores : Bool → SMTOption
• randomSeed : Nat → SMTOption
• regularOutputChannel : String → SMTOption
• reproducibleResourceLim : Nat → SMTOption
• verbosity : Nat → SMTOption
• attr : Attribute → SMTOption

def Auto.IR.SMT.SMTOption.toString : SMTOption → String

Equations

• (Auto.IR.SMT.SMTOption.diagnosticOC s).toString = toString ":diagnostic-output-channel " ++ toString s ++ toString ""
• (Auto.IR.SMT.SMTOption.globalDecl b).toString = toString ":global-declarations " ++ toString b ++ toString ""
• (Auto.IR.SMT.SMTOption.interactiveMode b).toString = toString ":interactive-mode " ++ toString b ++ toString ""
• (Auto.IR.SMT.SMTOption.printSuccess b).toString = toString ":print-success " ++ toString b ++ toString ""
• (Auto.IR.SMT.SMTOption.produceAssertions b).toString = toString ":produce-assertions " ++ toString b ++ toString ""
• (Auto.IR.SMT.SMTOption.produceAssignments b).toString = toString ":produce-assignments " ++ toString b ++ toString ""
• (Auto.IR.SMT.SMTOption.produceModels b).toString = toString ":produce-models " ++ toString b ++ toString ""
• (Auto.IR.SMT.SMTOption.produceProofs b).toString = toString ":produce-proofs " ++ toString b ++ toString ""
• (Auto.IR.SMT.SMTOption.produceUnsatAssumptions b).toString = toString ":produce-unsat-assumptions " ++ toString b ++ toString ""
• (Auto.IR.SMT.SMTOption.produceUnsatCores b).toString = toString ":produce-unsat-cores " ++ toString b ++ toString ""
• (Auto.IR.SMT.SMTOption.randomSeed n).toString = toString ":random-seed " ++ toString n ++ toString ""
• (Auto.IR.SMT.SMTOption.regularOutputChannel s).toString = toString ":regular-output-channel " ++ toString s ++ toString ""
• (Auto.IR.SMT.SMTOption.reproducibleResourceLim n).toString = toString ":reproducible-resource-limit " ++ toString n ++ toString ""
• (Auto.IR.SMT.SMTOption.verbosity n).toString = toString ":verbosity " ++ toString n ++ toString ""
• (Auto.IR.SMT.SMTOption.attr a).toString = toString a

instance Auto.IR.SMT.instToStringSMTOption : ToString SMTOption

Equations

• Auto.IR.SMT.instToStringSMTOption = { toString := Auto.IR.SMT.SMTOption.toString }

inductive Auto.IR.SMT.Command : Type

〈sorted_var〉 ::= ( 〈symbol〉 〈sort〉 ) 〈datatype_dec〉 ::= ( 〈constructor_dec〉+ ) | ( par ( 〈symbol〉+ ) ( 〈constructor_dec〉+ ) ) 〈function_dec〉 ::= ( 〈symbol〉 ( 〈sorted_var〉∗ ) 〈sort〉 ) 〈function_def〉 ::= 〈symbol〉 ( 〈sorted_var〉∗ ) 〈sort〉 〈term〉 command ::= ( assert 〈term〉 ) ( check-sat ) ... ( declare-fun 〈symbol〉 ( 〈sort〉∗ ) 〈sort〉 ) ( declare-sort 〈symbol〉 〈numeral〉 ) ( define-fun 〈function_def〉 ) ( define-fun-rec 〈function_def〉 ) ( define-funs-rec ( ⟨function_dec⟩ⁿ⁺¹ ) ( ⟨term⟩ⁿ⁺¹ ) ) ( define-sort 〈symbol〉 ( 〈symbol〉∗ ) 〈sort〉 ) ( declare-datatype 〈symbol〉 〈datatype_dec〉) ... ( get-model ) ( get-option 〈keyword〉 ) ( get-proof ) ( get-unsat-assumptions ) ( get-unsat-core ) ... ( set-option 〈option〉 ) ( set-logic 〈symbol 〉 )

• assert (prop : STerm) : Command
• setLogic : String → Command
• setOption : SMTOption → Command
• getModel : Command
• getOption : String → Command
• getProof : Command
• getUnsatAssumptions : Command
• getUnsatCore : Command
• checkSat : Command
• declFun (name : String) (argSorts : Array SSort) (resSort : SSort) : Command
• declSort (name : String) (arity : Nat) : Command
• defFun (isRec : Bool) (name : String) (args : Array (String × SSort)) (resTy : SSort) (body : STerm) : Command
• defFuns : Array (String × Array (String × SSort) × SSort × STerm) → Command
• defSort (name : String) (args : Array String) (body : SSort) : Command
• declDtype (name : String) : DatatypeDecl → Command
• declDtypes : Array (String × Nat × DatatypeDecl) → Command
• echo : String → Command
• exit : Command

def Auto.IR.SMT.Command.toString : Command → String

Equations

• One or more equations did not get rendered due to their size.
• (Auto.IR.SMT.Command.assert prop).toString = toString "(assert " ++ toString prop ++ toString ")"
• (Auto.IR.SMT.Command.setLogic l).toString = "(set-logic " ++ l ++ ")"
• (Auto.IR.SMT.Command.setOption o).toString = toString "(set-option " ++ toString o ++ toString ")"
• Auto.IR.SMT.Command.getModel.toString = "(get-model)"
• (Auto.IR.SMT.Command.getOption s).toString = toString "(get-option " ++ toString s ++ toString ")"
• Auto.IR.SMT.Command.getProof.toString = "(get-proof)"
• Auto.IR.SMT.Command.getUnsatAssumptions.toString = "(get-unsat-assumptions)"
• Auto.IR.SMT.Command.getUnsatCore.toString = "(get-unsat-core)"
• Auto.IR.SMT.Command.checkSat.toString = "(check-sat)"
• (Auto.IR.SMT.Command.declSort name arity).toString = toString "(declare-sort " ++ toString (Auto.IR.SMT.SIdent.symb name) ++ toString " " ++ toString arity ++ toString ")"
• (Auto.IR.SMT.Command.declDtype name ddecl).toString = toString "(declare-datatype " ++ toString (Auto.IR.SMT.SIdent.symb name) ++ toString " " ++ toString ddecl.toString ++ toString ")"
• (Auto.IR.SMT.Command.echo s).toString = toString "(echo \"" ++ toString s ++ toString "\")"
• Auto.IR.SMT.Command.exit.toString = "(exit)"

instance Auto.IR.SMT.instToStringCommand : ToString Command

Equations

• Auto.IR.SMT.instToStringCommand = { toString := Auto.IR.SMT.Command.toString }

structure Auto.IR.SMT.State (ω : Type) [BEq ω] [Hashable ω] (φ : Type) [BEq φ] [Hashable φ] : Type

The main purpose of this state is for name generation and symbol declaration/definition, so we do not distinguish between sort identifiers, datatype identifiers and function identifiers

• h2lMap : Std.HashMap ω String
• l2hMap : Std.HashMap String ω
• usedNames : Std.HashMap String Nat
• wfPredicatesMap : Std.HashMap φ (Option String)
• wfPredicatesInvMap : Std.HashMap String φ
• commands : Array Command

@[reducible, inline]

abbrev Auto.IR.SMT.TransM (ω : Type) [BEq ω] [Hashable ω] (φ : Type) [BEq φ] [Hashable φ] (α : Type) : Type

Equations

• Auto.IR.SMT.TransM ω φ = StateRefT' IO.RealWorld (Auto.IR.SMT.State ω φ) Lean.MetaM

@[always_inline]

instance Auto.IR.SMT.instMonadTransM (ω : Type) [BEq ω] [Hashable ω] (φ : Type) [BEq φ] [Hashable φ] : Monad (TransM ω φ)

Equations

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

instance Auto.IR.SMT.instInhabitedTransM (ω : Type) [BEq ω] [Hashable ω] (φ : Type) [BEq φ] [Hashable φ] {α : Type} : Inhabited (TransM ω φ α)

Equations

• Auto.IR.SMT.instInhabitedTransM ω φ = { default := fun (x : ST.Ref IO.RealWorld (Auto.IR.SMT.State ω φ)) => throw default }

@[inline]

def Auto.IR.SMT.TransM.run {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] {α : Type} (x : TransM ω φ α) (s : State ω φ := { }) : Lean.MetaM (α × State ω φ)

Equations

• x.run s = StateRefT'.run x s

@[inline]

def Auto.IR.SMT.TransM.run' {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] {α : Type} (x : TransM ω φ α) (s : State ω φ := { }) : Lean.MetaM α

Equations

• x.run' s = Prod.fst <$> StateRefT'.run x s

def Auto.IR.SMT.setH2lMap {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] (field : Std.HashMap ω String) : TransM ω φ PUnit

Equations

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

def Auto.IR.SMT.getUsedNames {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] : TransM ω φ (Std.HashMap String Nat)

Equations

• Auto.IR.SMT.getUsedNames = do let st ← get pure st.usedNames

def Auto.IR.SMT.setWfPredicatesMap {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] (field : Std.HashMap φ (Option String)) : TransM ω φ PUnit

Equations

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

def Auto.IR.SMT.getWfPredicatesMap {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] : TransM ω φ (Std.HashMap φ (Option String))

Equations

• Auto.IR.SMT.getWfPredicatesMap = do let st ← get pure st.wfPredicatesMap

def Auto.IR.SMT.setWfPredicatesInvMap {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] (field : Std.HashMap String φ) : TransM ω φ PUnit

Equations

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

def Auto.IR.SMT.setCommands {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] (field : Array Command) : TransM ω φ PUnit

Equations

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

def Auto.IR.SMT.getCommands {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] : TransM ω φ (Array Command)

Equations

• Auto.IR.SMT.getCommands = do let st ← get pure st.commands

def Auto.IR.SMT.setUsedNames {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] (field : Std.HashMap String Nat) : TransM ω φ PUnit

Equations

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

def Auto.IR.SMT.setL2hMap {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] (field : Std.HashMap String ω) : TransM ω φ PUnit

Equations

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

def Auto.IR.SMT.getWfPredicatesInvMap {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] : TransM ω φ (Std.HashMap String φ)

Equations

• Auto.IR.SMT.getWfPredicatesInvMap = do let st ← get pure st.wfPredicatesInvMap

def Auto.IR.SMT.getL2hMap {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] : TransM ω φ (Std.HashMap String ω)

Equations

• Auto.IR.SMT.getL2hMap = do let st ← get pure st.l2hMap

def Auto.IR.SMT.getH2lMap {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] : TransM ω φ (Std.HashMap ω String)

Equations

• Auto.IR.SMT.getH2lMap = do let st ← get pure st.h2lMap

def Auto.IR.SMT.getMapSize {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] : TransM ω φ Nat

Equations

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

def Auto.IR.SMT.hIn {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] (e : ω) : TransM ω φ Bool

Equations

• Auto.IR.SMT.hIn e = do let __do_lift ← Auto.IR.SMT.getH2lMap pure (__do_lift.contains e)

def Auto.IR.SMT.processSuggestedName {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] (nameSuggestion : String) : TransM ω φ String

Equations

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

def Auto.IR.SMT.processSuggestedName.allowed (c : Char) : Bool

Equations

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

def Auto.IR.SMT.disposableName {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] (nameSuggestion : String) : TransM ω φ String

Equations

• Auto.IR.SMT.disposableName nameSuggestion = Auto.IR.SMT.processSuggestedName nameSuggestion

def Auto.IR.SMT.h2Symb {ω : Type} [BEq ω] [Hashable ω] [ToString ω] {φ : Type} [BEq φ] [Hashable φ] (cstr : ω) (nameSuggestion : Option String) : TransM ω φ String

Turn high-level construct into low-level symbol Note that this function is idempotent

Equations

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

def Auto.IR.SMT.h2SymbWf {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] [ToString φ] (s : φ) (nameSuggestion : Option String) : TransM ω φ (Option String)

Like hySymb but produces names for well-formed predicates of sort s (of type φ) rather than of constructs (of type ω)

Equations

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

def Auto.IR.SMT.addCommand {ω : Type} [BEq ω] [Hashable ω] {φ : Type} [BEq φ] [Hashable φ] (c : Command) : TransM ω φ Unit

Equations

• Auto.IR.SMT.addCommand c = do let commands ← Auto.IR.SMT.getCommands Auto.IR.SMT.setCommands (commands.push c)