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 * COMPUTE THE VALUE OF A TERM IN A MODEL 21 */ 22 23 #ifndef __MODEL_EVAL_H 24 #define __MODEL_EVAL_H 25 26 #include <stdbool.h> 27 #include <stdint.h> 28 #include <setjmp.h> 29 30 #include "model/models.h" 31 #include "utils/int_hash_map.h" 32 #include "utils/int_stack.h" 33 #include "utils/int_vectors.h" 34 35 36 /* 37 * Error codes returned by eval_in_model 38 * - all are negative integers 39 * - a non-negative value means no error 40 * - the null_value is -1 so we start from -2 41 */ 42 enum { 43 MDL_EVAL_INTERNAL_ERROR = -2, 44 MDL_EVAL_UNKNOWN_TERM = -3, 45 MDL_EVAL_FREEVAR_IN_TERM = -4, 46 MDL_EVAL_QUANTIFIER = -5, 47 MDL_EVAL_LAMBDA = -6, 48 MDL_EVAL_FAILED = -7, // function equality involved 49 }; 50 51 52 53 /* 54 * Evaluator structure: 55 * - pointer to a model + term_table + value_table 56 * (term table and value table are extracted from 57 * model when the evaluator is initialized) 58 * - cache: keeps track of the value of evaluated terms 59 * - env: jump buffer for error handling 60 * - stack of integer arrays 61 */ 62 typedef struct evaluator_s { 63 model_t *model; 64 term_table_t *terms; 65 value_table_t *vtbl; 66 int_hmap_t cache; 67 int_stack_t stack; 68 jmp_buf env; 69 } evaluator_t; 70 71 72 73 74 /* 75 * Initialization for the given model 76 * 77 * NOTE: because the evaluator has side effects on model->vtbl, 78 * we can't attach several evaluators to the same model. 79 */ 80 extern void init_evaluator(evaluator_t *eval, model_t *model); 81 82 83 /* 84 * Deletion: free all memory 85 */ 86 extern void delete_evaluator(evaluator_t *eval); 87 88 89 /* 90 * Reset: empty the cache 91 */ 92 extern void reset_evaluator(evaluator_t *eval); 93 94 95 /* 96 * Compute the value of term t in the model 97 * - t must be a valid term 98 * - return a negative code if there's an error 99 * - return the id of a concrete objects of eval->model.vtbl otherwise 100 * 101 * Evaluation may create new objects. All these new objects are 102 * permanent in eval->vtbl. So they survive a call to delete_evaluator 103 * or reset_evaluator. 104 */ 105 extern value_t eval_in_model(evaluator_t *eval, term_t t); 106 107 108 /* 109 * Check whether t is true in the model 110 * - t must be a valid term 111 * - return true if t evaluates to true 112 * - return false if t can't be evaluated or 113 * if t's value is not boolean or not true. 114 */ 115 extern bool eval_to_true_in_model(evaluator_t *eval, term_t t); 116 117 118 /* 119 * Check whether t is false in the model 120 * - t must be a valid term 121 * - return true if t evaluates to false 122 * - return false if t can't be evaluated or it's not a boolean 123 * or if it evaluates to true. 124 */ 125 extern bool eval_to_false_in_model(evaluator_t *eval, term_t); 126 127 128 /* 129 * Check whether t is zero in the model 130 * - t must be a valid term 131 * - if t is an arithmetic term, this checks whether value(t) == 0 132 * - if t is a bit-vector term, this checks whether value(t) == 0b0000... 133 * - return false if t can't be evaluated, or if t is not an arithemtic 134 * term nor a bitvector term, or if t's value is not zero. 135 */ 136 extern bool eval_to_zero_in_model(evaluator_t *eval, term_t t); 137 138 139 /* 140 * Check whether t evaluates to +/-1 in the model 141 * - t must be a valid term 142 * - return false if t can't be evaluated or its value is not a rational 143 * - return true if t's value is either +1 or -1 144 */ 145 extern bool eval_to_unit_in_model(evaluator_t *eval, term_t t); 146 147 148 /* 149 * Compute the values of terms a[0 ... n-1] 150 * - don't return anything 151 * - the value of a[i] can be queried by using eval_in_model(eval, a[i]) later 152 * (this reads the value from eval->cache so that's cheap). 153 */ 154 extern void eval_terms_in_model(evaluator_t *eval, const term_t *a, uint32_t n); 155 156 157 /* 158 * Add useful uninterpreted terms to the model. 159 * 160 * A term t is useful if it's assigned a default value in eval_term. This means 161 * that the value of t is useful but was not assigned in the model. It makes 162 * sense then to print the value of t in print_model. To do this, we add an 163 * entry [t -> value(t)] for every useful term t. 164 */ 165 extern void eval_record_useful_terms(evaluator_t *eval); 166 167 168 /* 169 * Cached-term collector: 170 * - call f(aux, t) for every t that's stored in eval->cache 171 * if f(aux, t) returns true, add t to v 172 * - f must not have side effects 173 */ 174 // model_filter_t is defined in models.h 175 extern void evaluator_collect_cached_terms(evaluator_t *eval, void *aux, model_filter_t f, ivector_t *v); 176 177 178 #endif /* __MODEL_EVAL_H */ 179