///////////////////////////////////////////////////////////////////////////
//                   __                _      _   ________               //
//                  / /   ____  ____ _(_)____/ | / / ____/               //
//                 / /   / __ \/ __ `/ / ___/  |/ / / __                 //
//                / /___/ /_/ / /_/ / / /__/ /|  / /_/ /                 //
//               /_____/\____/\__, /_/\___/_/ |_/\____/                  //
//                           /____/                                      //
//                                                                       //
//               The Next Generation Logic Library                       //
//                                                                       //
///////////////////////////////////////////////////////////////////////////
//                                                                       //
//  Copyright 2015-20xx Christoph Zengler                                //
//                                                                       //
//  Licensed under the Apache License, Version 2.0 (the "License");      //
//  you may not use this file except in compliance with the License.     //
//  You may obtain a copy of the License at                              //
//                                                                       //
//  http://www.apache.org/licenses/LICENSE-2.0                           //
//                                                                       //
//  Unless required by applicable law or agreed to in writing, software  //
//  distributed under the License is distributed on an "AS IS" BASIS,    //
//  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or      //
//  implied.  See the License for the specific language governing        //
//  permissions and limitations under the License.                       //
//                                                                       //
///////////////////////////////////////////////////////////////////////////

package org.logicng.formulas;

import static org.assertj.core.api.Assertions.assertThat;
import static org.assertj.core.api.Assertions.assertThatThrownBy;

import org.junit.jupiter.api.Test;
import org.logicng.configurations.Configuration;
import org.logicng.configurations.ConfigurationType;
import org.logicng.io.parsers.ParserException;
import org.logicng.io.parsers.PropositionalParser;
import org.logicng.solvers.maxsat.algorithms.MaxSATConfig;
import org.logicng.solvers.sat.GlucoseConfig;
import org.logicng.solvers.sat.MiniSatConfig;

import java.util.ArrayList;
import java.util.Collections;
import java.util.List;

/**
 * Test some basic formula factory functionality.
 * @version 2.2.0
 * @since 1.0
 */
public class FormulaFactoryTest {

    @Test
    public void testPutConfigurationWithInvalidArgument() {
        assertThatThrownBy(() -> {
            final FormulaFactory f = new FormulaFactory();
            f.putConfiguration(FormulaFactoryConfig.builder().build());
        }).isInstanceOf(IllegalArgumentException.class)
                .hasMessage("Configurations for the formula factory itself can only be passed in the constructor.");
    }

    @Test
    public void testConstant() {
        final FormulaFactory f = new FormulaFactory();
        assertThat(f.constant(true)).isEqualTo(f.verum());
        assertThat(f.constant(false)).isEqualTo(f.falsum());
    }

    @Test
    public void testToString() {
        final FormulaFactory f = new FormulaFactory(FormulaFactoryConfig.builder().name("MyFormulaFactory").build());
        f.variable("a");
        f.literal("b", false);
        f.and(f.variable("a"), f.literal("b", false));
        f.or(f.variable("a"), f.literal("b", false), f.variable("x"), f.implication(f.variable("a"), f.variable("x")));
        final String expected = String.format("Name:              MyFormulaFactory%n" +
                "Positive Literals: 3%n" +
                "Negative Literals: 1%n" +
                "Negations:         0%n" +
                "Implications:      1%n" +
                "Equivalences:      0%n" +
                "Conjunctions (2):  1%n" +
                "Conjunctions (3):  0%n" +
                "Conjunctions (4):  0%n" +
                "Conjunctions (>4): 0%n" +
                "Disjunctions (2):  0%n" +
                "Disjunctions (3):  0%n" +
                "Disjunctions (4):  1%n" +
                "Disjunctions (>4): 0%n" +
                "Pseudo Booleans:   0%n" +
                "CCs:               0%n");
        assertThat(f.toString()).isEqualTo(expected);
    }

