Currently stevia was implemented without proper adjustment on the outer interfaces to the module. The ast module for example has a giantic interface which should and certainly could be minimized. To allow for later decoupling of modules this should be done beforehand.

Stevia requires support for SMTLib2 parsing to make it work with SMTLib2 inputs.

Implementation Status

• Raw Lexer: done
• Simple Lexer: done
• Parser: in progress
• SMTLib Solver Interface: in progress

Past Discussion & Design

For this the rsmt2 crate provides parsing support, however, its current implementation isn't flexible enough to allow for decoupled integration of other SMT solver than the currently implemented ones (Z3 and CVC4). This issue is described in detail here. Adrien Champion reported that this was a wrong assumption about rsmt2.

For the parsing of SMTLib2 there are effectively two approaches.

The eager approach would simply parse an SMTLib2 input, process it and directly returns the entire parsed construct represented as an apropriate data structure to feed into stevia. This approach is simple, however, has the downside to be very inflexible and may require more memory to store a temporary data structure and maybe even has negative performance implications.

A more flexible and thus superior approach is to define an interface to let an underlying SMT solver know about newly parsed entities. In this situation a proper interface has yet to be found but the advantage is that this should be more optimal for memory consumption and runtime performance.

Simplifications

The following simplifications on expression trees are listed here.

These are not currently implemented in Stevia but are planned or debated for future versions.

(Note: This list of planned simplification routines is not complete!)

General

• If

  • Const evaluation: (ite true a b) to a and (ite false a b) to b
  • Equivalence elimination: (ite c a a) to a
  • Not elimination: (ite (not c) a b) to (ite c b a)
  • Conditional constraint propagation: e.g.
    • (ite c (not c) a) to (ite c false a) works recursively
    • (ite (< a b) (div a b) 0) to 0 and handles semantics or relations

• Equals

  • Const evaluation: (= a b) to true where a and b are const and evaluate to the same value
  • Const contradiction: (= a b) to false where a and b are const and evaluate to a distinct value
  • Logical contradiction: (= a (not a)) to false and (= a (neg a)) to false
  • Flattening: (and (= a b) (= b c)) to (= a b c)
  • Normalization by ordering of child expressions.

• Symbol

  • Lookup of constrains that enforces a constant value for it. (Solvable by linear solver. Or maybe better?)

Formula

• Not

  • Involution: (not (not a)) to a
  • Const evaluation: (not c1) to c2 where c1 is const and c2 is not c1
  • GE lowering: (not (uge a b)) to (ult a b)
  • SignedGE lowering: (not (sge a b)) to (slt a b)
  • LE lowering: (not (ule a b)) to (ult b a)
  • SignedLE lowering: (not (sle a b)) to (slt b a)

• And

  • Constant taugology detection: (and true true) to true
  • Constant contradiction detection: (and true false) to false
  • Symbolic contradiction detection: (and a (not a)) to false
  • Demorgan-transformation: (and (not a) (not b)) to (not (or a b))
  • Flattening: (and (and a b) (and c d)) to (and a b c d)
  • Deduplication: (and a a b) to (and a b)
  • Normalization by ordering of child expressions.

• Or

  • Constant tautology extraction: (or false true) to true
  • Constant contradiction extraction: (or false false) to false
  • symbolic-tautology detection: (or a (not a)) to true
  • Demorgan-transformation: (or (not a) (not b)) to (not (and a b))
  • Flattening: (or (or a b) (or c d)) to (or a b c d)
  • Deduplication: (or a a b) to (or a b)
  • Normalization by ordering of child expressions.

• Xor

  • Const Eval: (xor true false) to true.
  • Normalization by ordering of child expressions.
  • Symbolic contradiction: (xor a a) to false
  • Symbolic tautology: (xor a (not a)) to true

• Iff (deprecated for equals?)

• Implies

  • Lowering to or: (implies a b) to (or (not a) b)

• Parametric Bool

Term

• Neg

  • Neutral Element: (- 0) to 0
  • Involution: (- (- a)) to a
  • Const evaluation: (- c1) to c2 where c1 is const and c2 is the negation of c1
  • Propagate Add: (- (+ a b c)) to (+ (- a) (- b) (- c))
  • Propagate Mul: (- (* a b c)) to (* (- a) b c)

• Add

  • Const Propagation: (+ c1 c2) to c3 where c1 and c2 are both constant and c3 = c1 + c2.
  • Neutral Element: (+ a 0) to a
  • Inverse Elimination: (+ a (-a)) to 0
  • Negation-Pulling: (+ (-a) (-b)) to (- (+ a b))
  • Lowering to mul: (+ a a) to (* 2 a)
  • Flattening: (+ (+ a b) (+ c d)) to (+ a b c d)
  • Normalization by ordering of child expressions.
  • Resolve multiplicities: (+ a (-a) (* 5 a) (* (-3) a) b) to (+ (* 2 a) b)

