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