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 * ENCODING OF BOOLEAN OPERATORS IN CLAUSAL FORM
21 */
22
23 /*
24 * This module is used to build auxiliary literal definition:
25 * For example, to create l0 = (OR l1 ... l_n)
26 * - the module simplifies (OR l1 ... l_n)
27 * - then it creates a fresh boolean l0 = pos_lit(v0)
28 * - and it asserts clauses equivalent to "l0 = (OR ....)"
29 * Hash consing is used to avoid duplications
30 */
31
32 #ifndef __GATES_MANAGER_H
33 #define __GATES_MANAGER_H
34
35 #include "solvers/cdcl/gates_hash_table.h"
36 #include "solvers/cdcl/smt_core.h"
37 #include "utils/int_vectors.h"
38
39
40 /*
41 * Manager = smt_core + hash table + an internal literal buffer
42 */
43 typedef struct gate_manager_s {
44 smt_core_t *core;
45 gate_table_t *htbl;
46 ivector_t buffer;
47 } gate_manager_t;
48
49
50 /*
51 * Hash consing bound: hash consing is not used for
52 * operators with more than MAX_HASHCONS_SIZE input parameters
53 * MAX_HASHCONS_SIZE must be no more than MAX_INDEGREE
54 */
55 #define MAX_HASHCONS_SIZE 50
56
57
58
59 /***********************************
60 * INITIALIZATION/PUSH/POP/RESET *
61 **********************************/
62
63 /*
64 * Initialization:
65 * - htbl is initialized to its default size
66 * - core must be initialized outside this function
67 */
68 extern void init_gate_manager(gate_manager_t *m, smt_core_t *core);
69
70 /*
71 * Deletion: doesn't delete the core, just the hash table
72 */
73 extern void delete_gate_manager(gate_manager_t *m);
74
75
76 /*
77 * Push/pop/reset: don't do anything. The gate table
78 * is now part of the smt_core and is updated by smt_push,
79 * smt_pop, reset_smt_core.
80 */
gate_manager_push(gate_manager_t * m)81 static inline void gate_manager_push(gate_manager_t *m) {
82 // gate_table_push(&m->htbl);
83 }
84
gate_manager_pop(gate_manager_t * m)85 static inline void gate_manager_pop(gate_manager_t *m) {
86 // gate_table_pop(&m->htbl);
87 }
88
reset_gate_manager(gate_manager_t * m)89 static inline void reset_gate_manager(gate_manager_t *m) {
90 // reset_gate_table(&m->htbl);
91 ivector_reset(&m->buffer);
92 }
93
94
95
96
97 /***********************
98 * GATE CONSTRUCTION *
99 **********************/
100
101 /*
102 * AND, OR, XOR, IFF, IMPLIES constructors
103 *
104 * The generic constructors take an array of n literals a[0 ... n-1] as input
105 * - they do the right thing if n=0 or n=1
106 * - short-cuts are provided for n=2 and n=3
107 * - the constructors do not modify array a
108 */
109 extern literal_t mk_or_gate(gate_manager_t *m, uint32_t n, literal_t *a);
110 extern literal_t mk_and_gate(gate_manager_t *m, uint32_t n, literal_t *a);
111 extern literal_t mk_xor_gate(gate_manager_t *m, uint32_t n, literal_t *a);
112
113 // two-arguments
114 extern literal_t mk_or_gate2(gate_manager_t *m, literal_t l1, literal_t l2);
115 extern literal_t mk_and_gate2(gate_manager_t *m, literal_t l1, literal_t l2);
116 extern literal_t mk_xor_gate2(gate_manager_t *m, literal_t l1, literal_t l2);
117
118 // three-arguments
119 extern literal_t mk_or_gate3(gate_manager_t *m, literal_t l1, literal_t l2, literal_t l3);
120 extern literal_t mk_and_gate3(gate_manager_t *m, literal_t l1, literal_t l2, literal_t l3);
121 extern literal_t mk_xor_gate3(gate_manager_t *m, literal_t l1, literal_t l2, literal_t l3);
122
123 // iff and implies are derived from xor and or
mk_iff_gate(gate_manager_t * m,literal_t l1,literal_t l2)124 static inline literal_t mk_iff_gate(gate_manager_t *m, literal_t l1, literal_t l2) {
125 return mk_xor_gate2(m, not(l1), l2);
126 }
127
mk_implies_gate(gate_manager_t * m,literal_t l1,literal_t l2)128 static inline literal_t mk_implies_gate(gate_manager_t *m, literal_t l1, literal_t l2) {
129 return mk_or_gate2(m, not(l1), l2);
130 }
131
132 /*
133 * returns l0 == (ITE c l1 l2)
134 */
135 extern literal_t mk_ite_gate(gate_manager_t *m, literal_t c, literal_t l1, literal_t l2);
136
137
138 /*
139 * Direct assertions for the following constraints
140 * (XOR l1 ... ln ) == v
141 * (XOR l1 l2) == v
142 * (XOR l1 l2 l3) == v
143 * (IFF l1 l2) == v
144 * (ITE c l1 l2) == v
145 * where v is true or false
146 */
147 extern void assert_xor(gate_manager_t *m, uint32_t n, literal_t *a, bool v);
148 extern void assert_xor2(gate_manager_t *m, literal_t l1, literal_t l2, bool v);
149 extern void assert_xor3(gate_manager_t *m, literal_t l1, literal_t l2, literal_t l3, bool v);
150
151 extern void assert_ite(gate_manager_t *m, literal_t c, literal_t l1, literal_t l2, bool v);
152
assert_iff(gate_manager_t * m,literal_t l1,literal_t l2,bool v)153 static inline void assert_iff(gate_manager_t *m, literal_t l1, literal_t l2, bool v) {
154 assert_xor2(m, l1, l2, ! v);
155 }
156
157
158
159
160 #endif /* __GATES_MANAGER_H */
161