PropLogicTest

Convenient abbreviations and combinations of often used functions

Various prime form generations

pdnf' :: Ord a => PropForm a -> PDNF a

pcnf' :: Ord a => PropForm a -> PCNF a

spdnf' :: Ord a => PropForm a -> SimpleDNF a

spcnf' :: Ord a => PropForm a -> SimpleCNF a

xpdnf' :: Ord a => PropForm a -> XPDNF a

xpcnf' :: Ord a => PropForm a -> XPCNF a

Various prime form generations with combined parsing and display

pdnf :: String -> IO ()

pcnf :: String -> IO ()

spdnf :: String -> IO ()

spcnf :: String -> IO ()

xpdnf :: String -> IO ()

xpcnf :: String -> IO ()

Random generation

Auxiliary random functions (probably obsolete)

randomListMember :: [a] -> IO a

For example,

 > randomListMember ['a','b','c','d']
 'b'
 > randomListMember ['a','b','c','d']
 'd'
 > randomListMember ['a','b','c','d']
 'c'

randomChoice :: [a] -> IO (a, [a])

Removes one random member from a given list and returns this member and the remaining list. For example,

 > randomChoice ["a", "b", "c"]
 ("c",["a","b"])
 > randomChoice ["a", "b", "c"]
 ("b",["a","c"])
 > randomChoice ["a", "b", "c"]
 ("a",["b","c"])
 > randomChoice ["a", "b", "c"]
 ("a",["b","c"])

shuffle :: [a] -> IO [a]

For example,

 > shuffle [1,2,3,2,1]
 [2,1,3,1,2]
 > shuffle [1,2,3,2,1]
 [1,2,3,2,1]
 > shuffle [1,2,3,2,1]
 [2,1,2,3,1]
 > shuffle [1,2,3,2,1]
 [2,3,1,1,2]
 > shuffle [1,2,3,2,1]
 [2,1,1,3,2]
 > shuffle [1,2,3,2,1]
 [1,2,1,3,2]

randomSublist :: [a] -> IO [a]

randomSublist xL deletes a random number of members and returns the result. For example,

 > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
 [4]
 > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
 [3,4]
 > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
 [2,3,4,5,6,7,7,7,8,8]
 > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
 [1,2,5,7,8]
 > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
 [4,5,8,8]
 > randomSublist [1,2,3,4,5,6,7,7,7,8,8,8]
 [1,2,3,5,6,7,7,8,8]

nRandomRIO :: Int -> (Int, Int) -> IO [Int]

nRandomRIO n (lower,upper) returns an list of n random integers between lower and upper. For example,

 > nRandomRIO 10 (1,3)
 [2,3,3,2,2,3,3,3,3,1]
 > nRandomRIO 10 (1,3)
 [3,2,1,2,2,3,3,1,1,1]
 > nRandomRIO 10 (1,3)
 [1,3,2,1,2,1,2,2,1,2]

weightedRandomMember :: [(a, Int)] -> IO a

weightedRandomMember takes a list [(x1,n1),...,(xM,nM)] of (a,Int) pairs and selects one of the x1,...,xM. The second integer value ni in each pair (xi,ni) represents the relative likelihood for the choice of xi compare to the other values. In the following example and on the long run, a is chosen 10 times more often than b, and c isn't chosen at all.

 > weightedRandomMember [("a",10),("b",1),("c",0)]
 "a"
 > weightedRandomMember [("a",10),("b",1),("c",0)]
 "a"
 > weightedRandomMember [("a",10),("b",1),("c",0)]
 "a"
 > weightedRandomMember [("a",10),("b",1),("c",0)]
 "a"
 > weightedRandomMember [("a",10),("b",1),("c",0)]
 "a"
 > weightedRandomMember [("a",10),("b",1),("c",0)]
 "a"
 > weightedRandomMember [("a",10),("b",1),("c",0)]
 "a"
 > weightedRandomMember [("a",10),("b",1),("c",0)]
 "b"
 > weightedRandomMember [("a",10),("b",1),("c",0)]
 "a"

appleBasketDistribution :: Int -> Int -> IO [Int]

appleBasketDistribution n k distributes n apples into k baskets in the sense that the result is a random integer list of length k, where the sum of its components is n.

 > appleBasketDistribution 10 4
 [4,2,2,2]
 > appleBasketDistribution 10 4
 [2,2,3,3]
 > appleBasketDistribution 10 4
 [3,2,1,4]
 > appleBasketDistribution 10 4
 [0,7,0,3]

Random I-Forms and X-Forms

averageLineLength :: IForm -> Float

randomILine :: Int -> Int -> IO ILine

randomIForm :: Int -> Int -> Int -> IO IForm

randomXForm :: Ord a => [a] -> Int -> Int -> IO (XForm a)

Random DNFs and CNFs

randomDNF :: Ord a => [a] -> Int -> Int -> IO (DNF a)

randomCNF :: Ord a => [a] -> Int -> Int -> IO (CNF a)

