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 * PRINT SMT-CORE STRUCTURE 21 */ 22 23 #ifndef __SMT_CORE_PRINTER_H 24 #define __SMT_CORE_PRINTER_H 25 26 #include <stdio.h> 27 28 #include "solvers/cdcl/smt_core.h" 29 30 /* 31 * Basic objects 32 */ 33 extern void print_bval(FILE *f, bval_t b); 34 extern void print_status(FILE *f, smt_status_t s); 35 extern void print_bvar(FILE *f, bvar_t x); 36 extern void print_literal(FILE *f, literal_t l); 37 38 39 /* 40 * Clauses 41 */ 42 extern void print_unit_clause(FILE *f, literal_t l); 43 extern void print_binary_clause(FILE *f, literal_t l1, literal_t l2); 44 extern void print_litarray(FILE *f, uint32_t n, literal_t *a); 45 extern void print_clause(FILE *f, clause_t *cl); 46 47 extern void print_unit_clauses(FILE *f, smt_core_t *core); 48 extern void print_binary_clauses(FILE *f, smt_core_t *core); 49 extern void print_problem_clauses(FILE *f, smt_core_t *core); 50 extern void print_learned_clauses(FILE *f, smt_core_t *core); 51 extern void print_clauses(FILE *f, smt_core_t *core); 52 extern void print_all_clauses(FILE *f, smt_core_t *core); 53 extern void print_lemmas(FILE *f, smt_core_t *core); 54 55 /* 56 * Core solver state 57 */ 58 extern void print_boolean_assignment(FILE *f, smt_core_t *core); 59 extern void print_conflict(FILE *f, smt_core_t *core); 60 extern void print_smt_core(FILE *f, smt_core_t *core); 61 62 63 #endif /* __SMT_CORE_PRINTER_H */ 64