Package | Description |
---|---|
de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
de.uka.ilkd.key.smt.lang | |
de.uka.ilkd.key.smt.model |
Class and Description |
---|
SMTFile |
SMTFunction |
SMTSort |
SMTTerm |
SMTTermNumber |
SMTTermVariable |
Class and Description |
---|
SMTFunction |
SMTSort |
SMTTerm |
SMTTermBinOp |
SMTTermBinOp.Op |
SMTTermBinOp.OpProperty |
SMTTermCall
SMTLib supports functions as well as predicates.
|
SMTTermMultOp |
SMTTermMultOp.Op |
SMTTermMultOp.OpProperty |
SMTTermNumber |
SMTTermQuant |
SMTTermQuant.Quant |
SMTTerms |
SMTTermUnaryOp |
SMTTermUnaryOp.Op |
SMTTermVariable |
Class and Description |
---|
SMTSort |
Copyright © 2003-2019 The KeY-Project.