SVM optimizations #130
SVM optimizations #130
Conversation
mxprshn
commented
Jun 2, 2022
mxprshn
commented
- constraint independence optimization
- condition evaluation on branching to avoid extra solver queries
- SMT solver incrementality mode
VSharp.SILI.Core/State.fs
Outdated
| @@ -141,3 +142,29 @@ and | |||
| IStatedSymbolicConstantSource = | |||
| inherit ISymbolicConstantSource | |||
| abstract Compose : state -> term | |||
|
|
|||
| module public State = | |||
| let makeEmpty modelState = { | |||
There was a problem hiding this comment.
Очень часто встречается State.makeEmpty None. Лучше сделать для этого отдельную функцию.
VSharp.SILI.Core/PathCondition.fs
Outdated
| isFalse <- true | ||
|
|
||
| new() = | ||
| PathCondition(HashSet<term>(), false) |
There was a problem hiding this comment.
Лучше вещи, которые можно уместить в одной строчке, умещать на ней
VSharp.SILI.Core/PathCondition.fs
Outdated
|
|
||
| override this.ToString() = | ||
| if (this :> IPathCondition).IsEmpty then | ||
| "true" |
There was a problem hiding this comment.
Аналогично тут и в других местах
|
|
||
| member this.Map mapper = | ||
| let mapped = PathCondition() :> IPathCondition | ||
| Seq.iter (mapper >> mapped.Add) constraints |
There was a problem hiding this comment.
Возможно, лучше будет сделать конструктор от списка условий
There was a problem hiding this comment.
В плане сделать PathCondition(HashSet(Seq.map mapper constraints), isFalse)? Тогда не произойдет упрощений, которые делаются внутри add (например, если маппер мапит все констрейнты в false, то условие пути не станет простым false)
VSharp.SILI.Core/PathCondition.fs
Outdated
| else | ||
| constantsToAdd | ||
| |> Seq.pairwise | ||
| |> Seq.iteri (fun i (previous, next) -> |
There was a problem hiding this comment.
Лучше вместо больших лямбд определять функции (которые можно определить внутри текущей функции)
VSharp.Solver/Z3.fs
Outdated
| @@ -803,15 +806,19 @@ module internal Z3 = | |||
| match result with | |||
| | Status.SATISFIABLE -> | |||
| let z3Model = optCtx.Model | |||
| let model = builder.MkModel z3Model | |||
| let updatedModel = {q.currentModel with state = {q.currentModel.state with model = q.currentModel.state.model}} | |||
There was a problem hiding this comment.
Значение state лучше вынести в отдельную функцию
There was a problem hiding this comment.
Просто для красоты? Или оно где-то еще используется?
VSharp.Solver/Z3.fs
Outdated
| seq { | ||
| yield! Seq.cast<BoolExpr> encoded.assumptions | ||
| yield encoded.expr :?> BoolExpr | ||
| } |
VSharp.Solver/Z3.fs
Outdated
| let boolConsts = seq { | ||
| for expr in exprs do | ||
| let mutable name = "" | ||
| if (assumptions.TryGetValue(expr, &name)) then |
VSharp.Solver/Z3.fs
Outdated
| yield boolConst | ||
| } | ||
| let names = boolConsts |> Seq.map (fun c -> c.ToString()) | ||
| let amp = " & " |
There was a problem hiding this comment.
Лучше заинлайнить это значение
VSharp.Utils/Stopwatch.fs
Outdated
| { | ||
| commitHash = commitHash | ||
| dateTime = currentDateTime | ||
| caseName = caseName | ||
| tag = tag | ||
| timesCalled = m.timesCalled | ||
| totalTicks = m.stopwatch.ElapsedTicks | ||
| totalMs = m.stopwatch.ElapsedMilliseconds | ||
| testsGenerated = testsGenerated | ||
| } |
There was a problem hiding this comment.
Можно сделать создание этой структуры в отдельной подфункции (определить ее внутри этой)
| member x.StateId | ||
| with get() = stateId | ||
| and set id = | ||
| stateId <- id | ||
|
|
||
| member x.Method with get() = m | ||
| member x.ThisArg |
There was a problem hiding this comment.
для чего обновилась версия зависимости runtime (см. ниже)?
There was a problem hiding this comment.
Упс, это что-то пошло не так
VSharp.Utils/TaggedLogger.fs
Outdated
| @@ -0,0 +1,39 @@ | |||
| namespace VSharp | |||
There was a problem hiding this comment.
зачем разводить много логгеров в проекте? этот вообще сейчас используется?
There was a problem hiding this comment.
Этот использовал, чтобы выводить логи для каждой ветки отдельно (заводил на каждую ветку тег). Наверное, можно его вместе со Stopwatch вынести в какую-нибудь другую ветку
VSharp.Utils/Stopwatch.fs
Outdated
| @@ -0,0 +1,122 @@ | |||
| namespace VSharp | |||
There was a problem hiding this comment.
этот класс точно нужен в мастере? может его вынести в отдельную ветку, а в мастере всё же профилироваться?
There was a problem hiding this comment.
upd (чтобы не забыть): выводить время работы солвера в статистику
VSharp.Test/IntegrationTests.cs
Outdated
| @@ -95,6 +96,8 @@ private class TestSvmCommand : DelegatingTestCommand | |||
| private TestResult Explore(TestExecutionContext context) | |||
| { | |||
| Core.API.ConfigureSolver(SolverPool.mkSolver()); | |||
| Core.API.SetFeatureFlags(new featureFlags(false, false, false)); | |||
There was a problem hiding this comment.
тут тоже выпилить фичу conditionEvaluation (пусть она работает всегда), а constraintIndependence включить по умолчанию.
VSharp.API/SvmOptions.cs
Outdated
| @@ -0,0 +1,24 @@ | |||
| using VSharp.Core; | |||
There was a problem hiding this comment.
этот файл надо смёржить с SILIOptions
VSharp.SILI.Core/API.fs
Outdated
| @@ -6,6 +6,9 @@ open FSharpx.Collections | |||
| open VSharp | |||
|
|
|||
| module API = | |||
| let SetFeatureFlags flags = | |||
There was a problem hiding this comment.
Предлагаю сделать более мелкозернистое управление фичами. Вместо создания FeatureFlags и установки их сюда, предлагаю сделать 1 метод в API -- setConstraintSlicingEnabled. Как писал выше, conditionEvaluation -- выпилить, а incrementality передавать в ConfigureSolver (см. следующий метод).
There was a problem hiding this comment.
Предлагаешь переименовать independence в slicing, или опечатка?
| @@ -0,0 +1,18 @@ | |||
| namespace VSharp.Core | |||
There was a problem hiding this comment.
как писал в API.fs, предлагаю избавиться от этого файла
| /// <summary> | ||
| /// Naive path condition implementation which maintains a single set of constraints | ||
| /// </summary> | ||
| type private PathCondition private (constraints : HashSet<term>, isFalse : bool) = |
There was a problem hiding this comment.
почему этот PathCondition стал мутабельным? форкать состояния будет же дороже теперь...
There was a problem hiding this comment.
Правильно же понимаю, что из-за того, что copy будет очень накладным? А в персистентном множестве будет оставаться общая часть?
| /// Find operation of the union-find structure. Returns not the representative element, but the element before it | ||
| /// (for convenience) | ||
| /// </summary> | ||
| let rec findPrevious constant = |
There was a problem hiding this comment.
почему find не перестраивает структуру данных? если этого не делать, дерево вытягивается в цепочку
| match (nextNode onePrevious), (nextNode anotherPrevious) with | ||
| | Tail(oneRepresentative, oneConstraints), Tail(anotherRepresentative, anotherConstraints) when | ||
| oneRepresentative <> anotherRepresentative -> | ||
| let constraintsUnion = PersistentSet.union oneConstraints anotherConstraints |
There was a problem hiding this comment.
в DSU еще есть эвристика объединения по размеру, чтобы держать дерево более сбалансированным. ее я тоже тут не вижу
There was a problem hiding this comment.
Возникла сложность с тем, что нужны были не только операции union и find, но и операция, которая возвращает одно из независимых подмножеств. Сходу не очень понял, как это можно было бы реализовать эффективно в дереве --- пришлось бы постоянно для каждого элемента искать его root. Из-за этого запилил циклические списки, но с ними как раз проблема, что не добавить эвристики, которые работают с деревьями.
Хотя, с другой стороны, если с эвристиками поиск рута в дереве может занимать константу --- то видимо это не так уж и неэффективно, и какие-то велосипеды изобретать было не нужно
…ndependentWith in struct field source, multiple frames in model
| yield! (Seq.cast<_> assumptions) | ||
| yield query.expr | ||
| } | ||
| |> Seq.distinct |> Array.ofSeq |
There was a problem hiding this comment.
Заметил, что могли возникать повторяющиеся assumptions (в т. ч. в мастере), пофиксил с помощью Seq.distinct
