Module prover 

Z3 SMT Solver integration for formal equation verification.

HARD REQUIREMENT: Every EDD simulation MUST prove its governing equations using the Z3 SMT solver from Microsoft Research.

Why Z3?

• 2019 Herbrand Award for Distinguished Contributions to Automated Reasoning
• 2015 ACM SIGPLAN Programming Languages Software Award
• 2018 ETAPS Test of Time Award
• In production at Microsoft since 2007
• Open source (MIT license) since 2015

References

• [56] de Moura, L. & Bjørner, N. (2008). “Z3: An Efficient SMT Solver”
• [57] Microsoft Research. “Z3 Theorem Prover”

Example

use simular::edd::prover::{Z3Provable, ProofResult};

impl Z3Provable for MySimulation {
    fn proof_description(&self) -> &'static str {
        "Energy Conservation: E(t) = E(0) for all t"
    }

    fn prove_equation(&self) -> Result<ProofResult, ProofError> {
        // Encode equation in Z3 and prove
    }
}

Structs

ProofResult

Result of a successful Z3 proof.

Enums

ProofError

Error type for Z3 proofs.

Traits

Z3Provable

MANDATORY trait for all EDD simulations.