|
44 | 44 | #include "utils/int_hash_sets.h" |
45 | 45 |
|
46 | 46 | #include "api/yices_globals.h" |
| 47 | +#include "api/yices_api_lock_free.h" |
47 | 48 | #include "mt/thread_macros.h" |
48 | 49 |
|
49 | 50 |
|
@@ -716,45 +717,14 @@ static void cache_unsat_core(context_t *ctx, const ivector_t *core) { |
716 | 717 | } |
717 | 718 |
|
718 | 719 | /* |
719 | | - * Check under assumptions given as terms. |
720 | | - * - if MCSAT is enabled, this uses temporary labels + model interpolation. |
721 | | - * - otherwise terms are converted to literals and handled by the CDCL(T) path. |
722 | | - * |
723 | | - * Preconditions: |
724 | | - * - context status must be IDLE. |
| 720 | + * MCSAT variant of check_context_with_term_assumptions. |
| 721 | + * Caller must hold __yices_globals.lock. |
725 | 722 | */ |
726 | | -smt_status_t check_context_with_term_assumptions(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) { |
| 723 | +static smt_status_t _o_check_context_with_term_assumptions_mcsat(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) { |
727 | 724 | smt_status_t stat; |
728 | 725 | ivector_t assumptions; |
729 | 726 | uint32_t i; |
730 | 727 |
|
731 | | - if (error != NULL) { |
732 | | - *error = CTX_NO_ERROR; |
733 | | - } |
734 | | - |
735 | | - context_invalidate_unsat_core_cache(ctx); |
736 | | - |
737 | | - if (ctx->mcsat == NULL) { |
738 | | - literal_t l; |
739 | | - |
740 | | - init_ivector(&assumptions, n); |
741 | | - for (i=0; i<n; i++) { |
742 | | - l = context_add_assumption(ctx, a[i]); |
743 | | - if (l < 0) { |
744 | | - if (error != NULL) { |
745 | | - *error = l; |
746 | | - } |
747 | | - delete_ivector(&assumptions); |
748 | | - return YICES_STATUS_ERROR; |
749 | | - } |
750 | | - ivector_push(&assumptions, l); |
751 | | - } |
752 | | - |
753 | | - stat = check_context_with_assumptions(ctx, params, n, assumptions.data); |
754 | | - delete_ivector(&assumptions); |
755 | | - return stat; |
756 | | - } |
757 | | - |
758 | 728 | /* |
759 | 729 | * MCSAT: create fresh labels b_i, assert (b_i => a_i), then solve with model b_i=true. |
760 | 730 | * We extract interpolant/core before cleanup, then restore sticky UNSAT artifacts. |
@@ -793,7 +763,7 @@ smt_status_t check_context_with_term_assumptions(context_t *ctx, const param_t * |
793 | 763 | term_t implication = mk_implies(&tm, b, a[i]); |
794 | 764 |
|
795 | 765 | int_hmap_add(&label_map, b, a[i]); |
796 | | - code = assert_formula(ctx, implication); |
| 766 | + code = _o_assert_formula(ctx, implication); |
797 | 767 | if (code < 0) { |
798 | 768 | if (error != NULL) { |
799 | 769 | *error = code; |
@@ -839,6 +809,52 @@ smt_status_t check_context_with_term_assumptions(context_t *ctx, const param_t * |
839 | 809 | } |
840 | 810 | } |
841 | 811 |
|
| 812 | +static smt_status_t check_context_with_term_assumptions_mcsat(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) { |
| 813 | + MT_PROTECT(smt_status_t, __yices_globals.lock, _o_check_context_with_term_assumptions_mcsat(ctx, params, n, a, error)); |
| 814 | +} |
| 815 | + |
| 816 | +/* |
| 817 | + * Check under assumptions given as terms. |
| 818 | + * - if MCSAT is enabled, this uses temporary labels + model interpolation. |
| 819 | + * - otherwise terms are converted to literals and handled by the CDCL(T) path. |
| 820 | + * |
| 821 | + * Preconditions: |
| 822 | + * - context status must be IDLE. |
| 823 | + */ |
| 824 | +smt_status_t check_context_with_term_assumptions(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) { |
| 825 | + if (error != NULL) { |
| 826 | + *error = CTX_NO_ERROR; |
| 827 | + } |
| 828 | + |
| 829 | + context_invalidate_unsat_core_cache(ctx); |
| 830 | + |
| 831 | + if (ctx->mcsat == NULL) { |
| 832 | + smt_status_t stat; |
| 833 | + ivector_t assumptions; |
| 834 | + uint32_t i; |
| 835 | + literal_t l; |
| 836 | + |
| 837 | + init_ivector(&assumptions, n); |
| 838 | + for (i=0; i<n; i++) { |
| 839 | + l = context_add_assumption(ctx, a[i]); |
| 840 | + if (l < 0) { |
| 841 | + if (error != NULL) { |
| 842 | + *error = l; |
| 843 | + } |
| 844 | + delete_ivector(&assumptions); |
| 845 | + return YICES_STATUS_ERROR; |
| 846 | + } |
| 847 | + ivector_push(&assumptions, l); |
| 848 | + } |
| 849 | + |
| 850 | + stat = check_context_with_assumptions(ctx, params, n, assumptions.data); |
| 851 | + delete_ivector(&assumptions); |
| 852 | + return stat; |
| 853 | + } |
| 854 | + |
| 855 | + return check_context_with_term_assumptions_mcsat(ctx, params, n, a, error); |
| 856 | +} |
| 857 | + |
842 | 858 | /* |
843 | 859 | * Check with given model |
844 | 860 | * - if mcsat status is not IDLE, return the status |
|
0 commit comments