1 /* 2 * This file is part of the Yices SMT Solver. 3 * Copyright (C) 2018 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 * WRAPPER FOR A SAT SOLVER OTHER THEN THE SMT_CORE 21 */ 22 23 #ifndef __DELEGATE_H 24 #define __DELEGATE_H 25 26 #include <stdbool.h> 27 #include <stdint.h> 28 29 #include "solvers/cdcl/smt_core.h" 30 #include "utils/int_vectors.h" 31 #include "yices_types.h" 32 33 34 /* 35 * For bitvector and purely propositional problems, we want to 36 * experiment with third-party sat solvers. The simplest way is 37 * to let the bvsolver + smt core do bit-blasting (i.e., produce 38 * a CNF formula) then call a sat solver on that CNF. 39 * 40 * To access the external solver, we assume the following API 41 * - add_empty_clause() 42 * - add_unit_clause(literal_t l) 43 * - add_binary_clause(literal_t l1, literal_t l2) 44 * - add_ternary_clause(literal_t l1, literal_t l2, literal_t l3) 45 * - add_clause(n: clause size, literal_t array_of_literals[]) 46 * - check() 47 * - get_value(bvar_t v): value of a boolean variable v 48 * - set_verbosity(int level): set verbosity lvel 49 * - delete() 50 * 51 * Optional/experimental functions: 52 * - keep_var(bvar_t v): tell the solver that v shouldn't be eliminated 53 * - var_def2(bvar_t v, uint32_t b, literal_t l1, literal_t l2) 54 * - var_def3(bvar_t v, uint32_t b, literal_t l1, literal_t l2, literal_t l3) 55 * - preprocess(): apply only preprocessing, not full check 56 * - export(const char*filename): export solver's state to file in DIMACS format 57 * 58 * The var_def functions state that v is a function of l1, l2, (and l3). 59 * The lower-order 8 bits of b define a truth table using the same conventions 60 * as in new_gates.h. 61 */ 62 typedef void (*add_empty_clause_fun_t)(void *solver); 63 typedef void (*add_unit_clause_fun_t)(void *solver, literal_t l); 64 typedef void (*add_binary_clause_fun_t)(void *solver, literal_t l1, literal_t l2); 65 typedef void (*add_ternary_clause_fun_t)(void *solver, literal_t l1, literal_t l2, literal_t l3); 66 typedef void (*add_clause_fun_t)(void *solver, uint32_t n, literal_t *a); 67 typedef smt_status_t (*check_sat_fun_t)(void *solver); 68 typedef bval_t (*get_value_fun_t)(void *solver, bvar_t x); 69 typedef void (*set_verbosity_fun_t)(void *solver, uint32_t level); 70 typedef void (*delete_fun_t)(void *solver); 71 72 typedef void (*keep_var_fun_t)(void *solver, bvar_t x); 73 typedef void (*var_def2_fun_t)(void *solver, bvar_t x, uint32_t b, literal_t l1, literal_t l2); 74 typedef void (*var_def3_fun_t)(void *solver, bvar_t x, uint32_t b, literal_t l1, literal_t l2, literal_t l3); 75 76 typedef smt_status_t (*preprocess_fun_t)(void *solver); 77 typedef void (*export_fun_t)(void *solver, FILE *f); 78 79 typedef struct delegate_s { 80 void *solver; // pointer to the sat solver 81 ivector_t buffer; // to make copy of clauses 82 add_empty_clause_fun_t add_empty_clause; 83 add_unit_clause_fun_t add_unit_clause; 84 add_binary_clause_fun_t add_binary_clause; 85 add_ternary_clause_fun_t add_ternary_clause; 86 add_clause_fun_t add_clause; 87 check_sat_fun_t check; 88 get_value_fun_t get_value; 89 set_verbosity_fun_t set_verbosity; 90 delete_fun_t delete; 91 keep_var_fun_t keep_var; 92 var_def2_fun_t var_def2; 93 var_def3_fun_t var_def3; 94 preprocess_fun_t preprocess; 95 export_fun_t export; 96 } delegate_t; 97 98 99 /* 100 * Create and initialize a delegate structure 101 * - solver_name specifies the external solver to use 102 * - nvars = number of variables 103 * - return true if that worked, false is the solver_name is not supported 104 * or if something else goes wrong. 105 * - allowed values for solver_name: TBD 106 */ 107 extern bool init_delegate(delegate_t *delegate, const char *solver_name, uint32_t nvars); 108 109 110 /* 111 * Test whether a solver is known and supported. 112 * - solver_name = external solver to use 113 * - return true if this solver is supported (i.e., can be used in init_delegate). 114 * - return false otherwise. 115 * - extra information is returned in *unknown: 116 * if we don't support the solver at all, *unknown is set to true 117 * if we have optional support (but not compiled), *unknown is set to fasle. 118 */ 119 extern bool supported_delegate(const char *solver_name, bool *unknown); 120 121 122 /* 123 * Delete the solver and free memory 124 */ 125 extern void delete_delegate(delegate_t *delegate); 126 127 /* 128 * Export the clauses from core to the delegate 129 * then check satsfiability: 130 * - return STATUS_SAT/STATUS_UNSAT if that works 131 * - return STATUS_UNKNOWN if the delegate fails 132 */ 133 extern smt_status_t solve_with_delegate(delegate_t *delegate, smt_core_t *core); 134 135 /* 136 * Export the clauses from the core to the delegate 137 * then appply delegate's CNF-level preprocessing 138 * - return STATUS_SAT/STATUS_UNSAT if that solves the problem 139 * - return STATUS_UNKNOWN otherwise (or if the delegate does not support this) 140 */ 141 extern smt_status_t preprocess_with_delegate(delegate_t *delegate, smt_core_t *core); 142 143 /* 144 * Write the delegate's CNF to a file in DIMACS format 145 * - f = output file. 146 * - f must be open and writable 147 */ 148 extern void export_to_dimacs_with_delegate(delegate_t *delegate, FILE *f); 149 150 151 /* 152 * Value assigned to variable x in the delegate 153 */ 154 extern bval_t delegate_get_value(delegate_t *delegate, bvar_t x); 155 156 /* 157 * Set verbosity level for the delegate 158 */ 159 extern void delegate_set_verbosity(delegate_t *delegate, uint32_t level); 160 161 162 163 164 #endif /* __DELEGATE_H */ 165