// Copyright Pierre Carbonnelle, 2024.

use std::fs::{self, File};
use std::io::Write;
use std::path::Path;

use m2csmt::solver::Solver;

fn test_file(file_name: &str) {

    // read file
    let input_path = Path::new("tests").join(file_name);
    let expected = fs::read_to_string(input_path.clone())
        .expect("Should have been able to read the input file");
    let input = expected.split("\n-------------------------\n").collect::<Vec<&str>>()[0];

    // execute file
    let mut solver = Solver::default();
    let results = solver.parse_and_execute(&input);
    let result = results.into_iter().collect::<Vec<_>>().join("\n");

    // compare to expected
    let actual = input.to_owned() + "\n-------------------------\n"+ &result;
    if actual != expected {  // write to file
        let mut expected_file = File::create(input_path).expect("creation failed");
        expected_file.write(actual.as_bytes(),).expect("write failed");
    }
    assert_eq!(actual, expected);

}


#[test]
fn test_inari() {
    use inari::*;
    let x = interval!("[-5.005, -5.0]").unwrap();  // -5.0
    let y = interval!("[-10.0, 10.0]").unwrap(); // unknown
    let sum = interval!("[5.0, 5.0]").unwrap();  // 5.0
    assert_eq!(interval!(f64::NEG_INFINITY, f64::INFINITY).unwrap(), Interval::ENTIRE);
    assert_eq!(sum-x, const_interval!(10.0, 10.005));
    assert_eq!((sum-x).intersection(y), const_interval!(10.0, 10.0));

    let x = interval!(0.0, f64::INFINITY).unwrap();  // -5.0
    assert_eq!(sum*x, x);
    assert_eq!(x-x, Interval::ENTIRE);
}
#[test]
fn test_0_degree() {  test_file( "0_degree.smt2") }

#[test]
fn test_1_degree() { test_file( "1_degree.smt2") }

#[test]
fn test_2_degrees() { test_file( "2_degree.smt2") }

#[test]
fn test_3_degrees() { test_file( "3_degree.smt2") }

#[test]
fn test_negation() { test_file( "negation.smt2") }

#[test]
fn test_double() { test_file( "double_negation.smt2") }

#[test]
fn test_contradiction() { test_file( "contradiction.smt2") }

#[test]
fn test_weighted_sum() { test_file( "WeightedSum.smt2") }

#[test]
fn test_minus() { test_file( "minus.smt2") }

#[test]
fn test_product() { test_file( "product.smt2") }

#[test]
fn test_div() { test_file( "div.smt2") }

#[test]
fn test_power() { test_file( "power.smt2") }

#[test]
fn test_cos() { test_file( "cos.smt2") }

#[test]
fn test_acos() { test_file( "acos.smt2") }

#[test]
fn test_exp() { test_file( "exp.smt2") }

#[test]
fn test_less_than() { test_file( "less_than.smt2") }

#[test]
fn test_less() { test_file( "less.smt2") }

#[test]
fn test_dreal() { test_file( "dReal.smt2") }

#[test]
fn test_demo() { test_file( "demo.smt2") }

// #[test]
// fn test_bellido() { test_file( "Bellido.smt2") }