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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144

--- ----------------------------------------------------------------------------
--- 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 August 2021
--- ----------------------------------------------------------------------------
module Solver.SMTLIB.Session
  ( module Solver.SMTLIB.Types
  , SMTError (..), SMTOpts (..), SMTSess, SMTSolver (..)
  , defSMTOpts, evalSessions, freshSMTVars, setSMTOpts, solveSMT, solveSMTVars
  , solveAllSMTVars, liftIOA
  ) where

import Control.Monad.Extra     (concatMapM)
import Data.List               (nub)
import Data.Maybe              (fromJust)

import Language.SMTLIB.Goodies (assert, (/=%))
import Language.SMTLIB.Types   ( Command (Push, Pop), 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

--- Solve the SMT problem specified by the given SMT-LIB commands and
--- try to find all bindings for the given variable.
--- The given integer determines how many counter examples are returned at
--- maximum for each variable.
solveAllSMTVars :: [Term] -> [Command] -> Int
                -> SMTSess (Either [SMTError] [[ValuationPair]])
solveAllSMTVars vars cmds i = 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
      case vps of
        Right vps' -> do
          vpss <- concatMapM (getCounterExamples vps' i) vars
          optReset
          return $ Right $ nub vpss
        Left e     -> optReset >> (return $ Left e)
    Unsat -> do
      info "No variable bindings found for given SMT problem"
      optReset
      return $ Right []
    res -> do
      info "An error occurred while solving given SMT problem"
      optReset
      return $ Left $ res2Msgs res
  where
    getCounterExamples :: [ValuationPair] -> Int -> Term
                       -> SMT [[ValuationPair]]
    getCounterExamples vps i' var = do
      bufferCmds [Push 1]
      vpss <- assertCounterExamples (fromJust $ lookup var vps) [vps] var i'
      bufferCmds [Pop 1]
      return vpss

    assertCounterExamples :: Term -> [[ValuationPair]] -> Term -> Int
                          -> SMT [[ValuationPair]]
    assertCounterExamples v vpss var i' = do
      sendCmds [assert [var /=% v]]
      isSat <- checkSat
      case isSat of
        Sat -> do
          vps <- getValues vars
          case vps of
            Right vps' | i' > 1 -> assertCounterExamples
                                     (fromJust $ lookup var vps')
                                     (vps':vpss) var (i' - 1)
            _                   -> return vpss
        _ -> return vpss