From faf3201241e29dcd69d4c778cf91542091977022 Mon Sep 17 00:00:00 2001 From: rahulk64 Date: Mon, 31 Jul 2023 12:27:49 -0500 Subject: [PATCH 1/2] Add bvugt and bvsub to SMT Extensions --- .../Smt/Extensions/SmtBitVectorsExtension.cs | 61 ++++++++++++++++++- 1 file changed, 60 insertions(+), 1 deletion(-) diff --git a/Semgus-Lib/Model/Smt/Extensions/SmtBitVectorsExtension.cs b/Semgus-Lib/Model/Smt/Extensions/SmtBitVectorsExtension.cs index 65747d5..8c4b88f 100644 --- a/Semgus-Lib/Model/Smt/Extensions/SmtBitVectorsExtension.cs +++ b/Semgus-Lib/Model/Smt/Extensions/SmtBitVectorsExtension.cs @@ -1,6 +1,6 @@ using Semgus.Model.Smt.Terms; using Semgus.Model.Smt.Theories; - +using System.Collections; using System.Diagnostics.CodeAnalysis; namespace Semgus.Model.Smt.Extensions @@ -94,6 +94,65 @@ internal SmtBitVectorsExtension(SmtCoreTheory core, SmtBitVectorsTheory bv) }); + sb.AddFn(name: "bvugt", + val: SmtSourceBuilder.CheckArgumentSortsEqual, + valCmt: "Argument sorts must be of the same size", + retCalc: SmtSourceBuilder.UseFirstArgumentSort, + bv0, + bv0, + bv0) + .DefinitionMissing((ctx, fn, rank) => + { + SmtIdentifier bvult_id = new("bvult"); + + var a1_id = new SmtIdentifier("a1"); + var a2_id = new SmtIdentifier("a2"); + + SmtScope scope = new(default); + scope.TryAddVariableBinding(a1_id, rank.ArgumentSorts[0], SmtVariableBindingType.Lambda, ctx, out var a1_binding, out _); + scope.TryAddVariableBinding(a2_id, rank.ArgumentSorts[1], SmtVariableBindingType.Lambda, ctx, out var a2_binding, out _); + + var a1 = new SmtVariable(a1_id, a1_binding!); + var a2 = new SmtVariable(a2_id, a2_binding!); + + var b = new SmtTermBuilder(ctx); + return b.Lambda(scope, + b.Apply(bvult_id, a2, a1)); + + }); + + sb.AddFn(name: "bvsub", + val: SmtSourceBuilder.CheckArgumentSortsEqual, + valCmt: "Argument sorts must be of the same size", + retCalc: SmtSourceBuilder.UseFirstArgumentSort, + bv0, + bv0, + bv0) + .DefinitionMissing((ctx, fn, rank) => + { + SmtIdentifier bvadd_id = new("bvadd"); + SmtIdentifier bvnot_id = new("bvnot"); + + var a1_id = new SmtIdentifier("a1"); + var a2_id = new SmtIdentifier("a2"); + var c1_id = new SmtIdentifier("c1"); + + SmtScope scope = new(default); + scope.TryAddVariableBinding(a1_id, rank.ArgumentSorts[0], SmtVariableBindingType.Lambda, ctx, out var a1_binding, out _); + scope.TryAddVariableBinding(a2_id, rank.ArgumentSorts[1], SmtVariableBindingType.Lambda, ctx, out var a2_binding, out _); + + var a1 = new SmtVariable(a1_id, a1_binding!); + var a2 = new SmtVariable(a2_id, a2_binding!); + var c1 = new SmtBitVectorLiteral(ctx, new BitArray(new int[] { 1 })); + + var b = new SmtTermBuilder(ctx); + // 2's complement + return b.Lambda(scope, + b.Apply(bvadd_id, b.Apply(bvadd_id, a1, b.Apply(bvnot_id, a2)), + c1)); + + }); + Functions = sb.Functions; PrimaryFunctionSymbols = sb.PrimaryFunctionSymbols; } From b25141d069d73545c49b3f4b0c3b6018dfdf09ea Mon Sep 17 00:00:00 2001 From: rahulk64 Date: Fri, 18 Aug 2023 13:58:53 -0500 Subject: [PATCH 2/2] add remaining bv comparisons --- .../Smt/Extensions/SmtBitVectorsExtension.cs | 100 +++++++++++++++++- 1 file changed, 97 insertions(+), 3 deletions(-) diff --git a/Semgus-Lib/Model/Smt/Extensions/SmtBitVectorsExtension.cs b/Semgus-Lib/Model/Smt/Extensions/SmtBitVectorsExtension.cs index 8c4b88f..c381e99 100644 --- a/Semgus-Lib/Model/Smt/Extensions/SmtBitVectorsExtension.cs +++ b/Semgus-Lib/Model/Smt/Extensions/SmtBitVectorsExtension.cs @@ -63,6 +63,7 @@ public bool TryGetSort(SmtSortIdentifier sortId, [NotNullWhen(true)] out SmtSort internal SmtBitVectorsExtension(SmtCoreTheory core, SmtBitVectorsTheory bv) { var bv0 = new SmtSort.WildcardSort(new(new SmtIdentifier("BitVec", "*"))); + var bool0 = core.Sorts[SmtCommonIdentifiers.BoolSortId.Name]; SmtSourceBuilder sb = new(this); sb.AddFn(name: "bvxor", val: SmtSourceBuilder.CheckArgumentSortsEqual, @@ -88,6 +89,7 @@ internal SmtBitVectorsExtension(SmtCoreTheory core, SmtBitVectorsTheory bv) var a2 = new SmtVariable(a2_id, a2_binding!); var b = new SmtTermBuilder(ctx); + // (xor a1 a2) = (bvor (bvand a1 (bvnot a2)) (bvand (not a1) a2)) return b.Lambda(scope, b.Apply(bvor_id, b.Apply(bvand_id, a1, b.Apply(bvnot_id, a2)), b.Apply(bvand_id, b.Apply(bvnot_id, a1), a2))); @@ -96,9 +98,9 @@ internal SmtBitVectorsExtension(SmtCoreTheory core, SmtBitVectorsTheory bv) sb.AddFn(name: "bvugt", val: SmtSourceBuilder.CheckArgumentSortsEqual, - valCmt: "Argument sorts must be of the same size", - retCalc: SmtSourceBuilder.UseFirstArgumentSort, - bv0, + valCmt: "Argument sorts must be the same", + retCalc: SmtSourceBuilder.UseReturnSort, + bool0, bv0, bv0) .DefinitionMissing((ctx, fn, rank) => @@ -116,11 +118,103 @@ internal SmtBitVectorsExtension(SmtCoreTheory core, SmtBitVectorsTheory bv) var a2 = new SmtVariable(a2_id, a2_binding!); var b = new SmtTermBuilder(ctx); + // (bvugt a1 a2) = (bvult a2 a1) return b.Lambda(scope, b.Apply(bvult_id, a2, a1)); }); + sb.AddFn(name: "bvule", + val: SmtSourceBuilder.CheckArgumentSortsEqual, + valCmt: "Argument sorts must be the same", + retCalc: SmtSourceBuilder.UseReturnSort, + ret: bool0, + bv0, + bv0) + .DefinitionMissing((ctx, fn, rank) => + { + SmtIdentifier bvult_id = new("bvult"); + SmtIdentifier eq_id = new("="); + SmtIdentifier or_id = new("or"); + + var a1_id = new SmtIdentifier("a1"); + var a2_id = new SmtIdentifier("a2"); + + SmtScope scope = new(default); + scope.TryAddVariableBinding(a1_id, rank.ArgumentSorts[0], SmtVariableBindingType.Lambda, ctx, out var a1_binding, out _); + scope.TryAddVariableBinding(a2_id, rank.ArgumentSorts[1], SmtVariableBindingType.Lambda, ctx, out var a2_binding, out _); + + var a1 = new SmtVariable(a1_id, a1_binding!); + var a2 = new SmtVariable(a2_id, a2_binding!); + + var b = new SmtTermBuilder(ctx); + // (bvule a1 a2) = (or (bvult a1 a2) (= a1 a2)) + return b.Lambda(scope, + b.Apply(or_id, + b.Apply(bvult_id, a1, a2), + b.Apply(eq_id, a1, a2))); + + }); + + sb.AddFn(name: "bvuge", + val: SmtSourceBuilder.CheckArgumentSortsEqual, + valCmt: "Argument sorts must be the same", + retCalc: SmtSourceBuilder.UseReturnSort, + bool0, + bv0, + bv0) + .DefinitionMissing((ctx, fn, rank) => + { + SmtIdentifier bvult_id = new("bvult"); + SmtIdentifier eq_id = new("="); + SmtIdentifier or_id = new("or"); + + var a1_id = new SmtIdentifier("a1"); + var a2_id = new SmtIdentifier("a2"); + + SmtScope scope = new(default); + scope.TryAddVariableBinding(a1_id, rank.ArgumentSorts[0], SmtVariableBindingType.Lambda, ctx, out var a1_binding, out _); + scope.TryAddVariableBinding(a2_id, rank.ArgumentSorts[1], SmtVariableBindingType.Lambda, ctx, out var a2_binding, out _); + + var a1 = new SmtVariable(a1_id, a1_binding!); + var a2 = new SmtVariable(a2_id, a2_binding!); + + var b = new SmtTermBuilder(ctx); + // (bvuge a1 a2) = (or (bvult a2 a1) (= a1 a2)) + return b.Lambda(scope, + b.Apply(or_id, + b.Apply(bvult_id, a2, a1), + b.Apply( eq_id, a1, a2))); + + }); + + sb.AddFn(name: "bveq", + val: SmtSourceBuilder.CheckArgumentSortsEqual, + valCmt: "Argument sorts must be the same", + retCalc: SmtSourceBuilder.UseReturnSort, + bool0, + bv0, + bv0) + .DefinitionMissing((ctx, fn, rank) => + { + SmtIdentifier bveq_id = new("="); + + var a1_id = new SmtIdentifier("a1"); + var a2_id = new SmtIdentifier("a2"); + + SmtScope scope = new(default); + scope.TryAddVariableBinding(a1_id, rank.ArgumentSorts[0], SmtVariableBindingType.Lambda, ctx, out var a1_binding, out _); + scope.TryAddVariableBinding(a2_id, rank.ArgumentSorts[1], SmtVariableBindingType.Lambda, ctx, out var a2_binding, out _); + + var a1 = new SmtVariable(a1_id, a1_binding!); + var a2 = new SmtVariable(a2_id, a2_binding!); + + var b = new SmtTermBuilder(ctx); + // (bvueq a1 a2) = (= a1 a2) + return b.Lambda(scope, b.Apply(bveq_id, a1, a2)); + + }); + sb.AddFn(name: "bvsub", val: SmtSourceBuilder.CheckArgumentSortsEqual, valCmt: "Argument sorts must be of the same size",