@[inline]

def Blaster.Smt.getProcStdIn : Optimize.TranslateEnvT IO.FS.Handle

Equations

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

@[inline]

def Blaster.Smt.getProcStdOut : Optimize.TranslateEnvT IO.FS.Handle

Equations

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

def Blaster.Smt.updateSymbolCache (s : SmtSymbol) (rep : String) : Optimize.TranslateEnvT Unit

Equations

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

@[inline]

def Blaster.Smt.withSymbolCache (s : SmtSymbol) : Optimize.TranslateEnvT String

Equations

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

def Blaster.Smt.SmtSymbol.emit (s : SmtSymbol) : Optimize.TranslateEnvT Unit

Equations

• s.emit = do let h ← Blaster.Smt.getProcStdIn let __do_lift ← Blaster.Smt.withSymbolCache s liftM (h.putStr __do_lift)

partial def Blaster.Smt.SortExpr.emit (e : SortExpr) : Optimize.TranslateEnvT Unit

def Blaster.Smt.SortedVars.emit (sv : SortedVars) : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.Smt.SmtQualifiedIdent.emit (id : SmtQualifiedIdent) : Optimize.TranslateEnvT Unit

Equations

• (Blaster.Smt.SmtQualifiedIdent.SimpleIdent nm).emit = nm.emit
• (Blaster.Smt.SmtQualifiedIdent.QualifiedIdent nm t).emit = do let h ← Blaster.Smt.getProcStdIn liftM (h.putStr "(as ") nm.emit liftM (h.putStr " ") t.emit liftM (h.putStr ")")

partial def Blaster.Smt.ArraySmtTerm.emit (terms : Array SmtTerm) : Optimize.TranslateEnvT Unit

partial def Blaster.Smt.SmtAttribute.emit (a : SmtAttribute) : Optimize.TranslateEnvT Unit

partial def Blaster.Smt.SmtTerm.emit (e : SmtTerm) : Optimize.TranslateEnvT Unit

def Blaster.Smt.SmtSelector.emit (s : SmtSelector) : Optimize.TranslateEnvT Unit

Equations

• s.emit = do let h ← Blaster.Smt.getProcStdIn liftM (h.putStr "(") s.fst.emit liftM (h.putStr " ") s.snd.emit liftM (h.putStr ")")

def Blaster.Smt.SmtConstructorDecl.emit (decl : SmtConstructorDecl) : Optimize.TranslateEnvT Unit

Equations

• decl.emit = do let h ← Blaster.Smt.getProcStdIn liftM (h.putStr "(") decl.fst.emit liftM (h.putStr " ") Blaster.Smt.SmtConstructorDecl.emit.selectorsEmit h decl.snd liftM (h.putStr ")\n")

def Blaster.Smt.SmtConstructorDecl.emit.selectorsEmit (h : IO.FS.Handle) (sels : Option (Array SmtSelector)) : Optimize.TranslateEnvT Unit

Equations

• Blaster.Smt.SmtConstructorDecl.emit.selectorsEmit h none = pure ()
• Blaster.Smt.SmtConstructorDecl.emit.selectorsEmit h (some sel) = Array.forM (fun (a : Blaster.Smt.SmtSelector) => do liftM (h.putStr " ") a.emit) sel

def Blaster.Smt.SmtDatatypeDecl.emit (d : SmtDatatypeDecl) : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.Smt.SmtDatatypeDecl.emit.ctorsEmit (h : IO.FS.Handle) (ctors : Array SmtConstructorDecl) : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.Smt.SmtSortDecl.emit (d : SmtSortDecl) : Optimize.TranslateEnvT Unit

Equations

• d.emit = do let h ← Blaster.Smt.getProcStdIn liftM (h.putStr "(") d.name.emit liftM (h.putStr (toString " " ++ toString d.arity ++ toString ")"))

def Blaster.Smt.SmtFunDecl.emit (d : SmtFunDecl) : Optimize.TranslateEnvT Unit

Equations

• d.emit = do let h ← Blaster.Smt.getProcStdIn liftM (h.putStr "(") d.name.emit liftM (h.putStr " (") d.params.emit liftM (h.putStr ") ") d.ret.emit liftM (h.putStr ")")

def Blaster.Smt.SmtCommand.emit (c : SmtCommand) : Optimize.TranslateEnvT Unit

Equations

• c.emit = do let h ← Blaster.Smt.getProcStdIn Blaster.Smt.SmtCommand.emit.emitAux h c liftM h.flush

def Blaster.Smt.SmtCommand.emit.sortArgsEmit (h : IO.FS.Handle) (nargs : Option (Array SmtSymbol)) : Optimize.TranslateEnvT Unit

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.SmtCommand.emit.sortArgsEmit h none = liftM (h.putStr "()")

def Blaster.Smt.SmtCommand.emit.emitAux (h : IO.FS.Handle) (c : SmtCommand) : Optimize.TranslateEnvT Unit

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Smt.SmtCommand.emit.emitAux h (Blaster.Smt.SmtCommand.assertTerm t) = do liftM (h.putStr "(assert ") t.emit liftM (h.putStr ")\n")
• Blaster.Smt.SmtCommand.emit.emitAux h Blaster.Smt.SmtCommand.checkSat = liftM (h.putStrLn "(check-sat)")
• Blaster.Smt.SmtCommand.emit.emitAux h (Blaster.Smt.SmtCommand.checkSatAssuming args) = do liftM (h.putStr "(check-sat-assuming (") Blaster.Smt.ArraySmtTerm.emit args liftM (h.putStr "))\n")
• Blaster.Smt.SmtCommand.emit.emitAux h (Blaster.Smt.SmtCommand.declareConst nm t) = do liftM (h.putStr "(declare-const ") nm.emit liftM (h.putStr " ") t.emit liftM (h.putStr ")\n")
• Blaster.Smt.SmtCommand.emit.emitAux h Blaster.Smt.SmtCommand.exitSmt = liftM (h.putStr "(exit)\n")
• Blaster.Smt.SmtCommand.emit.emitAux h Blaster.Smt.SmtCommand.getModel = liftM (h.putStr "(get-model)\n")
• Blaster.Smt.SmtCommand.emit.emitAux h Blaster.Smt.SmtCommand.getProof = liftM (h.putStr "(get-proof)\n")
• Blaster.Smt.SmtCommand.emit.emitAux h (Blaster.Smt.SmtCommand.evalTerm t) = do liftM (h.putStr "(eval ") t.emit liftM (h.putStr ")\n")
• Blaster.Smt.SmtCommand.emit.emitAux h (Blaster.Smt.SmtCommand.setLogic l) = do liftM (h.putStr "(set-logic ") liftM (h.putStr l) liftM (h.putStr ")\n")