This is a toy Rust SMT solver build using platsat and plat-egg that accepts a subset of SMT2LIB syntax for the logic QF_UF

Supported syntax:

• true, false, and, or, not,
• =>, xor
• =
• distinct
• as
• declare-sort
• declare-function
• assert
• check-sat
• check-sat-assuming
• let
• let* (sequential let binding)
• if
• get-value
• get-model
• :named
• get-unsat-core
• declare-const
• define-const
• push,pop,reset,reset-assertions
• set-option
• echo
• get-proof

Binary usage

The binary (produced by cargo build) takes in a list of .smt2 files and evaluates sequentially as if they were a single concatenated file. This list can optionally be followed by -i which enters interactive mode (reading from stdin) after the files are evaluated

Parameters (set-option)

Most parameters currently come from batsat, and are prefixed by sat., for example random initial activations would be enabled with:

(set-option :sat.rnd_init_act true)

plat-smt also supports the SMT-LIB standard parameters:

• :produce-models (default true)
• :produce-unsat-cores (default true)
• :print-success (default false)

Misc

• The yices-smt2 file is from https://yices.csl.sri.com/ and is only included for testing
• The scrambler and ModelValidator files are from https://smt-comp.github.io/2021/tools.html and are also only used for testing
• If the environment variable SEED is set the initial decisions made are randomized based on it when running the star exec tests (these should otherwise be configured via set-option)