Toggle navigation
PAKCS
All operations
All constructors
Curry Homepage
PAKCS Libraries
About CurryDoc
Index to all operations
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
*
*#
(
XFD.FD
)
*>
(
XFD.Parser
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
+
+#
(
XFD.FD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
-
-#
(
XFD.FD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
/
/=#
(
XFD.FD
)
/\
(
XFD.FD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
<
<#
(
XFD.FD
)
<$>
(
XFD.Parser
)
<*
(
XFD.Parser
)
<*>
(
XFD.Parser
)
<=#
(
XFD.FD
)
<|>
(
XFD.Parser
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
=
=#
(
XFD.FD
)
=>>
(
XFD.SMTLib.FromFD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
>
>#
(
XFD.FD
)
>=#
(
XFD.FD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
A
abs
(
XFD.FD
)
adder
(
Dimacs.FromFD
)
allC
(
XFD.FD
)
allDifferent
(
XFD.FD
)
allEFDVars
(
XFD.FD
)
allFDVars
(
XFD.FD
)
allFDVars'
(
XFD.FD
)
andC
(
XFD.FD
)
arithmetic
(
Dimacs.FromFD
)
assert
(
XFD.SMTLib.FromFD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
B
bindS
(
XFD.State
)
bindS_
(
XFD.State
)
binVal
(
Dimacs.FromFD
)
booleanEqual
(
Dimacs.FromFD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
C
checkSat
(
XFD.SMTLib.FromFD
)
convert
(
Dimacs.FromFD
)
convertCmdResponseToFD
(
XFD.SMTLib.FromFD
)
convertConstr
(
XFD.SMTLib.FromFD
)
convertEqual
(
Dimacs.FromFD
)
convertExpr
(
XFD.SMTLib.FromFD
)
convertFDConstr
(
Dimacs.FromFD
)
convertFDRel
(
Dimacs.FromFD
)
convertFDVar
(
Dimacs.FromFD
)
convertFDVars
(
Dimacs.FromFD
)
convertFunDefToFD
(
XFD.SMTLib.FromFD
)
convertModelResponseToFD
(
XFD.SMTLib.FromFD
)
convertSimplification
(
Dimacs.FromFD
)
convertSimplifications
(
Dimacs.FromFD
)
convertValueResponseToFD
(
XFD.SMTLib.FromFD
)
count
(
XFD.FD
)
cvc4Config
(
XFD.Solvers.CVC4
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
D
declare
(
XFD.SMTLib.FromFD
)
declareConst
(
XFD.SMTLib.FromFD
)
declareConst
(
XFD.SMTLib.Build
)
declareInt
(
XFD.SMTLib.Build
)
defaultConfig
(
XFD.Solver
)
defaultOptions
(
XFD.Solver
)
dFalse
(
Dimacs.FromFD
)
domain
(
XFD.FD
)
domainWPrefix
(
XFD.FD
)
dTrue
(
Dimacs.FromFD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
E
echo
(
XFD.SMTLib.FromFD
)
eof
(
XFD.Parser
)
evalState
(
XFD.State
)
excludeSolution
(
XFD.Dimacs
)
execState
(
XFD.State
)
executable
(
XFD.Solver
)
exit
(
XFD.SMTLib.FromFD
)
extractSolution
(
Dimacs.FromFD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
F
false
(
XFD.FD
)
fd
(
XFD.FD
)
fdVarEq
(
XFD.FD
)
filterFDVars
(
XFD.FD
)
filterVars
(
XFD.FD
)
flags
(
XFD.Solver
)
fullAdder
(
Dimacs.FromFD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
G
getFDVal
(
XFD.FD
)
getFDVarName
(
XFD.FD
)
getModel
(
XFD.SMTLib.FromFD
)
getS
(
XFD.State
)
getSolutions
(
XFD.Dimacs
)
getSolverOptions
(
XFD.Solver
)
getValue
(
XFD.SMTLib.FromFD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
I
ident
(
XFD.SMTLib.Build
)
ilog2
(
Dimacs.FromFD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
L
liftP2
(
XFD.Parser
)
liftS
(
XFD.State
)
liftS2
(
XFD.State
)
lingeling
(
XFD.Dimacs
)
lookupVar
(
Dimacs.FromFD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
M
mapS
(
XFD.State
)
mapS_
(
XFD.State
)
modifyS
(
XFD.State
)
mSome
(
XFD.SMTLib.NDParser
)
mStar
(
XFD.SMTLib.NDParser
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
N
notC
(
XFD.FD
)
numBits
(
Dimacs.FromFD
)
numBitsFor
(
Dimacs.FromFD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
O
orC
(
XFD.FD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
P
parse
(
XFD.SMTLib.NDParser
)
parse
(
XFD.SMTLib.RDParser
)
parseCheckSatResponse
(
XFD.SMTLib.NDParser
)
parseCmdCheckSatResponse
(
XFD.SMTLib.NDParser
)
parseCmdCheckSatResponse
(
XFD.SMTLib.RDParser
)
parseCmdGenResponse
(
XFD.SMTLib.NDParser
)
parseCmdGenResponse
(
XFD.SMTLib.RDParser
)
parseCmdGetModelResponse
(
XFD.SMTLib.NDParser
)
parseCmdGetValueResponse
(
XFD.SMTLib.NDParser
)
parseCmdGetValueResponse
(
XFD.SMTLib.RDParser
)
parseCmdResult
(
XFD.SMTLib.NDParser
)
parseCmdResult
(
XFD.SMTLib.RDParser
)
parseErrorResponse
(
XFD.SMTLib.NDParser
)
parseErrorResponse
(
XFD.SMTLib.RDParser
)
parseFunDef
(
XFD.SMTLib.NDParser
)
parseGenResponse
(
XFD.SMTLib.NDParser
)
parseGetModelResponse
(
XFD.SMTLib.NDParser
)
parseGetValueResponse
(
XFD.SMTLib.NDParser
)
parseGetValueResponse
(
XFD.SMTLib.RDParser
)
parseModelResponse
(
XFD.SMTLib.NDParser
)
parseString
(
XFD.SMTLib.NDParser
)
parseString
(
XFD.SMTLib.RDParser
)
parseTerm
(
XFD.SMTLib.NDParser
)
parseTerm
(
XFD.SMTLib.RDParser
)
parseTQId
(
XFD.SMTLib.NDParser
)
parseTSPC
(
XFD.SMTLib.NDParser
)
parseValuePair
(
XFD.SMTLib.NDParser
)
parseValuePair
(
XFD.SMTLib.RDParser
)
pop
(
XFD.SMTLib.FromFD
)
push
(
XFD.SMTLib.FromFD
)
putS
(
XFD.State
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
Q
qIdent
(
XFD.SMTLib.Build
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
R
returnS
(
XFD.State
)
runState
(
XFD.State
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
S
scalarProduct
(
XFD.FD
)
scan
(
XFD.SMTLib.Scanner
)
sequenceS
(
XFD.State
)
sequenceS_
(
XFD.State
)
setEq
(
Dimacs.FromFD
)
setLogic
(
XFD.SMTLib.FromFD
)
setOptions
(
XFD.SMTLib.FromFD
)
showSMT
(
XFD.SMTLib.FromFD
)
showSMTLib
(
XFD.SMTLib.Pretty
)
simplifyConstr
(
Dimacs.FromFD
)
smtLogic
(
XFD.Solver
)
smtOptions
(
XFD.Solver
)
solveD
(
XFD.Dimacs
)
solveDimacs
(
XFD.Dimacs
)
solveFD
(
XFD
)
solveFD
(
XFD.Solvers.SAT.Z3
)
solveFD
(
XFD.Solvers.SAT.Lingeling
)
solveFD
(
XFD.Solvers.SMT.Z3
)
solveFD
(
XFD.Solvers.SMT.MathSAT
)
solveFD
(
XFD.Solvers.SMT.CVC4
)
solveFD
(
XFD.Solvers.SMT.Yices
)
solveFDAll
(
XFD.Solvers.SAT.Z3
)
solveFDAll
(
XFD.Solvers.SAT.Lingeling
)
solveFDAll
(
XFD.Solvers.SMT.Z3
)
solveFDAll
(
XFD.Solvers.SMT.MathSAT
)
solveFDAll
(
XFD.Solvers.SMT.CVC4
)
solveFDAll
(
XFD.Solvers.SMT.Yices
)
solveFDAllwith
(
XFD.Solver
)
solveFDOne
(
XFD.Solvers.SAT.Z3
)
solveFDOne
(
XFD.Solvers.SAT.Lingeling
)
solveFDOne
(
XFD.Solvers.SMT.Z3
)
solveFDOne
(
XFD.Solvers.SMT.MathSAT
)
solveFDOne
(
XFD.Solvers.SMT.CVC4
)
solveFDOne
(
XFD.Solvers.SMT.Yices
)
solveFDOnewith
(
XFD.Solver
)
solveFDwith
(
XFD
)
solveFDwith
(
XFD.Solver
)
solverConfig
(
XFD.Solvers.SAT.Lingeling
)
solveSMT
(
XFD.SMTLib
)
solveWith
(
XFD.Solver
)
some
(
XFD.Parser
)
specConstNum
(
XFD.SMTLib.Build
)
star
(
XFD.Parser
)
sum
(
XFD.FD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
T
terminal
(
XFD.Parser
)
termQIdent
(
XFD.SMTLib.Build
)
termQIdentT
(
XFD.SMTLib.Build
)
termSpecConstNum
(
XFD.SMTLib.Build
)
test
(
XFD.Dimacs
)
testExtraction
(
XFD.Dimacs
)
toBits
(
Dimacs.FromFD
)
true
(
XFD.FD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
U
unexpected
(
XFD.Parser
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
Y
yield
(
XFD.Parser
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
Z
z3Config
(
XFD.Solvers.Z3
)
z3Dimacs
(
XFD.Dimacs
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\
\
\/
(
XFD.FD
)
*
+
-
/
<
=
>
A
B
C
D
E
F
G
I
L
M
N
O
P
Q
R
S
T
U
Y
Z
\