    @Test
    public void testDefaultName() {
        final FormulaFactory f = new FormulaFactory();
        assertThat(f.name()).isEqualTo("");
    }

    @Test
    public void testConfigurations() {
        final FormulaFactory f = new FormulaFactory();
        final Configuration configMaxSat = MaxSATConfig.builder().build();
        final Configuration configMiniSat = MiniSatConfig.builder().build();
        final Configuration configGlucose = GlucoseConfig.builder().build();
        f.putConfiguration(configMaxSat);
        f.putConfiguration(configMiniSat);
        f.putConfiguration(configGlucose);
        assertThat(f.configurationFor(ConfigurationType.MAXSAT)).isEqualTo(configMaxSat);
        assertThat(f.configurationFor(ConfigurationType.MINISAT)).isEqualTo(configMiniSat);
        assertThat(f.configurationFor(ConfigurationType.GLUCOSE)).isEqualTo(configGlucose);
    }

    @Test
    public void testGeneratedVariables() {
        FormulaFactory f = new FormulaFactory();
        Variable ccVar = f.newCCVariable();
        Variable cnfVar = f.newCNFVariable();
        Variable pbVar = f.newPBVariable();
        Variable var = f.variable("x");
        assertThat(f.isGeneratedVariable(ccVar)).isTrue();
        assertThat(f.isGeneratedVariable(cnfVar)).isTrue();
        assertThat(f.isGeneratedVariable(pbVar)).isTrue();
        assertThat(f.isGeneratedVariable(var)).isFalse();
        assertThat(ccVar.name()).isEqualTo("@RESERVED_CC_0");
        assertThat(pbVar.name()).isEqualTo("@RESERVED_PB_0");
        assertThat(cnfVar.name()).isEqualTo("@RESERVED_CNF_0");

        f = new FormulaFactory(FormulaFactoryConfig.builder().name("f").build());
        ccVar = f.newCCVariable();
        cnfVar = f.newCNFVariable();
        pbVar = f.newPBVariable();
        var = f.variable("x");
        assertThat(f.isGeneratedVariable(ccVar)).isTrue();
        assertThat(f.isGeneratedVariable(cnfVar)).isTrue();
        assertThat(f.isGeneratedVariable(pbVar)).isTrue();
        assertThat(f.isGeneratedVariable(var)).isFalse();
        assertThat(ccVar.name()).isEqualTo("@RESERVED_CC_f_0");
        assertThat(pbVar.name()).isEqualTo("@RESERVED_PB_f_0");
        assertThat(cnfVar.name()).isEqualTo("@RESERVED_CNF_f_0");
    }

    @Test
    public void testCNF() {
        final FormulaFactory f = new FormulaFactory();
        final Variable a = f.variable("A");
        final Variable b = f.variable("B");
        final Variable c = f.variable("C");
        final Variable d = f.variable("D");
        final Formula clause1 = f.or(a, b);
        final Formula clause2 = f.or(c, d.negate());
        final Formula nClause1 = f.implication(a, c);

        final List<Formula> clauses = new ArrayList<>();
        clauses.add(clause1);
        clauses.add(clause2);

        final List<Formula> nClauses = new ArrayList<>();
        nClauses.add(clause1);
        nClauses.add(clause2);
        nClauses.add(nClause1);

        final Formula cnf = f.cnf(clauses);
        final Formula nCnf = f.cnf(nClauses);
        assertThat(cnf.cnf()).isEqualTo(cnf);
        assertThat(nCnf.cnf()).isNotEqualTo(nCnf);
        assertThat(f.cnf(Collections.emptyList())).isEqualTo(f.verum());
    }

    @Test
    public void testImportFormula() throws ParserException {
        final FormulaFactory f = new FormulaFactory(FormulaFactoryConfig.builder().name("Factory F").build());
        final FormulaFactory g = new FormulaFactory(FormulaFactoryConfig.builder().name("Factory G").build());
        final PropositionalParser pf = new PropositionalParser(f);
        final String formula = "x1 & x2 & ~x3 => (x4 | (x5 <=> ~x1))";
        final Formula ff = pf.parse(formula);
        final Formula fg = g.importFormula(ff);
        assertThat(fg).isEqualTo(ff);
        assertThat(ff.factory()).isSameAs(f);
        assertThat(fg.factory()).isSameAs(g);
        assertThat(f.statistics()).isEqualToComparingOnlyGivenFields(g.statistics(), "positiveLiterals",
                "negativeLiterals", "negations", "implications", "equivalences", "conjunctions2", "conjunctions3",
                "conjunctions4", "conjunctionsN", "disjunctions2", "disjunctions3", "disjunctions4");
        for (final Literal litF : ff.literals()) {
            assertThat(litF.factory()).isSameAs(f);
        }
        for (final Literal litG : fg.literals()) {
            assertThat(litG.factory()).isSameAs(g);
        }
    }

    @Test
    public void testStatistics() {
        final FormulaFactory f = new FormulaFactory(FormulaFactoryConfig.builder().name("Factory F").build());
        final FormulaFactory g = new FormulaFactory(FormulaFactoryConfig.builder().name("Factory F").build());
        final FormulaFactory.FormulaFactoryStatistics statisticsF1 = f.statistics();
        final FormulaFactory.FormulaFactoryStatistics statisticsG = g.statistics();

        assertThat(statisticsF1.name()).isEqualTo("Factory F");
        assertThat(statisticsF1.positiveLiterals()).isEqualTo(0);
        assertThat(statisticsF1.negativeLiterals()).isEqualTo(0);
        assertThat(statisticsF1.negations()).isEqualTo(0);
        assertThat(statisticsF1.implications()).isEqualTo(0);
        assertThat(statisticsF1.equivalences()).isEqualTo(0);
        assertThat(statisticsF1.conjunctions2()).isEqualTo(0);
        assertThat(statisticsF1.conjunctions3()).isEqualTo(0);
        assertThat(statisticsF1.conjunctions4()).isEqualTo(0);
        assertThat(statisticsF1.conjunctionsN()).isEqualTo(0);
        assertThat(statisticsF1.disjunctions2()).isEqualTo(0);
        assertThat(statisticsF1.disjunctions3()).isEqualTo(0);
        assertThat(statisticsF1.disjunctions4()).isEqualTo(0);
        assertThat(statisticsF1.disjunctionsN()).isEqualTo(0);
        assertThat(statisticsF1.pbcs()).isEqualTo(0);
        assertThat(statisticsF1.ccs()).isEqualTo(0);
        assertThat(statisticsF1.ccCounter()).isEqualTo(0);
        assertThat(statisticsF1.pbCounter()).isEqualTo(0);
        assertThat(statisticsF1.cnfCounter()).isEqualTo(0);
        assertThat(statisticsF1.formulas()).isEqualTo(0);

        assertThat(statisticsF1.equals(statisticsF1)).isTrue();
        assertThat(statisticsF1).isEqualTo(statisticsF1);
        assertThat(statisticsF1.equals(42)).isFalse();
        assertThat(statisticsF1).isEqualTo(statisticsG);
        assertThat(statisticsG).isEqualTo(statisticsF1);
        assertThat(statisticsF1.hashCode()).isEqualTo(statisticsG.hashCode());

        assertThat(statisticsF1.toString()).isEqualTo(
                "FormulaFactoryStatistics{"
                        + "name='Factory F'"
                        + ", positiveLiterals=0"
                        + ", negativeLiterals=0"
                        + ", negations=0"
                        + ", implications=0"
                        + ", equivalences=0"
                        + ", conjunctions2=0"
                        + ", conjunctions3=0"
                        + ", conjunctions4=0"
                        + ", conjunctionsN=0"
                        + ", disjunctions2=0"
                        + ", disjunctions3=0"
                        + ", disjunctions4=0"
                        + ", disjunctionsN=0"
                        + ", pbcs=0"
                        + ", ccs=0"
                        + ", ccCounter=0"
                        + ", pbCounter=0"
                        + ", cnfCounter=0"
                        + '}');

        final Variable a = f.variable("A");
        final Variable b = f.variable("B");
        final Variable c = f.variable("C");
        final Variable d = f.variable("D");
        final Variable e = f.variable("E");
        final And and = (And) f.and(a, b);
        final And and3 = (And) f.and(a, b, c);
        final And and4 = (And) f.and(a, b, c, d);
        final And and5 = (And) f.and(a, b, c, d, e);
        final Or or2 = (Or) f.or(a, b);
        final Or or3 = (Or) f.or(a, b, c);
        final Or or4 = (Or) f.or(a, b, c, d);
        final Or or5 = (Or) f.or(a, b, c, d, e);
        assertThat(f.posLiterals).containsValue(b);
        assertThat(f.ands2).containsValue(and);
        assertThat(f.ands3).containsValue(and3);
        assertThat(f.ands4).containsValue(and4);
        assertThat(f.andsN).containsValue(and5);
        assertThat(f.ors2).containsValue(or2);
        assertThat(f.ors3).containsValue(or3);
        assertThat(f.ors4).containsValue(or4);
        assertThat(f.orsN).containsValue(or5);

        final FormulaFactory.FormulaFactoryStatistics statisticsF2 = f.statistics();

        assertThat(statisticsF2.name()).isEqualTo("Factory F");
        assertThat(statisticsF2.positiveLiterals()).isEqualTo(5);
        assertThat(statisticsF2.negativeLiterals()).isEqualTo(0);
        assertThat(statisticsF2.negations()).isEqualTo(0);
        assertThat(statisticsF2.implications()).isEqualTo(0);
        assertThat(statisticsF2.equivalences()).isEqualTo(0);
        assertThat(statisticsF2.conjunctions2()).isEqualTo(1);
        assertThat(statisticsF2.conjunctions3()).isEqualTo(1);
        assertThat(statisticsF2.conjunctions4()).isEqualTo(1);
        assertThat(statisticsF2.conjunctionsN()).isEqualTo(1);
        assertThat(statisticsF2.disjunctions2()).isEqualTo(1);
        assertThat(statisticsF2.disjunctions3()).isEqualTo(1);
        assertThat(statisticsF2.disjunctions4()).isEqualTo(1);
        assertThat(statisticsF2.disjunctionsN()).isEqualTo(1);
        assertThat(statisticsF2.pbcs()).isEqualTo(0);
        assertThat(statisticsF2.ccs()).isEqualTo(0);
        assertThat(statisticsF2.ccCounter()).isEqualTo(0);
        assertThat(statisticsF2.pbCounter()).isEqualTo(0);
        assertThat(statisticsF2.cnfCounter()).isEqualTo(0);
        assertThat(statisticsF2.formulas()).isEqualTo(13);

        assertThat(statisticsF2).isNotEqualTo(statisticsF1);
        assertThat(statisticsF1).isNotEqualTo(statisticsF2);

        assertThat(statisticsF2.toString()).isEqualTo(
                "FormulaFactoryStatistics{"
                        + "name='Factory F'"
                        + ", positiveLiterals=5"
                        + ", negativeLiterals=0"
                        + ", negations=0"
                        + ", implications=0"
                        + ", equivalences=0"
                        + ", conjunctions2=1"
                        + ", conjunctions3=1"
                        + ", conjunctions4=1"
                        + ", conjunctionsN=1"
                        + ", disjunctions2=1"
                        + ", disjunctions3=1"
                        + ", disjunctions4=1"
                        + ", disjunctionsN=1"
                        + ", pbcs=0"
                        + ", ccs=0"
                        + ", ccCounter=0"
                        + ", pbCounter=0"
                        + ", cnfCounter=0"
                        + '}');
    }
}
