From 98c21928d3392514babc04bf510ff229c58f88d4 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 12 May 2026 08:46:20 +0200 Subject: [PATCH 1/5] refactor error handling in consistency check --- src/lib/server/consistency.ts | 14 ++++----- src/lib/server/search.ts | 46 ++++++++++++++++-------------- src/routes/missing/+page.server.ts | 22 +++++++------- 3 files changed, 40 insertions(+), 42 deletions(-) diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index 449d0574e..b8c781711 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -13,13 +13,12 @@ type NormalizedCategoryImplication = { export function check_consistency( satisfied_properties: Set, unsatisfied_properties: Set, -): { consistent: boolean } | null { +): { consistent: boolean } { for (const p of satisfied_properties) { if (unsatisfied_properties.has(p)) return { consistent: false } } const implications = get_normalized_category_implications() - if (!implications) return null return check_consistency_worker( satisfied_properties, @@ -63,9 +62,7 @@ function check_consistency_worker( return { consistent: true } } -export function get_normalized_category_implications(): - | NormalizedCategoryImplication[] - | null { +function get_normalized_category_implications() { const { rows, err } = query<{ id: string assumptions: string @@ -75,7 +72,7 @@ export function get_normalized_category_implications(): sql`SELECT id, assumptions, conclusions, is_equivalence FROM category_implications_view`, ) - if (err) return null + if (err) throw err const implications: NormalizedCategoryImplication[] = [] @@ -107,14 +104,13 @@ export function get_normalized_category_implications(): export function get_missing_combinations() { const implications = get_normalized_category_implications() - if (!implications) return null const { rows: properties, err } = query<{ id: string dual_property_id: string | null }>(sql`SELECT id, dual_property_id FROM category_properties ORDER BY lower(id)`) - if (err) return null + if (err) throw err const { rows: existing, err: err_existing } = query<{ p: string @@ -127,7 +123,7 @@ export function get_missing_combinations() { WHERE cp.is_satisfied = TRUE AND cnp.is_satisfied = FALSE `) - if (err_existing) return null + if (err_existing) throw err_existing const witnessed_pairs = new Set(existing.map(({ p, q }) => `${p}|${q}`)) diff --git a/src/lib/server/search.ts b/src/lib/server/search.ts index 1478376b9..70924958a 100644 --- a/src/lib/server/search.ts +++ b/src/lib/server/search.ts @@ -71,29 +71,31 @@ export function search_handler(event: RequestEvent, type: 'category' | 'functor' // TODO: implement this for functors as well if (type === 'category') { - const check = check_consistency( - new Set(satisfied_properties), - new Set(unsatisfied_properties), - ) - - if (!check) error(500, 'Consistency check failed') - - if (!check.consistent) { - event.setHeaders({ - // shared cache for 30min - 'cache-control': 'public, max-age=0, s-maxage=1800', - }) - - return { - is_consistent: false, - all_properties, - satisfied_properties, - unsatisfied_properties, - found_objects: [], - dual_satisfied_properties, - dual_unsatisfied_properties, - dual_search_available, + try { + const { consistent } = check_consistency( + new Set(satisfied_properties), + new Set(unsatisfied_properties), + ) + + if (!consistent) { + event.setHeaders({ + // shared cache for 30min + 'cache-control': 'public, max-age=0, s-maxage=1800', + }) + + return { + is_consistent: false, + all_properties, + satisfied_properties, + unsatisfied_properties, + found_objects: [], + dual_satisfied_properties, + dual_unsatisfied_properties, + dual_search_available, + } } + } catch (err) { + error(500, 'Consistency check failed') } } diff --git a/src/routes/missing/+page.server.ts b/src/routes/missing/+page.server.ts index b28c822ca..bd2bf6c38 100644 --- a/src/routes/missing/+page.server.ts +++ b/src/routes/missing/+page.server.ts @@ -87,18 +87,18 @@ export const load = async () => { 0, ) - const missing_combinations = get_missing_combinations() + try { + const missing_combinations = get_missing_combinations() - if (!missing_combinations) { + return { + categories_with_unknown_properties, + total_unknown_pairs, + categories_with_missing_morphisms, + undistinguishable_category_pairs, + functors_with_unknown_properties, + missing_combinations, + } + } catch (err) { error(500, 'Failed to load missing combinations') } - - return { - categories_with_unknown_properties, - total_unknown_pairs, - categories_with_missing_morphisms, - undistinguishable_category_pairs, - functors_with_unknown_properties, - missing_combinations, - } } From 4d738100d991a80a3b0b44979da92ee5eda45e96 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 12 May 2026 09:09:18 +0200 Subject: [PATCH 2/5] show contradiction in srp (if found) --- src/lib/server/consistency.ts | 32 ++++++++++++------- src/lib/server/search.ts | 10 +++--- .../category-search/results/+page.svelte | 10 ++++-- 3 files changed, 34 insertions(+), 18 deletions(-) diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index b8c781711..5fc3e244f 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -10,32 +10,37 @@ type NormalizedCategoryImplication = { conclusion: string } -export function check_consistency( +export function get_contradiction( satisfied_properties: Set, unsatisfied_properties: Set, -): { consistent: boolean } { +): string[] | null { for (const p of satisfied_properties) { - if (unsatisfied_properties.has(p)) return { consistent: false } + if (unsatisfied_properties.has(p)) + return [`${p} cannot be both satisfied and unsatisfied`] } const implications = get_normalized_category_implications() - return check_consistency_worker( + return contradiction_worker( satisfied_properties, unsatisfied_properties, implications, ) } -function check_consistency_worker( +function contradiction_worker( satisfied_properties: Set, unsatisfied_properties: Set, implications: NormalizedCategoryImplication[], -): { consistent: boolean } { +): string[] | null { for (const p of satisfied_properties) { - if (unsatisfied_properties.has(p)) return { consistent: false } + if (unsatisfied_properties.has(p)) { + return [`${p} cannot be both satisfied and unsatisfied`] + } } + let contradiction: string[] = [] + const deduced_satisfied_properties = new Set(satisfied_properties) function get_next_implication() { @@ -52,14 +57,19 @@ function check_consistency_worker( const implication = get_next_implication() if (!implication) break + let segment = `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}` + if (unsatisfied_properties.has(implication.conclusion)) { - return { consistent: false } + segment += ` ↯` + contradiction.push(segment) + return contradiction } + contradiction.push(segment) deduced_satisfied_properties.add(implication.conclusion) } - return { consistent: true } + return null } function get_normalized_category_implications() { @@ -143,13 +153,13 @@ export function get_missing_combinations() { continue } - const { consistent } = check_consistency_worker( + const contradiction = contradiction_worker( new Set([p.id]), new Set([q.id]), implications, ) - if (consistent) missing_pairs.push([p.id, q.id]) + if (!contradiction) missing_pairs.push([p.id, q.id]) } } diff --git a/src/lib/server/search.ts b/src/lib/server/search.ts index 70924958a..538a64fcc 100644 --- a/src/lib/server/search.ts +++ b/src/lib/server/search.ts @@ -4,7 +4,7 @@ import { query } from '$lib/server/db.catdat' import { error } from '@sveltejs/kit' import sql from 'sql-template-tag' import { SEARCH_SEPARATOR } from '$lib/commons/search.config' -import { check_consistency } from '$lib/server/consistency' +import { get_contradiction } from '$lib/server/consistency' type NamedObject = { id: string @@ -72,19 +72,19 @@ export function search_handler(event: RequestEvent, type: 'category' | 'functor' // TODO: implement this for functors as well if (type === 'category') { try { - const { consistent } = check_consistency( + const contradiction = get_contradiction( new Set(satisfied_properties), new Set(unsatisfied_properties), ) - if (!consistent) { + if (contradiction) { event.setHeaders({ // shared cache for 30min 'cache-control': 'public, max-age=0, s-maxage=1800', }) return { - is_consistent: false, + contradiction, all_properties, satisfied_properties, unsatisfied_properties, @@ -125,7 +125,7 @@ export function search_handler(event: RequestEvent, type: 'category' | 'functor' }) return { - is_consistent: true, + contradiction: null, all_properties, satisfied_properties, unsatisfied_properties, diff --git a/src/routes/category-search/results/+page.svelte b/src/routes/category-search/results/+page.svelte index 8158d6244..260d0ec7b 100644 --- a/src/routes/category-search/results/+page.svelte +++ b/src/routes/category-search/results/+page.svelte @@ -63,7 +63,7 @@ {/if} -{#if data.is_consistent} +{#if !data.contradiction}

{pluralize(data.found_objects.length, { one: 'Found {count} category', @@ -73,8 +73,14 @@ {:else}

- No categories found because the requirements are inconsistent. + No categories found because the requirements are inconsistent:

+ +
    + {#each data.contradiction as segment} +
  1. {segment}
    2. + {/each} +
{/if} From fafc4182028e915fa3b9aba93b06f7d5633c263a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 12 May 2026 09:37:03 +0200 Subject: [PATCH 3/5] remove irrelevant implications in proof of contradiction --- src/lib/server/consistency.ts | 47 +++++++++++++++++++++++++++++------ 1 file changed, 40 insertions(+), 7 deletions(-) diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index 5fc3e244f..976f33dcd 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -39,7 +39,12 @@ function contradiction_worker( } } - let contradiction: string[] = [] + let contradictory_property: string | null = null + + const used_implications: { + implication: NormalizedCategoryImplication + relevant: boolean + }[] = [] const deduced_satisfied_properties = new Set(satisfied_properties) @@ -57,19 +62,47 @@ function contradiction_worker( const implication = get_next_implication() if (!implication) break - let segment = `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}` + used_implications.push({ implication, relevant: false }) + deduced_satisfied_properties.add(implication.conclusion) if (unsatisfied_properties.has(implication.conclusion)) { - segment += ` ↯` - contradiction.push(segment) - return contradiction + contradictory_property = implication.conclusion + break + } + } + + if (!contradictory_property) return null + + // remove irrelevant implications + + const relevant_properties = new Set([contradictory_property]) + + for (let i = used_implications.length - 1; i >= 0; i--) { + const { implication } = used_implications[i] + const is_relevant = relevant_properties.has(implication.conclusion) + + if (is_relevant) { + used_implications[i].relevant = is_relevant + for (const p of implication.assumptions) { + if (!satisfied_properties.has(p)) relevant_properties.add(p) + } } + } + const relevant_implications = used_implications + .filter((item) => item.relevant) + .map((item) => item.implication) + + const contradiction: string[] = [] + + for (let i = 0; i < relevant_implications.length; i++) { + const implication = relevant_implications[i] + let segment = `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}` + if (i === relevant_implications.length - 1) segment += ` ↯` contradiction.push(segment) - deduced_satisfied_properties.add(implication.conclusion) } - return null + return contradiction } function get_normalized_category_implications() { From c63c48114fc6c13ca245a163a3ab75a62f2a94ff Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 12 May 2026 13:28:21 +0200 Subject: [PATCH 4/5] use BFS to find shortest proof, use deduction dict to simplify proof construction --- src/lib/server/consistency.ts | 86 ++++++++++++++++------------------- 1 file changed, 39 insertions(+), 47 deletions(-) diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index 976f33dcd..d6cfc514a 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -15,8 +15,7 @@ export function get_contradiction( unsatisfied_properties: Set, ): string[] | null { for (const p of satisfied_properties) { - if (unsatisfied_properties.has(p)) - return [`${p} cannot be both satisfied and unsatisfied`] + if (unsatisfied_properties.has(p)) return [`${p} ⟹ ${p}`] } const implications = get_normalized_category_implications() @@ -34,74 +33,63 @@ function contradiction_worker( implications: NormalizedCategoryImplication[], ): string[] | null { for (const p of satisfied_properties) { - if (unsatisfied_properties.has(p)) { - return [`${p} cannot be both satisfied and unsatisfied`] - } + if (unsatisfied_properties.has(p)) return [`${p} ⟹ ${p}`] } - let contradictory_property: string | null = null + const deduction_dict: Record = {} + const deduced_satisfied_properties = new Set(satisfied_properties) - const used_implications: { - implication: NormalizedCategoryImplication - relevant: boolean - }[] = [] + // bfs to find contradiction - const deduced_satisfied_properties = new Set(satisfied_properties) + let contradictory_property: string | null = null + + while (!contradictory_property) { + const new_properties = new Set() - function get_next_implication() { for (const implication of implications) { const is_valid = is_subset(implication.assumptions, deduced_satisfied_properties) && - !deduced_satisfied_properties.has(implication.conclusion) - if (is_valid) return implication - } - return null - } + !deduced_satisfied_properties.has(implication.conclusion) && + !new_properties.has(implication.conclusion) + if (!is_valid) continue - while (true) { - const implication = get_next_implication() - if (!implication) break + new_properties.add(implication.conclusion) + deduction_dict[implication.conclusion] = implication - used_implications.push({ implication, relevant: false }) - deduced_satisfied_properties.add(implication.conclusion) - - if (unsatisfied_properties.has(implication.conclusion)) { - contradictory_property = implication.conclusion - break + if (unsatisfied_properties.has(implication.conclusion)) { + contradictory_property = implication.conclusion + break + } } + + if (!new_properties.size) break + + for (const p of new_properties) deduced_satisfied_properties.add(p) } if (!contradictory_property) return null - // remove irrelevant implications + // build minimal contradiction proof - const relevant_properties = new Set([contradictory_property]) + const contradiction: string[] = [] - for (let i = used_implications.length - 1; i >= 0; i--) { - const { implication } = used_implications[i] - const is_relevant = relevant_properties.has(implication.conclusion) + const visited_properties = new Set() - if (is_relevant) { - used_implications[i].relevant = is_relevant - for (const p of implication.assumptions) { - if (!satisfied_properties.has(p)) relevant_properties.add(p) - } - } - } + function build_proof(property: string) { + if (visited_properties.has(property)) return + if (satisfied_properties.has(property)) return + visited_properties.add(property) - const relevant_implications = used_implications - .filter((item) => item.relevant) - .map((item) => item.implication) + const implication = deduction_dict[property] + if (!implication) throw new Error(`Missing deduction for property: ${property}`) - const contradiction: string[] = [] + for (const p of implication.assumptions) build_proof(p) - for (let i = 0; i < relevant_implications.length; i++) { - const implication = relevant_implications[i] - let segment = `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}` - if (i === relevant_implications.length - 1) segment += ` ↯` - contradiction.push(segment) + contradiction.push(stringify_implication(implication)) } + build_proof(contradictory_property) + return contradiction } @@ -145,6 +133,10 @@ function get_normalized_category_implications() { return implications } +function stringify_implication(implication: NormalizedCategoryImplication) { + return `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}` +} + export function get_missing_combinations() { const implications = get_normalized_category_implications() From 02c5d733efffb6e1db2d16dd81ef94739a2fffae Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 12 May 2026 14:08:57 +0200 Subject: [PATCH 5/5] small refactor --- src/lib/server/consistency.ts | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index d6cfc514a..ce09f3d14 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -69,13 +69,23 @@ function contradiction_worker( if (!contradictory_property) return null - // build minimal contradiction proof + return build_shortest_proof( + satisfied_properties, + deduction_dict, + contradictory_property, + ) +} - const contradiction: string[] = [] +function build_shortest_proof( + satisfied_properties: Set, + deduction_dict: Record, + target_property: string, +) { + const proof: string[] = [] const visited_properties = new Set() - function build_proof(property: string) { + function derive(property: string) { if (visited_properties.has(property)) return if (satisfied_properties.has(property)) return visited_properties.add(property) @@ -83,14 +93,14 @@ function contradiction_worker( const implication = deduction_dict[property] if (!implication) throw new Error(`Missing deduction for property: ${property}`) - for (const p of implication.assumptions) build_proof(p) + for (const p of implication.assumptions) derive(p) - contradiction.push(stringify_implication(implication)) + proof.push(stringify_implication(implication)) } - build_proof(contradictory_property) + derive(target_property) - return contradiction + return proof } function get_normalized_category_implications() {