如果你在一篇论文中读到对静态分析的描述，你会发现什么？会有一些可爱的语言模型。也许有一些描述分析本身的推理规则，但这些规则可能依赖于各种帮助器函数。如今，分析可能涉及一些逻辑推理：关于语言中的术语、分支条件句等。
是什么使一种语言适合实现这样的分析？您需要各种功能：
Aaron Bembenek、Steve Chong和我开发的设计切中了这四点的最佳点：给定Datalog作为核心，您可以向SMT添加构造函数、纯ML和类型安全接口。如果您设置得恰到好处，则该系统是编写静态分析的一种功能强大且符合人体工程学的方法。
Formulog是我们设计的原型实现；我们关于Formulog及其设计的论文刚刚被OOPSLA 2020有条件地接受。为了给出我为什么兴奋的感觉，让我摘录一下我们简单的液体类型检查器。在不到400行非常短的代码行中，它很好地展示了Formulog是多么富有表现力。(我们的论文讨论的例子要复杂得多。)。
Type base=|base_booltype typ=|typ_TVAR(TVAR)|typ_un(var，typ，typ)|typ_forall(tvar，typ)|typ_ref(var，base，exp)和exp=|exp_var(Var)|exp_bool(Bool)|exp_op(Op)：|exp_op(Op)|exp|exp。
ADT允许您以简单的方式定义AST。这里，bool是我们唯一的基类型，但我们可以添加更多。让我们来看看一些推理规则：
(*子类型*)输出sub(ctx，type，type)(*双向类型规则*)输出synth(ctx，exp，type)输出检查(ctx，exp，type)(*细分类型之间的子类型是隐含的*)sub(G，typ_ref(X，B，E1)，typ_ref(Y，B，E2))：-4wf_ctx(G)，*exp_subst(Y，exp_vst(Y，exp_vst。*encode_exp(E2Prime，Phi2)，*is_Valid(`PhiG/\Phi1==>；Phi2`).(*lambda和应用合成规则*)synth(G，exp_lam(X，T1，E)，T)：-1wf_typ(G，T1)，3synth(ctx_var(G，X，T1)，E，T2)，9typ_Fun(X，T1，T2)=T.synth(G，exp_app(E1，E2)，T)：-5synth(G，E1，tyth。*typ_subst(X，E2，T2)=T(*唯一检查规则*)check(G，E，T)：-a synth(G，E，TPrime)，b sub(G，TPrime，T)。
首先，我们声明我们的关系-即我们将使用的(类型化)推理规则。我们展示了子类型最有趣的例子：精化蕴涵。几个帮助器关系(wf_ctx，encode_*)和帮助器函数(Exp_Subst)将事情修补在一起。下面的类型化规则遵循类似的模式，将synth和检查双向类型化关系与对助手函数(如typ_subst)的调用混合在一起。
Fun exp_subst(X：var，E：exp，etgt：exp)：exp=将Etgt与Etgt匹配|exp_var(Y)=>；如果X=Y，则E否则Etgt||exp_bool(_)=>；Etgt；|exp_op(_)=>；Etgt|exp_lam(Y，TLAM，ELAM)。如果让YFRESH=*FOR(Y，X：：APPEND(TLAM)，EXP_FREEVARS(ELAM))*，让ELAM_FRESH=FRESH_FOR(Y，X：：APPEND(TLAM)，EXP_FREEVARS(ELAM))*，那么*。*(Elamfresh)**|exp_tlam(A，Etlam)=>；**EXP_TLAM(A，EXP_SUBST(X，E，Etlam))*|EXP_APP(E1，E2)=>；*EXP_APP(EXP_SUST(X，E，E1)，EXP_SUST(X，E，E1)，EXP_SUPT(X，E，E2))|EXP_TAPP(ETAP，T)=>；*EXP_TAPP(EXP_Subst(X，E，EAPP))**EXP_TAPP(EXP_Subst(X，E，Etlam))|EXP_TAPP(EXP_SUST(X，E，Et))。
表达式替换可能很无聊，但是它很好地显示了ML片段。它或多或少是常见的ML，尽管函数需要有纯接口，而且我们在原型中有一些限制来保持输入简单。
本例中没有包含很多有趣的东西：不仅关系可以调用函数，而且函数可以检查关系(只要一切都是分层的)。隐藏在FRESH_FOR中的是一种巧妙的名称生成方法，它可以保证…的新鲜性。但也是确定性的，不会干扰并行执行。论文草稿中有更多实质性的例子。
我们并不是第一个将逻辑编程和SMT相结合的公司。使我们的设计成为一个甜蜜点的是，它不会让SMT妨碍Datalog简单而强大的执行模型。Datalog执行很容易并行化；魔术集转换可以将Datalog的穷举、自下而上的搜索转变为目标导向的搜索。Datalog可以改变这些技巧已经不是什么新闻了--Yanannis Smaragdakis多年来一直在这么说！--但是将Datalog与ML函数和SMT干净地集成在一起还是个新事物。请查看论文草稿，了解相关工作的详细比较。虽然我们的设计最终没有那么复杂，但要做到这一点是困难的。
与此相关的是，我们在ICLP 2020上也有一个扩展的摘要，详细介绍了使用Formulog中的增量求解模式的一些实验。您可能担心Datalog的BFS(或启发式)策略不适用于SMT解算器的推送/弹出(即DFS)断言堆栈-但是一些实现技巧和check-sat-假设确实提供了加速。