• Sub

  • Const Propagation: (- c1 c2) to c3 where c1 and c2 are both constant and c3 = c1 - c2.
  • Neural Element: (- a 0) to a and (- 0 a) to (-a)
  • Inverse Element: (- a a) to 0
  • Add Lowering: (- a b) to (+ a (- b))

• Mul

  • Neutral Element: (* a 1) to a
  • Null Element: (* a 0) to 0
  • Inverse Elimination: (* a (/ 1 a)) to 1
  • Powers-of-Two: (* a n) to (<< a (log n)) where n is a power of two.
  • Flattening: (* (* a b) (* c d)) to (* a b c d)
  • Normalization by ordering of expressions.
  • Negation Elimination: (mul a (-b) c (-d) (-e) f) to (mul (-a) b c d e f)
  • Negation-Pulling:
    • Left:(* (- a) b) to (- (* a b))
    • Right: (* a (-b)) to (- (* a b))
    • Both: (* (- a) (- b)) to (* a b)

• Div

  • Division by zero: (/ a 0) to Undefined <- signaling undefined behaviour to the user.
  • Neutral Element: (/ a 1) to a
  • Self-Division: (/ a a) to 1
  • Zero-Division: (/ 0 a) to 0 if a is not 0
  • Lower to Mul: (/ a (/ b c)) to (/ (* a c) b). Reason: mul is easier for the const evaluator.
  • Lower to Shift: (/ a n) to (>> a (log n)) where n is a power of two.
  • Const evaluation: (/ c1 c2) to 0 if (= (< c1 c2) true) and c1 and c2 are const.
  • Negation-Pulling:
    • Left:(/ (- a) b) to (- (/ a b))
    • Right: (/ a (-b)) to (- (/ a b))
    • Both: (/ (- a) (- b)) to (/ a b)

Bitwise Operations

• BitNot

  • Involution: (bvnot (bvnot x)) to x
  • Const eval: (bvnot c1) to c2 where c2 is equal to the bitnot application of c1.

• BitAnd

  • Identity detection:
    • (bitand x x) to x
    • (bitand x ..1..) to x
  • Nulling
    • (bitand x (bitnot x)) to 0
    • (bitand x ..0..) to 0

• BitOr

  • Identity detection:
    • (bitor x x) to x
    • (bitor x ..0..) to x
  • Oning
    • (bitor x (bitnot x)) to 1
    • (bitor x ..1..) to ..1..

• BitXor

  • Neutral element: (bitxor x ..0..) to x
  • Lower to bitnot: (bitxor x ..1..) to (bitnot x)
  • Null element: (bitxor x x) to 0
  • One element: (bitxor x (bitnot x)) to ..1..

• BitNand

• BitNor

• BitXnor

Shifts

• ShiftLeft

• ArithmeticShiftRight

• LogicalShiftRight

Compares

• LessThan

  • Const evaluation: (< c1 c2) evaluate for all constant c1 and c2
  • Symbolic contradiction: (< x x) to false
  • Neg elimination:
    • (< x (-y)) to (< y x)
    • (< (-x) y) to (< y x)
    • (< (-x) (-y)) to (< x y)

• LessEquals

  • Lowering: (ule x y) to (not (ult y x))

• GreaterThan

  • Lowering: (ugt x y) to (ult y x)

• GreaterEquals

  • Lowering: (uge x y) to (ule y x)

• Signed LessThan

  • Const evaluation: (< c1 c2) evaluate for all constant c1 and c2
  • Symbolic contradiction: (< x x) to false
  • Neg elimination:
    • (< x (-y)) to (< y x)
    • (< (-x) y) to (< y x)
    • (< (-x) (-y)) to (< x y)

• Signed LessEquals

  • Lowering: (sle x y) to (not (slt y x))

• Signed GreaterThan

  • Lowering: (sgt x y) to (slt y x)

• Signed GreaterEquals

  • Lowering: (sge x y) to (sle y x)

Extract & Extend

• Concat

• Extract

• ZeroExtend

• SignedExtend

Array

• Read

• Write

For stevia to be a more or less complete SMT solver the following high-level modules will need to be implemented in one form or another:

• AST: Data structures for the expression tree.
• Simplifier: Word-level simplifications on the AST data structure.
• Simple Serializer: Serialize AST data structure into human-readable form.
• SMTLib2 Parser: Parse input given in SMTLib2 compliant form.
  • WIP: https://github.com/Robbepop/stevia/tree/master/stevia_parser
• SAT Driver: Drives the underlying SAT solver with the given CNF formula.
  • FFI Bindings: https://github.com/Robbepop/ipasir-rs

With AIG optimizations:

