Grcov report - int

1

//! Materialising the SMT integer theories.

2

//!

3

//! [`SmtLia`] and [`SmtBv`] do not decompose a variable -- they leave one variable of the same

4

//! domain -- so all that is needed here is to point references at the variable the representation

5

//! introduced. The adaptor then reads the theory back off that variable's representation and gives

6

//! it the matching Z3 sort.

7

//!

8

//! A declaration carrying both representations gets a channelling equality between the two from the

9

//! representation machinery, which lands here as an equality between the two variables; the adaptor

10

//! bridges the sorts.

11

12

use conjure_cp::ast::{Atom, Expression as Expr, Reference, SymbolTable};

13

use conjure_cp::rule_engine::{

14

    ApplicationError::RuleNotApplicable, ApplicationResult, RuleEffect, register_rule,

15

};

16

17

use crate::types::int::{SmtBv, SmtLia};

18

use crate::types::matrix::MatrixArray;

19

20

/// Point a reference at the variable its linear-arithmetic representation introduced.

21

#[register_rule("Smt", 9500, [Atomic])]

22

552059

fn smt_int_lia_variable(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

23

552059

    let Expr::Atomic(_, Atom::Reference(reference)) = expr else {

24

283194

        return Err(RuleNotApplicable);

25

};

26

268865

    let state = reference.get_repr_as::<SmtLia>().ok_or(RuleNotApplicable)?;

27

28497

    Ok(RuleEffect::pure(Reference::new(state.value.clone()).into()))

28

552059

29

30

/// Point a reference at the variable its bit-vector representation introduced.

31

#[register_rule("Smt", 9500, [Atomic])]

32

552059

fn smt_int_bv_variable(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

33

552059

    let Expr::Atomic(_, Atom::Reference(reference)) = expr else {

34

283194

        return Err(RuleNotApplicable);

35

};

36

268865

    let state = reference.get_repr_as::<SmtBv>().ok_or(RuleNotApplicable)?;

37

17143

    Ok(RuleEffect::pure(Reference::new(state.value.clone()).into()))

38

552059

39

40

/// Point a reference at the array its layout representation introduced.

41

///

42

/// The array's element sort is not decided here: the variable this leaves behind goes on to pick

43

/// `lia` or `bv` for its integers like any other declaration.

44

#[register_rule("Smt", 9500, [Atomic])]

45

552059

fn smt_matrix_array_variable(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

46

552059

    let Expr::Atomic(_, Atom::Reference(reference)) = expr else {

47

283194

        return Err(RuleNotApplicable);

48

};

49

268865

    let state = reference

50

268865

        .get_repr_as::<MatrixArray>()

51

268865

        .ok_or(RuleNotApplicable)?;

52

30191

    Ok(RuleEffect::pure(Reference::new(state.value.clone()).into()))

53

552059