yaspar-ir 2.7.1

This crate provides a few representations of SMT scripts and other functionalities.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0

use crate::allocator::ObjectAllocatorExt;
use crate::ast::{FetchSort, HasArena, HasArenaAlt, TC, Term};
use crate::raw::tc::sort_mismatch;

/// check whether the given term is boolean
pub(crate) fn is_term_bool_alt<E: HasArenaAlt>(ctx: &mut E, t: &Term, meta: &str) -> TC<()> {
    let s = t.get_sort(ctx);
    if s.is_bool() {
        Ok(())
    } else {
        let bool = ctx.arena_alt().bool_sort();
        sort_mismatch(&bool, &s, t, meta)
    }
}

/// check whether the given term is boolean
pub fn is_term_bool<E: HasArena>(ctx: &mut E, t: &Term) -> TC<()> {
    is_term_bool_alt(ctx, t, "")
}