Merge pull request #7005 from esteffin/esteffin/smt-args-docs

Docs for incremental SMT backed

Author: tautschnig

doc/man/cbmc.1

@@ -174,6 +174,25 @@ Output formula to given file
 Never turn arrays into uninterpreted functions
 .IP --arrays-uf-always
 Always turn arrays into uninterpreted functions
+.IP "--incremental-smt2-solver <cmd>"
+Use the incremental SMT backend where <cmd> is the command to invoke the SMT
+solver of choice.
+.br
+Examples invocations:
+.br
+  --incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver).
+.br
+  --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' (use the CVC5 solver).
+.sp
+Note that:
+.br
+The solver name must be in the "PATH" or be an executable with full path.
+.br
+The SMT solver should accept incremental SMTlib v2.6 formatted input from the stdin.
+.br
+The SMT solver should support the QF_AUFBV logic.
+.br
+The flag --slice-formula should be added to remove some not-yet supported features.
 .SH ENVIRONMENT
 All tools honor the TMPDIR environment variable when generating temporary
 files and directories. Furthermore note that

src/solvers/smt2_incremental/README.md

@@ -0,0 +1,42 @@
+# Incremental SMT backend
+
+CBMC comes with a solver-agnostic incremental SMT backend.
+
+The SMT incremental backend supports the following `C` features:
+
+- Integers (via Bit vector arithmetics)
+- Pointers
+- Arrays (support is currently incomplete)
+
+Primitive not supported are:
+
+- Floating point values and arithmetics
+- Structs
+
+Usage of the incremental SMT backend requires a SMT solver compatible with
+incremental SMTlib v2.6 formatted input from the standard input and that
+supports the `QF_AUFBV` (Quantifier Free Array Uninterpreted Functions and Bit
+Vectors) logic.
+
+To use this functionality it is enough to add the argument
+`--incremental-smt2-solver <cmd>` where `<cmd>` is the command to invoke the SMT
+solver of choice using the incremental mode and accepting input from the
+standard input.
+
+Examples of invocations with various solvers:
+
+1. `--incremental-smt2-solver 'z3 -smt2 -in'` to use the Z3 solver.
+2. `--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental'` to use the
+   CVC5 solver.
+
+The new incremental SMT backend has been designed to interoperate with external
+solvers, so the solver name must be in the `PATH` or an executable with full
+path must be provided.
+
+Due to lack of support for conversion of `array_of` expressions that are added
+by CBMC in the before the new SMT backend is invoked, it is necessary to supply
+an extra argument `--slice-formula` so that instances of `arrayof_exprt` are
+removed from the formula to be converted.
+
+As we move forward with our array-support implementation, we anticipate that the
+need for this extra flag will be diminished.