From b98bc50012f3c46177e35e822fdb71a8fcba187d Mon Sep 17 00:00:00 2001 From: Ilya Shpilkov Date: Mon, 22 Jul 2024 19:32:13 +0300 Subject: [PATCH 1/8] Add sat solver results caching --- VSharp.Solver/Cache.fs | 164 +++++++++++++++++++++++++++++ VSharp.Solver/VSharp.Solver.fsproj | 1 + VSharp.Solver/Z3.fs | 86 ++++++++------- 3 files changed, 215 insertions(+), 36 deletions(-) create mode 100644 VSharp.Solver/Cache.fs diff --git a/VSharp.Solver/Cache.fs b/VSharp.Solver/Cache.fs new file mode 100644 index 000000000..37eac7dde --- /dev/null +++ b/VSharp.Solver/Cache.fs @@ -0,0 +1,164 @@ +namespace VSharp.Solver + +open System.Collections.Generic + +open VSharp +open VSharp.Core.SolverInteraction +open VSharp.Core +open VSharp.Prelude + +module Cache = + let transpose (xs: 'a option seq) : 'a seq option = + Seq.fold (fun acc x -> Option.map2 Seq.cons x acc) (Some Seq.empty) xs + + let rec coreParts (core: term) : term list = + match core with + | Conjunction(xs) -> List.collect coreParts xs + | _ -> List.singleton core + + let iteTerms (ite: iteType) : term seq = + seq { + yield! Seq.collect (fun (t1, t2) -> [ t1; t2 ]) ite.branches + yield ite.elseValue + } + + let sliceTerms (h: term) (slice: list) : term seq = + seq { + yield h + yield! Seq.collect (fun (t1, t2, t3) -> [ t1; t2; t3 ]) slice + } + + let dictValuesNotClash (dict: Dictionary<'k, 'v>) : bool = + dict.Count = (dict.Values |> Set |> Set.count) + + let addRenaming (namings: Dictionary<'k, 'v>) (k: 'k) (v: 'v) : bool = + if namings.ContainsKey(k) then + namings[k] = v + else + namings.Add(k, v) + true + + let (|SeqEmpty|SeqCons|) (xs: 'a seq) = + match Seq.tryHead xs with + | Some x -> SeqCons(x, Seq.tail xs) + | None -> SeqEmpty + + let rec tryRenameImpl (namings: Dictionary) (lhs: term) (rhs: term) : bool = + match lhs.term, rhs.term with + | Nop, Nop -> true + | Concrete(o1, _), Concrete(o2, _) when o1.Equals(o2) -> true + | Constant(v1, s1, ty1), Constant(v2, s2, ty2) when s1.Equals(s2) && ty1.Equals(ty2) -> + addRenaming namings v1.v v2.v + | Expression(op1, ts1, ty1), Expression(op2, ts2, ty2) when + op1.Equals(op2) && ty1.Equals(ty2) && List.length ts1 = List.length ts2 + -> + tryRenameSeq namings ts1 ts2 + | Struct(fs1, ty1), Struct(fs2, ty2) when + ty1.Equals(ty2) && Set(PersistentDict.keys fs1) = Set(PersistentDict.keys fs2) + -> + let ts = fs1 |> PersistentDict.toSeq |> Seq.map (fun (k, v) -> (v, fs2[k])) + let ts1 = Seq.map fst ts + let ts2 = Seq.map snd ts + tryRenameSeq namings ts1 ts2 + | HeapRef(addr1, ty1), HeapRef(addr2, ty2) when addr1.Equals(addr2) && ty1.Equals(ty2) -> true + | Ref addr1, Ref addr2 when addr1.Equals(addr2) -> true + | Ptr(base1, ty1, t1), Ptr(base2, ty2, t2) when base1 = base2 && ty1.Equals(ty2) -> tryRenameImpl namings t1 t2 + | Slice(h1, slice1), Slice(h2, slice2) when List.length slice1 = List.length slice2 -> + tryRenameSeq namings (sliceTerms h1 slice1) (sliceTerms h2 slice2) + | Ite ite1, Ite ite2 when List.length ite1.branches = List.length ite2.branches -> + tryRenameSeq namings (iteTerms ite1) (iteTerms ite2) + | _ -> false + + and tryRenameSeq (namings: Dictionary) (lhs: term seq) (rhs: term seq) : bool = + match lhs, rhs with + | SeqCons(x, xs), SeqCons(y, ys) -> tryRenameImpl namings x y && tryRenameSeq namings xs ys + | SeqCons(_), SeqEmpty -> false + | SeqEmpty, SeqCons(_) -> false + | SeqEmpty, SeqEmpty -> true + + let tryRename (namings: Dictionary) (lhs: term) (rhs: term) = + tryRenameImpl namings lhs rhs && dictValuesNotClash namings + + let public findRenaming (lhs: term) (rhs: term) : Map option = + let namings = Dictionary() + + if tryRename namings lhs rhs then + namings |> Seq.map (fun (KeyValue(k, v)) -> (k, v)) |> Map |> Some + else + None + + let (=~=) (lhs: term) (rhs: term) = + lhs.GetHashCode() = rhs.GetHashCode() + && tryRename (Dictionary()) lhs rhs + + let bigAnd (xs: term seq) : term = + match xs with + | SeqCons(x, xs) -> + Seq.fold (fun acc x -> Expression (Operator OperationType.LogicalAnd) [ acc; x ] typeof) x xs + | SeqEmpty -> failwith "cannot construct `and` from empty expression" + + let isSubset (core: term array) (q: term list) : bool = + core + |> Array.map (fun part -> List.tryFind ((=~=) part) q) + |> transpose + |> Option.map List.ofSeq + |> Option.filter (fun candidates -> bigAnd core =~= bigAnd candidates) + |> Option.isSome + + [] + type alphaTerm = + { inner: term } + + static member from(t: term) : alphaTerm = { inner = t } + + override self.Equals(o: obj) = + match o with + | :? alphaTerm as other -> self.inner =~= other.inner + | _ -> false + + override self.GetHashCode() = self.inner.GetHashCode() + + [] + type unsatCore = + { all: alphaTerm + parts: term array } + + static member fromParts(parts: term array) : unsatCore = + { all = alphaTerm.from (bigAnd parts) + parts = parts } + + static member size(core: unsatCore) : int = core.parts.Length + + override self.Equals(o: obj) = + match o with + | :? unsatCore as other -> self.all = other.all + | _ -> false + + override self.GetHashCode() = self.all.GetHashCode() + + let smtResults: Dictionary = Dictionary() + let unsatCores: HashSet = HashSet() + + // ======================= Public API ======================= + + let public update (q: term) (outcome: smtResult) : unit = + match outcome with + // TODO: Decoding of bool expression can fail, so current workaround is to return empty core + | SmtUnsat { core = core } when not (Array.isEmpty core) -> unsatCores.Add(unsatCore.fromParts core) |> ignore + | _ -> () + + smtResults.TryAdd(alphaTerm.from q, outcome) |> ignore + + // TODO: probably should substitute constants's names + let public lookup (q: term) : smtResult option = + let aq = { inner = q } + + if smtResults.ContainsKey(aq) then + Some smtResults[aq] + else + let qParts = coreParts q + + unsatCores + |> Seq.filter (fun core -> unsatCore.size core < List.length qParts) + |> Seq.tryFind (fun core -> isSubset core.parts qParts) + |> Option.map (fun core -> SmtUnsat { core = core.parts }) diff --git a/VSharp.Solver/VSharp.Solver.fsproj b/VSharp.Solver/VSharp.Solver.fsproj index 0dff8a882..efda382f3 100644 --- a/VSharp.Solver/VSharp.Solver.fsproj +++ b/VSharp.Solver/VSharp.Solver.fsproj @@ -17,6 +17,7 @@ + diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 35a4385ee..736994fa4 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -1505,44 +1505,58 @@ module internal Z3 = solver.Parameters <- parameters | None -> () - interface ISolver with - member x.CheckSat (q : term) : smtResult = - Logger.printLog Logger.Trace "SOLVER: trying to solve constraints..." - Logger.printLogLazy Logger.Trace "%s" (lazy q.ToString()) + let safeUnsatCore () : term array = + try + solver.UnsatCore |> Array.map (builder.Decode typeof) + with + | _ -> Array.empty + + let checkSatImpl (q : term) : smtResult = + Logger.printLog Logger.Trace "SOLVER: trying to solve constraints..." + Logger.printLogLazy Logger.Trace "%s" (lazy q.ToString()) + try try - try - let query = builder.EncodeTerm q - let assumptions = query.assumptions - let assumptions = - seq { - yield! (Seq.cast<_> assumptions) - yield query.expr - } |> Array.ofSeq - - let result = solver.Check assumptions - match result with - | Status.SATISFIABLE -> - Logger.trace "SATISFIABLE" - let z3Model = solver.Model - let model = builder.MkModel z3Model - SmtSat { mdl = model } - | Status.UNSATISFIABLE -> - Logger.trace "UNSATISFIABLE" - SmtUnsat { core = Array.empty (*optCtx.UnsatCore |> Array.map (builder.Decode Bool)*) } - | Status.UNKNOWN -> - Logger.error $"Solver returned Status.UNKNOWN. Reason: {solver.ReasonUnknown}\n\ - Expression: {assumptions |> Seq.map (fun a -> a.ToString()) |> Seq.toList}" - - Logger.trace "UNKNOWN" - SmtUnknown solver.ReasonUnknown - | _ -> __unreachable__() - with - | :? EncodingException as e -> - Logger.printLog Logger.Info "SOLVER: exception was thrown: %s" e.Message - SmtUnknown (sprintf "Z3 has thrown an exception: %s" e.Message) - finally - builder.Reset() + let query = builder.EncodeTerm q + let assumptions = query.assumptions + let assumptions = + seq { + yield! (Seq.cast<_> assumptions) + yield query.expr + } |> Array.ofSeq + + let result = solver.Check assumptions + match result with + | Status.SATISFIABLE -> + Logger.trace "SATISFIABLE" + let z3Model = solver.Model + let model = builder.MkModel z3Model + SmtSat { mdl = model } + | Status.UNSATISFIABLE -> + Logger.trace "UNSATISFIABLE" + SmtUnsat { core = safeUnsatCore () } + | Status.UNKNOWN -> + Logger.error $"Solver returned Status.UNKNOWN. Reason: {solver.ReasonUnknown}\n\ + Expression: {assumptions |> Seq.map (fun a -> a.ToString()) |> Seq.toList}" + + Logger.trace "UNKNOWN" + SmtUnknown solver.ReasonUnknown + | _ -> __unreachable__() + with + | :? EncodingException as e -> + Logger.printLog Logger.Info "SOLVER: exception was thrown: %s" e.Message + SmtUnknown (sprintf "Z3 has thrown an exception: %s" e.Message) + finally + builder.Reset() + interface ISolver with + member x.CheckSat (q : term) : smtResult = + Cache.lookup q + |> Option.defaultWith (fun () -> + let res = checkSatImpl q + Cache.update q res + res + ) + member x.Assert (fml : term) = Logger.printLogLazy Logger.Trace "SOLVER: Asserting: %s" (lazy fml.ToString()) let encoded = builder.EncodeTerm fml From 2f9b6a131f7f0a39b66d1d330a091a30607f17d5 Mon Sep 17 00:00:00 2001 From: Ilya Shpilkov Date: Thu, 25 Jul 2024 18:28:46 +0300 Subject: [PATCH 2/8] PathCondition: split conjunction into several sepate conditions --- VSharp.SILI.Core/PathCondition.fs | 1 + 1 file changed, 1 insertion(+) diff --git a/VSharp.SILI.Core/PathCondition.fs b/VSharp.SILI.Core/PathCondition.fs index f30f80b5c..dc5871ae7 100644 --- a/VSharp.SILI.Core/PathCondition.fs +++ b/VSharp.SILI.Core/PathCondition.fs @@ -33,6 +33,7 @@ module internal PC = | _ when List.isEmpty xs' -> falsePC() | _ when List.length xs' = List.length xs -> PersistentSet.add pc cond | _ -> add pc (disjunction xs') + | {term = Conjunction xs} -> List.fold add pc xs | _ -> let notCond = !!cond let pc' = pc |> PersistentSet.fold (fun pc e -> From 33a49c8f2d9c15b8e25bd989e7498b2dd337eb55 Mon Sep 17 00:00:00 2001 From: Ilya Shpilkov Date: Thu, 25 Jul 2024 19:02:03 +0300 Subject: [PATCH 3/8] Terms: normalize arguments of binary expressions --- VSharp.SILI.Core/Terms.fs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/VSharp.SILI.Core/Terms.fs b/VSharp.SILI.Core/Terms.fs index 756fe8b27..5cf00e01d 100644 --- a/VSharp.SILI.Core/Terms.fs +++ b/VSharp.SILI.Core/Terms.fs @@ -390,7 +390,13 @@ module internal Terms = let makeBinary operation x y t = assert(Operations.isBinary operation) - Expression (Operator operation) [x; y] t + match operation with + | OperationType.Greater -> Expression (Operator OperationType.Less) [y; x] t + | OperationType.GreaterOrEqual -> Expression (Operator OperationType.LessOrEqual) [y; x] t + | _ when Operations.isCommutative operation -> + let args = if x.GetHashCode() < y.GetHashCode() then [x; y] else [y; x] + Expression (Operator operation) args t + | _ -> Expression (Operator operation) [x; y] t let makeNAry operation x t = match x with From 49375571d92573b413307933eae855a35c217769 Mon Sep 17 00:00:00 2001 From: Ilya Shpilkov Date: Mon, 29 Jul 2024 03:58:26 +0300 Subject: [PATCH 4/8] Cache: change algorithm of cache checking --- VSharp.Solver/Cache.fs | 186 ++++++++++++++++++++++++++++++++--------- 1 file changed, 145 insertions(+), 41 deletions(-) diff --git a/VSharp.Solver/Cache.fs b/VSharp.Solver/Cache.fs index 37eac7dde..58b411a6c 100644 --- a/VSharp.Solver/Cache.fs +++ b/VSharp.Solver/Cache.fs @@ -8,8 +8,16 @@ open VSharp.Core open VSharp.Prelude module Cache = - let transpose (xs: 'a option seq) : 'a seq option = - Seq.fold (fun acc x -> Option.map2 Seq.cons x acc) (Some Seq.empty) xs + let (|SeqEmpty|SeqCons|) (xs: 'a seq) = + match Seq.tryHead xs with + | Some x -> SeqCons(x, Seq.tail xs) + | None -> SeqEmpty + + let rec transpose (xs: 'a option seq) : 'a seq option = + match xs with + | SeqCons(Some x, xs) -> transpose xs |> Option.map (Seq.cons x) + | SeqCons(None, _) -> None + | SeqEmpty -> Some Seq.empty let rec coreParts (core: term) : term list = match core with @@ -38,16 +46,24 @@ module Cache = namings.Add(k, v) true - let (|SeqEmpty|SeqCons|) (xs: 'a seq) = - match Seq.tryHead xs with - | Some x -> SeqCons(x, Seq.tail xs) - | None -> SeqEmpty + let rec isSourcePure (src: ISymbolicConstantSource) : bool = + match src with + | StackReading _ -> true + | GetHashCodeSource _ -> true + | :? functionResultConstantSource -> true + | StructFieldSource(src, _) -> isSourcePure src + | HeapAddressSource src -> isSourcePure src + | PointerOffsetSource src -> isSourcePure src + | PointerAddressSource src -> isSourcePure src + | _ -> false let rec tryRenameImpl (namings: Dictionary) (lhs: term) (rhs: term) : bool = match lhs.term, rhs.term with | Nop, Nop -> true | Concrete(o1, _), Concrete(o2, _) when o1.Equals(o2) -> true - | Constant(v1, s1, ty1), Constant(v2, s2, ty2) when s1.Equals(s2) && ty1.Equals(ty2) -> + | Constant(v1, s1, ty1), Constant(v2, s2, ty2) when + (isSourcePure s1 && isSourcePure s2) || (s1.Equals(s2) && ty1.Equals(ty2)) + -> addRenaming namings v1.v v2.v | Expression(op1, ts1, ty1), Expression(op2, ts2, ty2) when op1.Equals(op2) && ty1.Equals(ty2) && List.length ts1 = List.length ts2 @@ -87,36 +103,50 @@ module Cache = else None - let (=~=) (lhs: term) (rhs: term) = - lhs.GetHashCode() = rhs.GetHashCode() - && tryRename (Dictionary()) lhs rhs + let rec alphaHashCode (t: term) : int = + match t.term with + | Constant(_, src, t) when isSourcePure src -> t.GetHashCode() + | Expression(op, args, ty) -> + [ op.GetHashCode() + (List.map alphaHashCode args).GetHashCode() + ty.GetHashCode() ] + .GetHashCode() + | Struct(fields, t) -> + (fields + |> PersistentDict.toSeq + |> Seq.map (fun (id, field) -> [ id.GetHashCode(); alphaHashCode field ].GetHashCode()) + |> Seq.cons (t.GetHashCode()) + |> Seq.toList) + .GetHashCode() + | Ptr(b, ty, t) -> [ b.GetHashCode(); ty.GetHashCode(); alphaHashCode t ].GetHashCode() + | Slice(h, vals) -> (sliceTerms h vals |> Seq.map alphaHashCode |> Seq.toList).GetHashCode() + | Ite(ite) -> (iteTerms ite |> Seq.map alphaHashCode |> Seq.toList).GetHashCode() + // TODO: probably branch for address is needed + | _ -> t.GetHashCode() - let bigAnd (xs: term seq) : term = - match xs with - | SeqCons(x, xs) -> - Seq.fold (fun acc x -> Expression (Operator OperationType.LogicalAnd) [ acc; x ] typeof) x xs - | SeqEmpty -> failwith "cannot construct `and` from empty expression" - let isSubset (core: term array) (q: term list) : bool = - core - |> Array.map (fun part -> List.tryFind ((=~=) part) q) - |> transpose - |> Option.map List.ofSeq - |> Option.filter (fun candidates -> bigAnd core =~= bigAnd candidates) - |> Option.isSome + let (=~=) (lhs: term) (rhs: term) = + tryRename (Dictionary()) lhs rhs [] type alphaTerm = - { inner: term } + { value: term + hc: int } - static member from(t: term) : alphaTerm = { inner = t } + static member from(t: term) : alphaTerm = { value = t; hc = alphaHashCode t } override self.Equals(o: obj) = match o with - | :? alphaTerm as other -> self.inner =~= other.inner + | :? alphaTerm as other -> self.hc = other.hc && self.value =~= other.value | _ -> false - override self.GetHashCode() = self.inner.GetHashCode() + override self.GetHashCode() = self.hc + + let bigAnd (xs: term seq) : term = + match xs with + | SeqCons(x, xs) -> + Seq.fold (fun acc x -> Expression (Operator OperationType.LogicalAnd) [ acc; x ] typeof) x xs + | SeqEmpty -> failwith "cannot construct `and` from empty expression" [] type unsatCore = @@ -136,29 +166,103 @@ module Cache = override self.GetHashCode() = self.all.GetHashCode() - let smtResults: Dictionary = Dictionary() - let unsatCores: HashSet = HashSet() + let isSubset (core: unsatCore) (q: alphaTerm list) : bool = + core.parts + |> Array.map alphaTerm.from + |> Array.map (fun part -> List.tryFind ((=) part) q) + |> transpose + |> Option.map List.ofSeq + |> Option.filter (fun candidates -> + core.all = alphaTerm.from (candidates |> Seq.map (fun t -> t.value) |> bigAnd)) + |> Option.isSome + + [] + type partEntry = { core: int; idxInCore: int } + + let unsatCores: List = List() + let partsMapping: Dictionary> = Dictionary() // ======================= Public API ======================= let public update (q: term) (outcome: smtResult) : unit = match outcome with // TODO: Decoding of bool expression can fail, so current workaround is to return empty core - | SmtUnsat { core = core } when not (Array.isEmpty core) -> unsatCores.Add(unsatCore.fromParts core) |> ignore + | SmtUnsat { core = core } when not (Array.isEmpty core) -> + let core = unsatCore.fromParts core + let idx = unsatCores.Count + unsatCores.Add(core) + + for i, part in Seq.indexed core.parts do + let part = alphaTerm.from part + let entry = { core = idx; idxInCore = i } + + if partsMapping.ContainsKey(part) then + partsMapping[part].Add(entry) + else + partsMapping.Add(part, List [ entry ]) + + () | _ -> () - smtResults.TryAdd(alphaTerm.from q, outcome) |> ignore + let rec foreach (f: 'a -> 'b option) (seq: 'a seq) : 'b option = + match seq with + | SeqCons(x, xs) -> + match f x with + | Some x -> Some x + | None -> foreach f xs + | SeqEmpty -> None + + [] + type coreMatch = { partInCore: int; partInQuery: int } // TODO: probably should substitute constants's names let public lookup (q: term) : smtResult option = - let aq = { inner = q } - - if smtResults.ContainsKey(aq) then - Some smtResults[aq] - else - let qParts = coreParts q - - unsatCores - |> Seq.filter (fun core -> unsatCore.size core < List.length qParts) - |> Seq.tryFind (fun core -> isSubset core.parts qParts) - |> Option.map (fun core -> SmtUnsat { core = core.parts }) + let qParts = q |> coreParts |> List.map alphaTerm.from |> Array.ofList + let coreToEntriesInQuery: Dictionary> = Dictionary() + + let candidate = + qParts + |> Seq.indexed + |> foreach (fun (i, part) -> + let entries = + if partsMapping.ContainsKey(part) then + partsMapping[part] + else + List() + + entries + |> foreach (fun entry -> + let coreIdx = entry.core + + let coreEntry = + { partInCore = entry.idxInCore + partInQuery = i } + + if coreToEntriesInQuery.ContainsKey(coreIdx) then + coreToEntriesInQuery[coreIdx].Add(coreEntry) + else + coreToEntriesInQuery.Add(coreIdx, List [ coreEntry ]) + + Some coreIdx + |> Option.filter (fun idx -> coreToEntriesInQuery[idx].Count = unsatCores[idx].parts.Length) + |> Option.map (fun idx -> + let coreEntries = coreToEntriesInQuery[idx] + + let subQuery = + coreEntries + |> Seq.map (fun entry -> Array.get qParts entry.partInQuery) + |> Seq.map (fun t -> t.value) + |> bigAnd + + let core = unsatCores[idx] + + let core = + coreEntries + |> Seq.map (fun entry -> Array.get core.parts entry.partInCore) + |> bigAnd + + (subQuery, core)) + |> Option.filter (fun (subQuery, core) -> alphaTerm.from subQuery = alphaTerm.from core) + |> Option.map (fun _ -> unsatCores[coreIdx]))) + + candidate |> Option.map (fun core -> SmtUnsat { core = core.parts }) From e907707d885a766baa09afd4d465d399848f3d1a Mon Sep 17 00:00:00 2001 From: Ilya Shpilkov Date: Mon, 29 Jul 2024 04:00:38 +0300 Subject: [PATCH 5/8] Z3: split all top level conjuction in assumptions --- VSharp.Solver/Z3.fs | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 736994fa4..abdbfaf20 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -1516,13 +1516,14 @@ module internal Z3 = Logger.printLogLazy Logger.Trace "%s" (lazy q.ToString()) try try - let query = builder.EncodeTerm q - let assumptions = query.assumptions let assumptions = - seq { - yield! (Seq.cast<_> assumptions) - yield query.expr - } |> Array.ofSeq + Cache.coreParts q + |> Seq.map builder.EncodeTerm + |> Seq.collect (fun encoding -> seq { + yield! (Seq.cast<_> encoding.assumptions) + yield encoding.expr + }) + |> Seq.toArray let result = solver.Check assumptions match result with From 92e0d9a165c14abd4c5309f502954c5640315f62 Mon Sep 17 00:00:00 2001 From: Ilya Shpilkov Date: Mon, 29 Jul 2024 04:12:09 +0300 Subject: [PATCH 6/8] Cache: simplify check for candidate core --- VSharp.Solver/Cache.fs | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/VSharp.Solver/Cache.fs b/VSharp.Solver/Cache.fs index 58b411a6c..68ea3c25a 100644 --- a/VSharp.Solver/Cache.fs +++ b/VSharp.Solver/Cache.fs @@ -246,23 +246,15 @@ module Cache = Some coreIdx |> Option.filter (fun idx -> coreToEntriesInQuery[idx].Count = unsatCores[idx].parts.Length) |> Option.map (fun idx -> - let coreEntries = coreToEntriesInQuery[idx] - let subQuery = - coreEntries + coreToEntriesInQuery[idx] + |> Seq.sortBy (fun entry -> entry.partInCore) |> Seq.map (fun entry -> Array.get qParts entry.partInQuery) |> Seq.map (fun t -> t.value) |> bigAnd - let core = unsatCores[idx] - - let core = - coreEntries - |> Seq.map (fun entry -> Array.get core.parts entry.partInCore) - |> bigAnd - - (subQuery, core)) - |> Option.filter (fun (subQuery, core) -> alphaTerm.from subQuery = alphaTerm.from core) + (subQuery, unsatCores[idx])) + |> Option.filter (fun (subQuery, core) -> alphaTerm.from subQuery = core.all) |> Option.map (fun _ -> unsatCores[coreIdx]))) candidate |> Option.map (fun core -> SmtUnsat { core = core.parts }) From cd95a1d7726a1d395b96988c6dd5ccab349cdc74 Mon Sep 17 00:00:00 2001 From: Ilya Shpilkov Date: Mon, 29 Jul 2024 18:44:42 +0300 Subject: [PATCH 7/8] Add bench for smt solver --- VSharp.Test/Tests/SmtBenchmark.cs | 53 +++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 VSharp.Test/Tests/SmtBenchmark.cs diff --git a/VSharp.Test/Tests/SmtBenchmark.cs b/VSharp.Test/Tests/SmtBenchmark.cs new file mode 100644 index 000000000..ac736ab0f --- /dev/null +++ b/VSharp.Test/Tests/SmtBenchmark.cs @@ -0,0 +1,53 @@ +using NUnit.Framework; +using VSharp.Test; + +namespace IntegrationTests +{ + [TestSvmFixture] + public sealed class SmtBenchmark + { + [TestSvm] + public static int[] PrefixFunction(string s) + { + if (s.Length > 10) + { + return new int[0]; + } + + int[] p = new int[s.Length]; + p[0] = 0; + + for (int i = 1; i < s.Length; i++) + { + int k = p[i - 1]; + + while (k > 0 && s[i] != s[k]) + k = p[k - 1]; + + if (s[i] == s[k]) + k++; + + p[i] = k; + } + + return p; + } + + [TestSvm] + public static bool ContainsSubstring(string source, string pattern) + { + string text = $"{source}#{pattern}"; + int[] p = PrefixFunction(text); + + for (int i = source.Length; i < p.Length; i++) + { + if (p[i] == pattern.Length) + { + return true; + } + } + + return false; + } + } +} \ No newline at end of file From 3c338c94db020b78bc7735b9408c98991fc6b416 Mon Sep 17 00:00:00 2001 From: Ilya Shpilkov Date: Tue, 30 Jul 2024 19:41:24 +0300 Subject: [PATCH 8/8] Terms: doesn't swap terms with equal hash in binary --- VSharp.SILI.Core/Terms.fs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/VSharp.SILI.Core/Terms.fs b/VSharp.SILI.Core/Terms.fs index 5cf00e01d..37037cf1b 100644 --- a/VSharp.SILI.Core/Terms.fs +++ b/VSharp.SILI.Core/Terms.fs @@ -394,7 +394,7 @@ module internal Terms = | OperationType.Greater -> Expression (Operator OperationType.Less) [y; x] t | OperationType.GreaterOrEqual -> Expression (Operator OperationType.LessOrEqual) [y; x] t | _ when Operations.isCommutative operation -> - let args = if x.GetHashCode() < y.GetHashCode() then [x; y] else [y; x] + let args = if x.GetHashCode() <= y.GetHashCode() then [x; y] else [y; x] Expression (Operator operation) args t | _ -> Expression (Operator operation) [x; y] t