nx_scene_compose_gate.nx source
↩ module page · 146 lines · 8307 B
1// nx_scene_compose_gate.nx -- PG10: DOES A SCENE COMPOSE OVER THE LIVE SOLVER, AND DOES AN IMPOSSIBLE ONE REFUSE BY NAME?
2//
3// SUBJECT: nx_part_solver_lib.ps_scene_compose (in-process). The rung's done-rule in its own words: a scene composes
4// over ps_solve with no second solver, and an unsatisfiable scene REFUSES by name. Every geometric claim below is
5// RECOMPUTED from the solver's own positions and extents, never read back from the composer's say-so, and every
6// value is emitted with gv_kv. Fixtures are in-memory strings, so the gate leaks no filesystem state.
7import "nx_syscalls.nx"
8import "nx_gate_verdict.nx"
9import "nx_part_solver_lib.nx"
10const SG_SITE_EX: i64 = 120
11const SG_SITE_EY: i64 = 120
12const SG_BAND_LO: i64 = 16 // max(hut ex 12, ey 10) + being r 2 + SC_GAP 2 -- the composer's own derivation
13const SG_BAND_HI: i64 = 56 // lo + SC_NEAR
14const SG_SCENE_PARTS: i64 = 12 // site + sea + hut + shed + 6 trees + 2 beings
15
16func sg_scene() -> *u8 {
17 return "# a beach scene: one site, the sea along +y, two buildings, a grove, two beings\nseed 7\nsite 120 120 40\nwater sea 120 30 0 90\nroom hut 12 10 8\nroom shed 8 8 6\ntree p1 9\ntree p2 11\ntree p3 7\ntree p4 10\ntree p5 8\ntree p6 9\nbeing ana 2\nbeing bea 2\nnear ana bea 4 30\n" as *u8
18}
19func sg_unsat() -> *u8 {
20 return "site 20 20 10\nroom a 18 18 8\nroom b 18 18 8\n" as *u8
21}
22func sg_badrow() -> *u8 {
23 return "site 20 20 10\ntower t 5\n" as *u8
24}
25func sg_abs(v: i64) -> i64 { if v < 0 { return 0 - v } return v }
26func sg_max(a: i64, b: i64) -> i64 { if a > b { return a } return b }
27// footprint separation of two parts on the ground plane, minus the gap the composer asked for
28func sg_sep(i: i64, j: i64) -> i64 {
29 let sx: i64 = sg_abs(ps_x(i) - ps_x(j)) - (ps_exx(i) + ps_exx(j))
30 let sy: i64 = sg_abs(ps_y(i) - ps_y(j)) - (ps_eyy(i) + ps_eyy(j))
31 return sg_max(sx, sy)
32}
33
34func main() -> i64 {
35 let ctr: *i64 = gv_ctr()
36 gv_head("=== NX-SCENE-COMPOSE gate (PG10): a scene composes over the live part solver, an impossible one refuses by name ===" as *u8)
37 let scene: *u8 = sg_scene()
38 let rc: i64 = ps_scene_compose(scene, ps_slen(scene))
39 // the beach scene's own numbers, captured NOW: the neg-control scenes below overwrite the solver's statics,
40 // and a values block read after them describes the refused scene, not the composed one (measured on run one)
41 let np0: i64 = ps_np()
42 let nc0: i64 = ps_scene_nc()
43 let cb0: i64 = ps_scene_len()
44 let res0: i64 = ps_resid()
45 gv_check("beach-scene-composes: ps_scene_compose returns SOLVED (1)" as *u8, (rc == 1) as i64, ctr)
46 gv_check_eq("the solver holds exactly the scene's parts (site + 11 solids)" as *u8, ps_np(), SG_SCENE_PARTS, ctr)
47 gv_check("the composer wrote rows and the solver loaded them (constraints > 0, rows > 0)" as *u8, ((ps_scene_nc() > 0) as i64) * ((ps_scene_len() > 0) as i64), ctr)
48 let site: i64 = ps_find("site" as *u8)
49 let sea: i64 = ps_find("sea" as *u8)
50 let hut: i64 = ps_find("hut" as *u8)
51 let shed: i64 = ps_find("shed" as *u8)
52 let ana: i64 = ps_find("ana" as *u8)
53 let bea: i64 = ps_find("bea" as *u8)
54 gv_check("every named part resolves in the solver" as *u8, ((site >= 0) as i64) * ((sea >= 0) as i64) * ((hut >= 0) as i64) * ((shed >= 0) as i64) * ((ana >= 0) as i64) * ((bea >= 0) as i64), ctr)
55 // envelope: every solid inside the site box (recomputed from positions and EFFECTIVE extents)
56 var inside: i64 = 1
57 var i: i64 = 0
58 while i < ps_np() {
59 if i != site { if i != sea {
60 if sg_abs(ps_x(i)) + ps_exx(i) > SG_SITE_EX + PS_TOL { inside = 0 }
61 if sg_abs(ps_y(i)) + ps_eyy(i) > SG_SITE_EY + PS_TOL { inside = 0 }
62 } }
63 i = i + 1
64 }
65 gv_check("every solid lies inside the site (recomputed against the site's half-extents)" as *u8, inside, ctr)
66 // no clip: every solid pair on overlapping storeys is separated on some ground axis by its gap
67 var clips: i64 = 0
68 var pairs: i64 = 0
69 var worst_sep: i64 = 1000000
70 i = 0
71 while i < ps_np() {
72 var j: i64 = i + 1
73 while j < ps_np() {
74 if i != site { if j != site { if ps_zoverlap(i, j) == 1 {
75 pairs = pairs + 1
76 var gap: i64 = SC_GAP
77 if i == sea { gap = 0 }
78 if j == sea { gap = 0 }
79 let sep: i64 = sg_sep(i, j) - gap
80 if sep < worst_sep { worst_sep = sep }
81 if sep < 0 - PS_TOL { clips = clips + 1 }
82 } } }
83 j = j + 1
84 }
85 i = i + 1
86 }
87 gv_check("no-solid-pair-clips (denominator bound: pairs > 0)" as *u8, ((clips == 0) as i64) * ((pairs > 0) as i64), ctr)
88 // the water is where it was GIVEN: the sea is attached at (0, 90)
89 gv_check("water-is-given-not-solved: the sea sits at its declared offset" as *u8, ((ps_x(sea) == 0) as i64) * ((ps_y(sea) == 90) as i64), ctr)
90 // rooms face the water: facing equals the cardinal direction from the room to the sea
91 var faces: i64 = 1
92 if ps_fx(hut) != ps_cardx(ps_x(sea) - ps_x(hut), ps_y(sea) - ps_y(hut)) { faces = 0 }
93 if ps_fy(hut) != ps_cardy(ps_x(sea) - ps_x(hut), ps_y(sea) - ps_y(hut)) { faces = 0 }
94 if ps_fx(shed) != ps_cardx(ps_x(sea) - ps_x(shed), ps_y(sea) - ps_y(shed)) { faces = 0 }
95 if ps_fy(shed) != ps_cardy(ps_x(sea) - ps_x(shed), ps_y(sea) - ps_y(shed)) { faces = 0 }
96 gv_check("buildings-face-the-water (facing == cardinal toward the sea, both rooms)" as *u8, faces, ctr)
97 // beings live near the first room, inside the band the composer derived
98 let dxa: i64 = ps_x(ana) - ps_x(hut)
99 let dya: i64 = ps_y(ana) - ps_y(hut)
100 let da: i64 = ps_isqrt(dxa*dxa + dya*dya)
101 gv_check("being-lives-near-its-house: dist(ana, hut) inside the derived band" as *u8, ((da >= SG_BAND_LO - PS_TOL) as i64) * ((da <= SG_BAND_HI + PS_TOL) as i64), ctr)
102 let dxb: i64 = ps_x(ana) - ps_x(bea)
103 let dyb: i64 = ps_y(ana) - ps_y(bea)
104 let db: i64 = ps_isqrt(dxb*dxb + dyb*dyb)
105 gv_check("explicit-near-row-holds: dist(ana, bea) inside 4..30" as *u8, ((db >= 4 - PS_TOL) as i64) * ((db <= 30 + PS_TOL) as i64), ctr)
106 // determinism: the same scene composes to the same positions
107 let hx: i64 = ps_x(hut)
108 let hy: i64 = ps_y(hut)
109 let p3: i64 = ps_find("p3" as *u8)
110 let p3x: i64 = ps_x(p3)
111 let p3y: i64 = ps_y(p3)
112 let rc2: i64 = ps_scene_compose(scene, ps_slen(scene))
113 let hut2: i64 = ps_find("hut" as *u8)
114 let p32: i64 = ps_find("p3" as *u8)
115 gv_check("determinism: composing twice places the hut and a tree at identical coordinates" as *u8, ((rc2 == 1) as i64) * ((ps_x(hut2) == hx) as i64) * ((ps_y(hut2) == hy) as i64) * ((ps_x(p32) == p3x) as i64) * ((ps_y(p32) == p3y) as i64), ctr)
116 // neg-control: an impossible scene refuses through the solver's own worst constraint
117 let un: *u8 = sg_unsat()
118 let rcu: i64 = ps_scene_compose(un, ps_slen(un))
119 var named: i64 = 0
120 if rcu == 0 { if ps_worst() >= 0 {
121 let k: i64 = ps_ckind(ps_worst())
122 if k == PS_K_NOCLIP { named = 1 }
123 if k == PS_K_ENVELOPE { named = 1 }
124 } }
125 gv_check("neg-control-unsatisfiable-scene-REFUSES: two 18-half rooms in a 20-half site return INCONSISTENT with noclip or envelope named" as *u8, named, ctr)
126 // neg-control: an unknown scene row is refused as grammar, not composed
127 let bad: *u8 = sg_badrow()
128 let rcb: i64 = ps_scene_compose(bad, ps_slen(bad))
129 gv_check_eq("neg-control-unknown-row-REFUSES: rc is -SC_E_PARSE" as *u8, rcb, 0 - SC_E_PARSE, ctr)
130 gv_values_head()
131 gv_kv("scene_rc" as *u8, rc)
132 gv_kv("parts" as *u8, np0)
133 gv_kv("constraints" as *u8, nc0)
134 gv_kv("composed_bytes" as *u8, cb0)
135 gv_kv("residual" as *u8, res0)
136 gv_kv("pairs_checked" as *u8, pairs)
137 gv_kv("worst_pair_separation_minus_gap" as *u8, worst_sep)
138 gv_kv("hut_x" as *u8, hx)
139 gv_kv("hut_y" as *u8, hy)
140 gv_kv("dist_ana_hut" as *u8, da)
141 gv_kv("dist_ana_bea" as *u8, db)
142 gv_kv("unsat_rc" as *u8, rcu)
143 gv_kv("unsat_worst_idx" as *u8, ps_worst())
144 gv_kv("badrow_rc" as *u8, rcb)
145 return gv_verdict("NX-SCENE-COMPOSE" as *u8, ctr, "a scene is one constraint set the live solver places; an impossible one is refused by its worst constraint" as *u8)
146}