12367760548

Committed 17 Dec 2024 06:41AM UTC coverage: 65.285% (-0.6%) from 65.92%

Build # 12367760548

Build Type

push

github

Committed by

web-flow

Commit Message

Fixes GitHub coverage issue (#544)

* Update action.yml

* Update action.yml

Run Details

81020 of 124102 relevant lines covered (65.29%)

1509382.01 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

57.14

/src/solvers/bv/bvsolver.h

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef __BVSOLVER_H
#define __BVSOLVER_H

#include <stdbool.h>

#include "solvers/bv/bvsolver_types.h"



/*********************
 *  MAIN OPERATIONS  *
 ********************/

/*
 * Initialize a bit-vector solver
 * - core = the attached smt core
 * - egraph = the attached egraph (or NULL)
 */
extern void init_bv_solver(bv_solver_t *solver, smt_core_t *core, egraph_t *egraph);


/*
 * Attach a jump buffer for exception handling
 */
extern void bv_solver_init_jmpbuf(bv_solver_t *solver, jmp_buf *buffer);


/*
 * Delete solver
 */
extern void delete_bv_solver(bv_solver_t *solver);


/*
 * Get the solver's interface descriptors
 */
// internalization interface (used by the context)
extern bv_interface_t *bv_solver_bv_interface(bv_solver_t *solver);

// control and smt interfaces (used by the core and egraph)
extern th_ctrl_interface_t *bv_solver_ctrl_interface(bv_solver_t *solver);
extern th_smt_interface_t *bv_solver_smt_interface(bv_solver_t *solver);

// egraph-specific interfaces
extern th_egraph_interface_t *bv_solver_egraph_interface(bv_solver_t *solver);
extern bv_egraph_interface_t *bv_solver_bv_egraph_interface(bv_solver_t *solver);



/*
 * FOR TESTING: convert the constraints to CNF
 * - return false if there's a conflict
 */
extern bool bv_solver_bitblast(bv_solver_t *solver);
extern bool bv_solver_compile(bv_solver_t *solver);



/*******************************
 *  INTERNALIZATION FUNCTIONS  *
 ******************************/

/*
 * These functions are used by the context to create atoms and variables
 * in the bit-vector solver. We export them for testing. They are normally
 * called via the bvsolver_interface_t descriptor.
 */

/*
 * Create a new variable of n bits
 */
extern thvar_t bv_solver_create_var(bv_solver_t *solver, uint32_t n);

/*
 * Create a variable equal to constant c
 */
extern thvar_t bv_solver_create_const(bv_solver_t *solver, bvconst_term_t *c);
extern thvar_t bv_solver_create_const64(bv_solver_t *solver, bvconst64_term_t *c);


/*
 * Internalize the polynomial p
 * - map defines how terms of p are replaced by variables of solver:
 *   if p is of the form a_0 t_0 + ... + a_n t_n
 *   then map contains n+1 elements variables, and map[i] is the internalization of t_i
 * - exception: if t_0 is const_idx then map[0] = null_thvar
 */
extern thvar_t bv_solver_create_bvpoly(bv_solver_t *solver, bvpoly_t *p, thvar_t *map);
extern thvar_t bv_solver_create_bvpoly64(bv_solver_t *solver, bvpoly64_t *p, thvar_t *map);


/*
 * Internalize the power-product p = t_0^d_0 * ... * t_n^d_n
 * - map[i] stores the theory variable equal to the internalization of t_i
 */
extern thvar_t bv_solver_create_pprod(bv_solver_t *solver, pprod_t *p, thvar_t *map);


/*
 * Internalize the bit array a[0 ... n-1]
 * - each element a[i] is a literal in the core
 */
extern thvar_t bv_solver_create_bvarray(bv_solver_t *solver, literal_t *a, uint32_t n);


/*
 * Internalize the if-then-else term (ite c x y)
 * - c is a literal in the core
 * - x and y are two previously created theory variables
 */
extern thvar_t bv_solver_create_ite(bv_solver_t *solver, literal_t c, thvar_t x, thvar_t y);


/*
 * Internalize the binary operations
 */
extern thvar_t bv_solver_create_bvdiv(bv_solver_t *solver, thvar_t x, thvar_t y);
extern thvar_t bv_solver_create_bvrem(bv_solver_t *solver, thvar_t x, thvar_t y);
extern thvar_t bv_solver_create_bvsdiv(bv_solver_t *solver, thvar_t x, thvar_t y);
extern thvar_t bv_solver_create_bvsrem(bv_solver_t *solver, thvar_t x, thvar_t y);
extern thvar_t bv_solver_create_bvsmod(bv_solver_t *solver, thvar_t x, thvar_t y);

extern thvar_t bv_solver_create_bvshl(bv_solver_t *solver, thvar_t x, thvar_t y);
extern thvar_t bv_solver_create_bvlshr(bv_solver_t *solver, thvar_t x, thvar_t y);
extern thvar_t bv_solver_create_bvashr(bv_solver_t *solver, thvar_t x, thvar_t y);


/*
 * Return the i-th bit of theory variable x as a literal
 */
extern literal_t bv_solver_select_bit(bv_solver_t *solver, thvar_t x, uint32_t i);


/*
 * Create atoms and return the corresponding core literal
 * Three types of atoms are supported
 *  (eq x y): equality
 *  (ge x y):  (x >= y) with x and y interpreted as unsigned integers
 *  (sge x y): (x >= y) with x and y interpreted as signed integers
 */
extern literal_t bv_solver_create_eq_atom(bv_solver_t *solver, thvar_t x, thvar_t y);
extern literal_t bv_solver_create_ge_atom(bv_solver_t *solver, thvar_t x, thvar_t y);
extern literal_t bv_solver_create_sge_atom(bv_solver_t *solver, thvar_t x, thvar_t y);


/*
 * Assertion of top-level axioms
 * - tt indicates whether the axiom or its negation must be asserted
 *   tt = true --> assert (eq x y) or (ge x y) or (sge x y)
 *   tt = fasle --> assert (not (eq x y)) or (not (ge x y)) or (not (sge x y))
 */
extern void bv_solver_assert_eq_axiom(bv_solver_t *solver, thvar_t x, thvar_t y, bool tt);
extern void bv_solver_assert_ge_axiom(bv_solver_t *solver, thvar_t x, thvar_t y, bool tt);
extern void bv_solver_assert_sge_axiom(bv_solver_t *solver, thvar_t x, thvar_t y, bool tt);


/*
 * Assert that bit i of x is equal to tt
 */
extern void bv_solver_set_bit(bv_solver_t *solver, thvar_t x, uint32_t i, bool tt);


/*
 * Attach egraph term t to variable x
 */
extern void bv_solver_attach_eterm(bv_solver_t *solver, thvar_t x, eterm_t t);


/*
 * Get the egraph term attached to x
 * - return null_eterm if x has no term attached
 */
extern eterm_t bv_solver_eterm_of_var(bv_solver_t *solver, thvar_t x);



/*
 * Get the variables that x is compiled to
 * - return null_thvar if x is not compiled to anything
 */
extern thvar_t bv_solver_var_compiles_to(bv_solver_t *solver, thvar_t x);



/****************
 *  STATISTICS  *
 ***************/

/*
 * Number of variables and atoms
 */
static inline uint32_t bv_solver_num_vars(bv_solver_t *solver) {
  return solver->vtbl.nvars;
}

static inline uint32_t bv_solver_num_atoms(bv_solver_t *solver) {
  return solver->atbl.natoms;
}


/*
 * Number of nodes in the DAG
 */
static inline uint32_t bv_solver_dag_size(bv_solver_t *solver) {
  return (solver->compiler != NULL) ? solver->compiler->dag.nelems : 0;
}

static inline uint32_t bv_solver_num_leaf_nodes(bv_solver_t *solver) {
  return (solver->compiler != NULL) ? bvc_num_complex_nodes(&solver->compiler->dag) : 0;
}

static inline uint32_t bv_solver_num_elem_nodes(bv_solver_t *solver) {
  return (solver->compiler != NULL) ? bvc_num_elem_nodes(&solver->compiler->dag) : 0;
}

static inline uint32_t bv_solver_num_complex_nodes(bv_solver_t *solver) {
  return (solver->compiler != NULL) ? bvc_num_complex_nodes(&solver->compiler->dag) : 0;
}


/*
 * Atoms per type
 */
static inline uint32_t bv_solver_num_eq_atoms(bv_solver_t *solver) {
  return solver->stats.eq_atoms;
}

static inline uint32_t bv_solver_num_ge_atoms(bv_solver_t *solver) {
  return solver->stats.ge_atoms;
}

static inline uint32_t bv_solver_num_sge_atoms(bv_solver_t *solver) {
  return solver->stats.sge_atoms;
}


/*
 * Search statistics: these counters are all zero unless the solver
 * is attached to the egraph
 */
static inline uint32_t bv_solver_on_the_fly_atoms(bv_solver_t *solver) {
  return solver->stats.on_the_fly_atoms; // equality atoms created after bitblasting
}

static inline uint32_t bv_solver_equiv_lemmas(bv_solver_t *solver) {
  return solver->stats.equiv_lemmas;
}

static inline uint32_t bv_solver_interface_lemmas(bv_solver_t *solver) {
  return solver->stats.interface_lemmas;
}



/************************
 *  MODEL CONSTRUCTION  *
 ***********************/

/*
 * Build model: assign a concrete bitvector value to all variables
 * - when this is called, the context has determined that the
 *   constraints are SAT (so a model does exist)
 */
extern void bv_solver_build_model(bv_solver_t *solver);


/*
 * Copy the value assigned to x in the model into buffer c
 * - return true if the value is available
 * - return false if the solver has no model
 */
extern bool bv_solver_value_in_model(bv_solver_t *solver, thvar_t x, bvconstant_t *c);


/*
 * Delete whatever is used to store the model
 */
extern void bv_solver_free_model(bv_solver_t *solver);



/********************************
 *  EGRAPH INTERFACE FUNCTIONS  *
 *******************************/

/*
 * Assert that x1 and x2 are equal:
 * - id = edge index to be used in a subsequent call to egraph_explain_term_eq
 * - turn this into an axiom if possible
 * - otherwise push the equality into a queue for processing on the next
 *   call to propagate.
 */
extern void bv_solver_assert_var_eq(bv_solver_t *solver, thvar_t x1, thvar_t x2, int32_t id);


/*
 * Assert that x1 and x2 are distinct
 * - hint = egraph hint for the disequality
 * - turn this into an axiom if possible
 * - otherwise push the equality into a queue for processing on the next
 *   call to propagate.
 */
extern void bv_solver_assert_var_diseq(bv_solver_t *solver, thvar_t x1, thvar_t x2, composite_t *hint);

/*
 * Assert that a[0,...n-1] are all distinct
 * - hint = hint for egraph explanation
 * - this gets converted into n * (n-1) pairwise disequalities
 */
extern void bv_solver_assert_var_distinct(bv_solver_t *solver, uint32_t n, thvar_t *a, composite_t *hint);


/*
 * Check whether x1 and x2 are distinct at the base level
 */
extern bool bv_solver_check_disequality(bv_solver_t *solver, thvar_t x1, thvar_t x2);


/*
 * Generate interface equalities for conflicts between model and egraph
 * - return the number of interface equalities created
 * - max_eq = bound on the number of interface equalities allowed
 */
extern uint32_t bv_solver_reconcile_model(bv_solver_t *solver, uint32_t max_eq);




/***************************
 *  SMT/CONTROL FUNCTIONS  *
 **************************/

/*
 * The core or egraph invokes these functions via the smt or ctrl interface
 * descriptors. We export them for testing.
 */

/*
 * Prepare for search, after internalization
 */
extern void bv_solver_start_search(bv_solver_t *solver);

/*
 * Assert atom attached to literal l
 * This function is called when l is assigned to true by the core
 * - atom is the arithmetic atom attached to a boolean variable v = var_of(l)
 * - if l is positive (i.e., pos_lit(v)), assert the atom
 * - if l is negative (i.e., neg_lit(v)), assert its negation
 * Return false if that causes a conflict, true otherwise.
 */
extern bool bv_solver_assert_atom(bv_solver_t *solver, void *atom, literal_t l);

/*
 * Perform one round of propagation:
 * - return true if no conflict was detected
 * - return false if a conflict was detected, in that case the conflict
 *   clause is stored in the core
 */
extern bool bv_solver_propagate(bv_solver_t *solver);


/*
 * Support for theory-branching heuristic
 * - evaluate atom attached to l in the current simplex assignment
 * - the result is either l or (not l)
 * - if atom is true, return pos_lit(var_of(l))
 * - if atom is false, return neg_lit(var_of(l))
 */
extern literal_t bv_solver_select_polarity(bv_solver_t *solver, void *atom, literal_t l);


/*
 * Final check
 */
extern fcheck_code_t bv_solver_final_check(bv_solver_t *solver);


/*
 * Start a new decision level
 */
extern void bv_solver_increase_decision_level(bv_solver_t *solver);

/*
 * Backtrack to back_level
 */
extern void bv_solver_backtrack(bv_solver_t *solver, uint32_t back_level);


/*
 * Push/pop/reset
 */
extern void bv_solver_push(bv_solver_t *solver);
extern void bv_solver_pop(bv_solver_t *solver);
extern void bv_solver_reset(bv_solver_t *solver);




#endif /* __BVSOLVER_H */

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	#ifndef __BVSOLVER_H
20	#define __BVSOLVER_H
21
22	#include <stdbool.h>
23
24	#include "solvers/bv/bvsolver_types.h"
25
26
27
28	/*********************
29	* MAIN OPERATIONS *
30	********************/
31
32	/*
33	* Initialize a bit-vector solver
34	* - core = the attached smt core
35	* - egraph = the attached egraph (or NULL)
36	*/
37	extern void init_bv_solver(bv_solver_t solver, smt_core_t core, egraph_t *egraph);
38
39
40	/*
41	* Attach a jump buffer for exception handling
42	*/
43	extern void bv_solver_init_jmpbuf(bv_solver_t solver, jmp_buf buffer);
44
45
46	/*
47	* Delete solver
48	*/
49	extern void delete_bv_solver(bv_solver_t *solver);
50
51
52	/*
53	* Get the solver's interface descriptors
54	*/
55	// internalization interface (used by the context)
56	extern bv_interface_t bv_solver_bv_interface(bv_solver_t solver);
57
58	// control and smt interfaces (used by the core and egraph)
59	extern th_ctrl_interface_t bv_solver_ctrl_interface(bv_solver_t solver);
60	extern th_smt_interface_t bv_solver_smt_interface(bv_solver_t solver);
61
62	// egraph-specific interfaces
63	extern th_egraph_interface_t bv_solver_egraph_interface(bv_solver_t solver);
64	extern bv_egraph_interface_t bv_solver_bv_egraph_interface(bv_solver_t solver);
65
66
67
68	/*
69	* FOR TESTING: convert the constraints to CNF
70	* - return false if there's a conflict
71	*/
72	extern bool bv_solver_bitblast(bv_solver_t *solver);
73	extern bool bv_solver_compile(bv_solver_t *solver);
74
75
76
77	/*******************************
78	* INTERNALIZATION FUNCTIONS *
79	******************************/
80
81	/*
82	* These functions are used by the context to create atoms and variables
83	* in the bit-vector solver. We export them for testing. They are normally
84	* called via the bvsolver_interface_t descriptor.
85	*/
86
87	/*
88	* Create a new variable of n bits
89	*/
90	extern thvar_t bv_solver_create_var(bv_solver_t *solver, uint32_t n);
91
92	/*
93	* Create a variable equal to constant c
94	*/
95	extern thvar_t bv_solver_create_const(bv_solver_t solver, bvconst_term_t c);
96	extern thvar_t bv_solver_create_const64(bv_solver_t solver, bvconst64_term_t c);
97
98
99	/*
100	* Internalize the polynomial p
101	* - map defines how terms of p are replaced by variables of solver:
102	* if p is of the form a_0 t_0 + ... + a_n t_n
103	* then map contains n+1 elements variables, and map[i] is the internalization of t_i
104	* - exception: if t_0 is const_idx then map[0] = null_thvar
105	*/
106	extern thvar_t bv_solver_create_bvpoly(bv_solver_t solver, bvpoly_t p, thvar_t *map);
107	extern thvar_t bv_solver_create_bvpoly64(bv_solver_t solver, bvpoly64_t p, thvar_t *map);
108
109
110	/*
111	* Internalize the power-product p = t_0^d_0 * ... * t_n^d_n
112	* - map[i] stores the theory variable equal to the internalization of t_i
113	*/
114	extern thvar_t bv_solver_create_pprod(bv_solver_t solver, pprod_t p, thvar_t *map);
115
116
117	/*
118	* Internalize the bit array a[0 ... n-1]
119	* - each element a[i] is a literal in the core
120	*/
121	extern thvar_t bv_solver_create_bvarray(bv_solver_t solver, literal_t a, uint32_t n);
122
123
124	/*
125	* Internalize the if-then-else term (ite c x y)
126	* - c is a literal in the core
127	* - x and y are two previously created theory variables
128	*/
129	extern thvar_t bv_solver_create_ite(bv_solver_t *solver, literal_t c, thvar_t x, thvar_t y);
130
131
132	/*
133	* Internalize the binary operations
134	*/
135	extern thvar_t bv_solver_create_bvdiv(bv_solver_t *solver, thvar_t x, thvar_t y);
136	extern thvar_t bv_solver_create_bvrem(bv_solver_t *solver, thvar_t x, thvar_t y);
137	extern thvar_t bv_solver_create_bvsdiv(bv_solver_t *solver, thvar_t x, thvar_t y);
138	extern thvar_t bv_solver_create_bvsrem(bv_solver_t *solver, thvar_t x, thvar_t y);
139	extern thvar_t bv_solver_create_bvsmod(bv_solver_t *solver, thvar_t x, thvar_t y);
140
141	extern thvar_t bv_solver_create_bvshl(bv_solver_t *solver, thvar_t x, thvar_t y);
142	extern thvar_t bv_solver_create_bvlshr(bv_solver_t *solver, thvar_t x, thvar_t y);
143	extern thvar_t bv_solver_create_bvashr(bv_solver_t *solver, thvar_t x, thvar_t y);
144
145
146	/*
147	* Return the i-th bit of theory variable x as a literal
148	*/
149	extern literal_t bv_solver_select_bit(bv_solver_t *solver, thvar_t x, uint32_t i);
150
151
152	/*
153	* Create atoms and return the corresponding core literal
154	* Three types of atoms are supported
155	* (eq x y): equality
156	* (ge x y): (x >= y) with x and y interpreted as unsigned integers
157	* (sge x y): (x >= y) with x and y interpreted as signed integers
158	*/
159	extern literal_t bv_solver_create_eq_atom(bv_solver_t *solver, thvar_t x, thvar_t y);
160	extern literal_t bv_solver_create_ge_atom(bv_solver_t *solver, thvar_t x, thvar_t y);
161	extern literal_t bv_solver_create_sge_atom(bv_solver_t *solver, thvar_t x, thvar_t y);
162
163
164	/*
165	* Assertion of top-level axioms
166	* - tt indicates whether the axiom or its negation must be asserted
167	* tt = true --> assert (eq x y) or (ge x y) or (sge x y)
168	* tt = fasle --> assert (not (eq x y)) or (not (ge x y)) or (not (sge x y))
169	*/
170	extern void bv_solver_assert_eq_axiom(bv_solver_t *solver, thvar_t x, thvar_t y, bool tt);
171	extern void bv_solver_assert_ge_axiom(bv_solver_t *solver, thvar_t x, thvar_t y, bool tt);
172	extern void bv_solver_assert_sge_axiom(bv_solver_t *solver, thvar_t x, thvar_t y, bool tt);
173
174
175	/*
176	* Assert that bit i of x is equal to tt
177	*/
178	extern void bv_solver_set_bit(bv_solver_t *solver, thvar_t x, uint32_t i, bool tt);
179
180
181	/*
182	* Attach egraph term t to variable x
183	*/
184	extern void bv_solver_attach_eterm(bv_solver_t *solver, thvar_t x, eterm_t t);
185
186
187	/*
188	* Get the egraph term attached to x
189	* - return null_eterm if x has no term attached
190	*/
191	extern eterm_t bv_solver_eterm_of_var(bv_solver_t *solver, thvar_t x);
192
193
194
195	/*
196	* Get the variables that x is compiled to
197	* - return null_thvar if x is not compiled to anything
198	*/
199	extern thvar_t bv_solver_var_compiles_to(bv_solver_t *solver, thvar_t x);
200
201
202
203	/****************
204	* STATISTICS *
205	***************/
206
207	/*
208	* Number of variables and atoms
209	*/
210	static inline uint32_t bv_solver_num_vars(bv_solver_t *solver) {	75✔
211	return solver->vtbl.nvars;	75✔
212	}
213
214	static inline uint32_t bv_solver_num_atoms(bv_solver_t *solver) {	75✔
215	return solver->atbl.natoms;	75✔
216	}
217
218
219	/*
220	* Number of nodes in the DAG
221	*/
222	static inline uint32_t bv_solver_dag_size(bv_solver_t *solver) {
223	return (solver->compiler != NULL) ? solver->compiler->dag.nelems : 0;
224	}
225
226	static inline uint32_t bv_solver_num_leaf_nodes(bv_solver_t *solver) {
227	return (solver->compiler != NULL) ? bvc_num_complex_nodes(&solver->compiler->dag) : 0;
228	}
229
230	static inline uint32_t bv_solver_num_elem_nodes(bv_solver_t *solver) {
231	return (solver->compiler != NULL) ? bvc_num_elem_nodes(&solver->compiler->dag) : 0;
232	}
233
234	static inline uint32_t bv_solver_num_complex_nodes(bv_solver_t *solver) {
235	return (solver->compiler != NULL) ? bvc_num_complex_nodes(&solver->compiler->dag) : 0;
236	}
237
238
239	/*
240	* Atoms per type
241	*/
242	static inline uint32_t bv_solver_num_eq_atoms(bv_solver_t *solver) {	×
243	return solver->stats.eq_atoms;	×
244	}
245
246	static inline uint32_t bv_solver_num_ge_atoms(bv_solver_t *solver) {	×
247	return solver->stats.ge_atoms;	×
248	}
249
250	static inline uint32_t bv_solver_num_sge_atoms(bv_solver_t *solver) {	×
251	return solver->stats.sge_atoms;	×
252	}
253
254
255	/*
256	* Search statistics: these counters are all zero unless the solver
257	* is attached to the egraph
258	*/
259	static inline uint32_t bv_solver_on_the_fly_atoms(bv_solver_t *solver) {
260	return solver->stats.on_the_fly_atoms; // equality atoms created after bitblasting
261	}
262
263	static inline uint32_t bv_solver_equiv_lemmas(bv_solver_t *solver) {	75✔
264	return solver->stats.equiv_lemmas;	75✔
265	}
266
267	static inline uint32_t bv_solver_interface_lemmas(bv_solver_t *solver) {	75✔
268	return solver->stats.interface_lemmas;	75✔
269	}
270
271
272
273	/************************
274	* MODEL CONSTRUCTION *
275	***********************/
276
277	/*
278	* Build model: assign a concrete bitvector value to all variables
279	* - when this is called, the context has determined that the
280	* constraints are SAT (so a model does exist)
281	*/
282	extern void bv_solver_build_model(bv_solver_t *solver);
283
284
285	/*
286	* Copy the value assigned to x in the model into buffer c
287	* - return true if the value is available
288	* - return false if the solver has no model
289	*/
290	extern bool bv_solver_value_in_model(bv_solver_t solver, thvar_t x, bvconstant_t c);
291
292
293	/*
294	* Delete whatever is used to store the model
295	*/
296	extern void bv_solver_free_model(bv_solver_t *solver);
297
298
299
300	/********************************
301	* EGRAPH INTERFACE FUNCTIONS *
302	*******************************/
303
304	/*
305	* Assert that x1 and x2 are equal:
306	* - id = edge index to be used in a subsequent call to egraph_explain_term_eq
307	* - turn this into an axiom if possible
308	* - otherwise push the equality into a queue for processing on the next
309	* call to propagate.
310	*/
311	extern void bv_solver_assert_var_eq(bv_solver_t *solver, thvar_t x1, thvar_t x2, int32_t id);
312
313
314	/*
315	* Assert that x1 and x2 are distinct
316	* - hint = egraph hint for the disequality
317	* - turn this into an axiom if possible
318	* - otherwise push the equality into a queue for processing on the next
319	* call to propagate.
320	*/
321	extern void bv_solver_assert_var_diseq(bv_solver_t solver, thvar_t x1, thvar_t x2, composite_t hint);
322
323	/*
324	* Assert that a[0,...n-1] are all distinct
325	* - hint = hint for egraph explanation
326	* - this gets converted into n * (n-1) pairwise disequalities
327	*/
328	extern void bv_solver_assert_var_distinct(bv_solver_t solver, uint32_t n, thvar_t a, composite_t *hint);
329
330
331	/*
332	* Check whether x1 and x2 are distinct at the base level
333	*/
334	extern bool bv_solver_check_disequality(bv_solver_t *solver, thvar_t x1, thvar_t x2);
335
336
337	/*
338	* Generate interface equalities for conflicts between model and egraph
339	* - return the number of interface equalities created
340	* - max_eq = bound on the number of interface equalities allowed
341	*/
342	extern uint32_t bv_solver_reconcile_model(bv_solver_t *solver, uint32_t max_eq);
343
344
345
346
347	/***************************
348	* SMT/CONTROL FUNCTIONS *
349	**************************/
350
351	/*
352	* The core or egraph invokes these functions via the smt or ctrl interface
353	* descriptors. We export them for testing.
354	*/
355
356	/*
357	* Prepare for search, after internalization
358	*/
359	extern void bv_solver_start_search(bv_solver_t *solver);
360
361	/*
362	* Assert atom attached to literal l
363	* This function is called when l is assigned to true by the core
364	* - atom is the arithmetic atom attached to a boolean variable v = var_of(l)
365	* - if l is positive (i.e., pos_lit(v)), assert the atom
366	* - if l is negative (i.e., neg_lit(v)), assert its negation
367	* Return false if that causes a conflict, true otherwise.
368	*/
369	extern bool bv_solver_assert_atom(bv_solver_t solver, void atom, literal_t l);
370
371	/*
372	* Perform one round of propagation:
373	* - return true if no conflict was detected
374	* - return false if a conflict was detected, in that case the conflict
375	* clause is stored in the core
376	*/
377	extern bool bv_solver_propagate(bv_solver_t *solver);
378
379
380	/*
381	* Support for theory-branching heuristic
382	* - evaluate atom attached to l in the current simplex assignment
383	* - the result is either l or (not l)
384	* - if atom is true, return pos_lit(var_of(l))
385	* - if atom is false, return neg_lit(var_of(l))
386	*/
387	extern literal_t bv_solver_select_polarity(bv_solver_t solver, void atom, literal_t l);
388
389
390	/*
391	* Final check
392	*/
393	extern fcheck_code_t bv_solver_final_check(bv_solver_t *solver);
394
395
396	/*
397	* Start a new decision level
398	*/
399	extern void bv_solver_increase_decision_level(bv_solver_t *solver);
400
401	/*
402	* Backtrack to back_level
403	*/
404	extern void bv_solver_backtrack(bv_solver_t *solver, uint32_t back_level);
405
406
407	/*
408	* Push/pop/reset
409	*/
410	extern void bv_solver_push(bv_solver_t *solver);
411	extern void bv_solver_pop(bv_solver_t *solver);
412	extern void bv_solver_reset(bv_solver_t *solver);
413
414
415
416
417	#endif /* __BVSOLVER_H */

SRI-CSL / yices2 / 12367760548

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous