Skip to main content

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

rascal-0.40.16

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

Usage​

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

Dependencies​

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=<local.path.to.z3> 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)