3. What are we counting?

A backup configuration has local storage L, remote storage R, encryption E, and notifications N. The rules are (L ∨ R) ∧ (¬R ∨ E); notifications are optional. Three similar operations answer different questions: count configurations that match a choice, substitute its value into the rules, or count only selected options.

enum { LOCAL = 1, REMOTE, ENCRYPTED, NOTIFICATIONS };
TididiVtree *vtree = NULL;
check(tididi_vtree_balanced(4, &vtree));
const int64_t destinations[] = {LOCAL, REMOTE}, encryption[] = {-REMOTE, ENCRYPTED};
TididiCircuit *a = NULL, *b = NULL, *rules = NULL;
check(tididi_clause(vtree, destinations, 2, &a, NULL));
check(tididi_clause(vtree, encryption, 2, &b, NULL));
check(tididi_and(a, b, &rules, NULL));
printf("Valid configurations: %" PRIu64 "\n", count(rules));

Output:

Valid configurations: 8

3.1. Keep configurations consistent with a choice

Selecting remote backups means counting rules ∧ R. Conjunction creates that set; a counter answers the same question while retaining its counting cache:

const int64_t remote_choice[] = {REMOTE};
TididiCircuit *remote = NULL, *selected = NULL, *rules_copy = copy(rules);
check(tididi_literal(vtree, REMOTE, &remote, NULL));
check(tididi_and(rules_copy, remote, &selected, NULL));
printf("With remote backups: %" PRIu64 "\n", count(selected));
TididiCounter *counter = NULL;
TididiCircuit *counter_input = copy(rules);
check(tididi_counter(counter_input, &counter));
check(tididi_counter_observe(counter, remote_choice, 1));
uint64_t matching = 0;
check(tididi_counter_model_count(counter, &matching, NULL));
printf("Observed remote backups: %" PRIu64 "\n", matching);

Output:

With remote backups: 4
Observed remote backups: 4

Remote and encryption are true. Local storage and notifications each have two choices, giving four configurations.

3.2. Substitute a value into the rules

Substituting R = true simplifies the rules to E. The new function no longer depends on R, but the vtree still contains it. An ordinary count includes both values of that free variable. A projected count over the remaining options excludes it:

TididiCircuit *input = copy(rules), *residual = NULL;
check(tididi_condition(input, remote_choice, 1, &residual, NULL));
printf("After substituting remote = true: %" PRIu64 "\n", count(residual));
const uint32_t remaining[] = {LOCAL, ENCRYPTED, NOTIFICATIONS};
uint64_t distinct = 0;
check(tididi_projected_model_count(residual, remaining, 3, &distinct, NULL));
printf("Distinct remaining choices: %" PRIu64 "\n", distinct);

Output:

After substituting remote = true: 8
Distinct remaining choices: 4

Use tididi_condition() for the remaining function; use observation or conjunction to retain the selected value.

3.3. Count distinct choices for a subset of options

Local only, remote only, and both are valid destinations: three choices. A projected count excludes variations in encryption and notifications:

const uint32_t keep[] = {LOCAL, REMOTE}, eliminate[] = {ENCRYPTED, NOTIFICATIONS};
check(tididi_projected_model_count(rules, keep, 2, &distinct, NULL));
printf("Valid destination choices: %" PRIu64 "\n", distinct);
TididiCircuit *original = copy(rules), *destination_rule = NULL;
check(tididi_exists(original, eliminate, 2, &destination_rule, NULL));
printf("Destination rule over the full vtree: %" PRIu64 "\n", count(destination_rule));
check(tididi_projected_model_count(destination_rule, keep, 2, &distinct, NULL));
printf("Destination rule projected: %" PRIu64 "\n", distinct);

Output:

Valid destination choices: 3
Destination rule over the full vtree: 12
Destination rule projected: 3

Existential quantification builds L ∨ R, leaving E and N free in the unchanged vtree. Use tididi_projected_model_count() for the count and tididi_exists() for a circuit you can combine with other rules, as in Explore a directed graph.

3.4. Complete program

Download counting.c and the shared helper. Cleanup of consumed handles appears in the complete program.