Commit 2109a575 authored by Camil Staps's avatar Camil Staps 🐧

Move Z3 interface for ranking constraints to Cloogle submodule; prioritise StdEnv over Platform

parent 44b5bb3d
Pipeline #16499 passed with stage
in 15 minutes and 27 seconds
Subproject commit 196fee3253b2e55d09fc990b371d2672a7b79134
Subproject commit 9104d2c68f5b070416cfc816bbacb22510727c99
......@@ -327,53 +327,13 @@ computeRankConstraints constraintfile db w
# constraints = fromJSON $ fromString $ fromOk f
| isError f || isNothing constraints = errexit "Could not open rank settings constraints\n" -1 w
# constraints = fromJust constraints
# (constraints,db) = rankConstraints constraints db
# (z3,w) = runProcessIO "z3" ["-in"] Nothing w
| isError z3 = errexit "Failed to run z3\n" -1 w
# (z3h,z3io) = fromOk z3
# z3input = join "\n" (constraints ++ ["(check-sat)","(get-model)","(exit)"]) +++ "\n"
# (err,w) = writePipe z3input z3io.stdIn w
| isError err = errexit "Failed to write constraints to z3\n" -1 w
# (rcode,w) = waitForProcess z3h w
| isError rcode || fromOk rcode <> 0
= errexit
("z3 failed to compute a model with these constraints:\n" +++ z3input)
-1 w
# (out,w) = readPipeBlocking z3io.stdOut w
| isError out = errexit "Failed to read z3 output\n" -1 w
# out = split "\n" $ fromOk out
# settings = findSettings out
{ rs_ngram_distance = 0.0
, rs_exact_result = 0.0
, rs_record_field = 0.0
, rs_constructor = 0.0
, rs_unifier_size = 0.0
, rs_used_synonyms = 0.0
, rs_resolved_context = 0.0
, rs_unresolved_context = 0.0
}
# (settings,db,w) = findRankSettings constraints db w
| isError settings = errexit (fromError settings +++ "\n") -1 w
# settings = fromOk settings
# (io,w) = stdio w
# io = io <<< jsonPrettyPrint (toJSON settings) <<< "\n"
# (_,w) = fclose io w
= w
where
findSettings :: ![String] !RankSettings -> RankSettings
findSettings [s:v:ss] rs
| startsWith " (define-fun " s
# name = s % (14,size s-9) // strip off ' (define-fun ' and ' () Real'
# val = toReal (v % (4,size v-2))
# rs = case name of
"rs_ngram_distance" -> {rs & rs_ngram_distance =val}
"rs_exact_result" -> {rs & rs_exact_result =val}
"rs_record_field" -> {rs & rs_record_field =val}
"rs_constructor" -> {rs & rs_constructor =val}
"rs_unifier_size" -> {rs & rs_unifier_size =val}
"rs_used_synonyms" -> {rs & rs_used_synonyms =val}
"rs_resolved_context" -> {rs & rs_resolved_context =val}
"rs_unresolved_context" -> {rs & rs_unresolved_context=val}
= findSettings ss rs
findSettings [s:ss] rs = findSettings ss rs
findSettings [] rs = rs
:: LogMemory =
{ mem_ip :: IPAddress
......
......@@ -6,4 +6,5 @@
, [{"unify":"(m a) -> a"}, ["LT",["StdList","last"], ["StdGeneric","generic_dict"]]]
, [{"unify":"(m a) -> a"}, ["LT",["StdList","limit"], ["StdGeneric","generic_dict"]]]
, [{"unify":"(m a) -> a"}, ["LT",["StdOrdList","minList"], ["StdList","or"]]]
, [{"unify":"[a] -> a"}, ["LT",["StdList","last"], ["Data.List","head"]]]
]
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment