nx_inst_gen.nx source
↩ module page · 88 lines · 3402 B
1// nx_inst_gen.nx -- instance generation (Inst-Gen).
2//
3// Per Vampire-displacement roadmap Phase 2. Korovin + Voronkov 2003
4// alternative to resolution: instead of resolving complementary
5// literals away (producing a single resolvent), INSTANTIATE both
6// clauses with the unifier (producing two more-specific clauses).
7//
8// The downstream SAT-coupled prover (iProver, Vampire+SAT) then
9// works on ground instances to prove UNSAT. Inst-Gen excels at
10// problems with large finite Herbrand universes where resolution
11// blows up but ground reasoning succeeds.
12//
13// Standard formulation:
14//
15// C ∨ L D ∨ ¬L' σ = mgu(L, L')
16// ----------------------
17// (C ∨ L)σ (D ∨ ¬L')σ
18//
19// Both resulting clauses keep their full literal sets -- σ just
20// makes them more specific. No literals are removed. This is the
21// crucial difference from resolution.
22//
23// API:
24// nx_inst_gen(c1, i, c2, j, c1_out, c2_out) -> *NxResult
25//
26// Caller allocates c1_out + c2_out; primitive populates both with
27// the σ-applied versions.
28
29// nx_safety_envelope:
30// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
31// sil_target: SIL1
32// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
33// verdict: NOT_YET_EVALUATED
34
35import "nx_syscalls.nx"
36import "nx_runtime.nx"
37import "nx_tier.nx"
38import "nx_result.nx"
39import "nx_unify.nx"
40import "nx_resolution.nx"
41
42// Apply substitution to every literal of `c`, append to `out`.
43func nx_inst_apply_clause(c: *Clause, sigma: *Subst, out: *Clause) -> *NxResult {
44 var k: nx_int = 0
45 while k < c.n_lits {
46 let lk: *Literal = nx_clause_lit_at(c, k)
47 let lk_sub: *Literal = nx_lit_apply_subst(lk, sigma)
48 let r: *NxResult = nx_clause_add(out, lk_sub)
49 if nx_result_is_err(r) == 1 { return r }
50 k = k + 1
51 }
52 return nx_result_ok(out.n_lits)
53}
54
55// Main entry. Returns Result<n_lits_total, NX_ERR_*>:
56// NX_ERR_OUT_OF_RANGE -- bad index
57// NX_ERR_TAG_MISMATCH -- literals not complementary (same polarity)
58// underlying nx_unify err codes if atoms don't unify
59//
60// On success, c1_out has c1·σ and c2_out has c2·σ. The combined
61// literal count of both is returned.
62func nx_inst_gen(c1: *Clause, i: nx_int,
63 c2: *Clause, j: nx_int,
64 c1_out: *Clause, c2_out: *Clause) -> *NxResult {
65 if i < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
66 if i >= c1.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
67 if j < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
68 if j >= c2.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
69
70 let l1: *Literal = nx_clause_lit_at(c1, i)
71 let l2: *Literal = nx_clause_lit_at(c2, j)
72
73 // Must be complementary (opposite polarities).
74 if l1.sign != (0 - l2.sign) { return nx_result_err(NX_ERR_TAG_MISMATCH) }
75
76 // Unify the atoms.
77 let sigma: *Subst = nx_subst_new()
78 let r_un: *NxResult = nx_unify(l1.atom, l2.atom, sigma)
79 if nx_result_is_err(r_un) == 1 { return r_un }
80
81 // Instantiate both clauses (entire literal sets, no removal).
82 let r1: *NxResult = nx_inst_apply_clause(c1, sigma, c1_out)
83 if nx_result_is_err(r1) == 1 { return r1 }
84 let r2: *NxResult = nx_inst_apply_clause(c2, sigma, c2_out)
85 if nx_result_is_err(r2) == 1 { return r2 }
86
87 return nx_result_ok(c1_out.n_lits + c2_out.n_lits)
88}