I’m working on integrating two SMT solvers with Wenxin Feng, therefore it is necessary to understand the SMT-LIB 2.0 logic, which can be used as an input language for both solvers (AltErgo, CVC4). Part of the project is to classify formulas which can be solved by one solver, while not by the others. Therefore knowing how theories and logics are defined in SMT-LIB is also important.

## SMT-LIB Logics

• $$\mathcal{S}$$: Infinite set of sort symbols, containing $$\tt BOOL$$.
• $$\mathcal{U}$$: Infinite set of sort parameters
• $$\mathcal{X}$$: Infinite set of variables
• $$\mathcal{F}$$: Infinite set of function symbols
• $$\mathcal{B}$$: Boolean values $$\tt \{true, false\}$$

## Sorts

Sorts over a set of sort symbols $$\mathcal{S}$$ are defined as $$\tt Sort(\mathcal{S})$$.

• $$\sigma \in \mathcal{S}$$ of arity 0 is a sort
• $$\sigma \sigma_1, \sigma_2, \sigma_3, \ldots, \sigma_n$$ is a sort if $$\sigma \in \mathcal{S}$$ of arity $$n$$, $$\sigma_1$$ to $$\sigma_n$$ are sorts

## Signature

Baiscly, $$\Sigma$$ defines sort symbols and arities, function symbols and ranks, some variables and their sorts.

• $$\Sigma^\mathcal{S} \subset \mathcal{S}$$: sort symbols, containing $$\tt BOOL$$
• $$\Sigma^\mathcal{F} \subset \mathcal{F}$$: function symbols, containing equality, conjunction, and negation
• $$\Sigma^\mathcal{S}$$ to $$\mathbb{N}$$: a total mapping from sort symbol to its arity, including $$\tt BOOL \Rightarrow 0$$
• $$\Sigma^\mathcal{F}$$ to $$\tt Sort(\Sigma^\mathcal{S})+$$: a left total mapping from a function symbol to its rank, containing $$=(\sigma, \sigma, {\tt BOOL} )$$, $$\neg({\tt BOOL},{\tt BOOL})$$, $$\wedge ({\tt BOOL}, {\tt BOOL}, {\tt BOOL})$$.
• $$\mathcal{X}$$ to $$\tt Sort(\Sigma^\mathcal{S})$$: a partial mapping from a variable to its sort.

## Formulas

Well sorted terms of sort $$\tt BOOL$$ over $$\Sigma$$

## Structure

$$\bf A$$ can be regarded as a model.

• $$A$$: the universe (of values) of $$\bf A$$, including $$\tt BOOL^{\bf A} = \{true, false\}$$.
• $$\sigma^{\bf A} \subset A$$: give the sort $$\sigma \in \tt Sort(\Sigma^\mathcal{S})$$ a universe $$\sigma^{\bf A} \subset A$$. For example, $$\tt BOOL^{\bf A}$$ is $$\{true, false\} \subset \rm A$$. $$\tt INT^{\bf A}$$ could be all the integers $$\mathbb{Z} \subset A$$.
• $$(f:\sigma)^{\bf A} \in \sigma^{\bf A}$$: give the constant symbol $$f:\sigma$$ a value in the universe of $\sigma$
• $$(f:\sigma_1,\sigma_2,\ldots,\sigma_n,\sigma)^{\bf A}$$: define the function symbol as a relation from $$(\sigma_1,\sigma_2,…,\sigma_n)^{\bf A}$$ to $$\sigma^{\bf A}$$. This must include the equality relations (or identity predicate over $$\sigma^{\bf A}$$, that is $$\tt = (\sigma, \sigma, BOOL)$$ as standard equality relations from $$(\sigma^{\bf A}, \sigma^{\bf A})$$ to $$\{true, false\}$$).

$$\sigma^{\bf A}$$ is called the extension of $$\sigma$$ in $$\bf A$$.

## Valuation and Interpretation

