1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83

--- ----------------------------------------------------------------------------
--- This module provides operations for an interactive communication with
--- SMT solvers - which implement the SMT-LIB interface - via stdin and stdout.
--- Currently only the Z3 SMT solver is supported.
---
--- @author  Jan Tikovsky, Marcellus Siegburg
--- @version January 2018
--- ----------------------------------------------------------------------------
module Solver.SMTLIB.Session
  ( module Solver.SMTLIB.Types
  , SMTError (..), SMTOpts (..), SMTSess, SMTSolver (..)
  , defSMTOpts, evalSessions, freshSMTVars, setSMTOpts, solveSMT, solveSMTVars
  , liftIOA
  ) where

import Language.SMTLIB.Types (Command, ModelRsp, Sort, Term, ValuationPair)

import Solver.SMTLIB.Internal.Interaction
import Solver.SMTLIB.Types

--- default options for SMT solving
defSMTOpts :: SMTOpts
defSMTOpts = SMTOpts
  { incremental = False
  , quiet       = True
  , tracing     = False
  , globalCmds  = []
  }

--- Evaluate SMT sessions by applying given solver and options
evalSessions :: SMTSolver -> SMTOpts -> SMTSess a -> IO a
evalSessions = evalSessionsImpl

--- Set options for SMT solving
setSMTOpts :: SMTOpts -> SMTSess ()
setSMTOpts opts = evalSession $ do
  resetSession
  modify $ \s -> s { options = opts }

--- Get n fresh variables of given sort
freshSMTVars :: Int -> Sort -> SMTSess [Term]
freshSMTVars n s = evalSession $ declareVars n s

--- Solve the SMT problem specified by the given SMT-LIB commands and
--- try to find a binding for all variables used
solveSMT :: [Command] -> SMTSess (Either [SMTError] [ModelRsp])
solveSMT cmds = evalSession $ do
  bufferGlobalDefs
  info "Asserting definitions and constraints"
  sendCmds cmds
  info "Checking satisfiability of constraints"
  isSat <- checkSat
  case isSat of
    Sat -> do
      info "Satisfiable -> Getting model for SMT problem"
      m <- getModel
      optReset
      return m
    res -> do
      info "No model found for given SMT problem"
      optReset
      return $ Left $ res2Msgs res

--- Solve the SMT problem specified by the given SMT-LIB commands and
--- try to find a binding for all given variables
solveSMTVars :: [Term] -> [Command]
             -> SMTSess (Either [SMTError] [ValuationPair])
solveSMTVars vars cmds = evalSession $ do
  bufferGlobalDefs
  info "Asserting definitions and constraints"
  sendCmds cmds
  info "Checking satisfiability of constraints"
  isSat <- checkSat
  case isSat of
    Sat -> do
      info "Satisfiable -> Getting bindings of given variables for SMT problem"
      vps <- getValues vars
      optReset
      return vps
    res -> do
      info "No variable bindings found for given SMT problem"
      optReset
      return $ Left $ res2Msgs res