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 * EF-Solver 21 */ 22 23 /* 24 * Input problems are stored in an ef_prob structure. 25 * - prob->evars = existential variables (denoted by X) 26 * - prob->uvars = universal variables (denoted by Y) 27 * - prob->conditions = a set of constraints on X: 28 * A1(X) and ... and At(X) 29 * - and a finite list of universal constraints 30 * 31 * Each universal constraint has the form 32 * 33 * (FORALL Y_i: B_i(Y_i) => C_i(X_i, Y_i)) 34 * 35 * where Y_i is a subset of the universal variables 36 * X_i is a subset of the existential variables 37 * B_i is the assumption (on Y_i) 38 * C_i is the guarantee 39 * 40 * 41 * The goal is to solve the exists/forall problem: 42 * 43 * EXISTS X: A1(X) and ... and At(X) 44 * AND (FORALL Y_1: B_1(Y_1) => C_1(X_1, Y_1)) 45 * ... 46 * AND (FORALL Y_k: B_k(Y_k) => C_k(X_k, Y_k)) 47 * 48 * 49 * General procedure 50 * ----------------- 51 * 52 * 1) initialize a context ctx with A1(X) ... At(X) 53 * 54 * 2) iterate the following loop 55 * 56 * a) check whether ctx is satisfiable. 57 * If it's not, we're done. The EF-problem has no solution. 58 * If it is, let x be a model for ctx 59 * 60 * b) check whether x is a solution: 61 * 62 * For each universal constraint, check whether 63 * 64 * B_i(Y_i) AND not C_i(X_i, Y_i) is satisfiable 65 * under the mapping X_i := x_i. 66 * 67 * If it is, then let y_i be a model of this constraint. 68 * 69 * c) If we find no witness in step b: exit. The model x is 70 * a solution to the EF-problem. 71 * 72 * Otherwise, we have a witness y_i that shows why x is not 73 * good. That is, y_i is a counterexample to 74 * 75 * (forall Y_i: B_i(Y_i) => C_i(X_i, Y_i)) with [X := x] 76 * 77 * So y_i eliminates x from the candidate spaces. 78 * We want to generalize y_i: construct a formula Z(X_i) such 79 * that: 1) x satisfies Z(X_i) 80 * 2) no other solution to Z(X_i) is a good candidate. 81 * 82 * Once we have Z(X_i), we add \not Z(X_i) to the ctx and 83 * go back to a). 84 * 85 * 86 * Different options for constructing Z 87 * ------------------------------------ 88 * - Option 1: no generalization: Z(X_i) is (X_i /= x_i) 89 * (just eliminate x_i) 90 * 91 * - Option 2: generalization by substitution: 92 * Z(X_i) is C(X_i, Y_i) with [Y_i := y_i] 93 * (eliminate any x_i for which y_i is a witness). 94 * 95 * - Option 3: quantifier elimination: 96 * rewrite (FORALL Y_i: B_i(Y_i) AND not C_i(X_i, Y_i)) 97 * to Z(X_i) 98 * 99 * - Other options: cheaper forms of quantifier elimination, 100 * driven by the witness y_i. 101 * 102 * Variant for initializing the exist context 103 * ------------------------------------------ 104 * - Given constraint 105 * 106 * (FORALL Y_i: B_i(Y_i) => C_i(X_i, Y_i)) 107 * 108 * we can sample y_s that satisfy B_i(Y_i). For every 109 * such y_i, we get a constraint C_i(X_i, y_i) by substitution. 110 * Then this constraint depends only on the existential 111 * variable, so we can add (C_i(X_i, y_i))) to the 112 * exists context (i.e., any good X_i must satisfy C_i(X_i, y_i)). 113 * 114 * Baseline implementation 115 * ----------------------- 116 * - support Option 1 and 2. 117 */ 118 119 #ifndef __EFSOLVER_H 120 #define __EFSOLVER_H 121 122 #include <stdint.h> 123 #include <stdbool.h> 124 #include <stdio.h> 125 126 127 #include "api/search_parameters.h" 128 #include "api/smt_logic_codes.h" 129 #include "context/context_types.h" 130 #include "exists_forall/ef_problem.h" 131 #include "io/tracer.h" 132 133 #include "yices_types.h" 134 135 136 /* 137 * efsolver: stores a pointer to the ef_prob_t descriptor 138 * + flags for context initialization: logic/arch 139 * + search parameters (for now we use the same parameters for exists and forall) 140 * + generalization option 141 * + presampling setting: if max_samples is 0, no presampling 142 * otherwise, max_samples is used for sampling 143 * 144 * Internal data structures: 145 * - exists_context, forall_context: pointers to contexts, allocated and initialized 146 * when needed 147 * - evalue = array large enough to store the value of all exists variables 148 * - uvalue = array large enough to store the value of all universal variables 149 * - evalue_aux and uvalue_aux = auxiliary vectors (to store value vector of smaller 150 * sizes than evalue/uvalue) 151 * 152 * Flags for diagnostic 153 * - status = status of the last call to check (either in the exists or 154 * the forall context) 155 * - code = result of the last assertion (negative code is an error) 156 */ 157 typedef enum ef_gen_option { 158 EF_NOGEN_OPTION, // option 1 above 159 EF_GEN_BY_SUBST_OPTION, // option 2 above 160 EF_GEN_BY_PROJ_OPTION, // model-based projection (cheap quantifier elimination) 161 EF_GEN_AUTO_OPTION, // select between PROJ or SUBST depending on variables 162 } ef_gen_option_t; 163 164 165 /* 166 * Status + error report 167 */ 168 typedef enum ef_status { 169 EF_STATUS_IDLE, // before call to efsolver_check 170 EF_STATUS_SEARCHING, // while in efsolver_check 171 EF_STATUS_UNKNOWN, // max_iters reached 172 EF_STATUS_SAT, // satisfiable 173 EF_STATUS_UNSAT, // unsat 174 EF_STATUS_INTERRUPTED, // timeout 175 EF_STATUS_SUBST_ERROR, // error in a substitution 176 EF_STATUS_TVAL_ERROR, // error when converting model to constant terms 177 EF_STATUS_CHECK_ERROR, // unexpected status in check_context 178 EF_STATUS_ASSERT_ERROR, // error in assert formulas 179 EF_STATUS_MDL_ERROR, // error in model_from_map 180 EF_STATUS_IMPLICANT_ERROR, // error in get_implicant 181 EF_STATUS_PROJECTION_ERROR, // error in projection 182 EF_STATUS_ERROR, // any other internal error 183 } ef_status_t; 184 185 #define NUM_EF_STATUSES (EF_STATUS_ERROR+1) 186 187 /* 188 * error_code below can be used for diagnostic 189 * when status is EF_STATUS_..._ERROR: 190 * - status = EF_STATUS_SUBST_ERROR 191 * error_code = negative code from apply_term_subst 192 * - status = EF_STATUS_TVAL_ERROR 193 * error_code = not used (error from yices_term_array_value) 194 * - status = EF_STATUS_CHECK_ERROR: 195 * error_code = the unexpected status 196 * - status = EF_STATUS_ASSERT_ERROR 197 * error_code = exception code from context_assert_formulas 198 */ 199 typedef struct ef_solver_s { 200 // Input problem + logic and architecture codes 201 ef_prob_t *prob; 202 smt_logic_t logic; 203 context_arch_t arch; 204 ef_status_t status; 205 int32_t error_code; // for diagnostic 206 207 // Parameters used during the search 208 const param_t *parameters; // search parameters 209 ef_gen_option_t option; // generalization mode 210 uint32_t max_samples; // bound on pre-sampling: 0 means no pre-sampling 211 uint32_t max_iters; // bound on outer iterations 212 uint32_t iters; // number of outer iterations 213 uint32_t scan_idx; // first universal constraint to check 214 215 // Exists and forall contexts + exists model 216 context_t *exists_context; 217 context_t *forall_context; 218 model_t *exists_model; 219 term_t *evalue; 220 term_t *uvalue; 221 222 // Support for implicant construction and projection 223 model_t *full_model; 224 ivector_t implicant; 225 ivector_t projection; 226 227 // Auxiliary buffers 228 ivector_t evalue_aux; 229 ivector_t uvalue_aux; 230 ivector_t all_vars; 231 ivector_t all_values; 232 233 // For verbose output (default = NULL) 234 tracer_t *trace; 235 } ef_solver_t; 236 237 238 239 /* 240 * Initialize solver: 241 * - prob = problem descriptor 242 * - logic/arch = for context initialization 243 * - the logic must be supported by the context (so it must be QF_XXX). 244 */ 245 extern void init_ef_solver(ef_solver_t *solver, ef_prob_t *prob, smt_logic_t logic, context_arch_t arch); 246 247 248 /* 249 * Delete the whole thing 250 */ 251 extern void delete_ef_solver(ef_solver_t *solver); 252 253 254 /* 255 * Set the trace: 256 * - the current tracer must be NULL. 257 */ 258 extern void ef_solver_set_trace(ef_solver_t *solver, tracer_t *trace); 259 260 261 /* 262 * Check satisfiability: 263 * 264 * The result is stored in solver->status: 265 * - EF_STATUS_ERROR if something goes wrong 266 * - EF_STATUS_INTERRUPTED if one of the calls to check_context is interrupted 267 * - EF_STATUS_UNSAT if all exists models have been tried and none of them worked 268 * - EF_STATUS_UNKNOWN if the iteration limit is reached 269 * - EF_STATUS_SAT if a good model is found 270 * 271 * In the later case, 272 * - the model is stored in solver->exists_model 273 * - also it's available as a mapping form solver->prob->evars to solver->evalues 274 * 275 * Also solver->iters stores the number of iterations required. 276 */ 277 extern void ef_solver_check(ef_solver_t *solver, const param_t *parameters, 278 ef_gen_option_t gen_mode, uint32_t max_samples, uint32_t max_iters); 279 280 281 /* 282 * Stop the search 283 */ 284 extern void ef_solver_stop_search(ef_solver_t *solver); 285 286 287 /* 288 * Print solution 289 */ 290 extern void print_ef_solution(FILE *f, ef_solver_t *solver); 291 292 293 294 #endif /* __EFSOLVER_H */ 295