smt_lang/solve/
response.rs

1use crate::problem::{Problem, ToEntry, ToLang};
2use crate::solution::Solution;
3
4pub enum Response {
5    NoSolution,
6    Unknown,
7    Solution(Solution),
8}
9
10//------------------------- To Lang -------------------------
11
12impl ToLang for Response {
13    fn to_lang(&self, problem: &Problem) -> String {
14        match self {
15            Response::NoSolution => "no solution".to_string(),
16            Response::Unknown => "unknown".to_string(),
17            Response::Solution(solution) => format!("one solution:\n{}", solution.to_lang(problem)),
18        }
19    }
20}
21
22//------------------------- To Entry -------------------------
23
24impl ToEntry for Response {
25    fn to_entry(&self, problem: &Problem) -> d_stuff::Entry {
26        match self {
27            Response::NoSolution => d_stuff::Entry::new(
28                d_stuff::Status::Failure,
29                d_stuff::Text::new(
30                    "Solve   ",
31                    termion::style::Bold.to_string(),
32                    termion::color::Blue.fg_str(),
33                ),
34                Some(d_stuff::Text::new(
35                    "UNSAT",
36                    termion::style::Reset.to_string(),
37                    termion::color::Red.fg_str(),
38                )),
39                vec![],
40            ),
41            Response::Unknown => d_stuff::Entry::new(
42                d_stuff::Status::Question,
43                d_stuff::Text::new(
44                    "Solve   ",
45                    termion::style::Bold.to_string(),
46                    termion::color::Blue.fg_str(),
47                ),
48                Some(d_stuff::Text::new(
49                    "UNKNOWN",
50                    termion::style::Reset.to_string(),
51                    termion::color::Red.fg_str(),
52                )),
53                vec![],
54            ),
55            Response::Solution(solution) => d_stuff::Entry::new(
56                d_stuff::Status::Success,
57                d_stuff::Text::new(
58                    "Solve   ",
59                    termion::style::Bold.to_string(),
60                    termion::color::Blue.fg_str(),
61                ),
62                Some(d_stuff::Text::new(
63                    "SAT",
64                    termion::style::Reset.to_string(),
65                    termion::color::Green.fg_str(),
66                )),
67                vec![d_stuff::Message::new(
68                    None,
69                    d_stuff::Text::new(
70                        solution.to_lang(problem),
71                        termion::style::Reset.to_string(),
72                        termion::color::White.fg_str(),
73                    ),
74                )],
75            ),
76        }
77    }
78}
smt_lang/solve/response.rs

smt_lang/solve/
response.rs