• SMT -> AIG: Bit Blaster: Transform a given AST expression tree into a pure boolean formula. The resulting boolean formula should be cheaply convertible to an AIG representation.
• AIG Driver: Drives processing AIG input.
• AIG -> CNF: Tseytin Transformation -> Transforms AIG represented data to CNF format.

Additional optimizations:

• Abstraction Refinement: Heuristics and driver for the array-abstraction-refinement. Maybe this could also handle the newly developed copy-abstraction-refinement.
• Linear Bitvector Solver: Optimizer and solver for some specialized bitvector terms. Also involves writing of some word-level transformations to preprocess AST data into normalized form.

The current Read-over-Write simplification might expand its input exponentially.
This could impose significant performance penalties and should be avoided.
By the newly introduced SymbolProxy in Context proxy symbols can be generated to substitute to-be-copied expression trees temporarily. They can be inserted back into the expression tree at a later point where they can be processed in isolation to their former parent until they are merged back again.

The same procedure can and should be implemented for Eliminate-Array-Read and Eliminate-Array-Write simplifications.

Currently the stevia_ast module interface is extremely polluted because every item is exported on global scope. Only the actual expression items have their own module.

We could need further modules to separate functionality:

1. type: For types and handling types and errors around typing issues.
2. transformer: For the AST transformer interfaces and utilities.
3. checks: For (general purpose) checks of the AST invariants.
4. iter: For iteration methods and structures over the AST.
5. utils: We also might need a utilities module for everything that acts as convenience or ... utility.

Also the expr sub module should receive another utils module where all the helper structures like BinaryChildren are located.

The new stevia_bitvec crate and its provided Bitvec implementation is still missing some core QF_BV functions. Namely, bvcomp with proper error handling (not panicking), rotate_left and rotate_right (supported in the upcoming apint version 0.3), and repeat.

For more information visit this page: http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV

Since cargo supports workspaces and since stevias modules (currently ast and simplifier) are far larger than expected it should be ideal for code reuse to seperate them more clearly by restructuring them into libraries connected in the stevia workspace. This makes it possible to implement later sub-libraries that depend on certain other stevia libraries.

Currently the simplification procedure naively simplifies any expression exactly five times since the simplifier is currently not tracking state changes due to successful simplifications. This should be changed to dynamically simplify until a fix-point has been reached.

• Evaluate the situation for other simplifiers and designs for more general solutions.
• Implement simplification tracking in Simplifier.
• Implement dynamic iteration in simplify.

Find and depend on decent library implementation similar or equal to STP's ABC library for and-inverter-graph (AIG) computation. A pure Rust implementation is favoured over any other implementation to avoid having non-ecosystem dependencies.

The current implementation of Bitvec::is_smax and Bitvec::is_smin is suboptimal because there is no native implementation for it in apint and we have to emulate the logic for it in stevia_bitvec. To improve this we could try implementing these (or similar) checks in apint since they might be reasonable to add there because of the already existing constructors unsigned_max_value etc.

Stevia could profit by implementing or at least providing Nand, Nor and Xnor in addition to And, Or and Xor that currently exist. This could make some simplifications involving negation simpler or at least more performant temporarily.

These additional expression types could be implemented on several different layers.

1. Factory-layer: Only provided by the expression build interface that internally directly forwards to And, Or and Xor. The downside is that this is quite intransparent to users that might be confused why no actual negated versions are created.
2. In the expression AST. The advantage is that it is transparent, the downside is that it is a lot of repetition and requires another set of simplification rules for them. They could be simply directly reduced to their non-negated counterparts upon simplification without other simplifications occuring.

Find out what scopes push & pop in STP are and how to incorporate them into this SMT solver.

Note: STP has a stack of vectors that acts as assertion scope level. Users may wish to add or remove such scopes to add or remove entire groups of assertions that have been added to the removed scope level. The STP scope design is inefficient and should not be taken over to Stevia. Stevia should model this concept with a single vector for the assertions and another vector for entry points to new scope levels.

Stevia should handle complex array expressions and thus be able to word-level simplify those together with array abstraction refinement.

To be implemented are:

1. Array-Read-Elimination: Eliminates ArrayRead expressions by replacing them with appropriate equi-satisfiable local- and root expressions.
2. Array-Write-Elimination: Eliminates ArrayWrite expressions by replacing them with appropriate equisatisfiable local- and root expressions.

Both simplifications require refinement expressions on the root scope of the input expression which can be refined by lazy insertion similar to how STP handles them via its array abstraction refinement.

Stevia could profit greatly from fuzz testing.

This could be more or less easily implemented at least for SMTLib2 parsing once implemented and for the word-level simplifier. Maybe later even for the bit blaster module.

For this there is a tool called cargo-fuzz that should work out of the box but we need parsing support for SMTLib2 before we can do any proper fuzz testing at all.