randomCharDNF :: Int -> IO (DNF Char)

randomCharCNF :: Int -> IO (CNF Char)

randomIntDNF :: Int -> IO (DNF Int)

randomIntCNF :: Int -> IO (CNF Int)

Random propositional formulas in general

Size parameter

type SizeTriple = (Int, Int, Int)

sizeTriple :: Ord a => PropForm a -> SizeTriple

Random formulas

data JunctorSymbol

Constructors

T_

F_

N_

CJ_

DJ_

SJ_

EJ_

Instances

Eq JunctorSymbol

Ord JunctorSymbol

Read JunctorSymbol

Show JunctorSymbol

type JunctorWeighting = [(JunctorSymbol, Int)]

defaultJunctorWeighting :: JunctorWeighting

weightedRandomPropForm :: JunctorWeighting -> Olist a -> (Int, Int) -> IO (PropForm a)

randomPropForm :: Olist a -> (Int, Int) -> IO (PropForm a)

randomPropForm aL (aSize,jSize) returns a randomly generated propositional formula p such that

     atoms p    == aL
     atomSize p == aSize
     juncSize p == jSize

If atomSize is smaller than the length of aL, an error message is returned. For example,

 > randomPropForm ["x", "y"] (3,3)
 EJ [A "y",T,A "y",A "x",DJ []]
 > randomPropForm ["x", "y"] (3,3)
 EJ [SJ [A "y",A "y"],DJ [A "x"]]
 > randomPropForm ["x", "y"] (3,3)
 EJ [EJ [],A "x",CJ [A "y"],A "x"]
 > randomPropForm ['x','y','z'] (1,1)
 *** Exception: randomPropForm -- atom size smaller than ordered atom list

randomCharProp :: SizeTriple -> IO (PropForm Char)

randomCharProp (aCard,aSize,jSize) is randomPropForm aL (aSize,jSize), where aL is the ordered list of the first aCard small characters a, b, c, .... If the atom cardinality is undefined, i.e. if not 0<=aCard<=26, or if it exceeds aSize, an error message is returned. For example,

 > randomCharProp (3,5,5)
 SJ [A 'c',EJ [A 'a',A 'c'],F,T,DJ [A 'b'],A 'c']
 > randomCharProp (3,5,5)
 SJ [A 'a',A 'c',DJ [T,CJ [A 'b',A 'a',A 'b'],T]]
 > randomCharProp (3,5,5)
 DJ [F,A 'b',SJ [F],A 'c',DJ [A 'a'],A 'c',A 'a']

randomIntProp :: SizeTriple -> IO (PropForm Int)

Testing

Testing a propositional algebra

Axioms of propositional algebras

axiom_reflexivity_of_subvalence :: PropAlg a p => p -> Bool

axiom_transitivity_of_subvalence :: PropAlg a p => (p, p, p) -> Bool

axiom_criterion_for_equivalence :: PropAlg a p => (p, p) -> Bool

CONTINUEHERE ..............................................................!!

The summarized test function for a propositional algebra

test_prop_alg :: (Show a, Show p, PropAlg a p) => IO a -> IO p -> Int -> IO ()

Tests for DefaultPropLogic

Testing the normalizations

...continuehere...............................

Testing the default propositional algebras

Tests for FastPropLogic

Testing of the M- and P-procedure

continuehere ............................

Correctness of the Prime Normal Form constructions

continuehere ...........................

Test for the total package

total_test :: Int -> IO ()

Profiling - first version

Measures

type Msec = Integer

type CanonPerformance = (SizeTriple, (Msec, SizeTriple), (Msec, SizeTriple))

type Verbose = Bool

correctness tests (move these correctness tests)--!!!!!!!!!!1

pnfCorrect :: (Display a, Show a, Ord a) => Verbose -> PropForm a -> IO (Either (PropForm a) CanonPerformance)

pnfCorrectRepeat :: Verbose -> (Int, Int, Int) -> IO (PropForm Char)

performance tests

pnfPerform :: (Display a, Show a, Ord a) => PropForm a -> IO CanonPerformance

pnfPerformRandom :: SizeTriple -> IO CanonPerformance

pnfPerformRepeat :: SizeTriple -> IO ()

Profiling - second version

type Seconds = Double

verboseRandomPrimeTest :: (Int, Int, Int) -> IO (Int, Int, Int, Seconds)

randomPrimeTest (atomNum, formLen, averLineLen) = (atomNum', formLen', vol', secs')

verboseRandomPrimeTesting :: (Int, Int, Int) -> Int -> IO (Int, Int, Seconds, Seconds, Seconds)

verboseRandomPrimeTesting (atomNum, formLen, averLineLen) numberOfTests = (maxFormLen, averFormLen, maxTime, averTime, standDev)

meanValue :: [Seconds] -> Seconds

standDeviation :: [Seconds] -> Seconds

normSeconds :: Seconds -> Seconds