From 19652ec48be4c6faf3f7815a9281b611aed94727 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Thu, 12 Mar 2026 15:37:53 +0100 Subject: changed to float --- xor.in | 110 ++++++++++++++++++++++++++++++++--------------------------------- 1 file changed, 55 insertions(+), 55 deletions(-) (limited to 'xor.in') diff --git a/xor.in b/xor.in index a382883..6a71e7b 100644 --- a/xor.in +++ b/xor.in @@ -4,8 +4,8 @@ // Dup: duplicates other agents recursively // Implemented -// Linear(x, int q, int r): represent "q*x + r" -// Concrete(int k): represent a concrete value k +// Linear(x, float q, float r): represent "q*x + r" +// Concrete(float k): represent a concrete value k // Symbolic(id): represent the variable id // Add(out, b): represent the addition (has various steps AddCheckLinear/AddCheckConcrete) // Mul(out, b): represent the multiplication (has various steps MulCheckLinear/MulCheckConcrete) @@ -15,55 +15,55 @@ // TODO: add range information to enable ReLU elimination // Rules -Linear(x, int q, int r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r); +Linear(x, float q, float r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r); -Concrete(int k) >< Add(out, b) +Concrete(float k) >< Add(out, b) | k == 0 => out ~ b | _ => b ~ AddCheckConcrete(out, k); -Linear(y, int s, int t) >< AddCheckLinear(out, x, int q, int r) +Linear(y, float s, float t) >< AddCheckLinear(out, x, float q, float r) | (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser | (s == 0) && (t == 0) => Linear(x, q, r) ~ Materialize(out), y ~ Eraser | (q == 0) && (r == 0) => (*L)Linear(y, s, t) ~ Materialize(out), x ~ Eraser | _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0); -Concrete(int j) >< AddCheckLinear(out, x, int q, int r) => out ~ Linear(x, q, r + j); +Concrete(float j) >< AddCheckLinear(out, x, float q, float r) => out ~ Linear(x, q, r + j); -Linear(y, int s, int t) >< AddCheckConcrete(out, int k) => out ~ Linear(y, s, t + k); +Linear(y, float s, float t) >< AddCheckConcrete(out, float k) => out ~ Linear(y, s, t + k); -Concrete(int j) >< AddCheckConcrete(out, int k) +Concrete(float j) >< AddCheckConcrete(out, float k) | j == 0 => out ~ Concrete(k) | _ => out ~ Concrete(k + j); -Linear(x, int q, int r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r); +Linear(x, float q, float r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r); -Concrete(int k) >< Mul(out, b) +Concrete(float k) >< Mul(out, b) | k == 0 => b ~ Eraser, out ~ (*L)Concrete(0) | k == 1 => out ~ b | _ => b ~ MulCheckConcrete(out, k); -Linear(y, int s, int t) >< MulCheckLinear(out, x, int q, int r) +Linear(y, float s, float t) >< MulCheckLinear(out, x, float q, float r) | (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser | (s == 0) && (t == 0) => Linear(x, q, r) ~ Materialize(out), y ~ Eraser | (q == 0) && (r == 0) => (*L)Linear(y, s, t) ~ Materialize(out), x ~ Eraser | _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0); -Concrete(int j) >< MulCheckLinear(out, x, int q, int r) => out ~ Linear(x, q * j, r * j); +Concrete(float j) >< MulCheckLinear(out, x, float q, float r) => out ~ Linear(x, q * j, r * j); -Linear(y, int s, int t) >< MulCheckConcrete(out, int k) => out ~ Linear(y, s * k, t * k); +Linear(y, float s, float t) >< MulCheckConcrete(out, float k) => out ~ Linear(y, s * k, t * k); -Concrete(int j) >< MulCheckConcrete(out, int k) +Concrete(float j) >< MulCheckConcrete(out, float k) | j == 0 => out ~ Concrete(0) | j == 1 => out ~ Concrete(k) | _ => out ~ Concrete(k * j); -Linear(x, int q, int r) >< ReLU(out) => (*L)Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0); +Linear(x, float q, float r) >< ReLU(out) => (*L)Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0); -Concrete(int k) >< ReLU(out) +Concrete(float k) >< ReLU(out) | k > 0 => out ~ (*L)Concrete(k) | _ => out ~ Concrete(0); -Linear(x, int q, int r) >< Materialize(out) +Linear(x, float q, float r) >< Materialize(out) | (q == 0) => out ~ Concrete(r), x ~ Eraser | (q == 1) && (r == 0) => out ~ x | (q == 1) && (r != 0) => out ~ TermAdd(x, Concrete(r)) @@ -72,35 +72,35 @@ Linear(x, int q, int r) >< Materialize(out) // Network A -Dup(v0, Dup(v1, Dup(v2, v3))) ~ Linear(Symbolic(0), 1, 0); -Mul(v4, Concrete(-729)) ~ v0; -Add(v5, v4) ~ Concrete(732); -Mul(v6, Concrete(707)) ~ v1; -Add(v7, v6) ~ Concrete(106); -Mul(v8, Concrete(-577)) ~ v2; -Add(v9, v8) ~ Concrete(-502); -Mul(v10, Concrete(1070)) ~ v3; -Add(v11, v10) ~ Concrete(-1068); -Dup(v12, Dup(v13, Dup(v14, v15))) ~ Linear(Symbolic(1), 1, 0); -Mul(v16, Concrete(-725)) ~ v12; +Dup(v0, Dup(v1, Dup(v2, v3))) ~ Linear(Symbolic(X_0), 1.0, 0.0); +Mul(v4, Concrete(1.249051570892334)) ~ v0; +Add(v5, v4) ~ Concrete(-2.076689270325005e-05); +Mul(v6, Concrete(0.8312496542930603)) ~ v1; +Add(v7, v6) ~ Concrete(-0.8312351703643799); +Mul(v8, Concrete(0.9251033663749695)) ~ v2; +Add(v9, v8) ~ Concrete(-0.9250767230987549); +Mul(v10, Concrete(0.3333963453769684)) ~ v3; +Add(v11, v10) ~ Concrete(0.05585573986172676); +Dup(v12, Dup(v13, Dup(v14, v15))) ~ Linear(Symbolic(X_1), 1.0, 0.0); +Mul(v16, Concrete(0.8467237949371338)) ~ v12; Add(v17, v16) ~ v5; -Mul(v18, Concrete(708)) ~ v13; +Mul(v18, Concrete(0.8312491774559021)) ~ v13; Add(v19, v18) ~ v7; -Mul(v20, Concrete(220)) ~ v14; +Mul(v20, Concrete(0.9251176118850708)) ~ v14; Add(v21, v20) ~ v9; -Mul(v22, Concrete(1066)) ~ v15; +Mul(v22, Concrete(1.084873080253601)) ~ v15; Add(v23, v22) ~ v11; ReLU(v24) ~ v17; ReLU(v25) ~ v19; ReLU(v26) ~ v21; ReLU(v27) ~ v23; -Mul(v28, Concrete(-642)) ~ v24; -Add(v29, v28) ~ Concrete(390); -Mul(v30, Concrete(753)) ~ v25; +Mul(v28, Concrete(0.7005411982536316)) ~ v24; +Add(v29, v28) ~ Concrete(-0.02095046266913414); +Mul(v30, Concrete(-0.9663007259368896)) ~ v25; Add(v31, v30) ~ v29; -Mul(v32, Concrete(235)) ~ v26; +Mul(v32, Concrete(-1.293721079826355)) ~ v26; Add(v33, v32) ~ v31; -Mul(v34, Concrete(-1440)) ~ v27; +Mul(v34, Concrete(0.3750816583633423)) ~ v27; Add(v35, v34) ~ v33; Materialize(result0) ~ v35; result0; @@ -108,35 +108,35 @@ free ifce; // Network B -Dup(v0, Dup(v1, Dup(v2, v3))) ~ Linear(Symbolic(0), 1, 0); -Mul(v4, Concrete(-181)) ~ v0; -Add(v5, v4) ~ Concrete(-142); -Mul(v6, Concrete(-1061)) ~ v1; -Add(v7, v6) ~ Concrete(1050); -Mul(v8, Concrete(1181)) ~ v2; -Add(v9, v8) ~ Concrete(-568); -Mul(v10, Concrete(-627)) ~ v3; -Add(v11, v10) ~ Concrete(1236); -Dup(v12, Dup(v13, Dup(v14, v15))) ~ Linear(Symbolic(1), 1, 0); -Mul(v16, Concrete(-609)) ~ v12; +Dup(v0, Dup(v1, Dup(v2, v3))) ~ Linear(Symbolic(X_0), 1.0, 0.0); +Mul(v4, Concrete(1.1727254390716553)) ~ v0; +Add(v5, v4) ~ Concrete(-0.005158121697604656); +Mul(v6, Concrete(1.1684346199035645)) ~ v1; +Add(v7, v6) ~ Concrete(-1.1664382219314575); +Mul(v8, Concrete(-0.2502972185611725)) ~ v2; +Add(v9, v8) ~ Concrete(-0.10056735575199127); +Mul(v10, Concrete(-0.6796815395355225)) ~ v3; +Add(v11, v10) ~ Concrete(-0.32640340924263); +Dup(v12, Dup(v13, Dup(v14, v15))) ~ Linear(Symbolic(X_1), 1.0, 0.0); +Mul(v16, Concrete(1.1758666038513184)) ~ v12; Add(v17, v16) ~ v5; -Mul(v18, Concrete(-1058)) ~ v13; +Mul(v18, Concrete(1.1700055599212646)) ~ v13; Add(v19, v18) ~ v7; -Mul(v20, Concrete(1404)) ~ v14; +Mul(v20, Concrete(0.02409248612821102)) ~ v14; Add(v21, v20) ~ v9; -Mul(v22, Concrete(-311)) ~ v15; +Mul(v22, Concrete(-0.43328654766082764)) ~ v15; Add(v23, v22) ~ v11; ReLU(v24) ~ v17; ReLU(v25) ~ v19; ReLU(v26) ~ v21; ReLU(v27) ~ v23; -Mul(v28, Concrete(-313)) ~ v24; -Add(v29, v28) ~ Concrete(1112); -Mul(v30, Concrete(-1571)) ~ v25; +Mul(v28, Concrete(0.8594199419021606)) ~ v24; +Add(v29, v28) ~ Concrete(7.867255291671427e-09); +Mul(v30, Concrete(-1.7184218168258667)) ~ v25; Add(v31, v30) ~ v29; -Mul(v32, Concrete(-615)) ~ v26; +Mul(v32, Concrete(-0.207244873046875)) ~ v26; Add(v33, v32) ~ v31; -Mul(v34, Concrete(434)) ~ v27; +Mul(v34, Concrete(-0.14912307262420654)) ~ v27; Add(v35, v34) ~ v33; Materialize(result0) ~ v35; result0; \ No newline at end of file -- cgit v1.2.3