Home
last modified time | relevance | path

Searched refs:bv64_constant (Results 1 – 7 of 7) sorted by relevance

/dports/math/yices/yices-2.6.2/src/model/
H A Dval_to_term.c89 t = bv64_constant(terms, n, x); in convert_bitvector()
/dports/math/yices/yices-2.6.2/src/terms/
H A Dterm_manager.c566 t = bv64_constant(terms, n, bvarray_get_constant64(a, n)); in bvarray_get_term()
3947 t = bv64_constant(manager->terms, n, x); in mk_bv_constant()
4132 t = bv64_constant(manager->terms, n, bvlogic_buffer_get_constant64(b)); in mk_bvlogic_term()
4431 return bv64_constant(manager->terms, n, 0); in make_zero_bv()
4699 t = bv64_constant(manager->terms, n, m->coeff); in mk_bvarith64_term()
5039 return bv64_constant(manager->terms, n, x); in bvdiv_const64()
5124 return bv64_constant(manager->terms, n, x); in bvrem_const64()
5209 return bv64_constant(manager->terms, n, x); in bvsdiv_const64()
5269 return bv64_constant(manager->terms, n, x); in bvsrem_const64()
5329 return bv64_constant(manager->terms, n, x); in bvsmod_const64()
H A Dterm_utils.c2865 t = bv64_constant(tbl, n, b->constant64); in bvfactor_constant_to_term()
2900 t = bv64_constant(tbl, nbits, c); in bvpoly_buffer_to_term()
3027 t = bv64_constant(tbl, nbits, 0); in zero_bv_constant()
H A Dterms.h741 extern term_t bv64_constant(term_table_t *table, uint32_t n, uint64_t bv);
H A Dterms.c2616 term_t bv64_constant(term_table_t *table, uint32_t n, uint64_t bv) { in bv64_constant() function
/dports/math/yices/yices-2.6.2/tests/unit/
H A Dtest_terms.c1862 x = bv64_constant(&terms, 5, c); in test_bvconst64()
1867 y = bv64_constant(&terms, 5, c); in test_bvconst64()
/dports/math/yices/yices-2.6.2/src/api/
H A Dyices_api.c7175 return bv64_constant(__yices_globals.terms, n, c); in yices_bvconst64_term()