• Valuations $$v$$: a partial mapping $$v$$ from $$\mathcal{X} \times \tt Sort(\Sigma^\mathcal{S})$$ to $$\sigma^{\bf A}$$. That is to give variable $$x$$ of sort $$\sigma$$ a value in $$\sigma^{\bf A}$$.
• Interpretation $$\mathcal{I}$$: $$\mathcal{I} = ({\bf A}, v)$$, that is the structure together with the valuations make the $$\Sigma$$-interpretation.
• Semantics: $$\mathcal{I}$$ will assign a meaning to well-sorted terms by uniquely mapping them into the $$\bf A$$.
• Satisfiability: if $$\varphi$$ is mapped to $$\tt true$$ by some $$\mathcal{I}$$, then it is satisfiable.
• if $$\varphi$$ is not closed, we say $$\mathcal{I} = ({\bf A}, v)$$ makes true $$\varphi$$
• if $$\varphi$$ is closed, we say the structure $$\bf A$$ makes true $$\varphi$$. (Since it doesn’t matter what valuation it is.)
• if $$\varphi$$ is closed, we say the structure $$\bf A$$ a model of $$\varphi$$.

## Theories

• Traditionally, its a set of axioms
• Here it consists of three parts
• Signature: $$\Sigma$$
• Axioms:
• I think this part is left for the people who implement solvers. Take $$\tt INT$$ theory as an example, since we have the plus sign in our signature (we just denote it as $$\tt ADD$$, so that you know it is only a symbol, not the actual operation), we will have an axiom like $$\forall x:{\tt INT}. y:{\tt INT}. \exists z:{\tt INT}. {\tt ADD}(x,y,z) \leftrightarrow x + y = z$$. Therefore, our model (or structure) must contain the correct relations to map $$\tt ADD$$ to the actual addition operation to satisfy this axiom.
• Also, some theories like $$\tt REAL$$ include those axioms as plain text, like associativity, commutativity, etc.
• Models: A set of $$\Sigma$$-structures, all of which are models of the theory.

## Logics

• Sublogic: it is a sublogic of SMT-LIB logic
• Restrictions:
• fixing a signature $$\Sigma$$ and its theory $$\mathcal{T}$$
• restricting structures to the models of $$\mathcal{T}$$
• restricting input sentences as subset of $$\Sigma$$-sentences
Tagged with:

