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 * ARITHMETIC OPERATIONS INVOLVING BALANCED BUFFERS AND TERMS 21 */ 22 23 #ifndef __RBA_BUFFER_TERMS_H 24 #define __RBA_BUFFER_TERMS_H 25 26 #include "terms/balanced_arith_buffers.h" 27 #include "terms/terms.h" 28 29 30 /* 31 * Binary operations: 32 * - t must be defined in table and must be an arithmetic term 33 * (i.e., t must have type int or real) 34 * - b->ptbl must be the same as table->pprods 35 * 36 * All operations update the buffer. 37 */ 38 extern void rba_buffer_add_term(rba_buffer_t *b, term_table_t *table, term_t t); 39 extern void rba_buffer_sub_term(rba_buffer_t *b, term_table_t *table, term_t t); 40 extern void rba_buffer_mul_term(rba_buffer_t *b, term_table_t *table, term_t t); 41 42 extern void rba_buffer_add_const_times_term(rba_buffer_t *b, term_table_t *table, rational_t *a, term_t t); 43 44 extern void rba_buffer_mul_term_power(rba_buffer_t *b, term_table_t *table, term_t t, uint32_t d); 45 46 47 48 #endif /* __RBA_BUFFER_TERMS_H */ 49