| /dports/math/boolector/boolector-3.2.2/test/ |
| H A D | test_inc.cpp | 71 res = boolector_sat (d_btor); in test_inc_counter()
122 res = boolector_sat (d_btor); in test_inc_lt()
145 res = boolector_sat (d_btor); in TEST_F()
149 res = boolector_sat (d_btor); in TEST_F()
205 sat_result = boolector_sat (d_btor); in TEST_F()
208 sat_result = boolector_sat (d_btor); in TEST_F()
211 sat_result = boolector_sat (d_btor); in TEST_F()
243 sat_result = boolector_sat (d_btor); in TEST_F()
246 sat_result = boolector_sat (d_btor); in TEST_F()
|
| H A D | test_misc.cpp | 92 ASSERT_EQ (boolector_sat (btor), BOOLECTOR_SAT); in slice_test_misc()
173 ASSERT_EQ (boolector_sat (btor), BOOLECTOR_SAT); in ext_test_misc()
243 ASSERT_EQ (boolector_sat (btor), BOOLECTOR_SAT); in concat_test_misc()
297 ASSERT_EQ (boolector_sat (btor), BOOLECTOR_SAT); in cond_test_misc()
353 ASSERT_EQ (boolector_sat (btor), BOOLECTOR_SAT); in read_test_misc()
|
| H A D | test_logic.cpp | 58 ASSERT_EQ (boolector_sat (d_btor), BOOLECTOR_SAT); in not_logic_test()
112 ASSERT_EQ (boolector_sat (d_btor), BOOLECTOR_SAT); in binary_logic_test()
163 ASSERT_EQ (boolector_sat (d_btor), BOOLECTOR_SAT); in xnor_logic_test()
213 sat_res = boolector_sat (d_btor); in red_logic_test()
|
| H A D | test_comp.cpp | 61 sat_res = boolector_sat (d_btor); in u_comp_test()
115 sat_res = boolector_sat (d_btor); in s_comp_test()
|
| H A D | test_arithmetic.cpp | 64 ASSERT_EQ (boolector_sat (d_btor), BOOLECTOR_SAT); in u_arithmetic_test()
122 ASSERT_EQ (boolector_sat (d_btor), BOOLECTOR_SAT); in s_arithmetic_test()
|
| H A D | test_overflow.cpp | 115 sat_res = boolector_sat (d_btor); in u_overflow_test()
214 sat_res = boolector_sat (d_btor); in s_overflow_test()
|
| H A D | test_rotate.cpp | 67 res = boolector_sat (d_btor); in test_rot()
|
| H A D | test.h | 198 sat_res = boolector_sat (d_btor);
|
| H A D | test_shift.cpp | 117 res = boolector_sat (btor); in test_shift()
|
| /dports/math/boolector/boolector-3.2.2/examples/api/c/array/ |
| H A D | array3.c | 34 result = boolector_sat (btor); in main()
44 result = boolector_sat (btor); in main()
48 result = boolector_sat (btor); in main()
|
| H A D | array1.c | 74 result = boolector_sat (btor); in main()
|
| H A D | array2.c | 44 result = boolector_sat (btor); in main()
|
| /dports/math/boolector/boolector-3.2.2/examples/api/c/bv/ |
| H A D | bv1.c | 60 result = boolector_sat (btor); in main()
|
| H A D | bv2.c | 47 result = boolector_sat (btor); in main()
|
| /dports/math/boolector/boolector-3.2.2/examples/api/c/ |
| H A D | quickstart.c | 46 int result = boolector_sat (btor); in main()
|
| /dports/math/boolector/boolector-3.2.2/doc/ |
| H A D | cboolector.rst | 51 Assumptions are invalidated after a call to :c:func:`boolector_sat`.
104 :c:func:`boolector_sat`.
279 For each call to :c:func:`boolector_sat`, various simplification techniques
|
| /dports/math/boolector/boolector-3.2.2/ |
| H A D | NEWS | 27 + boolector_sat is not automatically called on smt2 input anymore, must be
338 + limited boolector_sat calls
|
| /dports/math/boolector/boolector-3.2.2/examples/api/c/sudoku/ |
| H A D | sudoku.c | 351 sat_result = boolector_sat (btor); in main()
|
| /dports/math/boolector/boolector-3.2.2/src/ |
| H A D | boolector.h | 338 int32_t boolector_sat (Btor *btor);
|
| H A D | btormc.c | 1384 res = boolector_sat (mc->forward); in check_last_forward_frame()
1422 res = boolector_sat (mc->forward); in check_last_forward_frame()
|
| H A D | btormain.c | 1540 sat_res = boolector_sat (btor); in boolector_main()
|
| H A D | btoruntrace.c | 765 ret_int = boolector_sat (btor); in parse()
|
| /dports/math/boolector/boolector-3.2.2/src/api/python/ |
| H A D | btorapi.pxd | 100 int32_t boolector_sat (Btor * btor) \
|
| H A D | pyboolector.pyx | 770 boolector_sat call no matter at what level they were assumed.
787 boolector_sat call no matter at what level they were assumed.
930 return btorapi.boolector_sat(self._c_btor)
|
| /dports/math/boolector/boolector-3.2.2/src/parser/ |
| H A D | btorsmt.c | 2462 satres = boolector_sat (parser->btor); in smt_parser_inc_add_release_sat()
|