Grcov report - bitvector

1

use conjure_cp::ast::{Expression, Metadata, Moo, SymbolTable};

2

use conjure_cp::rule_engine::{

3

    ApplicationError, ApplicationResult, Reduction, register_rule, register_rule_set,

4

};

5

use conjure_cp::solver::SolverFamily;

6

use conjure_cp::solver::adaptors::smt::{IntTheory, TheoryConfig};

7

8

// Only applicable when the Bitvector theory is being used for integers

9

register_rule_set!("SmtBvInts", ("Base"), |f: &SolverFamily| matches!(

10

f,

11

    SolverFamily::Smt(TheoryConfig {

12

        ints: IntTheory::Bv,

13

..

14

})

15

));

16

17

#[register_rule(("SmtBvInts", 1000))]

18

fn fold_list_exprs_pairwise(expr: &Expression, _: &SymbolTable) -> ApplicationResult {

19

    match expr {

20

        Expression::Sum(_, vec_expr) => fold_list_pairwise(vec_expr, Expression::PairwiseSum),

21

        Expression::Product(_, vec_expr) => {

22

            fold_list_pairwise(vec_expr, Expression::PairwiseProduct)

23

24

        _ => Err(ApplicationError::RuleNotApplicable),

25

26

27

28

fn fold_list_pairwise(

29

    exprs: &Expression,

30

    op: impl Fn(Metadata, Moo<Expression>, Moo<Expression>) -> Expression,

31

) -> ApplicationResult {

32

    exprs

33

        .clone()

34

        .unwrap_list()

35

        .ok_or(ApplicationError::RuleNotApplicable)?

36

        .iter()

37

        .cloned()

38

        .reduce(|a, b| (op)(Default::default(), Moo::new(a), Moo::new(b)))

39

        .map(Reduction::pure)

40

        .ok_or(ApplicationError::RuleNotApplicable)

41