1/*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
17 */
18
19/*
20 * Test assumption processing and retract,
21 * and unsat core construction in bit_solver.
22 */
23
24#include <stdio.h>
25#include <inttypes.h>
26
27#include "int_vectors.h"
28#include "bit_solver.h"
29#include "solver_printer.h"
30
31
32static bit_solver_t solver;
33
34static bvar_t v[10]; // 10 variables
35
36static ivector_t unsat_core;
37
38
39/*
40 * Create and initialize solver
41 * - add variables and clauses
42 */
43static void init_solver1(void) {
44  uint32_t i;
45
46  init_ivector(&unsat_core, 20);
47  init_bit_solver(&solver, 20);
48  for (i=0; i<10; i++) {
49    v[i] = bit_solver_new_var(&solver);
50  }
51
52  // add test clauses
53  bit_solver_add_ternary_clause(&solver, pos_lit(v[0]), pos_lit(v[1]), pos_lit(v[2]));
54  bit_solver_add_ternary_clause(&solver, pos_lit(v[0]), pos_lit(v[3]), pos_lit(v[4]));
55  bit_solver_add_ternary_clause(&solver, pos_lit(v[0]), pos_lit(v[1]), neg_lit(v[2]));
56  bit_solver_add_ternary_clause(&solver, pos_lit(v[0]), pos_lit(v[5]), pos_lit(v[6]));
57  bit_solver_add_unit_clause(&solver, neg_lit(v[5]));
58}
59
60
61/*
62 * Print solver content
63 */
64static void print_solver(void) {
65  printf("Clauses:\n");
66  print_bit_solver_clauses(stdout, &solver);
67  printf("Assignment\n");
68  print_bit_solver_assignment(stdout, &solver);
69  printf("Assumptions\n");
70  print_bit_solver_assumptions(stdout, &solver);
71  printf("Base level = %"PRIu32"\n", solver.base_level);
72  printf("Decision level = %"PRIu32"\n", solver.decision_level);
73  printf("Status: ");
74  print_status(stdout, bit_solver_status(&solver));
75  printf("\n");
76}
77
78
79/*
80 * Print the unsat core
81 */
82static void print_core(void) {
83  ivector_t *v;
84  uint32_t i, n;
85
86  printf("unsat core:");
87  v = &unsat_core;
88  n = v->size;
89  for (i=0; i<n; i++) {
90    printf(" ");
91    print_literal(stdout, v->data[i]);
92  }
93  printf("\n");
94}
95
96
97/*
98 * First test
99 */
100static void test1(void) {
101  bool ok;
102
103  printf("\n**** TEST 1 ****\n\n");
104  init_solver1();
105  print_solver();
106  printf("\n---> Start search\n");
107  ok = bit_solver_start_search(&solver);
108  print_solver();
109  if (ok) {
110    printf("---> OK\n");
111  } else {
112    printf("---> UNSAT\n");
113    return;
114  }
115
116  printf("\n---> Assumption: ");
117  print_literal(stdout, neg_lit(v[0]));
118  printf("\n");
119  ok = bit_solver_assume(&solver, neg_lit(v[0]));
120  print_solver();
121  if (ok) {
122    printf("---> OK\n");
123  } else {
124    printf("---> UNSAT\n");
125    ivector_reset(&unsat_core);
126    bit_solver_get_unsat_core(&solver, &unsat_core);
127    print_core();
128    return;
129  }
130
131
132  printf("\n---> Assumption: ");
133  print_literal(stdout, neg_lit(v[0]));
134  printf("\n");
135  ok = bit_solver_assume(&solver, neg_lit(v[0]));
136  print_solver();
137  if (ok) {
138    printf("---> OK\n");
139  } else {
140    printf("---> UNSAT\n");
141    ivector_reset(&unsat_core);
142    bit_solver_get_unsat_core(&solver, &unsat_core);
143    print_core();
144    return;
145  }
146
147
148  printf("\n---> Assumption: ");
149  print_literal(stdout, neg_lit(v[6]));
150  printf("\n");
151  ok = bit_solver_assume(&solver, neg_lit(v[6]));
152  print_solver();
153  if (ok) {
154    printf("---> OK\n");
155  } else {
156    printf("---> UNSAT\n");
157    ivector_reset(&unsat_core);
158    bit_solver_get_unsat_core(&solver, &unsat_core);
159    print_core();
160
161    printf("---> RETRACT\n");
162    bit_solver_retract(&solver);
163    print_solver();
164  }
165
166
167  printf("\n---> Assumption: ");
168  print_literal(stdout, neg_lit(v[4]));
169  printf("\n");
170  ok = bit_solver_assume(&solver, neg_lit(v[4]));
171  print_solver();
172  if (ok) {
173    printf("---> OK\n");
174  } else {
175    printf("---> UNSAT\n");
176    ivector_reset(&unsat_core);
177    bit_solver_get_unsat_core(&solver, &unsat_core);
178    print_core();
179
180    printf("---> RETRACT\n");
181    bit_solver_retract(&solver);
182    print_solver();
183  }
184
185  printf("\n---> Assumption: ");
186  print_literal(stdout, neg_lit(v[1]));
187  printf("\n");
188  ok = bit_solver_assume(&solver, neg_lit(v[1]));
189  print_solver();
190  if (ok) {
191    printf("---> OK\n");
192  } else {
193    printf("---> UNSAT\n");
194    ivector_reset(&unsat_core);
195    bit_solver_get_unsat_core(&solver, &unsat_core);
196    print_core();
197    printf("---> RETRACT\n");
198    bit_solver_retract(&solver);
199    print_solver();
200  }
201
202  while (solver.base_level > 0) {
203    printf("\n---> RETRACT\n");
204    bit_solver_retract(&solver);
205    print_solver();
206  }
207}
208
209
210/*
211 * Run test1 then exit
212 */
213int main(void) {
214  test1();
215  delete_bit_solver(&solver);
216  delete_ivector(&unsat_core);
217  return 0;
218}
219