Module Solver.SMTLIB.Types

This module provides types for representing SMT solvers and options in Curry.

Author: Jan Tikovsky

Version: November 2017

Summary of exported operations:

Exported datatypes:

SMTSolver

SMT solver configuration

Constructors:

  • SMTSolver :: String -> [String] -> SMTSolver

    Fields:

    • executable :: String
    • flags :: [String]
SMTOpts

Options for SMT solving incremental - solve SMT problems incrementally quiet - work quietly tracing - produce SMT-LIB script with all commands used during a session globalCmds - set commands which are globally valid during a session

Constructors:

  • SMTOpts :: Bool -> Bool -> Bool -> [Command] -> SMTOpts

    Fields:

    • incremental :: Bool
    • quiet :: Bool
    • tracing :: Bool
    • globalCmds :: [Command]
SMTError

SMT solver error

Constructors:

  • SolverError :: String -> SMTError
  • ParserError :: String -> SMTError
  • OtherError :: String -> SMTError

Exported operations: