Move Z3 interface for ranking constraints from cloogle.org to here; add feature for StdEnv

parent 196fee32
definition module Cloogle.Search.Rank
from Clean.Types import :: TypeDef
from Data.Error import :: MaybeError
from Data.Map import :: Map
from Data.Maybe import :: Maybe
......@@ -19,12 +20,16 @@ from Cloogle.DB import :: AnnotationKey, :: CloogleEntry, :: CloogleDB
:: RankSettings =
{ rs_ngram_distance :: !Real //* n-gram distance
, rs_exact_result :: !Real //* results with an exact match
, rs_record_field :: !Real //* record fields
, rs_constructor :: !Real //* constructors
, rs_unifier_size :: !Real //* large unifiers
, rs_used_synonyms :: !Real //* the number of synonyms required
, rs_resolved_context :: !Real //* class contexts with known instances
, rs_unresolved_context :: !Real //* class contexts without known instances
, rs_lib_stdenv :: !Real //* thing comes from StdEnv
}
/**
......@@ -46,7 +51,8 @@ symbolicDistance :: !CloogleEntry !(Map AnnotationKey Int) !(Maybe TypeRankInfo)
:: UniqueResultIdentifier :== (!String, !String)
/**
* Generate Z3 constraints based on a set of constraints on the order of
* results for queries.
* Find suitable ranking settings given a set of constraints. This requires Z3
* to be installed on the system.
*/
rankConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)
findRankSettings :: ![(Request, RankConstraint)] !*CloogleDB !*World
-> *(!MaybeError String RankSettings, *CloogleDB, !*World)
implementation module Cloogle.Search.Rank
import StdArray
import StdBool
import StdInt
import StdList
......@@ -8,12 +9,14 @@ import StdReal
import StdString
import Clean.Types
import Data.Error
from Data.Func import $
import Data.Functor
from Data.List import foldr1
import qualified Data.Map as M
import Data.Maybe
import Data.Tuple
import System.Process
import Text
import Cloogle.API
......@@ -29,18 +32,20 @@ distance settings entry annots tri = let info = symbolicDistance entry annots tr
settings.rs_unifier_size * info.rs_unifier_size +
settings.rs_used_synonyms * info.rs_used_synonyms +
settings.rs_resolved_context * info.rs_resolved_context +
settings.rs_unresolved_context * info.rs_unresolved_context
settings.rs_unresolved_context * info.rs_unresolved_context +
settings.rs_lib_stdenv * info.rs_lib_stdenv
symbolicDistance :: !CloogleEntry !(Map AnnotationKey Int) !(Maybe TypeRankInfo) -> RankInformation
symbolicDistance entry annots tri =
{ rs_ngram_distance = fromMaybe 0.0 $ toReal <$> 'M'.get NGramDistance annots
, rs_exact_result = fromMaybe 0.0 $ toReal <$> 'M'.get ExactResult annots
, rs_record_field = case entry of FunctionEntry {fe_kind=k=:RecordField} -> 1.0; _ -> 0.0
, rs_constructor = case entry of FunctionEntry {fe_kind=k=:Constructor} -> 1.0; _ -> 0.0
, rs_record_field = if entry=:(FunctionEntry {fe_kind=RecordField}) 1.0 0.0
, rs_constructor = if entry=:(FunctionEntry {fe_kind=Constructor}) 1.0 0.0
, rs_unifier_size = fromMaybe 0.0 $ toReal <$> 'M'.get UnifierSize annots
, rs_used_synonyms = case tri of Nothing -> 0.0; Just tri -> toReal $ length tri.tri_used_synonyms
, rs_resolved_context = resolved_context
, rs_unresolved_context = unresolved_context
, rs_lib_stdenv = if (getLocation entry)=:(Just (Location "StdEnv" _ _ _ _ _)) 1.0 0.0
}
where
(resolved_context,unresolved_context) = case tri of
......@@ -60,6 +65,54 @@ match (mod,name) ce = case getLocation ce of
Just (Builtin cename _) -> mod == "_builtin" && name == cename
_ -> abort "error in match of UniqueResultIdentifier\n"
findRankSettings :: ![(Request, RankConstraint)] !*CloogleDB !*World
-> *(!MaybeError String RankSettings, *CloogleDB, !*World)
findRankSettings constraints db w
# (constraints,db) = rankConstraints constraints db
# (z3,w) = runProcessIO "z3" ["-in"] Nothing w
| isError z3 = (Error "Failed to run z3", db, w)
# (z3h,z3io) = fromOk z3
# z3input = join "\n" (constraints ++ ["(check-sat)","(get-model)","(exit)"]) +++ "\n"
# (err,w) = writePipe z3input z3io.stdIn w
| isError err = (Error "Failed to write constraints to z3", db, w)
# (rcode,w) = waitForProcess z3h w
| isError rcode || fromOk rcode <> 0
= (Error ("z3 failed to compute a model with these constraints:\n" +++ z3input), db, w)
# (out,w) = readPipeBlocking z3io.stdOut w
| isError out = (Error "Failed to read z3 output", db, 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
, rs_lib_stdenv = 0.0
}
= (Ok settings, db, 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 {#c \\ c <-: v | isDigit c || c == '.' || c == '-'}
# 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}
"rs_lib_stdenv" -> {rs & rs_lib_stdenv =val}
= findSettings ss rs
findSettings [s:ss] rs = findSettings ss rs
findSettings [] rs = rs
rankConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)
rankConstraints constraints db
# (constraints,db) = findConstraints constraints db
......@@ -74,6 +127,7 @@ where
, "(declare-const rs_used_synonyms Real)"
, "(declare-const rs_resolved_context Real)"
, "(declare-const rs_unresolved_context Real)"
, "(declare-const rs_lib_stdenv Real)"
]
findConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)
......@@ -112,6 +166,7 @@ where
, "* rs_used_synonyms " <+ ri.rs_used_synonyms
, "* rs_resolved_context " <+ ri.rs_resolved_context
, "* rs_unresolved_context " <+ ri.rs_unresolved_context
, "* rs_lib_stdenv " <+ ri.rs_lib_stdenv
]
where
sum :: [String] -> String
......
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