Searched refs:SMTMode (Results 1 – 5 of 5) sorted by relevance
932 show (SMTMode qc ISafe True _) = "Safety setup (" ++ show qc ++ ")"933 show (SMTMode qc IRun True _) = "Satisfiability (" ++ show qc ++ ")"934 show (SMTMode qc ISetup False _) = "Proof setup (" ++ show qc ++ ")"936 show (SMTMode qc IRun False _) = "Proof (" ++ show qc ++ ")"947 SMTMode{} -> False1153 SMTMode{} -> True1217 SMTMode _ IRun _ _ -> interactiveUpdate1292 SMTMode _ _ True _ -> EX1293 SMTMode _ _ False _ -> ALL1553 (Just q, SMTMode{} ) -> mkS q[all …]
357 …fst <$> runSymbolic (SMTMode QueryInternal ISetup True cfg) (forSome_ a >> Control.executeQuery Qu…618 …(_, res) <- runSymbolic (SMTMode QueryInternal ISetup isSat cfg) $ (if isSat then forSome_ else fo…620 …let SMTProblem{smtLibPgm} = Control.runProofOn (SMTMode QueryInternal IRun isSat cfg) QueryInterna…755 runSMTWith cfg a = fst <$> runSymbolic (SMTMode QueryExternal ISetup True cfg) a759 runWithQuery isSAT q cfg a = fst <$> runSymbolic (SMTMode QueryInternal ISetup isSAT cfg) comp849 … fst <$> runSymbolic (SMTMode QueryInternal ISafe True cfg) (sName_ a >> check mkRelative)
1465 … SMTMode _ stage s c -> (c, s, isSafetyCheckingIStage stage, isSetupIStage stage)1504 … (QueryExternal, SMTMode QueryExternal ISetup _ _) -> return () -- legitimate runSMT call1536 SMTMode _ _ _ cfg -> allowQuantifiedQueries cfg1565 SMTMode qc stage isSAT cfg | not (isRunIStage stage) -> do1588 liftIO $ writeIORef (runMode st) $ SMTMode qc IRun isSAT cfg1626 SMTMode _ IRun _ _ -> error $ unlines [ ""
321 SMTMode _ _ isSAT _ -> do
141 runSAT cmp = snd <$> runSymbolic (SMTMode QueryInternal ISetup True defaultSMTCfg) cmp