Searched refs:btor_exp_exists_n (Results 1 – 4 of 4) sorted by relevance
| /dports/math/boolector/boolector-3.2.2/test/ |
| H A D | test_normquant.cpp | 36 exists = btor_exp_exists_n (d_btor, x, 2, eqx); in TEST_F()
77 expected = btor_exp_exists_n (d_btor, y, 2, btor_node_invert (eqy)); in TEST_F()
157 expected = btor_exp_exists_n (d_btor, y, 2, eqy); in TEST_F()
406 exists = btor_exp_exists_n (d_btor, xy, 2, ult); in TEST_F()
429 expected = btor_exp_exists_n (d_btor, V, 4, and3); in TEST_F()
526 expected = btor_exp_exists_n (d_btor, V, 2, forallX); in TEST_F()
620 expected = btor_exp_exists_n (d_btor, V, 4, and1);
|
| /dports/math/boolector/boolector-3.2.2/src/ |
| H A D | btorexp.h | 514 BtorNode *btor_exp_exists_n (Btor *btor,
|
| H A D | btorexp.c | 1929 btor_exp_exists_n (Btor *btor, BtorNode *params[], uint32_t n, BtorNode *body) in btor_exp_exists_n() function
|
| H A D | boolector.c | 3415 res = btor_exp_exists_n (btor, params, paramc, body); in boolector_exists()
|