Module uvls::smt

Implements the semantic analysis using Z3

SMT semantic analysis with Z3, communication with the solver happens over stdio and SMT-LIB2. While the performance is worse than linking with Z3, we are solver independent and don’t have to interact with any C-Bindings. UVL is translated directly into SMT-LIB, both attributes and features are treated as free variables. The rest is encoded in named asserts, this allows to get a accurate unsat core. Eg. each attribute is restricted with an assert that allows it to either be its defined value or 0 depending on the parent feature value. Using functions might be more efficient, but this way we can reconfigure and detect if an attribute value contributes to the unsat core. Variables are named as v{n} where n is an index into a lookup table of UVL ModuleSymbols Asserts are encoded similarly as a{n} where n is and index into a list of naming information that links uvl expression to asserts.

Re-exports

• pub use smt_lib::*;

Modules

• parse 🔒
  Turn smt-lib strings to rust. (currently incomplete)
• smt_lib

Structs

• HAS_Z3 🔒
  A static reference wether a client has z3 installed
• OwnedSMTModel
• SmtSolver
  Z3 process interface(over stdio)

Enums

• SMTModel
  This stores the Z3 solution
• SMTValueState

Functions

• can_run_z3
  This function is a helper function which checks if a LSP can run z3.
• check_base_sat 🔒
  This function checks the SAT Level of a FileID
• check_config 🔒
  checks if config is SAT Solvable
• check_handler
• create_model 🔒
  Creator for SMTModel
• find_fixed 🔒
  find constant boolean values for dead features and other cool analysis
• web_view_handler
  runs smt-analysis on configurations.