I have updated my ATS CMake modules at GitHub (https://github.com/steinwaywhw/ATS-CMake/) , and the documentation is also available at ReadTheDocs.org, https://ats-cmake-documentaition.readthedocs.org/en/latest/.

By the way, I strongly recommend you to try ReadTheDocs, which is built on top of Sphinx, a Python documentation tool. It’s simple syntax (reST), powerful functions, simple yet clean interface, and GitHub integration, is really amazing. At least, it makes me enjoy documenting projects.

Check it out!

Tagged with:

Tagged with:

Tagged with:

Tagged with:

Tagged with:

Note: This is a short introduction of my ongoing project. It is copied from the Wikipage of GitHub repository. Welcome to check it out at HERE!

## What is CMake-ATS Project

This is a project aiming at developing a build tool for ATS. It is based on CMake. Currently, it provides some very useful CMake modules for ATS users to simplify building processes. In the near future, it will support downloading artifacts from a server to help you utilize third party ATS libraries.

## Quick Start

• Install CMake. (2.8+ preferred)
• Install ATS. (Setup environment variables ATSHOME and PATH properly)
• Copy FindATS.cmake and ATSCC.cmake into CMake module dir. (Normally /usr/share/cmake-x.x.x/Modules on Linux)
• Start using it!

## Quick Demo

• Say you have a small project containing hello.sats, hello.dats and main.dats. Then, you need to write a CMakeLists.txt like this:
CMAKE_MINIMUM_REQUIRED (VERSION 2.8)

#Specify project name as HELLOWORLD, and project language as C. Yes, it is C
PROJECT (HELLOWORLD C)

#Actually, this makes CMake to find ATSCC.cmake using FindATS.cmake
FIND_PACKAGE (ATS REQUIRED)

#The ATS_FOUND is automatically set by CMake
IF (NOT ATS_FOUND)
ENDIF ()

#ATS_COMIPLE is the core of this project. To put it simple,
#you just specify related SATS/DATS files hear, and use a variable like TEST_SRC
#to stored the output. ATS_COMPILE will analyze their dependencies,
#compile them into #C files, and store those C file names into TEST_SRC
#You can use ATS_INCLUDE to add search paths for the compiler to find proper SATS/HATS files.
ATS_COMPILE (TEST_SRC hello.sats hello.dats main.dats)

#It generate the final file "test" using all the C files in TEST_SRC

• Then, to do out-of-source build, you need to make a sub-dir, say ./build/. Then your project looks like this
ProjectParent/
+-- CMakeLists.txt
+-- hello.dats
+-- hello.sats
+-- main.dats
+-- /build
+-- ...

• Go to ./build/, type cmake ... It will generate a Makefile for you under ./build/
• Type make to make. And the test will show up in ./build/
Tagged with:

Tagged with:

Downtown Sunset

Currently, I am learning Lambda Calculus, and the Y combinator. And I am going to talk about why people need such kind of combinators, but how it is derived will not be covered since there are a lot of great articles explaining it. Great thanks to the explanation given by my senior, Zhiqiang (Alex) Ren!

These materials are really great and very important. Be sure you read them first if you really want to know fixpoint combinator.

## Why We Need Fixpoint Combinator

In pure untyped lambda calculus, we cannot define a recursive term like we do in programming languages like C. For example, we give the factorial function (lambda abstraction) the name fact, then it could be expressed as,

$$\lambda n. \verb!if !n < 1 \verb! then !1 \verb! else fact! (n – 1)$$

However, the fact in this lambda term is a free variable, and there is actually no way to do the same thing as we say “we give the factorial function a name” and use that name in the body recursively in lambda calculus. If you really want to do “give something a name”, you may try to introduce bindings by using lambda abstraction, which seems like this,

$$(\lambda \verb!fact!. \lambda n. \ldots \verb! else fact! (n-1)) (\lambda n. \ldots \verb! else fact!(n-1))$$

Yes, you see that we pass the recursive function itself to itself, so that we can call the function recursively. (This idea could be furture expanded in those “Great to Read” materials. Check them out, strongly recommended!) But there are two problems. First, the fact in the second part, is still undefined, it’s a free variable. Second, since the second fact is not bound, this definition can only “recurs” once. If you really want to define a factorial function that can compute for all valid N, the definition could result in a infinite loop.

Thus, we need fixpoint in lambda calculus so that we can define terms to compute recursive problems.

## Usage of Fixpoint Combinator

It doesn’t mean that any languages that support recursive definitions are implemented using fixpoint combinators. For example, C language simply uses “call” to call itself. And it is recursive with the help of function call stack and the hardware. It just works that way, and has nothing to do with lambda calculus and fixpoint. But, if someone implements a language that based on lambda calculus, it should provide fixpoint combinator internally, to support recursive definition on the grammar level. (That means, by parsing the recursive source code, it will generate non-recursive lambda terms, and combine it with fixpoint combinator to compute data recursively.)

## Types of Fixpoint Combinator

Because different interpreters have different evaluation strategies, like call-by-value (applicative-order), call-by-name (normal-order), call-by-need (an optimized implementation of call-by-name) and call-by-reference, you need to supply different combinators to avoid evaluation problems. Call-by-name combinators may be result in an infinite substitution in a call-by-value interpreter. These are explained in those materials.

One way to avoid an infinite substitution is to wrap a lambda expression into a lambda abstraction. Because lambda expression is going to be evaluated immediately, but a lambda abstraction will only be evaluated when it is applied. This is a great idea I found in those materials.

Tagged with: