LeventErkok

import Data.SBV

leftAppend :: SInteger -> SInteger -> SInteger
leftAppend k n = ite (n .< 10       ) (n + k *10)
               $ ite (n .< 100      ) (n + k *100)
               $ ite (n .< 1000     ) (n + k * 1000)
               $ ite (n .< 10000    ) (n + k * 10000)
               $ ite (n .< 100000   ) (n + k * 100000)
               $ ite (n .< 1000000  ) (n + k * 1000000)
               $ ite (n .< 10000000 ) (n + k * 10000000)

LeventErkok

import Control.Monad.Trans  (liftIO)
import Control.Monad.Reader (ask)

import Data.SBV.Dynamic

--------------------------------------------------------------------------------
-- I should really export the following four definitions from SBV.Dynamic
mkWordN :: Int -> String -> Symbolic SVal
mkWordN w nm = ask >>= liftIO . svMkSymVar Nothing (KBounded False w) (Just nm)

LeventErkok

import Data.SBV
import Data.List (zip4)

import qualified Data.Map as M

data MyTestData = TD0 Bool
                | TD1 Integer
                | TD2 Word32
                deriving Show

LeventErkok

import Data.SBV

p :: Goal
p = do a  <- sInteger "a"
       b  <- sInteger "b"
       ab <- sInteger "ab"

       constrain $ a*a - b*b .== 21
       constrain $ a*a + b*b .== 29

LeventErkok

import Data.SBV

p :: Bool -> Predicate
p bug = do
    a <- sInteger "a"
    b <- sInteger "b"

    -- We'll do our proof with a two-level case split. First on 'a', then on 'b'
    -- The conditions are rather arbitrary for illustrative examples here. But they
    -- are arbitrary SBool's, so you can code anything you want.

LeventErkok

stgEqType: unequal                                                                                                                                                  
  ((State                                                                                                                                                           
    -> Exp -> State# RealWorld -> (# State# RealWorld, State #)) :: *)                                                                                              
  ~R#                                                                                                                                                               
  ((State -> Exp -> IO State) :: *)                                                                                                                                 
  (() :: *) ~# (() :: *)                                                                                                                                            
ghc: panic! (the 'impossible' happ

LeventErkok

{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}

module Check where

import Data.SBV
import Data.Generics

-- One of three states we can be in
data State  = S0 | S1 | S2 deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind)

LeventErkok

rm -rf lingeling*
tar xf archives/lingeling*.tar.gz
mv lingeling* lingeling
cd lingeling && ./configure.sh && make
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA
gcc -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA -c lglib.c
lglib.c:19486:7: warning: variable 'res' is used uninitialized whenever 'if' condition is false
      [-Wsometimes-uninitialized]
  if (lglgaussextractexactly1 (lgl, c)) res = 1;
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

LeventErkok

{-
 - DFA minimizer. See:
 -
 - https://www.tutorialspoint.com/automata_theory/dfa_minimization.htm
 -}

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns             #-}
module DFA (main) where

LeventErkok

module Main(main) where

import Data.Maybe (fromJust)
import Data.List (nub)

import Text.Parsec
import Text.Parsec.Language
import qualified Text.Parsec.Token as P

-- For the SMT solver interface