1
use std::fs::File;
2
use std::io::Write;
3
use std::path::PathBuf;
4
use std::process::exit;
5
use std::sync::Arc;
6

            
7
use anyhow::Result as AnyhowResult;
8
use anyhow::{anyhow, bail};
9
use clap::{arg, command, Parser};
10
use conjure_core::rule_engine::rewrite_naive;
11
use conjure_core::Model;
12
use conjure_oxide::defaults::get_default_rule_sets;
13
use schemars::schema_for;
14
use serde_json::to_string_pretty;
15

            
16
use conjure_core::context::Context;
17
use conjure_oxide::find_conjure::conjure_executable;
18
use conjure_oxide::rule_engine::{resolve_rule_sets, rewrite_model};
19
use conjure_oxide::{get_rules, model_from_json};
20

            
21
use conjure_oxide::utils::conjure::{get_minion_solutions, minion_solutions_to_json};
22
use conjure_oxide::SolverFamily;
23
use git_version::git_version;
24
use tracing_subscriber::filter::LevelFilter;
25
use tracing_subscriber::layer::SubscriberExt as _;
26
use tracing_subscriber::util::SubscriberInitExt as _;
27
use tracing_subscriber::{EnvFilter, Layer};
28

            
29
static AFTER_HELP_TEXT: &str = include_str!("help_text.txt");
30

            
31
#[derive(Parser, Clone)]
32
#[command(author, about, long_about = None, after_long_help=AFTER_HELP_TEXT)]
33
struct Cli {
34
    #[arg(value_name = "INPUT_ESSENCE", help = "The input Essence file")]
35
    input_file: Option<PathBuf>,
36

            
37
    #[arg(
38
        long,
39
        value_name = "EXTRA_RULE_SETS",
40
        help = "Names of extra rule sets to enable"
41
    )]
42
    extra_rule_sets: Vec<String>,
43

            
44
    #[arg(
45
        long,
46
        value_enum,
47
        value_name = "SOLVER",
48
        short = 's',
49
        help = "Solver family use (Minion by default)"
50
    )]
51
    solver: Option<SolverFamily>, // ToDo this should probably set the solver adapter
52

            
53
    #[arg(
54
        long,
55
        default_value_t = 0,
56
        short = 'n',
57
        help = "number of solutions to return (0 for all)"
58
    )]
59
    number_of_solutions: i32,
60
    // TODO: subcommands instead of these being a flag.
61
    #[arg(
62
        long,
63
        default_value_t = false,
64
        help = "Print the schema for the info JSON and exit"
65
    )]
66
    print_info_schema: bool,
67

            
68
    #[arg(
69
        long = "version",
70
        short = 'V',
71
        help = "Print the version of the program (git commit) and exit"
72
    )]
73
    version: bool,
74

            
75
    #[arg(long, help = "Save execution info as JSON to the given file-path.")]
76
    info_json_path: Option<PathBuf>,
77

            
78
    #[arg(
79
        long,
80
        help = "use the, in development, dirty-clean optimising rewriter",
81
        default_value_t = false
82
    )]
83
    use_optimising_rewriter: bool,
84

            
85
    #[arg(
86
        long,
87
        short = 'o',
88
        help = "Save solutions to a JSON file (prints to stdout by default)"
89
    )]
90
    output: Option<PathBuf>,
91

            
92
    #[arg(long, short = 'v', help = "Log verbosely to sterr")]
93
    verbose: bool,
94

            
95
    /// Do not run the solver.
96
    ///
97
    /// The rewritten model is printed to stdout in an Essence-style syntax (but is not necessarily
98
    /// valid Essence).
99
    #[arg(long, default_value_t = false)]
100
    no_run_solver: bool,
101

            
102
    // --no-x flag disables --x flag : https://jwodder.github.io/kbits/posts/clap-bool-negate/
103
    /// Check for multiple equally applicable rules, exiting if any are found.
104
    ///
105
    /// Only compatible with the default rewriter.
106
    #[arg(
107
        long,
108
        overrides_with = "_no_check_equally_applicable_rules",
109
        default_value_t = false
110
    )]
111
    check_equally_applicable_rules: bool,
112

            
113
    /// Do not check for multiple equally applicable rules [default].
114
    ///
115
    /// Only compatible with the default rewriter.
116
    #[arg(long)]
117
    _no_check_equally_applicable_rules: bool,
