想要看smt-lib是因为文章2018.learn.wwwang.asplos.11

Introduction

Quick Start

The SMT-LIB Language

Some logical concepts

Satisfiability and Validity

满足性问题（Satisfiability）和成立问题（Validity）可以互相等价转换。

表达式$P$成立$\iff$表达式$\neg P$不可满足。

Quantified formulas and SMT solvers

量词（Quantifier，例如$\exist,\forall$）对于SMT solvers是难题。

Many-Sorted Logic

这里的sort指type。

按我的理解这段话在说SMT-LIB是强类型语言

Formulas and terms

SMT-LIB不区分Formulas和terms，虽然它也没描述清楚区别。

Abstract and concrete syntax

语法参考SMT-LIB的reference《The SMT-LIB Standard》。

杂记

常数是没有参数的函数。

constants are simply functions with no arguments

不同类型（sort）在不同理论（theory）中可能会有不同含义。

Remember that the interpretation and sort of these literals depends on the theories that have been defined in the current solver environment (by a set-logic command).