2. Choose valid configurations

A backup service offers local storage, remote storage, encryption and notifications. At least one destination is required, and remote storage requires encryption:

(L ∨ R) ∧ (¬R ∨ E).

Notifications are optional. They remain part of each complete configuration, even though they do not occur in the rules.

2.1. Build the rules

A clause is a disjunction of signed literals. Join the two clauses with AND.

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

Output:

Valid configurations: 8

2.2. Select remote storage

Intersect the valid configurations with the remote literal, then inspect what that choice forces. Positive returned literals are true; negative ones are false.

TididiCircuit *remote = NULL, *selected = NULL, *rules_copy = copy(valid);
check(tididi_literal(vtree, REMOTE, &remote, NULL));
check(tididi_and(rules_copy, remote, &selected, NULL));
printf("Valid remote configurations: %" PRIu64 "\n", count(selected));
TididiLiterals *forced = NULL;
check(tididi_implied_literals(selected, &forced, NULL));
printf("Forced literals:");
for (size_t i = 0; i < tididi_literals_len(forced); ++i)
    printf(" %" PRId64, tididi_literals_data(forced)[i]);
printf("\n");

Output:

Valid remote configurations: 4
Forced literals: 2 3

2.3. Change choices repeatedly

A counter owns a circuit and reuses its counting cache while observations change. Observations restrict the assignments counted; they do not consume the counter. Copy the rules when you also need to keep them outside the counter.

TididiCounter *counter = NULL;
TididiCircuit *counter_input = copy(valid);
check(tididi_counter(counter_input, &counter));
const int64_t remote_choice[] = {REMOTE};
const int64_t quiet[] = {-NOTIFICATIONS};
uint64_t remaining = 0;
check(tididi_counter_observe(counter, remote_choice, 1));
check(tididi_counter_model_count(counter, &remaining, NULL));
printf("Remote: %" PRIu64 "\n", remaining);
check(tididi_counter_observe(counter, quiet, 1));
check(tididi_counter_model_count(counter, &remaining, NULL));
printf("Remote, notifications off: %" PRIu64 "\n", remaining);
check(tididi_counter_clear_all(counter));
check(tididi_counter_model_count(counter, &remaining, NULL));
printf("All choices open: %" PRIu64 "\n", remaining);

Output:

Remote: 4
Remote, notifications off: 2
All choices open: 8

2.4. Complete program

Download configurations.c and the shared helper. The source includes cleanup for all handles. Both files are included in the source checkout.