118
}
119

            
120
#[allow(clippy::unwrap_used)]
121
pub fn main() -> AnyhowResult<()> {
122
    let cli = Cli::parse();
123

            
124
    #[allow(clippy::unwrap_used)]
125
    if cli.print_info_schema {
126
        let schema = schema_for!(Context);
127
        println!("{}", serde_json::to_string_pretty(&schema).unwrap());
128
        return Ok(());
129
    }
130

            
131
    let target_family = cli.solver.unwrap_or(SolverFamily::Minion);
132
    let mut extra_rule_sets: Vec<String> = get_default_rule_sets();
133
    extra_rule_sets.extend(cli.extra_rule_sets.clone());
134

            
135
    // Logging:
136
    //
137
    // Using `tracing` framework, but this automatically reads stuff from `log`.
138
    //
139
    // A Subscriber is responsible for logging.
140
    //
141
    // It consists of composable layers, each of which logs to a different place in a different
142
    // format.
143
    let json_log_file = File::options()
144
        .create(true)
145
        .append(true)
146
        .open("conjure_oxide_log.json")?;
147

            
148
    let log_file = File::options()
149
        .create(true)
150
        .append(true)
151
        .open("conjure_oxide.log")?;
152

            
153
    // get log level from env-var RUST_LOG
154

            
155
    let json_layer = tracing_subscriber::fmt::layer()
156
        .json()
157
        .with_writer(Arc::new(json_log_file))
158
        .with_filter(LevelFilter::TRACE);
159

            
160
    let file_layer = tracing_subscriber::fmt::layer()
161
        .compact()
162
        .with_ansi(false)
163
        .with_writer(Arc::new(log_file))
164
        .with_filter(LevelFilter::TRACE);
165

            
166
    let default_stderr_level = if cli.verbose {
167
        LevelFilter::DEBUG
168
    } else {
169
        LevelFilter::WARN
170
    };
171

            
172
    let env_filter = EnvFilter::builder()
173
        .with_default_directive(default_stderr_level.into())
174
        .from_env_lossy();
175

            
176
    let stderr_layer = if cli.verbose {
177
        Layer::boxed(
178
            tracing_subscriber::fmt::layer()
179
                .pretty()
180
                .with_writer(Arc::new(std::io::stderr()))
181
                .with_ansi(true)
182
                .with_filter(env_filter),
183
        )
184
    } else {
185
        Layer::boxed(
186
            tracing_subscriber::fmt::layer()
187
                .compact()
188
                .with_writer(Arc::new(std::io::stderr()))
189
                .with_ansi(true)
190
                .with_filter(env_filter),
191
        )
192
    };
193

            
194
    if cli.version {
195
        println!("Version: {}", git_version!());
196
        return Ok(());
197
    }
198

            
199
    // load the loggers
200
    tracing_subscriber::registry()
201
        .with(json_layer)
202
        .with(stderr_layer)
203
        .with(file_layer)
204
        .init();
205

            
206
    if target_family != SolverFamily::Minion {
207
        tracing::error!("Only the Minion solver is currently supported!");
208
        exit(1);
209
    }
210

            
211
    let rule_sets = match resolve_rule_sets(target_family, &extra_rule_sets) {
212
        Ok(rs) => rs,
213
        Err(e) => {
214
            tracing::error!("Error resolving rule sets: {}", e);
215
            exit(1);
216
        }
217
    };
218

            
219
    let pretty_rule_sets = rule_sets
220
        .iter()
221
        .map(|rule_set| rule_set.name)
222
        .collect::<Vec<_>>()
223
        .join(", ");
224

            
225
    tracing::info!("Enabled rule sets: [{}]", pretty_rule_sets);
226
    tracing::info!(
227
        target: "file",
228
        "Rule sets: {}",
229
        pretty_rule_sets
230
    );
231

            
232
    let rules = get_rules(&rule_sets)?.into_iter().collect::<Vec<_>>();
233
    tracing::info!(
234
        target: "file",
235
        "Rules: {}",
236
        rules.iter().map(|rd| format!("{}", rd)).collect::<Vec<_>>().join("\n")
237
    );
238
    let input = cli.input_file.clone().expect("No input file given");
239
    tracing::info!(target: "file", "Input file: {}", input.display());
240
    let input_file: &str = input.to_str().ok_or(anyhow!(
241
        "Given input_file could not be converted to a string"
242
    ))?;
243

            
244
    /******************************************************/
245
    /*        Parse essence to json using Conjure         */
246
    /******************************************************/
247

            
248
    conjure_executable()
249
        .map_err(|e| anyhow!("Could not find correct conjure executable: {}", e))?;
250

            
251
    let mut cmd = std::process::Command::new("conjure");
252
    let output = cmd
253
        .arg("pretty")
254
        .arg("--output-format=astjson")
255
        .arg(input_file)
256
        .output()?;
257

            
258
    let conjure_stderr = String::from_utf8(output.stderr)?;
259
    if !conjure_stderr.is_empty() {
260
        bail!(conjure_stderr);
261
    }
262

            
263
    let astjson = String::from_utf8(output.stdout)?;
264

            
265
    let context = Context::new_ptr(
266
        target_family,
267
        extra_rule_sets.clone(),
268
        rules,
269
        rule_sets.clone(),
270
    );
271

            
272
    context.write().unwrap().file_name = Some(input.to_str().expect("").into());
273

            
274
    if cfg!(feature = "extra-rule-checks") {
275
        tracing::info!("extra-rule-checks: enabled");
276
    } else {
277
        tracing::info!("extra-rule-checks: disabled");
278
    }
279

            
280
    let mut model = model_from_json(&astjson, context.clone())?;
281

            
282
    tracing::info!("Initial model: \n{}\n", model);
283

            
284
    tracing::info!("Rewriting model...");
285

            
286
    if cli.use_optimising_rewriter {
287
        tracing::info!("Using the dirty-clean rewriter...");
288
        model = rewrite_model(&model, &rule_sets)?;
289
    } else {
290
        tracing::info!("Rewriting model...");
291
        model = rewrite_naive(&model, &rule_sets, cli.check_equally_applicable_rules)?;
292
    }
293

            
294
    tracing::info!("Rewritten model: \n{}\n", model);
295

            
296
    if cli.no_run_solver {
297
        println!("{}", model);
298
    } else {
299
        run_solver(&cli.clone(), model)?;
300
    }
301

            
302
    // still do postamble even if we didn't run the solver
303
    if let Some(path) = cli.info_json_path {
304
        #[allow(clippy::unwrap_used)]
305
        let context_obj = context.read().unwrap().clone();
306
        let generated_json = &serde_json::to_value(context_obj)?;
307
        let pretty_json = serde_json::to_string_pretty(&generated_json)?;
308
        File::create(path)?.write_all(pretty_json.as_bytes())?;
309
    }
310
    Ok(())
311
}
312

            
313
/// Runs the solver
314
fn run_solver(cli: &Cli, model: Model) -> anyhow::Result<()> {
315
    let out_file: Option<File> = match &cli.output {
316
        None => None,
317
        Some(pth) => Some(
318
            File::options()
319
                .create(true)
320
                .truncate(true)
321
                .write(true)
322
                .open(pth)?,
323
        ),
324
    };
325

            
326
    let solutions = get_minion_solutions(model, cli.number_of_solutions)?; // ToDo we need to properly set the solver adaptor here, not hard code minion
327
    tracing::info!(target: "file", "Solutions: {}", minion_solutions_to_json(&solutions));
328

            
329
    let solutions_json = minion_solutions_to_json(&solutions);
330
    let solutions_str = to_string_pretty(&solutions_json)?;
331
    match out_file {
332
        None => {
333
            println!("Solutions:");
334
            println!("{}", solutions_str);
335
        }
336
        Some(mut outf) => {
337
            outf.write_all(solutions_str.as_bytes())?;
338
            println!(
339
                "Solutions saved to {:?}",
340
                &cli.output.clone().unwrap().canonicalize()?
341
            )
342
        }
343
    }
344
    Ok(())
345
}
346

            
347
#[cfg(test)]
348
mod tests {
349
    use conjure_oxide::{get_example_model, get_example_model_by_path};
350

            
351
    #[test]
352
1
    fn test_get_example_model_success() {
353
1
        let filename = "input";
354
1
        get_example_model(filename).unwrap();
355
1
    }
356

            
357
    #[test]
358
1
    fn test_get_example_model_by_filepath() {
359
1
        let filepath = "tests/integration/xyz/input.essence";
360
1
        get_example_model_by_path(filepath).unwrap();
361
1
    }
362

            
363
    #[test]
364
1
    fn test_get_example_model_fail_empty_filename() {
365
1
        let filename = "";
366
1
        get_example_model(filename).unwrap_err();
367
1
    }
368

            
369
    #[test]
370
1
    fn test_get_example_model_fail_empty_filepath() {
371
1
        let filepath = "";
372
1
        get_example_model_by_path(filepath).unwrap_err();
373
1
    }
374
}