smt-lang 0.7.5

Sat Modulo Theory Language
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

use clap::Parser;
use smt_lang::{load_file, problem::*, solve::solve};

/// Simple program to greet a person
#[derive(Parser, Debug)]
#[command(author, version, about, long_about = None)]
struct Args {
    /// input file
    #[arg(short, long)]
    file: String,
    /// verbose level
    #[arg(short, long, default_value_t = 1)]
    verbose: u8,
    /// parallel N (number of threads)
    #[arg(short, long, default_value_t = 1)]
    parallel: u32,
    /// Optimize solver
    #[arg(short, long, default_value_t = false)]
    optimize: bool,
}

fn main() {
    let mut pretty = d_stuff::Pretty::new();

    let args = Args::parse();
    //
    let mut problem = Problem::new();

    match load_file(&mut pretty, &mut problem, &args.file, args.verbose) {
        Ok(_) => {
            if args.verbose >= 2 {
                pretty.add(problem.to_entry());
                pretty.print();
            }
            let response = solve(
                &mut pretty,
                &problem,
                args.verbose,
                args.parallel,
                args.optimize,
            );
            pretty.add(response.to_entry(&problem));
            if args.verbose > 0 {
                pretty.print();
            } else {
                println!("{}", response.to_lang(&problem));
            }
        }
        Err(e) => {
            pretty.add(e.to_entry(&problem));
            if args.verbose > 0 {
                pretty.print();
            }
        }
    }
}