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