summaryrefslogtreecommitdiff
path: root/tests/calls.hs
blob: 16c2d576a4b9ef442a769b022ec6d1197d9b91e7 (plain)
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
import Yices.Base

main = do
    print version

    setVerbosity 7
    setMaxSatInitialCost 99
    setMaxNumConflictsInMaxSatIteration 100
    setTypeChecker True
    setMaxNumIterationsInMaxSat 1000
    setMaxSatInitialCost 200
    setArithmeticOnly True
    setLogFile "x.dat"

    c <- empty        
    reset c
    dump c
    push c
    pop c
    print =<< inconsistent c

    print =<< check c

    setVerbosity 0
    print =<< check c

    print =<< getUnsatCoreSize c

    print =<< getModel c

    print =<< getUnsatCore c