Verified Commit a41eaffb authored by Camil Staps's avatar Camil Staps 🚀

Let Z3 output decimals instead of fractions (easier to parse)

parent d7b379e2
......@@ -34,7 +34,7 @@ from Cloogle.DB import :: Annotation, :: CloogleEntry, :: CloogleDB
*/
:: RankInformation :== RankSettings
distance :: !RankSettings !CloogleEntry ![Annotation] -> Int
distance :: !RankSettings !CloogleEntry ![Annotation] -> Real
symbolicDistance :: !CloogleEntry ![Annotation] -> RankInformation
......
......@@ -24,8 +24,8 @@ import Cloogle.API
import Cloogle.DB
import Cloogle.Search
distance :: !RankSettings !CloogleEntry ![Annotation] -> Int
distance settings entry annots = let info = symbolicDistance entry annots in toInt $
distance :: !RankSettings !CloogleEntry ![Annotation] -> Real
distance settings entry annots = let info = symbolicDistance entry annots in
settings.rs_ngram_distance * info.rs_ngram_distance +
settings.rs_exact_result * info.rs_exact_result +
settings.rs_record_field * info.rs_record_field +
......@@ -109,7 +109,7 @@ findRankSettings constraints cdb w
# (z3,w) = runProcessIO "z3" ["-in"] Nothing w
| isError z3 = (Error "Failed to run z3", cdb, w)
# (z3h,z3io) = fromOk z3
# z3input = join "\n" (constraints ++ ["(check-sat)","(get-model)","(exit)"]) +++ "\n"
# z3input = join "\n" (constraints ++ ["(set-option :pp.decimal true)","(check-sat)","(get-model)","(exit)"]) +++ "\n"
# (err,w) = writePipe z3input z3io.stdIn w
| isError err = (Error "Failed to write constraints to z3", cdb, w)
# (rcode,w) = waitForProcess z3h w
......
Subproject commit 49a6c636f3888f129807cd2b9d1a9cfe53e44bfd
Subproject commit 6379c20283a97f37fb76b44dc7869869f0f32065
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