///|
/// Nonnegative multipliers of input-derived chemical constraints. Their exact
/// combination is 0 <= a negative number, so the declared study has no history.
pub(all) struct ConflictTerm {
constraint : String
weight : Exact
} derive(Debug, ToJson)
///|
pub extend ConflictTerm with @debug.Debug::{to_repr}
///|
pub extend ConflictTerm with @json.ToJson::{to_json}
///|
/// Compatible includes one joint history. Conflict includes a checkable linear
/// contradiction. ResourceLimit is undecided and never means compatible.
pub(all) struct AliquotAssessment {
status : String
history : HandlingHistory?
conflict : Array[ConflictTerm]
parameter_count : Int32
constraint_count : Int32
diagnostics : Array[String]
} derive(Debug, ToJson)
///|
pub extend AliquotAssessment with @debug.Debug::{to_repr}
///|
pub extend AliquotAssessment with @json.ToJson::{to_json}
///|
priv struct ProofRow {
coefficients : Array[R]
upper : R
weights : Array[R]
}
///|
priv struct Level {
variable : Int32
rows : Array[ProofRow]
}
///|
priv enum Elimination {
Point(Array[R])
Impossible(Array[R])
Limit(String)
}
///|
fn sum_products(a : Array[R], b : Array[R]) -> R {
let mut value = r(0)
for i = 0; i < a.length(); i = i + 1 {
value = value + a[i] * b[i]
}
value
}
///|
fn multiply_row(row : ProofRow, factor : R) -> ProofRow {
{
coefficients: row.coefficients.map(fn(x) { x * factor }),
upper: row.upper * factor,
weights: row.weights.map(fn(x) { x * factor }),
}
}
///|
fn normalized(row : ProofRow) -> ProofRow {
for value in row.coefficients {
if value != r(0) {
let magnitude = if value < r(0) { -value } else { value }
return multiply_row(row, r(1) / magnitude)
}
}
row
}
///|
fn insert_row(rows : Array[ProofRow], row : ProofRow) -> Unit {
let row = normalized(row)
for i = 0; i < rows.length(); i = i + 1 {
if rows[i].coefficients == row.coefficients {
if row.upper < rows[i].upper {
rows[i] = row
}
return
}
}
if row.coefficients.any(fn(x) { x != r(0) }) || row.upper < r(0) {
rows.push(row)
}
}
///|
fn large_fraction(x : R) -> Bool {
x.n.bit_length() > 2048 || x.d.bit_length() > 2048
}
///|
// Fourier-Motzkin is a known elimination method. It is deliberately internal:
// callers provide chemical histories, never arbitrary linear programs.
fn eliminate(rows : Array[Row], dimension : Int32) -> Elimination {
let mut current : Array[ProofRow] = []
for i = 0; i < rows.length(); i = i + 1 {
insert_row(current, {
coefficients: rows[i].coefficients,
upper: rows[i].upper,
weights: Array::makei(rows.length(), fn(j) {
if i == j {
r(1)
} else {
r(0)
}
}),
})
}
let remaining = Array::make(dimension, true)
let levels : Array[Level] = []
for pass = 0; pass <= dimension; pass = pass + 1 {
for row in current {
if large_fraction(row.upper) ||
row.coefficients.any(large_fraction) ||
row.weights.any(large_fraction) {
return Limit(
"normalized exact fraction size budget exceeded; study remains undecided",
)
}
if !row.coefficients.any(fn(x) { x != r(0) }) && row.upper < r(0) {
return Impossible(row.weights)
}
}
if pass == dimension {
break
}
let mut variable = -1
let mut best = 1000000000
for i = 0; i < dimension; i = i + 1 {
if remaining[i] {
let mut pos = 0
let mut neg = 0
for row in current {
if row.coefficients[i] > r(0) {
pos = pos + 1
}
if row.coefficients[i] < r(0) {
neg = neg + 1
}
}
let cost = pos * neg
if cost < best {
best = cost
variable = i
}
}
}
if variable < 0 || best > 20000 || current.length() > 2048 {
return Limit("exact elimination budget exceeded; study remains undecided")
}
levels.push({ variable, rows: current, })
remaining[variable] = false
let next : Array[ProofRow] = []
let positive = current.filter(fn(row) { row.coefficients[variable] > r(0) })
let negative = current.filter(fn(row) { row.coefficients[variable] < r(0) })
for row in current {
if row.coefficients[variable] == r(0) {
insert_row(next, row)
}
}
for p in positive {
let a = multiply_row(p, r(1) / p.coefficients[variable])
for n in negative {
let b = multiply_row(n, -r(1) / n.coefficients[variable])
let row = ProofRow::{
coefficients: Array::makei(dimension, fn(i) {
a.coefficients[i] + b.coefficients[i]
}),
upper: a.upper + b.upper,
weights: Array::makei(rows.length(), fn(i) {
a.weights[i] + b.weights[i]
}),
}
if large_fraction(row.upper) ||
row.coefficients.any(large_fraction) ||
row.weights.any(large_fraction) {
return Limit(
"exact fraction size budget exceeded; study remains undecided",
)
}
if !row.coefficients.any(fn(x) { x != r(0) }) && row.upper < r(0) {
return Impossible(row.weights)
}
insert_row(next, row)
if next.length() > 2048 {
return Limit(
"projected constraint budget exceeded; study remains undecided",
)
}
}
}
current = next
}
let values = Array::make(dimension, r(0))
for li = levels.length() - 1; li >= 0; li = li - 1 {
let level = levels[li]
let index = level.variable
let mut lower : R? = None
let mut upper : R? = None
for row in level.rows {
let coefficient = row.coefficients[index]
if coefficient == r(0) {
continue
}
let limit = (row.upper - sum_products(row.coefficients, values)) /
coefficient
if coefficient > r(0) {
upper = Some(
match upper {
Some(old) => if limit < old { limit } else { old }
None => limit
},
)
} else {
lower = Some(
match lower {
Some(old) => if limit > old { limit } else { old }
None => limit
},
)
}
}
values[index] = match (lower, upper) {
(Some(lo), Some(hi)) => {
if lo > hi {
return Limit("internal reconstruction disagreement")
}
(lo + hi) / r(2)
}
(Some(lo), None) => lo
(None, Some(hi)) => hi
(None, None) => r(0)
}
if large_fraction(values[index]) {
return Limit(
"reconstructed exact fraction size budget exceeded; study remains undecided",
)
}
}
for row in rows {
if sum_products(row.coefficients, values) > row.upper {
return Limit("reconstructed history failed exact input-constraint replay")
}
}
Point(values)
}
///|
fn assess_compiled(compiled : Compiled) -> AliquotAssessment {
let (status, h, conflict, diagnostic) = match
eliminate(compiled.rows, compiled.parameters.length()) {
Point(values) =>
(
"Compatible",
Some(history(compiled, values)),
[],
"One shared source and handling history satisfies every declared assay bound exactly.",
)
Impossible(weights) => {
let terms : Array[ConflictTerm] = []
for i = 0; i < weights.length(); i = i + 1 {
if weights[i] != r(0) {
terms.push({
constraint: compiled.rows[i].id,
weight: exact(weights[i]),
})
}
}
(
"Conflict",
None,
terms,
"No common history exists under the declared five-inventory model.",
)
}
Limit(reason) => ("ResourceLimit", None, [], reason)
}
{
status,
history: h,
conflict,
parameter_count: compiled.parameters.length(),
constraint_count: compiled.rows.length(),
diagnostics: [
diagnostic, "Conditional on declared volumes, complete counterions, perfect mixing and the listed processes. This is not a pH, equilibrium, kinetic or experimental prediction.",
],
}
}
///|
/// Reconcile every bottle simultaneously, retaining the same uncertain source
/// and upstream dose in all descendants. Marginal interval agreement is weaker.
pub fn reconcile_aliquots(
study : AliquotStudy,
) -> Result[AliquotAssessment, String] {
match compile_study(study) {
Ok(compiled) => Ok(assess_compiled(compiled))
Err(error) => Err(error)
}
}