veripb-parser 0.1.2

use logos::Logos;
use veripb_formula::prelude::*;
use veripb_parser::{
    opb_parser::{parse_opb_from_file, parse_opb_objective, parse_single_constraint},
    opb_token::OPBToken,
};

#[test]
fn parse_general_opb_i64() {
    let (formula, var_names, _) = match parse_opb_from_file("./tests/instances/general_i64.opb") {
        Ok(formula) => formula,
        Err(e) => {
            eprintln!("Parsing error: {e:?}");
            panic!();
        }
    };

    assert_eq!(formula.len(), 2, "Should parse 2 constraint.");
    assert_eq!(var_names.len(), 4, "Formula should contain 4 variables.")
}

#[test]
fn parse_general_opb_i64_with_equal() {
    let (formula, var_names, _) =
        match parse_opb_from_file("./tests/instances/general_i64_equal.opb") {
            Ok(formula) => formula,
            Err(e) => {
                eprintln!("Parsing error: {e:?}");
                panic!();
            }
        };

    assert_eq!(formula.len(), 3, "Should parse 3 constraint.");
    assert_eq!(var_names.len(), 4, "Formula should contain 4 variables.")
}

#[test]
fn parse_mixed_opb_i64() {
    let (formula, var_names, _) = match parse_opb_from_file("./tests/instances/mixed_i64.opb") {
        Ok(formula) => formula,
        Err(e) => {
            eprintln!("Parsing error: {e:?}");
            panic!();
        }
    };

    assert_eq!(formula.len(), 3, "Should parse 3 constraint.");
    assert_eq!(var_names.len(), 4, "Formula should contain 4 variables.");
    assert!(
        matches!(formula.constraints[0], PBConstraintEnum::GeneralPBI64(..)),
        "The first constraint should be a general arbitrary size PB constraint."
    );
    assert!(
        matches!(formula.constraints[1], PBConstraintEnum::Cardinality(..)),
        "The third constraint should be a cardinality constraint."
    );
    assert!(
        matches!(formula.constraints[2], PBConstraintEnum::Clause(..)),
        "The fourth constraint should be a clause."
    );
}

#[test]
fn parse_general_opb_arbitrary() {
    let (formula, var_names, _) =
        match parse_opb_from_file("./tests/instances/general_arbitrary.opb") {
            Ok(formula) => formula,
            Err(e) => {
                eprintln!("Parsing error: {e:?}");
                panic!();
            }
        };

    assert_eq!(formula.len(), 2, "Should parse 2 constraint.");
    assert_eq!(var_names.len(), 4, "Formula should contain 4 variables.")
}

#[test]
fn parse_mixed_opb_arbitrary() {
    let (formula, var_names, _) = match parse_opb_from_file("./tests/instances/mixed_arbitrary.opb")
    {
        Ok(formula) => formula,
        Err(e) => {
            eprintln!("Parsing error: {e:?}");
            panic!();
        }
    };

    assert_eq!(formula.len(), 7, "Should parse 7 constraint.");
    assert_eq!(var_names.len(), 4, "Formula should contain 4 variables.");
    assert!(
        matches!(
            formula.constraints[0],
            PBConstraintEnum::GeneralPBBigInt(..)
        ),
        "The first constraint should be a general arbitrary size PB constraint."
    );
    assert!(
        matches!(formula.constraints[1], PBConstraintEnum::GeneralPBI128(..)),
        "The second constraint should be a general 128 bit PB constraint."
    );
    assert!(
        matches!(formula.constraints[2], PBConstraintEnum::Cardinality(..)),
        "The third constraint should be a cardinality constraint."
    );
    assert!(
        matches!(formula.constraints[3], PBConstraintEnum::Clause(..)),
        "The fourth constraint should be a clause."
    );
    assert!(
        matches!(
            formula.constraints[4],
            PBConstraintEnum::GeneralPBBigInt(..)
        ),
        "The fifth constraint should be a general arbitrary size PB constraint."
    );
    assert!(
        matches!(
            formula.constraints[5],
            PBConstraintEnum::GeneralPBBigInt(..)
        ),
        "The sixth constraint should be a general arbitrary size PB constraint."
    );
    assert!(
        matches!(formula.constraints[6], PBConstraintEnum::GeneralPBI128(..)),
        "The seventh constraint should be a general 128 bit PB constraint."
    );
}

