Skip to content

Commit ff0afc8

Browse files
committed
Add independent C-based check tests for example outputs.
1 parent efb7952 commit ff0afc8

12 files changed

+301050
-1
lines changed
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <stdio.h>
2+
#include <stdlib.h>
3+
4+
int main(void) {
5+
if (printf("@prefix : <http://eulersharp.sourceforge.net/2009/12dtb/test#> .\n\n") < 0) {
6+
return EXIT_FAILURE;
7+
}
8+
9+
for (int i = 1; i <= 100000; i++) {
10+
if (printf(":ind a :N%d .\n:ind a :I%d .\n:ind a :J%d .\n", i, i, i) < 0) {
11+
return EXIT_FAILURE;
12+
}
13+
}
14+
15+
if (printf(":ind a :A2 .\n:test :is true .\n") < 0) {
16+
return EXIT_FAILURE;
17+
}
18+
19+
return EXIT_SUCCESS;
20+
}

examples/check/input/gps.c

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
#include <stdio.h>
2+
#include <stdlib.h>
3+
#include <string.h>
4+
5+
typedef struct {
6+
const char *from;
7+
const char *to;
8+
const char *action;
9+
double duration;
10+
double cost;
11+
double belief;
12+
double comfort;
13+
} Edge;
14+
15+
typedef struct {
16+
const char *actions[8];
17+
int action_count;
18+
double duration;
19+
double cost;
20+
double belief;
21+
double comfort;
22+
} Path;
23+
24+
static const Edge EDGES[] = {
25+
{"Gent", "Brugge", ":drive_gent_brugge", 1500.0, 0.006, 0.96, 0.99},
26+
{"Gent", "Kortrijk", ":drive_gent_kortrijk", 1600.0, 0.007, 0.96, 0.99},
27+
{"Kortrijk", "Brugge", ":drive_kortrijk_brugge", 1600.0, 0.007, 0.96, 0.99},
28+
{"Brugge", "Oostende", ":drive_brugge_oostende", 900.0, 0.004, 0.98, 1.0}
29+
};
30+
31+
static void print_decimal(double value) {
32+
char buf[64];
33+
snprintf(buf, sizeof(buf), "%.15f", value);
34+
char *p = buf + strlen(buf) - 1;
35+
while (p > buf && *p == '0') {
36+
*p-- = '\0';
37+
}
38+
if (p > buf && *p == '.') {
39+
*p = '\0';
40+
}
41+
printf("\"%s\"^^xsd:decimal", buf);
42+
}
43+
44+
static int contains_city(const char *visited[], int visited_count, const char *city) {
45+
for (int i = 0; i < visited_count; ++i) {
46+
if (strcmp(visited[i], city) == 0) {
47+
return 1;
48+
}
49+
}
50+
return 0;
51+
}
52+
53+
static void emit_path(const Path *path) {
54+
printf(":i1 gps:path ((");
55+
for (int i = 0; i < path->action_count; ++i) {
56+
if (i > 0) {
57+
putchar(' ');
58+
}
59+
fputs(path->actions[i], stdout);
60+
}
61+
printf(") ");
62+
print_decimal(path->duration);
63+
printf(" ");
64+
print_decimal(path->cost);
65+
printf(" ");
66+
print_decimal(path->belief);
67+
printf(" ");
68+
print_decimal(path->comfort);
69+
printf(") .\n");
70+
}
71+
72+
static void dfs(const char *current,
73+
const char *goal,
74+
const char *visited[],
75+
int visited_count,
76+
Path *path) {
77+
if (strcmp(current, goal) == 0) {
78+
emit_path(path);
79+
return;
80+
}
81+
82+
for (size_t i = 0; i < sizeof(EDGES) / sizeof(EDGES[0]); ++i) {
83+
const Edge *e = &EDGES[i];
84+
if (strcmp(e->from, current) != 0) {
85+
continue;
86+
}
87+
if (contains_city(visited, visited_count, e->to)) {
88+
continue;
89+
}
90+
91+
path->actions[path->action_count++] = e->action;
92+
path->duration += e->duration;
93+
path->cost += e->cost;
94+
path->belief *= e->belief;
95+
path->comfort *= e->comfort;
96+
97+
const char *next_visited[16];
98+
for (int j = 0; j < visited_count; ++j) {
99+
next_visited[j] = visited[j];
100+
}
101+
next_visited[visited_count] = e->to;
102+
103+
dfs(e->to, goal, next_visited, visited_count + 1, path);
104+
105+
path->action_count--;
106+
path->duration -= e->duration;
107+
path->cost -= e->cost;
108+
path->belief /= e->belief;
109+
path->comfort /= e->comfort;
110+
}
111+
}
112+
113+
int main(void) {
114+
puts("@prefix : <https://eyereasoner.github.io/eye/reasoning#> .");
115+
puts("@prefix gps: <https://eyereasoner.github.io/eye/reasoning/gps/gps-schema#> .");
116+
puts("@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .");
117+
putchar('\n');
118+
119+
Path path;
120+
memset(&path, 0, sizeof(path));
121+
path.belief = 1.0;
122+
path.comfort = 1.0;
123+
124+
const char *visited[] = {"Gent"};
125+
dfs("Gent", "Oostende", visited, 1, &path);
126+
return 0;
127+
}
Lines changed: 148 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,148 @@
1+
#include <math.h>
2+
#include <stdbool.h>
3+
#include <stdio.h>
4+
#include <string.h>
5+
6+
typedef struct {
7+
const char *name;
8+
int canonicalTripleCount;
9+
int spoIndexTripleCount;
10+
int bloomBits;
11+
int hashFunctions;
12+
int negativeLookupsPerBatch;
13+
double fpRateBudget;
14+
double extraExactLookupsBudget;
15+
const char *exactTranscendentalSymbol;
16+
double certifiedLambda;
17+
double expMinusLambdaLower;
18+
double expMinusLambdaUpper;
19+
const char *maybePositivePolicy;
20+
const char *definiteNegativePolicy;
21+
} Artifact;
22+
23+
typedef struct {
24+
bool parameterSanity;
25+
bool indexAgreement;
26+
double lambda;
27+
bool expIntervalCertificate;
28+
double fpRateLower;
29+
double fpRateUpper;
30+
bool withinFpRateBudget;
31+
double expectedExtraExactLookupsUpper;
32+
bool withinExactLookupBudget;
33+
bool accepted;
34+
} Evaluation;
35+
36+
static bool same_policy(const char *lhs, const char *rhs) {
37+
return strcmp(lhs, rhs) == 0;
38+
}
39+
40+
static Evaluation evaluate_artifact(const Artifact *a) {
41+
Evaluation ev;
42+
memset(&ev, 0, sizeof(ev));
43+
44+
ev.parameterSanity =
45+
a->canonicalTripleCount > 0 &&
46+
a->spoIndexTripleCount > 0 &&
47+
a->bloomBits > 0 &&
48+
a->hashFunctions > 0 &&
49+
a->negativeLookupsPerBatch > 0 &&
50+
a->fpRateBudget > 0.0 &&
51+
a->extraExactLookupsBudget > 0.0;
52+
53+
ev.indexAgreement = (a->canonicalTripleCount == a->spoIndexTripleCount);
54+
55+
if (ev.parameterSanity) {
56+
ev.lambda = ((double)a->hashFunctions * (double)a->canonicalTripleCount) /
57+
(double)a->bloomBits;
58+
}
59+
60+
ev.expIntervalCertificate =
61+
ev.lambda > 0.0 &&
62+
a->certifiedLambda == ev.lambda &&
63+
a->expMinusLambdaLower < a->expMinusLambdaUpper &&
64+
a->expMinusLambdaLower > 0.0 &&
65+
a->expMinusLambdaUpper < 1.0;
66+
67+
if (ev.expIntervalCertificate) {
68+
const double oneMinusLo = 1.0 - a->expMinusLambdaUpper;
69+
const double oneMinusHi = 1.0 - a->expMinusLambdaLower;
70+
ev.fpRateLower = pow(oneMinusLo, a->hashFunctions);
71+
ev.fpRateUpper = pow(oneMinusHi, a->hashFunctions);
72+
}
73+
74+
ev.withinFpRateBudget =
75+
ev.fpRateUpper > 0.0 &&
76+
ev.fpRateUpper < a->fpRateBudget;
77+
78+
ev.expectedExtraExactLookupsUpper =
79+
(double)a->negativeLookupsPerBatch * ev.fpRateUpper;
80+
81+
ev.withinExactLookupBudget =
82+
ev.expectedExtraExactLookupsUpper > 0.0 &&
83+
ev.expectedExtraExactLookupsUpper < a->extraExactLookupsBudget;
84+
85+
ev.accepted =
86+
ev.parameterSanity &&
87+
ev.indexAgreement &&
88+
ev.expIntervalCertificate &&
89+
ev.withinFpRateBudget &&
90+
ev.withinExactLookupBudget &&
91+
same_policy(a->maybePositivePolicy, ":ConfirmAgainstCanonicalGraph") &&
92+
same_policy(a->definiteNegativePolicy, ":ReturnAbsent");
93+
94+
return ev;
95+
}
96+
97+
int main(void) {
98+
const Artifact artifact = {
99+
.name = ":artifact",
100+
.canonicalTripleCount = 1200,
101+
.spoIndexTripleCount = 1200,
102+
.bloomBits = 16384,
103+
.hashFunctions = 7,
104+
.negativeLookupsPerBatch = 50000,
105+
.fpRateBudget = 0.002,
106+
.extraExactLookupsBudget = 100.0,
107+
.exactTranscendentalSymbol = "exp(-k*n/m)",
108+
.certifiedLambda = 0.5126953125,
109+
.expMinusLambdaLower = 0.5988792348,
110+
.expMinusLambdaUpper = 0.5988792349,
111+
.maybePositivePolicy = ":ConfirmAgainstCanonicalGraph",
112+
.definiteNegativePolicy = ":ReturnAbsent"
113+
};
114+
115+
const Evaluation ev = evaluate_artifact(&artifact);
116+
117+
printf("@prefix : <http://example.org/high-trust-rdf#> .\n");
118+
printf("@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .\n\n");
119+
120+
if (ev.expIntervalCertificate) {
121+
printf(":result :expIntervalCertificate :CertifiedDecimalInterval .\n");
122+
}
123+
124+
if (ev.accepted) {
125+
printf(":result :summary (\"parameter-sanity\" true ");
126+
printf("\"index-agreement\" true ");
127+
printf("\"transcendental\" \"%s\" ", artifact.exactTranscendentalSymbol);
128+
printf("\"lambda\" \"%.10f\"^^xsd:decimal ", ev.lambda);
129+
printf("\"certified-lambda\" %.10f ", artifact.certifiedLambda);
130+
printf("\"exp-lower\" %.10f ", artifact.expMinusLambdaLower);
131+
printf("\"exp-upper\" %.10f ", artifact.expMinusLambdaUpper);
132+
printf("\"fp-lower\" \"%.19f\"^^xsd:decimal ", ev.fpRateLower);
133+
printf("\"fp-upper\" \"%.19f\"^^xsd:decimal ", ev.fpRateUpper);
134+
printf("\"expected-extra-exact-lookups-upper\" \"%.14f\"^^xsd:decimal ",
135+
ev.expectedExtraExactLookupsUpper);
136+
printf("\"decision\" :AcceptForHighTrustUse) .\n");
137+
}
138+
139+
if (ev.withinExactLookupBudget) {
140+
printf(":result :withinExactLookupBudget true .\n");
141+
}
142+
143+
if (ev.withinFpRateBudget) {
144+
printf(":result :withinFpRateBudget true .\n");
145+
}
146+
147+
return 0;
148+
}

0 commit comments

Comments
 (0)