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