Skip to content

Latest commit

 

History

History
47 lines (41 loc) · 1.82 KB

README.md

File metadata and controls

47 lines (41 loc) · 1.82 KB
Raw

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)