Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Christian Müller
NIWO
Commits
12106957
Commit
12106957
authored
Feb 07, 2019
by
Christian Müller
Browse files
z3 quantified
parent
34ba7fdf
Changes
20
Hide whitespace changes
Inline
Side-by-side
src/main/scala/de/tum/workflows/InvariantInspector.scala
View file @
12106957
...
...
@@ -46,7 +46,7 @@ object InvariantInspector extends App with LazyLogging {
val
lastlabels
=
afterlabels
.
last
val
inv
=
lastlabels
(
2
)
val
emptyinv
=
inv
.
assumeEmpty
(
List
(
"informed"
,
"Read"
,
"Comm"
)).
simplify
()
logger
.
info
(
s
"empty: ${emptyinv.pretty
()
}"
)
logger
.
info
(
s
"empty: ${emptyinv.pretty}"
)
// val auxes = List("O", "choice2")
// Different Os
...
...
@@ -59,15 +59,15 @@ object InvariantInspector extends App with LazyLogging {
FOTransformers
.
eliminateAuxiliaryPredicate
(
inv
,
p
)
)
val
simped
=
auxless
.
toCNF
.
simplify
()
logger
.
info
(
s
"auxless: ${simped.pretty
()
}"
)
logger
.
info
(
s
"auxless: ${simped.pretty}"
)
logger
.
info
(
"Computing with B now"
)
val
withB
=
simped
everywhere
{
case
Fun
(
"Assign"
,
t
,
vars
)
=>
And
(
Fun
(
"Assign"
,
t
,
vars
),
Neg
(
Fun
(
"B"
,
vars
)))
// case Fun("Assign",t,vars) => Fun("B",vars)
}
logger
.
info
(
s
"withB: ${withB.simplify().pretty
()
}"
)
logger
.
info
(
s
"withB CNF: ${withB.toCNF.simplify().pretty
()
}"
)
logger
.
info
(
s
"withB: ${withB.simplify().pretty}"
)
logger
.
info
(
s
"withB CNF: ${withB.toCNF.simplify().pretty}"
)
logger
.
info
(
s
"Graph: $graph"
)
logger
.
info
(
s
"Final Invariants:\n${afterlabels.last}"
)
...
...
src/main/scala/de/tum/workflows/MainInvariantsInference.scala
View file @
12106957
...
...
@@ -64,7 +64,7 @@ object MainInvariantsInference extends App with LazyLogging {
}
logger
.
info
(
s
"Model Facts: ${facts}"
)
val
vars
=
z3model
.
flatMap
{
case
(
f
:
Fun
,
b
:
Formula
)
=>
f
.
freeVars
()
}.
distinct
val
vars
=
z3model
.
flatMap
{
case
(
f
:
Fun
,
b
:
Formula
)
=>
f
.
freeVars
}.
distinct
val
groupedvars
=
vars
.
groupBy
{
_
.
typ
}
// These should only contain Choice and Oracle predicates
...
...
src/main/scala/de/tum/workflows/MainLTL.scala
View file @
12106957
...
...
@@ -21,8 +21,8 @@ object MainLTL extends App with LazyLogging {
var
metrics
=
List
[
String
]()
write
(
name
,
s
"$name.foltl"
,
prop
.
pretty
()
)
metrics
:+=
s
"$name.foltl: ${prop.opsize
()
}"
write
(
name
,
s
"$name.foltl"
,
prop
.
pretty
)
metrics
:+=
s
"$name.foltl: ${prop.opsize}"
if
(!
FormulaFunctions
.
checkSanity
(
prop
))
{
logger
.
error
(
"Property didn't pass sanity check"
)
...
...
@@ -42,11 +42,11 @@ object MainLTL extends App with LazyLogging {
val
quantfree
=
FOTransformers
.
eliminateUniversals
(
res
,
agents
)
val
ltlprop
=
FOTransformers
.
eliminatePredicates
(
quantfree
)
metrics
:+=
s
"$name.ltl: ${ltlprop.opsize
()
}"
metrics
:+=
s
"$name.ltl: ${ltlprop.opsize}"
metrics
:+=
s
"Universe: $universe"
write
(
name
,
s
"$name.ltl"
,
ltlprop
.
toString
())
write
(
name
,
s
"$name.ppltl"
,
ltlprop
.
pretty
()
)
write
(
name
,
s
"$name.ppltl"
,
ltlprop
.
pretty
)
val
owlform
=
OwlTransformer
.
toOwl
(
ltlprop
)
...
...
src/main/scala/de/tum/workflows/Preconditions.scala
View file @
12106957
...
...
@@ -98,7 +98,7 @@ object Preconditions extends LazyLogging {
val
guard
=
And
(
s
.
guard
,
con
).
simplify
()
// val guard = True
val
frees
=
guard
.
freeVars
()
--
s
.
tuple
.
toSet
val
frees
=
guard
.
freeVars
--
s
.
tuple
.
toSet
val
form
=
s
match
{
case
Add
(
_
,
_
,
_
)
=>
{
...
...
src/main/scala/de/tum/workflows/Utils.scala
View file @
12106957
...
...
@@ -85,13 +85,13 @@ object Utils extends LazyLogging {
Utils
.
write
(
name
,
s
"${filenames}_elaborated.dot"
,
elabdot
)
val
labels
=
(
for
((
node
,
inv
)
<-
labelling
.
last
)
yield
{
s
"Node ${node}:\n${inv.pretty
()
}\n"
s
"Node ${node}:\n${inv.pretty}\n"
}).
mkString
(
"\n"
)
Utils
.
write
(
name
,
s
"$filenames.invariants"
,
labels
)
val
wfsize
=
graph
.
edges
.
size
-
1
val
invsizes
=
labelling
.
last
.
map
(
_
.
_2
.
opsize
()
)
val
invsizes
=
labelling
.
last
.
map
(
_
.
_2
.
opsize
)
val
maxsize
=
invsizes
.
max
val
avgsize
=
invsizes
.
sum
/
invsizes
.
size
Utils
.
write
(
name
,
s
"$filenames.metrics"
,
...
...
src/main/scala/de/tum/workflows/WorkflowParser.scala
View file @
12106957
...
...
@@ -109,7 +109,7 @@ object WorkflowParser extends RegexParsers with LazyLogging {
// all variable names contained in bound
val
names
=
bound
.
map
(
_
.
name
)
val
unbound
=
stmts
.
flatMap
(
_
.
freeVars
()
).
filterNot
(
v
=>
names
.
contains
(
v
.
name
))
val
unbound
=
stmts
.
flatMap
(
_
.
freeVars
).
filterNot
(
v
=>
names
.
contains
(
v
.
name
))
if
(
unbound
.
nonEmpty
)
{
logger
.
error
(
s
"Variables $unbound appear unbound."
)
}
...
...
src/main/scala/de/tum/workflows/blocks/Workflow.scala
View file @
12106957
...
...
@@ -33,7 +33,7 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
val
ta
=
target
.
params
.
head
// check declass bindings
for
((
o
,
(
f
,
t
))
<-
declass
if
!
t
.
freeVars
()
.
forall
(
v
=>
(
f
.
contains
(
v
)
||
(
v
==
ta
))))
{
for
((
o
,
(
f
,
t
))
<-
declass
if
!
t
.
freeVars
.
forall
(
v
=>
(
f
.
contains
(
v
)
||
(
v
==
ta
))))
{
logger
.
error
(
s
"Not all variables of the declassification condition for $o bound by the oracle"
)
sane
=
false
}
...
...
@@ -117,7 +117,7 @@ abstract class Statement {
def
fun
:
String
def
tuple
:
List
[
Var
]
def
freeVars
()
=
guard
.
freeVars
()
++
tuple
lazy
val
freeVars
=
guard
.
freeVars
++
tuple
}
case
class
Add
(
guard
:
Formula
,
fun
:
String
,
tuple
:
List
[
Var
])
extends
Statement
{
...
...
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
View file @
12106957
...
...
@@ -8,7 +8,10 @@ import scala.annotation.tailrec
object
FOLTL
{
abstract
class
Formula
{
def
simplify
()
:
Formula
=
FormulaFunctions
.
simplify
(
this
)
def
freeVars
()
:
Set
[
Var
]
=
FormulaFunctions
.
freeVars
(
this
)
lazy
val
freeVars
:
Set
[
Var
]
=
FormulaFunctions
.
freeVars
(
this
)
lazy
val
opsize
:
Int
=
FormulaFunctions
.
opsize
(
this
)
def
everywhere
(
trans
:
PartialFunction
[
Formula
,
Formula
])
:
Formula
=
FormulaFunctions
.
everywhere
(
trans
,
this
)
def
assumeEmpty
(
name
:
String
)
:
Formula
=
FormulaFunctions
.
assumeEmpty
(
this
,
name
)
def
assumeEmpty
(
names
:
List
[
String
])
:
Formula
=
FormulaFunctions
.
assumeAllEmpty
(
this
,
names
)
...
...
@@ -16,18 +19,18 @@ object FOLTL {
def
in
(
name
:
String
,
ignore
:
Set
[
String
])
:
Formula
=
FormulaFunctions
.
annotate
(
this
,
name
,
ignore
)
def
collect
[
T
](
coll
:
PartialFunction
[
Formula
,
List
[
T
]])
:
List
[
T
]
=
FormulaFunctions
.
collect
(
coll
,
this
)
def
hasSubFormula
(
coll
:
PartialFunction
[
Formula
,
Boolean
])
:
Boolean
=
FormulaFunctions
.
hasSubFormula
(
coll
,
this
)
def
opsize
()
:
Int
=
FormulaFunctions
.
opsize
(
this
)
def
toPrenex
:
Formula
=
FormulaFunctions
.
toPrenex
(
this
)
def
toNegNf
:
Formula
=
FormulaFunctions
.
toNegNf
(
this
)
def
toCNF
:
Formula
=
FormulaFunctions
.
toCNF
(
this
)
def
isBS
:
Boolean
=
FormulaFunctions
.
isBS
(
this
)
def
isQFree
:
Boolean
=
FormulaFunctions
.
isQFree
(
this
)
lazy
val
isBS
:
Boolean
=
FormulaFunctions
.
isBS
(
this
)
lazy
val
isQFree
:
Boolean
=
FormulaFunctions
.
isQFree
(
this
)
def
removeOTQuantifiers
()
:
Formula
=
FormulaFunctions
.
removeOTQuantifiers
(
this
)
def
parallelRename
(
vars
:
List
[
Var
],
newvars
:
List
[
Var
])
:
Formula
=
FormulaFunctions
.
parallelRename
(
this
,
vars
,
newvars
)
def
bracketed
()
:
String
=
this
match
{
lazy
val
bracketed
:
String
=
this
match
{
case
_:
BinOp
=>
"("
+
this
+
")"
case
_
=>
this
.
toString
()
}
...
...
@@ -37,7 +40,7 @@ object FOLTL {
def
∨
(
f2
:
Formula
)
=
Or
(
this
,
f2
)
// TODO: better line breaking
def
pretty
()
:
String
=
{
lazy
val
pretty
:
String
=
{
val
remeq
=
this
.
everywhere
{
case
Eq
(
t1
,
t2
)
if
FormulaFunctions
.
annotateOverwrite
(
t1
,
Properties
.
T1
,
Properties
.
T2
)
==
t2
=>
Eq
(
t1
,
Fun
(
"eq"
,
List
()))
...
...
@@ -119,7 +122,7 @@ object FOLTL {
override
def
toString
()
=
{
// show types only in quantifiers
qname
+
" "
+
vars
.
map
(
_
.
withType
()).
mkString
(
","
)
+
". "
+
t
.
bracketed
()
qname
+
" "
+
vars
.
map
(
_
.
withType
()).
mkString
(
","
)
+
". "
+
t
.
bracketed
}
}
...
...
@@ -154,7 +157,7 @@ object FOLTL {
val
qname
=
"∀"
val
make
=
ForallOtherThan
.
apply
(
_:
List
[
Var
],
otherthan
,
_:
Formula
)
override
def
toString
()
=
{
s
"$qname ${vars.map(_.withType()).mkString("
,
")} ∉ {${otherthan.map(_.withType()).mkString("
,
")}}. ${t.bracketed
()
}"
s
"$qname ${vars.map(_.withType()).mkString("
,
")} ∉ {${otherthan.map(_.withType()).mkString("
,
")}}. ${t.bracketed}"
}
}
...
...
@@ -188,7 +191,7 @@ object FOLTL {
def
opname
:
String
def
t
:
Formula
override
def
toString
()
=
opname
+
" "
+
t
.
bracketed
()
override
def
toString
()
=
opname
+
" "
+
t
.
bracketed
}
object
UnOp
{
...
...
@@ -206,9 +209,9 @@ object FOLTL {
override
def
toString
()
=
{
(
t1
,
t2
)
match
{
case
(
t1
:
BinOp
,
t2
:
BinOp
)
if
(
opname
==
t1
.
opname
&&
opname
==
t2
.
opname
)
=>
t1
+
" "
+
opname
+
" "
+
t2
case
(
t1
:
BinOp
,
_
)
if
(
opname
==
t1
.
opname
)
=>
t1
+
" "
+
opname
+
" "
+
t2
.
bracketed
()
case
(
_
,
t2
:
BinOp
)
if
(
opname
==
t2
.
opname
)
=>
t1
.
bracketed
()
+
" "
+
opname
+
" "
+
t2
case
_
=>
t1
.
bracketed
()
+
" "
+
opname
+
" "
+
t2
.
bracketed
()
case
(
t1
:
BinOp
,
_
)
if
(
opname
==
t1
.
opname
)
=>
t1
+
" "
+
opname
+
" "
+
t2
.
bracketed
case
(
_
,
t2
:
BinOp
)
if
(
opname
==
t2
.
opname
)
=>
t1
.
bracketed
+
" "
+
opname
+
" "
+
t2
case
_
=>
t1
.
bracketed
+
" "
+
opname
+
" "
+
t2
.
bracketed
}
}
}
...
...
src/main/scala/de/tum/workflows/foltl/FOTransformers.scala
View file @
12106957
...
...
@@ -163,7 +163,7 @@ object FOTransformers extends LazyLogging {
val
nf
=
f
.
toNegNf
val
(
agents
,
inner
)
=
FOTransformers
.
eliminateExistentials
(
nf
)
val
existbound
=
Exists
(
agents
,
inner
)
val
constants
=
existbound
.
freeVars
()
val
constants
=
existbound
.
freeVars
FOTransformers
.
eliminateUniversals
(
existbound
,
constants
.
toList
)
}
...
...
src/main/scala/de/tum/workflows/foltl/FormulaFunctions.scala
View file @
12106957
...
...
@@ -123,15 +123,15 @@ object FormulaFunctions extends LazyLogging {
f
everywhere
{
case
Forall
(
vars
,
BinOp
(
make
,
f1
,
f2
))
if
{
val
leftvars
=
f1
.
freeVars
()
val
rightvars
=
f2
.
freeVars
()
val
leftvars
=
f1
.
freeVars
val
rightvars
=
f2
.
freeVars
val
varset
=
vars
.
toSet
val
onlyleft
=
leftvars
.
intersect
(
varset
)
--
rightvars
val
onlyright
=
rightvars
.
intersect
(
varset
)
--
leftvars
!
onlyleft
.
isEmpty
||
!
onlyright
.
isEmpty
}
=>
{
val
leftvars
=
f1
.
freeVars
()
val
rightvars
=
f2
.
freeVars
()
val
leftvars
=
f1
.
freeVars
val
rightvars
=
f2
.
freeVars
val
varset
=
vars
.
toSet
val
bothvars
=
leftvars
.
intersect
(
rightvars
).
intersect
(
varset
)
val
onlyleft
=
leftvars
.
intersect
(
varset
)
--
rightvars
...
...
@@ -221,9 +221,9 @@ object FormulaFunctions extends LazyLogging {
def
opsize
(
t
:
Formula
)
:
Int
=
{
t
match
{
// Extractors
case
Quantifier
(
_
,
ps
,
t
)
=>
1
+
t
.
opsize
()
case
UnOp
(
_
,
t
)
=>
1
+
t
.
opsize
()
case
BinOp
(
_
,
t1
,
t2
)
=>
1
+
t1
.
opsize
()
+
t2
.
opsize
()
case
Quantifier
(
_
,
ps
,
t
)
=>
1
+
t
.
opsize
case
UnOp
(
_
,
t
)
=>
1
+
t
.
opsize
case
BinOp
(
_
,
t1
,
t2
)
=>
1
+
t1
.
opsize
+
t2
.
opsize
case
x
=>
1
}
}
...
...
@@ -307,7 +307,7 @@ object FormulaFunctions extends LazyLogging {
def
checkSanity
(
t
:
Formula
)
=
{
// TODO add more things, f.e. existentials
// T1, T2 can appear freely
val
frees
=
t
.
freeVars
()
--
Set
(
Var
(
Properties
.
T1
),
Var
(
Properties
.
T2
))
val
frees
=
t
.
freeVars
--
Set
(
Var
(
Properties
.
T1
),
Var
(
Properties
.
T2
))
if
(
frees
.
nonEmpty
)
{
logger
.
warn
(
s
"Sanity check failed: $frees appear free in the property."
)
}
...
...
@@ -496,7 +496,7 @@ object FormulaFunctions extends LazyLogging {
// FIXME: can we do it without prenex? may be expensive later on
val
normalized
=
f
.
toNegNf
.
simplify
().
toPrenex
.
simplify
()
logger
.
debug
(
s
"Computing CNF of prenex formula of opsize ${normalized.opsize
()
}"
)
logger
.
debug
(
s
"Computing CNF of prenex formula of opsize ${normalized.opsize}"
)
// normalized is now Quantifiers, then only And/Or with Negation inside
// no simplification here
...
...
src/main/scala/de/tum/workflows/foltl/Properties.scala
View file @
12106957
...
...
@@ -130,7 +130,7 @@ object Properties {
val
cfg
=
sanecfg
(
graph
)
val
sem
=
exec
(
spec
.
w
.
sig
,
graph
)
val
agents
=
spec
.
target
freeVars
()
toList
val
agents
=
spec
.
target
.
freeVars
.
toList
// choice and node predicates are equal in both runs (stubborn)
val
nodes
=
nodepredicates
(
graph
)
map
(
_
.
name
)
...
...
@@ -151,7 +151,7 @@ object Properties {
val
cfg
=
sanecfg
(
graph
)
val
sem
=
exec
(
spec
.
w
.
sig
,
graph
)
val
agents
=
spec
.
target
freeVars
()
toList
val
agents
=
spec
.
target
.
freeVars
.
toList
val
nodes
=
nodepredicates
(
graph
)
map
(
_
.
name
)
val
choices
=
allchoices
(
spec
.
w
)
...
...
src/main/scala/de/tum/workflows/synth/Model.scala
View file @
12106957
...
...
@@ -15,7 +15,7 @@ case class Model(universe: Map[String, List[Var]], steering: Formula, state:Map[
// ignore negated tuples
val
rels
=
for
((
s
,
l
)
<-
state
)
yield
{
s
->
(
for
(
f
<-
l
;
if
f
.
opsize
()
!=
2
)
yield
{
for
(
f
<-
l
;
if
f
.
opsize
!=
2
)
yield
{
f
})
}
...
...
src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala
View file @
12106957
...
...
@@ -113,7 +113,7 @@ object InvariantChecker extends LazyLogging {
val
(
status2
,
solver2
)
=
Z3QFree
.
checkUniversal
(
Implies
(
newinv
,
False
))
if
(
status2
==
Status
.
SATISFIABLE
)
{
// Negation of newinv still sat, newinv does not imply false)
logger
.
info
(
s
"Relabeling ${nextEdge._1}. New size: ${newinv.opsize
()
}. Continuing."
)
logger
.
info
(
s
"Relabeling ${nextEdge._1}. New size: ${newinv.opsize}. Continuing."
)
checkInvariantRec
(
newlabels
::
labellist
,
newproven
::
provenlist
)
}
else
{
logger
.
info
(
s
"New invariant for ${nextEdge._1} not satisfiable. Terminating."
)
...
...
@@ -141,7 +141,7 @@ object InvariantChecker extends LazyLogging {
val
dot1
=
labellings
.
zip
(
proven
).
reverse
val
dot2
=
dot1
.
map
(
tup
=>
Encoding
.
toDot
(
graph
)(
tup
.
_1
.
map
(
t
=>
(
t
.
_1
,
{
// if (t._2.opsize() <= 5000) t._2.pretty() else "TOO BIG"
t
.
_2
.
pretty
()
t
.
_2
.
pretty
})),
tup
.
_2
))
(
result
,
graph
,
labellings
.
reverse
,
proven
.
reverse
,
dot2
,
time
)
...
...
@@ -164,7 +164,7 @@ object InvariantChecker extends LazyLogging {
val
untouched
=
Encoding
.
untouchedMap
(
graph
,
spec
.
w
.
sig
)
val
msg
=
new
StringBuilder
()
msg
++=
s
"Trying to prove safe with invariant:\n\n${inv.pretty
()
}\n\n"
msg
++=
s
"Trying to prove safe with invariant:\n\n${inv.pretty}\n\n"
// Check all edges
val
list
=
for
(
e
<-
graph
.
edges
)
yield
{
...
...
@@ -181,7 +181,7 @@ object InvariantChecker extends LazyLogging {
msg
++=
s
"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
if
(
res
==
Status
.
SATISFIABLE
)
{
msg
++=
"Satisfying model:\n"
msg
++=
Z3
.
printModel
(
solver
.
getModel
()).
lines
.
map
(
" "
+
_
).
mkString
(
"\n"
)
msg
++=
Z3
LTL
.
printModel
(
solver
.
getModel
()).
lines
.
map
(
" "
+
_
).
mkString
(
"\n"
)
}
else
if
(
res
==
Status
.
UNKNOWN
)
{
msg
++=
s
"Z3 result: $res (${solver.getReasonUnknown()})\n"
}
...
...
@@ -196,7 +196,7 @@ object InvariantChecker extends LazyLogging {
val
safe
=
list
.
reduceLeft
(
_
&&
_
)
if
(
safe
)
{
msg
++=
s
"Proven safe.\n"
logger
.
info
(
s
"Workflow ${spec.w}\n proven safe for invariant:\n${inv.pretty
()
}"
)
logger
.
info
(
s
"Workflow ${spec.w}\n proven safe for invariant:\n${inv.pretty}"
)
}
(
safe
,
msg
)
}
...
...
src/main/scala/de/tum/workflows/toz3/Z3BSFO.scala
0 → 100644
View file @
12106957
package
de.tum.workflows.toz3
import
com.microsoft.z3.
{
Expr
,
Sort
}
import
com.typesafe.scalalogging.LazyLogging
import
java.util
import
de.tum.workflows.foltl.
{
FOLTL
,
FOTransformers
,
FormulaFunctions
}
import
de.tum.workflows.foltl.FOLTL._
import
com.microsoft.z3._
import
de.tum.workflows.Utils
import
de.tum.workflows.toz3.Z3QFree.
{
TIMEOUT
,
logger
}
object
Z3BSFO
extends
LazyLogging
{
def
checkAE
(
f
:
Formula
)
=
{
val
(
time
,
res
)
=
Utils
.
time
{
// Set up Z3
val
cfg
=
new
util
.
HashMap
[
String
,
String
]()
cfg
.
put
(
"timeout"
,
TIMEOUT
.
toString
())
val
ctx
=
new
Context
(
cfg
)
val
params
=
ctx
.
mkParams
()
params
.
add
(
"mbqi"
,
true
)
params
.
add
(
"mbqi.trace"
,
true
)
val
s
=
ctx
.
mkSolver
()
s
.
setParameters
(
params
)
val
neg
=
Neg
(
f
).
simplify
()
// Can only check universal things
if
(!
neg
.
isBS
)
{
logger
.
error
(
"Z3-BSFO: Trying to encode formula not in Bernays-Schönfinkel"
)
}
// neg is now in E*A*, so can be solved by bounded instantiation
s
.
add
(
translate
(
neg
,
ctx
))
// Send to z3
val
c
=
s
.
check
()
if
(
c
==
Status
.
UNKNOWN
)
{
logger
.
warn
(
s
"Z3-BSFO: Status unknown - ${s.getReasonUnknown()}"
)
}
// if (c == Status.SATISFIABLE) {
// logger.info(s"Z3 status satisfiable")
// logger.info(s"${s.getModel()}")
// }
(
c
,
s
)
}
// Logging only calls that take longer than a second
if
(
time
>
1000
)
{
logger
.
debug
(
s
"Z3-BSFO call took $time ms"
)
}
res
}
type
VarCtx
=
Map
[
Var
,
(
Option
[
Int
]
,
Expr
,
Sort
)]
var
counter
=
0
// TODO: how to not make this static?
val
fun_ctx
=
new
util
.
HashMap
[
String
,
FuncDecl
]()
def
buildVarCtx
(
ctx
:
Context
,
var_ctx
:
VarCtx
,
vars
:
List
[
Var
])
:
VarCtx
=
{
val
indices
=
(
vars
.
size
-
1
)
to
0
by
-
1
val
newexprs
=
(
for
((
v
,
i
)
<-
vars
.
zip
(
indices
))
yield
{
// count = count - 1;
val
sort
=
if
(
v
.
typ
.
equals
(
"Int"
))
{
ctx
.
getIntSort
()
}
else
if
(
v
.
typ
.
equals
(
"Bool"
))
{
ctx
.
getBoolSort
()
}
else
{
ctx
.
mkUninterpretedSort
(
v
.
typ
)
// TODO: finite domain? sort size?
}
v
->
(
Some
(
i
),
ctx
.
mkBound
(
i
,
sort
),
sort
)
})
toMap
// if the index is defined, increment, otherwise use the expr (which is a constant f.e.)
val
oldvars
=
(
for
((
v
,
(
i
,
e
,
s
))
<-
var_ctx
)
yield
{
if
(
i
.
isDefined
)
{
val
newi
=
i
.
get
+
vars
.
size
val
newbound
=
ctx
.
mkBound
(
newi
,
s
)
v
->
(
Some
(
newi
),
newbound
,
s
)
}
else
{
v
->
(
i
,
e
,
s
)
}
})
newexprs
++
oldvars
}
def
toBoolZ3
(
ctx
:
Context
,
f
:
Formula
,
var_ctx
:
VarCtx
)
:
BoolExpr
=
{
// texpr is an expression e with the form given by the following grammar:
// e ::= 0 | t | succ(e)
// tvar is Some(t) if e contains t or None otherwise
f
match
{
case
Fun
(
name
,
ind
,
params
)
=>
{
val
pi
=
if
(
ind
.
isDefined
)
"_"
+
ind
.
get
else
""
val
indexedname
=
name
+
pi
var
fdecl
=
fun_ctx
.
get
(
indexedname
)
if
(
fdecl
==
null
)
{
val
pi
=
if
(
ind
.
isDefined
)
"_"
+
ind
.
get
else
""
val
sorts
=
params
.
map
(
x
=>
var_ctx
(
x
).
_3
)
fdecl
=
ctx
.
mkFuncDecl
(
indexedname
,
sorts
.
toArray
,
ctx
.
getBoolSort
())
fun_ctx
.
put
(
indexedname
,
fdecl
)
}
// all variables should be quantified, so they should be part of var_ctx
// TODO: support constants/free variables
val
all_args
=
params
.
map
(
x
=>
var_ctx
(
x
).
_2
)
fdecl
.
apply
(
all_args
:
_
*
).
asInstanceOf
[
BoolExpr
]
}
case
Exists
(
vars
,
f1
)
=>
{
val
names
:
Array
[
Symbol
]
=
vars
.
map
(
v
=>
ctx
.
mkSymbol
(
v
.
name
)).
toArray
val
newctx
=
buildVarCtx
(
ctx
,
var_ctx
,
vars
)
val
sorts
=
vars
.
map
(
newctx
(
_
).
_3
).
toArray
val
e1
=
toBoolZ3
(
ctx
,
f1
,
newctx
)
ctx
.
mkExists
(
sorts
,
names
,
e1
,
0
,
null
,
null
,
null
,
null
)
}
case
Forall
(
vars
,
f1
)
=>
{
val
names
:
Array
[
Symbol
]
=
vars
.
map
(
v
=>
ctx
.
mkSymbol
(
v
.
name
)).
toArray
val
newctx
=
buildVarCtx
(
ctx
,
var_ctx
,
vars
)
val
sorts
=
vars
.
map
(
newctx
(
_
).
_3
).
toArray
val
e1
=
toBoolZ3
(
ctx
,
f1
,
newctx
)
ctx
.
mkForall
(
sorts
,
names
,
e1
,
0
,
null
,
null
,
null
,
null
)
}
case
And
(
f1
,
f2
)
=>
{
val
e1
=
toBoolZ3
(
ctx
,
f1
,
var_ctx
)
val
e2
=
toBoolZ3
(
ctx
,
f2
,
var_ctx
)
ctx
.
mkAnd
(
e1
,
e2
)
}
case
Eq
(
f1
,
f2
)
=>
{
val
e1
=
toSortedZ3
(
ctx
,
f1
,
var_ctx
)
val
e2
=
toSortedZ3
(
ctx
,
f2
,
var_ctx
)
ctx
.
mkEq
(
e1
,
e2
)
}
case
Or
(
f1
,
f2
)
=>
{
val
e1
=
toBoolZ3
(
ctx
,
f1
,
var_ctx
)
val
e2
=
toBoolZ3
(
ctx
,
f2
,
var_ctx
)
ctx
.
mkOr
(
e1
,
e2
)
}
case
Implies
(
f1
,
f2
)
=>
{
val
e1
=
toBoolZ3
(
ctx
,
f1
,
var_ctx
)
val
e2
=
toBoolZ3
(
ctx
,
f2
,
var_ctx
)
ctx
.
mkImplies
(
e1
,
e2
)
}
case
Neg
(
f1
)
=>
{
val
e
=
toBoolZ3
(
ctx
,
f1
,
var_ctx
)
ctx
.
mkNot
(
e
)
}
case
True
=>
{
ctx
.
mkTrue
()
}
case
False
=>
{
ctx
.
mkFalse
()
}
}
}
def
toSortedZ3
(
ctx
:
Context
,
f
:
Formula
,
var_ctx
:
VarCtx
)
:
Expr
=
{
f
match
{
case
v
:
Var
=>
{
var_ctx
(
v
).
_2
}
case
_
=>
{
toBoolZ3
(
ctx
,
f
,
var_ctx
)
}
}
}
def
translate
(
f
:
Formula
,
ctx
:
Context
)
=
{
// logger.info(s"Using formula:\n$f")
if
(
f
.
freeVars
.
nonEmpty
)
{
logger
.
error
(
s
"Cannot check - formula contains free variables ${f.freeVars}"
)
}
fun_ctx
.
clear
()
val
expr
=
toBoolZ3
(
ctx
,
f
,
Map
())
// logger.info(s"Built Z3 expression:\n$expr")
expr
}
def
translate
(
f
:
Formula
,
ctx
:
Context
,
varctx
:
VarCtx
)
=
{
// logger.info(s"Using formula:\n${f.pretty()}")
if
(
f
.
freeVars
.
nonEmpty
)
{
logger
.
error
(
s
"Cannot check - formula contains free variables ${f.freeVars}"
)
}
fun_ctx
.
clear
()
val
expr
=
toBoolZ3
(
ctx
,
f
,
varctx
)
// logger.info(s"Built Z3 expression:\n$expr")
expr
}
//
// def printModel(model: Model) = {
//
// val sb = new StringBuilder()
//
// // val consts = model.getConstDecls()
// //
// // val vals = consts.map(_.apply())
// // val typedvals = vals.groupBy(_.getSort)
// //
// // sb ++= "Universe:\n"
// // for ((k, v) <- typedvals) {
// // sb ++= s"Type $k: ${v.mkString(",")}\n"
// // }
//
// sb ++= "Relations:\n"
// val sortedConsts = model.getConstDecls().sortBy(_.getName.toString())
//
// val (l1, l2) = sortedConsts.partition(s => {
// s.getName.toString() match {
// case FunFromVar(_) => true
// case _ => false
// }
// })
//
// val funs = l1.map(s => {
// val interp = model.getConstInterp(s)
// (FunFromVar.unapply(s.getName.toString).get, interp.toString)
// }) toList
//
// val grouped = funs.groupBy(f => (f._1.name, f._1.ind))