xlsynth-prover 0.76.0

XLS formal pProvers
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

// SPDX-License-Identifier: Apache-2.0

pub mod cosliced;
pub mod focus;
pub mod utils;

use self::cosliced::CoslicedTactic;
use self::focus::FocusTactic;
use crate::dslx_tactics::obligations::ProverObligation;
use serde::de::DeserializeOwned;
use serde::{Deserialize, Serialize};

/// Object-safe tactic interface. Tactics transform a base obligation into
/// zero or more sub-obligations.
pub trait IsTactic: Send + Sync + std::fmt::Debug + Serialize + DeserializeOwned {
    /// Human-readable tactic name.
    fn name(&self) -> &'static str;

    /// Applies the tactic to the given base obligation.
    fn apply(&self, base: &ProverObligation) -> Result<Vec<ProverObligation>, String>;
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub enum Tactic {
    Cosliced(CoslicedTactic),
    Focus(FocusTactic),
}

impl IsTactic for Tactic {
    fn name(&self) -> &'static str {
        match self {
            Tactic::Cosliced(t) => t.name(),
            Tactic::Focus(t) => t.name(),
        }
    }

    fn apply(&self, base: &ProverObligation) -> Result<Vec<ProverObligation>, String> {
        match self {
            Tactic::Cosliced(t) => t.apply(base),
            Tactic::Focus(t) => t.apply(base),
        }
    }
}