Skip to content

Commit 87ac95b

Browse files
CopilotNikolajBjorner
Copilot
and
NikolajBjorner
committed
Format code with prettier
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
1 parent c18e9d5 commit 87ac95b

3 files changed

Lines changed: 143 additions & 80 deletions

File tree

‎src/api/js/src/high-level/high-level.test.ts‎

Lines changed: 30 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@ describe('high-level', () => {
183183
const solver = new Solver();
184184
// At most 2 of x, y, z can be true
185185
solver.add(AtMost([x, y, z], 2));
186-
186+
187187
// All three being true should be unsat
188188
solver.add(x, y, z);
189189
expect(await solver.check()).toStrictEqual('unsat');
@@ -198,7 +198,7 @@ describe('high-level', () => {
198198
const solver = new Solver();
199199
// At least 2 of x, y, z must be true
200200
solver.add(AtLeast([x, y, z], 2));
201-
201+
202202
// Only one being true should be unsat
203203
solver.add(x, y.not(), z.not());
204204
expect(await solver.check()).toStrictEqual('unsat');
@@ -572,7 +572,10 @@ describe('high-level', () => {
572572
const set = Z3.Set.const('set', Z3.Int.sort());
573573
const [a, b] = Z3.Int.consts('a b');
574574

575-
const conjecture = set.contains(a).and(set.contains(b)).implies(Z3.Set.val([a, b], Z3.Int.sort()).subsetOf(set));
575+
const conjecture = set
576+
.contains(a)
577+
.and(set.contains(b))
578+
.implies(Z3.Set.val([a, b], Z3.Int.sort()).subsetOf(set));
576579
await prove(conjecture);
577580
});
578581

@@ -582,7 +585,10 @@ describe('high-level', () => {
582585
const set = Z3.Set.const('set', Z3.Int.sort());
583586
const [a, b] = Z3.Int.consts('a b');
584587

585-
const conjecture = set.contains(a).and(set.contains(b)).and(Z3.Set.val([a, b], Z3.Int.sort()).eq(set));
588+
const conjecture = set
589+
.contains(a)
590+
.and(set.contains(b))
591+
.and(Z3.Set.val([a, b], Z3.Int.sort()).eq(set));
586592
await solve(conjecture);
587593
});
588594

@@ -596,7 +602,7 @@ describe('high-level', () => {
596602
const conjecture = set.intersect(abset).subsetOf(abset);
597603
await prove(conjecture);
598604
});
599-
605+
600606
it('Intersection 2', async () => {
601607
const Z3 = api.Context('main');
602608

@@ -618,7 +624,7 @@ describe('high-level', () => {
618624
const conjecture = set.subsetOf(set.union(abset));
619625
await prove(conjecture);
620626
});
621-
627+
622628
it('Union 2', async () => {
623629
const Z3 = api.Context('main');
624630

@@ -629,14 +635,14 @@ describe('high-level', () => {
629635
const conjecture = set.union(abset).subsetOf(abset);
630636
await solve(conjecture);
631637
});
632-
638+
633639
it('Complement 1', async () => {
634640
const Z3 = api.Context('main');
635641

636642
const set = Z3.Set.const('set', Z3.Int.sort());
637643
const a = Z3.Int.const('a');
638644

639-
const conjecture = set.complement().complement().eq(set)
645+
const conjecture = set.complement().complement().eq(set);
640646
await prove(conjecture);
641647
});
642648
it('Complement 2', async () => {
@@ -645,28 +651,28 @@ describe('high-level', () => {
645651
const set = Z3.Set.const('set', Z3.Int.sort());
646652
const a = Z3.Int.const('a');
647653

648-
const conjecture = set.contains(a).implies(Z3.Not(set.complement().contains(a)))
654+
const conjecture = set.contains(a).implies(Z3.Not(set.complement().contains(a)));
649655
await prove(conjecture);
650656
});
651-
657+
652658
it('Difference', async () => {
653659
const Z3 = api.Context('main');
654660

655661
const [set1, set2] = Z3.Set.consts('set1 set2', Z3.Int.sort());
656662
const a = Z3.Int.const('a');
657663

658-
const conjecture = set1.contains(a).implies(Z3.Not(set2.diff(set1).contains(a)))
659-
664+
const conjecture = set1.contains(a).implies(Z3.Not(set2.diff(set1).contains(a)));
665+
660666
await prove(conjecture);
661667
});
662-
668+
663669
it('FullSet', async () => {
664670
const Z3 = api.Context('main');
665671

666672
const set = Z3.Set.const('set', Z3.Int.sort());
667673

668674
const conjecture = set.complement().eq(Z3.FullSet(Z3.Int.sort()).diff(set));
669-
675+
670676
await prove(conjecture);
671677
});
672678

@@ -677,7 +683,7 @@ describe('high-level', () => {
677683
const [a, b] = Z3.Int.consts('a b');
678684

679685
const conjecture = empty.add(a).add(b).del(a).del(b).eq(empty);
680-
686+
681687
await prove(conjecture);
682688
});
683689
});
@@ -957,14 +963,14 @@ describe('high-level', () => {
957963
Color.declare('red');
958964
Color.declare('green');
959965
Color.declare('blue');
960-
966+
961967
const ColorSort = Color.create();
962-
968+
963969
// Test that we can access the constructors
964970
expect(typeof (ColorSort as any).red).not.toBe('undefined');
965971
expect(typeof (ColorSort as any).green).not.toBe('undefined');
966972
expect(typeof (ColorSort as any).blue).not.toBe('undefined');
967-
973+
968974
// Test that we can access the recognizers
969975
expect(typeof (ColorSort as any).is_red).not.toBe('undefined');
970976
expect(typeof (ColorSort as any).is_green).not.toBe('undefined');
@@ -978,9 +984,9 @@ describe('high-level', () => {
978984
const List = Datatype('List');
979985
List.declare('cons', ['car', Int.sort()], ['cdr', List]);
980986
List.declare('nil');
981-
987+
982988
const ListSort = List.create();
983-
989+
984990
// Test that constructors and accessors exist
985991
expect(typeof (ListSort as any).cons).not.toBe('undefined');
986992
expect(typeof (ListSort as any).nil).not.toBe('undefined');
@@ -996,20 +1002,20 @@ describe('high-level', () => {
9961002
// Create mutually recursive Tree and TreeList datatypes
9971003
const Tree = Datatype('Tree');
9981004
const TreeList = Datatype('TreeList');
999-
1005+
10001006
Tree.declare('leaf', ['value', Int.sort()]);
10011007
Tree.declare('node', ['children', TreeList]);
10021008
TreeList.declare('nil');
10031009
TreeList.declare('cons', ['car', Tree], ['cdr', TreeList]);
1004-
1010+
10051011
const [TreeSort, TreeListSort] = Datatype.createDatatypes(Tree, TreeList);
1006-
1012+
10071013
// Test that both datatypes have their constructors
10081014
expect(typeof (TreeSort as any).leaf).not.toBe('undefined');
10091015
expect(typeof (TreeSort as any).node).not.toBe('undefined');
10101016
expect(typeof (TreeListSort as any).nil).not.toBe('undefined');
10111017
expect(typeof (TreeListSort as any).cons).not.toBe('undefined');
1012-
1018+
10131019
// Test accessors exist
10141020
expect(typeof (TreeSort as any).value).not.toBe('undefined');
10151021
expect(typeof (TreeSort as any).children).not.toBe('undefined');

‎src/api/js/src/high-level/high-level.ts‎

Lines changed: 60 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -808,12 +808,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
808808
sort<ElemSort extends AnySort<Name>>(sort: ElemSort): SMTSetSort<Name, ElemSort> {
809809
return Array.sort(sort, Bool.sort());
810810
},
811-
const<ElemSort extends AnySort<Name>>(name: string, sort: ElemSort) : SMTSet<Name, ElemSort> {
811+
const<ElemSort extends AnySort<Name>>(name: string, sort: ElemSort): SMTSet<Name, ElemSort> {
812812
return new SetImpl<ElemSort>(
813813
check(Z3.mk_const(contextPtr, _toSymbol(name), Array.sort(sort, Bool.sort()).ptr)),
814814
);
815815
},
816-
consts<ElemSort extends AnySort<Name>>(names: string | string[], sort: ElemSort) : SMTSet<Name, ElemSort>[] {
816+
consts<ElemSort extends AnySort<Name>>(names: string | string[], sort: ElemSort): SMTSet<Name, ElemSort>[] {
817817
if (typeof names === 'string') {
818818
names = names.split(' ');
819819
}
@@ -822,14 +822,17 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
822822
empty<ElemSort extends AnySort<Name>>(sort: ElemSort): SMTSet<Name, ElemSort> {
823823
return EmptySet(sort);
824824
},
825-
val<ElemSort extends AnySort<Name>>(values: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>[], sort: ElemSort): SMTSet<Name, ElemSort> {
825+
val<ElemSort extends AnySort<Name>>(
826+
values: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>[],
827+
sort: ElemSort,
828+
): SMTSet<Name, ElemSort> {
826829
var result = EmptySet(sort);
827830
for (const value of values) {
828831
result = SetAdd(result, value);
829832
}
830833
return result;
831-
}
832-
}
834+
},
835+
};
833836

834837
const Datatype = Object.assign(
835838
(name: string): DatatypeImpl => {
@@ -838,8 +841,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
838841
{
839842
createDatatypes(...datatypes: DatatypeImpl[]): DatatypeSortImpl[] {
840843
return createDatatypes(...datatypes);
841-
}
842-
}
844+
},
845+
},
843846
);
844847

845848
////////////////
@@ -1322,41 +1325,69 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
13221325
}
13231326

13241327
function SetUnion<ElemSort extends AnySort<Name>>(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort> {
1325-
return new SetImpl<ElemSort>(check(Z3.mk_set_union(contextPtr, args.map(arg => arg.ast))));
1328+
return new SetImpl<ElemSort>(
1329+
check(
1330+
Z3.mk_set_union(
1331+
contextPtr,
1332+
args.map(arg => arg.ast),
1333+
),
1334+
),
1335+
);
13261336
}
1327-
1337+
13281338
function SetIntersect<ElemSort extends AnySort<Name>>(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort> {
1329-
return new SetImpl<ElemSort>(check(Z3.mk_set_intersect(contextPtr, args.map(arg => arg.ast))));
1339+
return new SetImpl<ElemSort>(
1340+
check(
1341+
Z3.mk_set_intersect(
1342+
contextPtr,
1343+
args.map(arg => arg.ast),
1344+
),
1345+
),
1346+
);
13301347
}
1331-
1332-
function SetDifference<ElemSort extends AnySort<Name>>(a: SMTSet<Name, ElemSort>, b: SMTSet<Name, ElemSort>): SMTSet<Name, ElemSort> {
1348+
1349+
function SetDifference<ElemSort extends AnySort<Name>>(
1350+
a: SMTSet<Name, ElemSort>,
1351+
b: SMTSet<Name, ElemSort>,
1352+
): SMTSet<Name, ElemSort> {
13331353
return new SetImpl<ElemSort>(check(Z3.mk_set_difference(contextPtr, a.ast, b.ast)));
13341354
}
1335-
13361355

1337-
function SetAdd<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>, elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort> {
1356+
function SetAdd<ElemSort extends AnySort<Name>>(
1357+
set: SMTSet<Name, ElemSort>,
1358+
elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
1359+
): SMTSet<Name, ElemSort> {
13381360
const arg = set.elemSort().cast(elem as any);
13391361
return new SetImpl<ElemSort>(check(Z3.mk_set_add(contextPtr, set.ast, arg.ast)));
13401362
}
1341-
function SetDel<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>, elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort> {
1363+
function SetDel<ElemSort extends AnySort<Name>>(
1364+
set: SMTSet<Name, ElemSort>,
1365+
elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
1366+
): SMTSet<Name, ElemSort> {
13421367
const arg = set.elemSort().cast(elem as any);
13431368
return new SetImpl<ElemSort>(check(Z3.mk_set_del(contextPtr, set.ast, arg.ast)));
13441369
}
13451370
function SetComplement<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>): SMTSet<Name, ElemSort> {
13461371
return new SetImpl<ElemSort>(check(Z3.mk_set_complement(contextPtr, set.ast)));
13471372
}
1348-
1373+
13491374
function EmptySet<ElemSort extends AnySort<Name>>(sort: ElemSort): SMTSet<Name, ElemSort> {
13501375
return new SetImpl<ElemSort>(check(Z3.mk_empty_set(contextPtr, sort.ptr)));
13511376
}
13521377
function FullSet<ElemSort extends AnySort<Name>>(sort: ElemSort): SMTSet<Name, ElemSort> {
13531378
return new SetImpl<ElemSort>(check(Z3.mk_full_set(contextPtr, sort.ptr)));
13541379
}
1355-
function isMember<ElemSort extends AnySort<Name>>(elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>, set: SMTSet<Name, ElemSort>): Bool<Name> {
1380+
function isMember<ElemSort extends AnySort<Name>>(
1381+
elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
1382+
set: SMTSet<Name, ElemSort>,
1383+
): Bool<Name> {
13561384
const arg = set.elemSort().cast(elem as any);
13571385
return new BoolImpl(check(Z3.mk_set_member(contextPtr, arg.ast, set.ast)));
13581386
}
1359-
function isSubset<ElemSort extends AnySort<Name>>(a: SMTSet<Name, ElemSort>, b: SMTSet<Name, ElemSort>): Bool<Name> {
1387+
function isSubset<ElemSort extends AnySort<Name>>(
1388+
a: SMTSet<Name, ElemSort>,
1389+
b: SMTSet<Name, ElemSort>,
1390+
): Bool<Name> {
13601391
return new BoolImpl(check(Z3.mk_set_subset(contextPtr, a.ast, b.ast)));
13611392
}
13621393

@@ -2675,7 +2706,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
26752706
}
26762707
}
26772708

2678-
class SetImpl<ElemSort extends Sort<Name>> extends ExprImpl<Z3_ast, ArraySortImpl<[ElemSort], BoolSort<Name>>> implements SMTSet<Name, ElemSort> {
2709+
class SetImpl<ElemSort extends Sort<Name>>
2710+
extends ExprImpl<Z3_ast, ArraySortImpl<[ElemSort], BoolSort<Name>>>
2711+
implements SMTSet<Name, ElemSort>
2712+
{
26792713
declare readonly __typename: 'Array';
26802714

26812715
elemSort(): ElemSort {
@@ -2803,7 +2837,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
28032837

28042838
for (const [fieldName, fieldSort] of fields) {
28052839
fieldNames.push(fieldName);
2806-
2840+
28072841
if (fieldSort instanceof DatatypeImpl) {
28082842
// Reference to another datatype being defined
28092843
const refIndex = datatypes.indexOf(fieldSort);
@@ -2826,7 +2860,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
28262860
Z3.mk_string_symbol(contextPtr, `is_${constructorName}`),
28272861
fieldNames.map(name => Z3.mk_string_symbol(contextPtr, name)),
28282862
fieldSorts,
2829-
fieldRefs
2863+
fieldRefs,
28302864
);
28312865
constructors.push(constructor);
28322866
scopedConstructors.push(constructor);
@@ -2844,33 +2878,33 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
28442878
const results: DatatypeSortImpl[] = [];
28452879
for (let i = 0; i < resultSorts.length; i++) {
28462880
const sortImpl = new DatatypeSortImpl(resultSorts[i]);
2847-
2881+
28482882
// Attach constructor, recognizer, and accessor functions dynamically
28492883
const numConstructors = sortImpl.numConstructors();
28502884
for (let j = 0; j < numConstructors; j++) {
28512885
const constructor = sortImpl.constructorDecl(j);
28522886
const recognizer = sortImpl.recognizer(j);
28532887
const constructorName = constructor.name().toString();
2854-
2888+
28552889
// Attach constructor function
28562890
if (constructor.arity() === 0) {
28572891
// Nullary constructor (constant)
28582892
(sortImpl as any)[constructorName] = constructor.call();
28592893
} else {
28602894
(sortImpl as any)[constructorName] = constructor;
28612895
}
2862-
2896+
28632897
// Attach recognizer function
28642898
(sortImpl as any)[`is_${constructorName}`] = recognizer;
2865-
2899+
28662900
// Attach accessor functions
28672901
for (let k = 0; k < constructor.arity(); k++) {
28682902
const accessor = sortImpl.accessor(j, k);
28692903
const accessorName = accessor.name().toString();
28702904
(sortImpl as any)[accessorName] = accessor;
28712905
}
28722906
}
2873-
2907+
28742908
results.push(sortImpl);
28752909
}
28762910

0 commit comments

Comments
 (0)