simple theorem prover smt solver

I found it could be generated as program analysis tools, theorem provers, automated bug finders and so on which means it is a very crucial research. STP is a constraint solver aimed at solving constraints of bit vectors and arrays. It
can read CVC, SMT-LIB1 and SMT-LIB2 formats files. It also could be used by Python, SMT-LIBv2 and even C library. STP preprocesses the input through the application of mathematical and logical identities, and then eagerly translates
constraints into a purely propositional logic formula that it feeds to an off-the-shelf SAT solver.

STP views memory as untyped bytes. It provides only three data types: booleans, bitvectors, and arrays of bitvectors. A bitvector is an unsigned, fixed-length sequence of bits. For example, “0010” is a constant, 4-bit bitvector representing
the constant 2.

Build and Run

We can build this project on Linux or Docker, however, you know, Google isn’t well supported in China, so I can’t use “repo” execution which needed by Docker. In this document, I will use a quick install.

Firstly, we need to install many dependencies. Then, since STP uses “minisat” as its SAT solver by default, we need to install it first. It is very simple to do this by “cmake”. The following is part of the output.

Then we could start to install STP (To get the code, we need to use “git clone” but not download it directly).

This project depends on various external tools to do testing. Here we install “lit” and do some individual tests and use “GoogleTest” to write some unit tests.

Analyze Individual Test

An individual test is like this.

In this screenshot, we can see that this file is judging “b = (c || b)” and “((c || b) = b) < c < b”. We could find that an individual test file may contain these components:

• “; line”: comments;
• “set-info”: set some configuration information for running this file;
• “declare-fun”: definite some functions and their return types;
• “assert”: like C lang, do some judgement;
• “exit”: return.

Analyze Unit Test

We can simply run unit test by giving “lit” the individual tests directory or run “make C-api-tests” to build the C-api tests as unit tests. The Cpp file is like this.

From this picture, we can see that a C-api test contains many simple verifications.

Analyze the Code Structure

From the above picture, I give the following simple understandings to this project.

• “Interface”: Define a C interface to achieve the file ins and outs;
• “Sat”: Copy from “minisat” to call SAT solver.
• “AST”: Implement the abstract syntax tree for parsed solver inputs;
• “Util”: Store some header files for small tasks;
• “Printer”: Appoint some output formats;
• “Simplifier”: Simplify algorithms for AST;
• “Parser”: Store some parsers for the CVC, SMT-LIB1, SMT-LIB2 inputs;
• “STPManager”: Hold all components together.

本文链接： http://www.meng.uno/articles/cd3afb7d/ 欢迎转载！