Home
last modified time | relevance | path

Searched refs:yices_not (Results 1 – 10 of 10) sorted by relevance

/dports/math/yices/yices-2.6.2/tests/unit/
H A Dtest_truth_tables.c389 t = yices_not(t); in ttbl_test_pair()
394 t = yices_not(t); in ttbl_test_pair()
399 t = yices_not(t); in ttbl_test_pair()
404 t = yices_not(t); in ttbl_test_pair()
409 t = yices_not(t); in ttbl_test_pair()
423 t = yices_ite(t1, yices_not(t2), t3); in ttbl_test_triple()
426 t = yices_ite(t1, t2, yices_not(t3)); in ttbl_test_triple()
429 t = yices_ite(t1, yices_not(t2), yices_not(t3)); in ttbl_test_triple()
435 t = yices_or3(yices_not(t1), t2, t3); in ttbl_test_triple()
437 u = yices_and2(t2, yices_not(t3)); in ttbl_test_triple()
[all …]
H A Dtest_fvar_collector.c153 ivector_push(&all, yices_not(bin_app(q, a, a))); in init_terms()
155 ivector_push(&all, forall1(a, yices_not(bin_app(q, a, a)))); in init_terms()
156 ivector_push(&all, forall1(b, yices_not(bin_app(q, a, a)))); in init_terms()
157 ivector_push(&all, forall2(x, y, yices_not(bin_app(q, a, a)))); in init_terms()
H A Dtest_api3.c545 add_term(yices_not(t)); in init_base_terms()
549 add_term(yices_not(t)); in init_base_terms()
553 add_term(yices_not(t)); in init_base_terms()
557 add_term(yices_not(t)); in init_base_terms()
561 add_term(yices_not(t)); in init_base_terms()
1008 bvarray[i] = yices_not(t1); in test_bvarray1()
1049 bvarray[i] = yices_not(t1); in test_bvarray2()
1057 bvarray[i] = yices_not(t2); in test_bvarray2()
H A Dtest_api4.c298 term_store_add_term(&all_terms, yices_not(t)); in init_store()
H A Dtest_api2.c465 add_term(yices_not(t)); in init_base_terms()
469 add_term(yices_not(t)); in init_base_terms()
473 add_term(yices_not(t)); in init_base_terms()
H A Dtest_intern_table.c429 t = yices_not(t); in random_bool_term()
/dports/math/yices/yices-2.6.2/examples/
H A Dexample_unsat_core.c159 assumption[0] = yices_not(assumption[0]); // x >= y in unsat_core_test()
160 assumption[1] = yices_not(assumption[1]); // x <= y in unsat_core_test()
161 assumption[2] = yices_not(assumption[2]); // x != y in unsat_core_test()
/dports/math/py-pysmt/pysmt-0.9.0/pysmt/solvers/
H A Dyices.py325 res = yicespy.yices_not(args[0])
/dports/math/yices/yices-2.6.2/src/include/
H A Dyices.h742 __YICES_DLLSPEC__ extern term_t yices_not(term_t arg);
/dports/math/yices/yices-2.6.2/src/api/
H A Dyices_api.c3098 EXPORTED term_t yices_not(term_t arg) { in yices_not() function