Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
i7
peregrine
Commits
2f387156
Commit
2f387156
authored
Aug 08, 2018
by
Philipp Meyer
Browse files
Rename LinearInequation to Equation
parent
ebce00a0
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/Parser/PP.hs
View file @
2f387156
...
...
@@ -107,12 +107,12 @@ parseOp = (reservedOp "<" *> return Lt) <|>
(
reservedOp
"=%"
*>
(
ModEq
<$>
integer
))
<|>
(
reservedOp
"!=%"
*>
(
ModNe
<$>
integer
))
linIneq
::
Parser
(
Formula
String
)
linIneq
=
do
equation
::
Parser
(
Formula
String
)
equation
=
do
lhs
<-
term
op
<-
parseOp
rhs
<-
term
return
(
LinearIne
quation
lhs
op
rhs
)
return
(
E
quation
lhs
op
rhs
)
formOperatorTable
::
[[
Operator
String
()
Identity
(
Formula
String
)]]
formOperatorTable
=
...
...
@@ -122,7 +122,7 @@ formOperatorTable =
]
formAtom
::
Parser
(
Formula
String
)
formAtom
=
try
linIneq
formAtom
=
try
equation
<|>
(
reserved
"true"
*>
return
FTrue
)
<|>
(
reserved
"false"
*>
return
FFalse
)
<|>
parens
formula
...
...
src/Property.hs
View file @
2f387156
...
...
@@ -64,7 +64,7 @@ negateOp (ModNe m) = (ModEq m)
data
Formula
a
=
FTrue
|
FFalse
|
LinearIne
quation
(
Term
a
)
Op
(
Term
a
)
|
E
quation
(
Term
a
)
Op
(
Term
a
)
|
Neg
(
Formula
a
)
|
Formula
a
:&:
Formula
a
|
Formula
a
:|:
Formula
a
...
...
@@ -78,11 +78,11 @@ negationNormalForm (Neg (FTrue)) = FFalse
negationNormalForm
(
Neg
(
FFalse
))
=
FTrue
negationNormalForm
(
Neg
(
g
:&:
h
))
=
(
negationNormalForm
(
Neg
g
))
:|:
(
negationNormalForm
(
Neg
h
))
negationNormalForm
(
Neg
(
g
:|:
h
))
=
(
negationNormalForm
(
Neg
g
))
:&:
(
negationNormalForm
(
Neg
h
))
negationNormalForm
(
Neg
(
LinearIne
quation
u
op
t
))
=
LinearIne
quation
u
(
negateOp
op
)
t
negationNormalForm
(
Neg
(
E
quation
u
op
t
))
=
E
quation
u
(
negateOp
op
)
t
negationNormalForm
(
Neg
(
Neg
g
))
=
negationNormalForm
g
negationNormalForm
(
g
:&:
h
)
=
(
negationNormalForm
g
)
:&:
(
negationNormalForm
h
)
negationNormalForm
(
g
:|:
h
)
=
(
negationNormalForm
g
)
:|:
(
negationNormalForm
h
)
negationNormalForm
f
@
(
LinearIne
quation
_
_
_
)
=
f
negationNormalForm
f
@
(
E
quation
_
_
_
)
=
f
negationNormalForm
FTrue
=
FTrue
negationNormalForm
FFalse
=
FFalse
...
...
@@ -91,14 +91,14 @@ eliminateModulo = eliminateModulo' 0
eliminateModulo'
::
Int
->
(
Int
->
a
)
->
Formula
a
->
(
Formula
a
,
[
a
])
eliminateModulo'
_
_
(
Neg
g
)
=
error
"Formula not in negation normal form: cannot eliminate modulo"
eliminateModulo'
n
makeVar
(
LinearIne
quation
lhs
(
ModEq
m
)
rhs
)
=
eliminateModulo'
n
makeVar
(
E
quation
lhs
(
ModEq
m
)
rhs
)
=
let
k
=
makeVar
n
in
(
LinearIne
quation
lhs
Eq
(
rhs
:+:
((
Const
m
)
:*:
(
Var
k
))),
[
k
])
eliminateModulo'
n
makeVar
(
LinearIne
quation
lhs
(
ModNe
m
)
rhs
)
=
in
(
E
quation
lhs
Eq
(
rhs
:+:
((
Const
m
)
:*:
(
Var
k
))),
[
k
])
eliminateModulo'
n
makeVar
(
E
quation
lhs
(
ModNe
m
)
rhs
)
=
let
j
=
makeVar
(
n
+
1
)
k
=
makeVar
n
in
((
LinearIne
quation
lhs
Eq
(
rhs
:+:
((
Var
j
)
:+:
((
Const
m
)
:*:
(
Var
k
)))))
:&:
(
LinearIne
quation
(
Const
0
)
Lt
(
Var
j
))
:&:
(
LinearIne
quation
(
Var
j
)
Lt
(
Const
m
)),
[
k
,
j
])
in
((
E
quation
lhs
Eq
(
rhs
:+:
((
Var
j
)
:+:
((
Const
m
)
:*:
(
Var
k
)))))
:&:
(
E
quation
(
Const
0
)
Lt
(
Var
j
))
:&:
(
E
quation
(
Var
j
)
Lt
(
Const
m
)),
[
k
,
j
])
eliminateModulo'
n
makeVar
(
g
:|:
h
)
=
let
(
g'
,
ag
)
=
eliminateModulo'
n
makeVar
g
(
h'
,
ah
)
=
eliminateModulo'
(
n
+
length
ag
)
makeVar
h
...
...
@@ -112,7 +112,7 @@ eliminateModulo' _ _ f = (f, [])
instance
(
Show
a
)
=>
Show
(
Formula
a
)
where
show
FTrue
=
"true"
show
FFalse
=
"false"
show
(
LinearIne
quation
lhs
op
rhs
)
=
show
(
E
quation
lhs
op
rhs
)
=
show
lhs
++
" "
++
show
op
++
" "
++
show
rhs
show
(
Neg
p
)
=
"¬"
++
"("
++
show
p
++
")"
show
(
p
:&:
q
)
=
"("
++
show
p
++
" ∧ "
++
show
q
++
")"
...
...
@@ -121,8 +121,8 @@ instance (Show a) => Show (Formula a) where
instance
Functor
Formula
where
fmap
_
FTrue
=
FTrue
fmap
_
FFalse
=
FFalse
fmap
f
(
LinearIne
quation
lhs
op
rhs
)
=
LinearIne
quation
(
fmap
f
lhs
)
op
(
fmap
f
rhs
)
fmap
f
(
E
quation
lhs
op
rhs
)
=
E
quation
(
fmap
f
lhs
)
op
(
fmap
f
rhs
)
fmap
f
(
Neg
p
)
=
Neg
(
fmap
f
p
)
fmap
f
(
p
:&:
q
)
=
fmap
f
p
:&:
fmap
f
q
fmap
f
(
p
:|:
q
)
=
fmap
f
p
:|:
fmap
f
q
...
...
src/Solver/Formula.hs
View file @
2f387156
...
...
@@ -27,7 +27,7 @@ opToFunction Lt = (.<)
evaluateFormula
::
(
Ord
a
,
Show
a
)
=>
Formula
a
->
SIMap
a
->
SBool
evaluateFormula
FTrue
_
=
true
evaluateFormula
FFalse
_
=
false
evaluateFormula
(
LinearIne
quation
lhs
op
rhs
)
m
=
evaluateFormula
(
E
quation
lhs
op
rhs
)
m
=
opToFunction
op
(
evaluateTerm
lhs
m
)
(
evaluateTerm
rhs
m
)
evaluateFormula
(
Neg
p
)
m
=
bnot
$
evaluateFormula
p
m
evaluateFormula
(
p
:&:
q
)
m
=
evaluateFormula
p
m
&&&
evaluateFormula
q
m
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment