evaltor 0.1.0

A tool for evaluating the evaluatees on benchmarks
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75

use super::{result_analyse, EvaluationResult};
use crate::EvaluateeIF;
use std::{
    path::{Path, PathBuf},
    process::Command,
};

pub struct IC3;

impl EvaluateeIF for IC3 {
    fn name(&self) -> String {
        "rIC3".to_string()
    }

    fn version(&self) -> Option<String> {
        Some("dynamic".to_string())
    }

    fn mount(&self) -> Vec<PathBuf> {
        vec![PathBuf::from("/root/rIC3")]
    }

    fn evaluate(&self, model: &Path) -> Command {
        let mut command = Command::new("/root/rIC3/target/release/rIC3");
        command.arg("-e");
        command.arg("ic3");
        command.arg("--ic3-ctg");
        command.arg("--ic3-dynamic");
        command.arg("-v0");
        // command.arg("--ic3-inn");
        // command.arg("--ic3-no-dynamic");
        // command.arg("--ic3-ctg-limit");
        // command.arg("5");
        // command.arg("--certify");
        // command.arg("--ic3-inn");
        command.arg(model);
        command
    }

    fn evaluate_with_certify(&self, model: &Path, certificate: &Path) -> Command {
        let mut cmd = self.evaluate(model);
        cmd.arg(certificate);
        cmd
    }

    fn certify(&self, model: &Path, certificate: &Path) -> bool {
        let output = Command::new("docker")
            .args([
                "run",
                "--rm",
                "-v",
                &format!("{}:{}", model.display(), model.display()),
                "-v",
                &format!("{}:{}", certificate.display(), certificate.display()),
                "ghcr.io/gipsyh/certifaiger",
            ])
            .arg(model)
            .arg(certificate)
            .output()
            .unwrap();
        if output.status.success() {
            true
        } else if let Some(1) = output.status.code() {
            false
        } else {
            panic!(
                    "certifaiger maybe not avaliable, please build docker image from https://github.com/Froleyks/certifaiger"
                );
        }
    }

    fn result_analyse(&self, code: i64, time: std::time::Duration) -> EvaluationResult {
        result_analyse(code, time, |c| matches!(c, 10 | 20))
    }
}