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 #pragma once 20 21 #include "nra_plugin_internal.h" 22 #include "utils/int_vectors.h" 23 24 /** 25 * Explain the core in the conflict. Core is a set of constraint variables, 26 * and conflict will a set if terms. 27 * 28 * pos: set of positive assumptions (to extend the trail) 29 * neg: set of negative assumptions (to extend the trail) 30 * 31 * */ 32 void nra_plugin_explain_conflict(nra_plugin_t* nra, const int_mset_t* pos, const int_mset_t* neg, 33 const ivector_t* core, const ivector_t* lemma_reasons, ivector_t* conflict); 34