Package edu.udel.cis.vsl.sarl.prove.z3

package edu.udel.cis.vsl.sarl.prove.z3

This package provides implementations of the TheoremProver and TheoremProverFactory interfaces based on Microsoft's Z3 theorem prover. See the Z3 web page.

Classes

Class	Description
RobustZ3TheoremProver	An implementation of TheoremProver using the automated theorem provers Z3.
RobustZ3TheoremProverFactory	Factory for producing new instances of RobustCVCTheoremProver.
Z3Translator	Translates SARL SymbolicExpressions to the language of the automated theorem prover Z3.