1 #include <clingo.h>
2 #include <stdlib.h>
3 #include <stdio.h>
4 #include <assert.h>
5
print_model(clingo_model_t const * model)6 bool print_model(clingo_model_t const *model) {
7 bool ret = true;
8 clingo_symbol_t *atoms = NULL;
9 size_t atoms_n;
10 clingo_symbol_t const *it, *ie;
11 char *str = NULL;
12 size_t str_n = 0;
13
14 // determine the number of (shown) symbols in the model
15 if (!clingo_model_symbols_size(model, clingo_show_type_shown, &atoms_n)) { goto error; }
16
17 // allocate required memory to hold all the symbols
18 if (!(atoms = (clingo_symbol_t*)malloc(sizeof(*atoms) * atoms_n))) {
19 clingo_set_error(clingo_error_bad_alloc, "could not allocate memory for atoms");
20 goto error;
21 }
22
23 // retrieve the symbols in the model
24 if (!clingo_model_symbols(model, clingo_show_type_shown, atoms, atoms_n)) { goto error; }
25
26 printf("Model:");
27
28 for (it = atoms, ie = atoms + atoms_n; it != ie; ++it) {
29 size_t n;
30 char *str_new;
31
32 // determine size of the string representation of the next symbol in the model
33 if (!clingo_symbol_to_string_size(*it, &n)) { goto error; }
34
35 if (str_n < n) {
36 // allocate required memory to hold the symbol's string
37 if (!(str_new = (char*)realloc(str, sizeof(*str) * n))) {
38 clingo_set_error(clingo_error_bad_alloc, "could not allocate memory for symbol's string");
39 goto error;
40 }
41
42 str = str_new;
43 str_n = n;
44 }
45
46 // retrieve the symbol's string
47 if (!clingo_symbol_to_string(*it, str, n)) { goto error; }
48
49 printf(" %s", str);
50 }
51
52 printf("\n");
53 goto out;
54
55 error:
56 ret = false;
57
58 out:
59 if (atoms) { free(atoms); }
60 if (str) { free(str); }
61
62 return ret;
63 }
64
solve(clingo_control_t * ctl,clingo_solve_result_bitset_t * result)65 bool solve(clingo_control_t *ctl, clingo_solve_result_bitset_t *result) {
66 bool ret = true;
67 clingo_solve_handle_t *handle;
68 clingo_model_t const *model;
69
70 // get a solve handle
71 if (!clingo_control_solve(ctl, clingo_solve_mode_yield, NULL, 0, NULL, NULL, &handle)) { goto error; }
72 // loop over all models
73 while (true) {
74 if (!clingo_solve_handle_resume(handle)) { goto error; }
75 if (!clingo_solve_handle_model(handle, &model)) { goto error; }
76 // print the model
77 if (model) { print_model(model); }
78 // stop if there are no more models
79 else { break; }
80 }
81 // close the solve handle
82 if (!clingo_solve_handle_get(handle, result)) { goto error; }
83
84 goto out;
85
86 error:
87 ret = false;
88
89 out:
90 // free the solve handle
91 return clingo_solve_handle_close(handle) && ret;
92 }
93
main(int argc,char const ** argv)94 int main(int argc, char const **argv) {
95 char const *error_message;
96 int ret = 0;
97 size_t offset;
98 clingo_solve_result_bitset_t solve_ret;
99 clingo_control_t *ctl;
100 clingo_symbolic_atoms_t const *atoms;
101 clingo_backend_t *backend;
102 clingo_atom_t atom_ids[4];
103 char const *atom_strings[] = {"a", "b", "c"};
104 clingo_literal_t body[2];
105 clingo_part_t parts[] = {{ "base", NULL, 0 }};
106
107 // create a control object and pass command line arguments
108 if (!clingo_control_new(argv+1, argc-1, NULL, NULL, 20, &ctl) != 0) { goto error; }
109
110 // add a logic program to the base part
111 if (!clingo_control_add(ctl, "base", NULL, 0, "{a; b; c}.")) { goto error; }
112
113 // ground the base part
114 if (!clingo_control_ground(ctl, parts, 1, NULL, NULL)) { goto error; }
115
116 // get the container for symbolic atoms
117 if (!clingo_control_symbolic_atoms(ctl, &atoms)) { goto error; }
118 // get the ids of atoms a, b, and c
119 offset = 0;
120 for (char const **it = atom_strings, **ie = it + sizeof(atom_strings) / sizeof(*atom_strings); it != ie; ++it) {
121 clingo_symbol_t sym;
122 clingo_symbolic_atom_iterator_t atom_it, atom_ie;
123 clingo_literal_t lit;
124 bool equal;
125
126 // lookup the atom
127 if (!clingo_symbol_create_id(*it, true, &sym)) { goto error; }
128 if (!clingo_symbolic_atoms_find(atoms, sym, &atom_it)) { goto error; }
129 if (!clingo_symbolic_atoms_end(atoms, &atom_ie)) { goto error; }
130 if (!clingo_symbolic_atoms_iterator_is_equal_to(atoms, atom_it, atom_ie, &equal)) { goto error; }
131 assert(!equal); (void)equal;
132
133 // get the atom's id
134 if (!clingo_symbolic_atoms_literal(atoms, atom_it, &lit)) { goto error; }
135 atom_ids[offset++] = lit;
136 }
137
138 // get the backend
139 if (!clingo_control_backend(ctl, &backend)) { goto error; }
140
141 // prepare the backend for adding rules
142 if (!clingo_backend_begin(backend)) { goto error; }
143
144 // add an additional atom (called d below)
145 if (!clingo_backend_add_atom(backend, NULL, &atom_ids[3])) { goto error; }
146
147 // add rule: d :- a, b.
148 body[0] = atom_ids[0];
149 body[1] = atom_ids[1];
150 if (!clingo_backend_rule(backend, false, &atom_ids[3], 1, body, sizeof(body)/sizeof(*body))) { goto error; }
151
152 // add rule: :- not d, c.
153 body[0] = -(clingo_literal_t)atom_ids[3];
154 body[1] = atom_ids[2];
155 if (!clingo_backend_rule(backend, false, NULL, 0, body, sizeof(body)/sizeof(*body))) { goto error; }
156
157 // finalize the backend
158 if (!clingo_backend_end(backend)) { goto error; }
159
160 // solve
161 if (!solve(ctl, &solve_ret)) { goto error; }
162
163 goto out;
164
165 error:
166 if (!(error_message = clingo_error_message())) { error_message = "error"; }
167
168 printf("%s\n", error_message);
169 ret = clingo_error_code();
170
171 out:
172 if (ctl) { clingo_control_free(ctl); }
173
174 return ret;
175 }
176
177