Skip to main content

module lang::smtlib2::\solve::Z3


Wrapper around the Microsoft Z3 solver. Lets you execute SMT statements (as SMTLIBv2 AST commands) and returns the found answer (if any).


import lang::smtlib2::\solve::Z3;


import String;
import IO;
import util::SystemAPI;
import util::ShellExec;
import lang::smtlib2::Compiler;
import lang::smtlib2::command::Ast;
import lang::smtlib2::command::response::Implode;
import lang::smtlib2::command::response::Ast;

function startZ3

Starts the Z3 solver. To run the solver the path to Z3 needs to be configure either by adding the -Dsolver.z3.path=<> to your eclipse.ini configuration or by supplying it when you call the solver using the keyword parameter 'pathToZ3'

PID startZ3(str pathToZ3 = getSystemProperty("solver.z3.path"))

function stopZ3

void stopZ3(PID z3)

function \run

Response \run(PID z3, Script script, bool debug = false)

function read

str read(PID z3)

function printIfDebug

void printIfDebug(str line, bool debug)