#[test]
fn parse_no_terms() {
    let (formula, var_names, _) = match parse_opb_from_file("./tests/instances/no_terms.opb") {
        Ok(formula) => formula,
        Err(e) => {
            eprintln!("Parsing error: {e:?}");
            panic!();
        }
    };

    assert_eq!(formula.len(), 5, "Should parse 5 constraint.");
    assert_eq!(var_names.len(), 0, "Formula should contain 0 variables.");

    assert!(matches!(
        formula.constraints[0],
        PBConstraintEnum::Cardinality(..)
    ));
    assert!(matches!(
        formula.constraints[1],
        PBConstraintEnum::GeneralPBI128(..)
    ));
    assert!(matches!(
        formula.constraints[2],
        PBConstraintEnum::GeneralPBBigInt(..)
    ));
    assert!(matches!(
        formula.constraints[3],
        PBConstraintEnum::Clause(..)
    ));
    assert!(matches!(
        formula.constraints[4],
        PBConstraintEnum::Cardinality(..)
    ));
}

#[test]
fn parse_objective() {
    let (formula, var_names, _) = match parse_opb_from_file("./tests/instances/objective.opb") {
        Ok(formula) => formula,
        Err(e) => {
            eprintln!("Parsing error: {e:?}");
            panic!();
        }
    };

    assert_eq!(formula.len(), 0, "Should parse 0 constraint.");
    assert_eq!(var_names.len(), 3, "Formula should contain 3 variables.");
    assert_eq!(
        formula.objective.as_ref().unwrap().len(),
        3,
        "Objective should have 3 terms."
    );

    assert_eq!(formula.objective.unwrap().constant, 4.into());
}

#[test]
fn parse_only_constraint() {
    let mut lex = OPBToken::lexer("1 z1 2414213213 ~fddsewr >= 20431412 ;");
    let mut var_names = VarNameManager::default();

    let (geq, leq) =
        parse_single_constraint(&mut lex, &mut var_names).expect("Constraint should be parsed");

    assert!(matches!(geq, PBConstraintEnum::GeneralPBI64(..)));
    assert!(leq.is_none());
}

#[test]
fn parse_only_constraint_equality() {
    let mut lex = OPBToken::lexer("1 z1 2414213213 ~fddsewr = 20431412 ;");
    let mut var_names = VarNameManager::default();

    let (geq, leq) =
        parse_single_constraint(&mut lex, &mut var_names).expect("Constraint should be parsed");

    assert!(matches!(geq, PBConstraintEnum::GeneralPBI64(..)));
    assert!(leq.is_some());
    let leq = leq.unwrap();
    assert!(matches!(leq, PBConstraintEnum::GeneralPBI64(..)));
}

#[test]
fn parse_only_objective() {
    let mut lex = OPBToken::lexer("1 x1 2 ~x2 3 x3 4 ;");
    let mut var_names = VarNameManager::default();

    let objective =
        parse_opb_objective(&mut lex, &mut var_names, false).expect("Objective should be parsed.");

    assert_eq!(objective.len(), 3);
    assert_eq!(objective.constant, 4.into());
}

#[test]
fn parse_only_objective_negative() {
    let mut lex = OPBToken::lexer("-1 x1 -2 ~x2 -3 x3 4 ;");
    let mut var_names = VarNameManager::default();

    let objective =
        parse_opb_objective(&mut lex, &mut var_names, false).expect("Objective should be parsed.");

    assert_eq!(objective.len(), 3);
    assert_eq!(objective.constant, (-2).into());
}