Skip to content

Commit

Permalink
Merge pull request #106 from SemGuS-git/bv-ext
Browse files Browse the repository at this point in the history 
Move BV extensions
  • Loading branch information
@kjcjohnson
kjcjohnson authored Aug 22, 2023
2 parents 25f6d51 + b25141d commit 31624ca
Showing 1 changed file with 154 additions and 1 deletion.
155 changes: 154 additions & 1 deletion Semgus-Lib/Model/Smt/Extensions/SmtBitVectorsExtension.cs
View file
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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,
Expand All @@ -88,12 +89,164 @@ 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)));
});

sb.AddFn(name: "bvugt",
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");
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);
// (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",
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;
}
Expand Down

0 comments on commit 31624ca

Please sign in to comment.