///////////////////////////////////////////////////////////////////////////
//                   __                _      _   ________               //
//                  / /   ____  ____ _(_)____/ | / / ____/               //
//                 / /   / __ \/ __ `/ / ___/  |/ / / __                 //
//                / /___/ /_/ / /_/ / / /__/ /|  / /_/ /                 //
//               /_____/\____/\__, /_/\___/_/ |_/\____/                  //
//                           /____/                                      //
//                                                                       //
//               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.util;

import org.logicng.configurations.Configuration;
import org.logicng.configurations.ConfigurationType;
import org.logicng.formulas.Variable;

import java.util.Collection;

/**
 * A configuration for randomizing formulas. The following things can be configured:
 * <ul>
 *     <li>the seed -- use a value {@code != 0} to get deterministic results</li>
 *     <li>the variables -- if {@link #variables} is not {@code null} this list of variables will be used,
 *     otherwise {@link #numVars} variables will be generated. The probabilities of being chosen are the
 *     same for all variables.</li>
 *     <li>weights for different formula types, defining how often a formula type is generated compared to other types</li>
 *     <li>weights for comparator types in pseudo boolean constraints and cardinality constraints</li>
 *     <li>maximum numbers of operands for conjunctions, disjunctions, PBCs, and CCs</li>
 * </ul>
 * Note that the weights can only be applied for inner nodes of the generated formula,
 * since the 'leaves' of a formula in LogicNG are <b>always</b> literals or PBCs. So the weight of literals and PBCs
 * will effectively be higher and the weights of all other formula types (especially conjunctions and disjunctions)
 * will be lower. Similarly, the weight of constants will usually be lower, because they are always reduced in LogicNG
 * unless they are a single formula.
 * @version 2.0.0
 * @since 2.0.0
 */
public final class FormulaRandomizerConfig extends Configuration {

    final long seed;
    final Collection<Variable> variables;
    final int numVars;
    final double weightConstant;
    final double weightPositiveLiteral;
    final double weightNegativeLiteral;
    final double weightOr;
    final double weightAnd;
    final double weightNot;
    final double weightImpl;
    final double weightEquiv;
    final int maximumOperandsAnd;
    final int maximumOperandsOr;

    final double weightPbc;
    final double weightPbcCoeffPositive;
    final double weightPbcCoeffNegative;
    final double weightPbcTypeLe;
    final double weightPbcTypeLt;
    final double weightPbcTypeGe;
    final double weightPbcTypeGt;
    final double weightPbcTypeEq;
    final int maximumOperandsPbc;
    final int maximumCoefficientPbc;

    final double weightCc;
    final double weightAmo;
    final double weightExo;
    final int maximumOperandsCc;

    @Override
    public String toString() {
        final StringBuilder sb = new StringBuilder("FormulaRandomizerConfig{").append(System.lineSeparator());
        sb.append("seed=").append(this.seed).append(System.lineSeparator());
        sb.append("variables=").append(this.variables).append(System.lineSeparator());
        sb.append("numVars=").append(this.numVars).append(System.lineSeparator());
        sb.append("weightConstant=").append(this.weightConstant).append(System.lineSeparator());
        sb.append("weightPositiveLiteral=").append(this.weightPositiveLiteral).append(System.lineSeparator());
        sb.append("weightNegativeLiteral=").append(this.weightNegativeLiteral).append(System.lineSeparator());
        sb.append("weightOr=").append(this.weightOr).append(System.lineSeparator());
        sb.append("weightAnd=").append(this.weightAnd).append(System.lineSeparator());
        sb.append("weightNot=").append(this.weightNot).append(System.lineSeparator());
        sb.append("weightImpl=").append(this.weightImpl).append(System.lineSeparator());
        sb.append("weightEquiv=").append(this.weightEquiv).append(System.lineSeparator());
        sb.append("maximumOperandsAnd=").append(this.maximumOperandsAnd).append(System.lineSeparator());
        sb.append("maximumOperandsOr=").append(this.maximumOperandsOr).append(System.lineSeparator());
        sb.append("weightPbc=").append(this.weightPbc).append(System.lineSeparator());
        sb.append("weightPbcCoeffPositive=").append(this.weightPbcCoeffPositive).append(System.lineSeparator());
        sb.append("weightPbcCoeffNegative=").append(this.weightPbcCoeffNegative).append(System.lineSeparator());
        sb.append("weightPbcTypeLe=").append(this.weightPbcTypeLe).append(System.lineSeparator());
        sb.append("weightPbcTypeLt=").append(this.weightPbcTypeLt).append(System.lineSeparator());
        sb.append("weightPbcTypeGe=").append(this.weightPbcTypeGe).append(System.lineSeparator());
        sb.append("weightPbcTypeGt=").append(this.weightPbcTypeGt).append(System.lineSeparator());
        sb.append("weightPbcTypeEq=").append(this.weightPbcTypeEq).append(System.lineSeparator());
        sb.append("maximumOperandsPbc=").append(this.maximumOperandsPbc).append(System.lineSeparator());
        sb.append("maximumCoefficientPbc=").append(this.maximumCoefficientPbc).append(System.lineSeparator());
        sb.append("weightCc=").append(this.weightCc).append(System.lineSeparator());
        sb.append("weightAmo=").append(this.weightAmo).append(System.lineSeparator());
        sb.append("weightExo=").append(this.weightExo).append(System.lineSeparator());
        sb.append("maximumOperandsCc=").append(this.maximumOperandsCc).append(System.lineSeparator());
        sb.append('}');
        return sb.toString();
    }

    /**
     * Constructs a new configuration from a given builder.
     * @param builder the builder
     */
    private FormulaRandomizerConfig(final Builder builder) {
        super(ConfigurationType.FORMULA_RANDOMIZER);
        this.seed = builder.seed;
        this.variables = builder.variables;
        this.numVars = builder.numVars;
        this.weightConstant = builder.weightConstant;
        this.weightPositiveLiteral = builder.weightPositiveLiteral;
        this.weightNegativeLiteral = builder.weightNegativeLiteral;
        this.weightOr = builder.weightOr;
        this.weightAnd = builder.weightAnd;
        this.weightNot = builder.weightNot;
        this.weightImpl = builder.weightImpl;
        this.weightEquiv = builder.weightEquiv;
        this.maximumOperandsAnd = builder.maximumOperandsAnd;
        this.maximumOperandsOr = builder.maximumOperandsOr;
        this.weightPbc = builder.weightPbc;
        this.weightPbcCoeffPositive = builder.weightPbcCoeffPositive;
        this.weightPbcCoeffNegative = builder.weightPbcCoeffNegative;
        this.weightPbcTypeLe = builder.weightPbcTypeLe;
        this.weightPbcTypeLt = builder.weightPbcTypeLt;
        this.weightPbcTypeGe = builder.weightPbcTypeGe;
        this.weightPbcTypeGt = builder.weightPbcTypeGt;
        this.weightPbcTypeEq = builder.weightPbcTypeEq;
        this.maximumOperandsPbc = builder.maximumOperandsPbc;
        this.maximumCoefficientPbc = builder.maximumCoefficientPbc;
        this.weightCc = builder.weightCc;
        this.weightAmo = builder.weightAmo;
        this.weightExo = builder.weightExo;
        this.maximumOperandsCc = builder.maximumOperandsCc;
    }

    /**
     * Returns a new builder for the configuration.
     * @return the builder
     */
    public static Builder builder() {
        return new Builder();
    }

    /**
     * The builder for a formula randomizer configuration.
     * @version 2.0.0
     * @since 2.0.0
     */
    public static class Builder {
        private long seed = 0;
        private Collection<Variable> variables = null;
        private int numVars = 25;
        private double weightConstant = 0.1;
        private double weightPositiveLiteral = 1.0;
        private double weightNegativeLiteral = 1.0;
        private double weightOr = 30.0;
        private double weightAnd = 30.0;
        private double weightNot = 1.0;
        private double weightImpl = 1.0;
        private double weightEquiv = 1.0;
        private int maximumOperandsAnd = 5;
        private int maximumOperandsOr = 5;
        private double weightPbc = 0.0;
        private double weightPbcCoeffPositive = 1.0;
        private double weightPbcCoeffNegative = 0.2;
        private double weightPbcTypeLe = 0.2;
        private double weightPbcTypeLt = 0.2;
        private double weightPbcTypeGe = 0.2;
        private double weightPbcTypeGt = 0.2;
        private double weightPbcTypeEq = 0.2;
        private int maximumOperandsPbc = 5;
        private int maximumCoefficientPbc = 10;
        private double weightCc = 0.0;
        private double weightAmo = 0.0;
        private double weightExo = 0.0;
        private int maximumOperandsCc = 5;

        /**
         * Builds the formula randomizer configuration.
         * @return the formula randomizer configuration
         */
        public FormulaRandomizerConfig build() {
            return new FormulaRandomizerConfig(this);
        }

        /**
         * Sets the seed of the randomizer (passed to the constructor of {@link java.util.Random}).
         * This provides the possibility to get deterministic random formulas. Just choose an arbitrary
         * number, and you get the same random formulas with every run.
         * <p>
         * The default value is 0, meaning that the seed depends on the system time, so determinism
         * is lost.
         * @param seed the seed
         * @return the builder
         */
        public Builder seed(final long seed) {
            this.seed = seed;
            return this;
        }

        /**
         * Sets the variables which may occur in the generated formulas.
         * <p>
         * If this value is set, the {@link #numVars number of variables} will be ignored.
         * <p>
         * The default value is {@code null} (i.e. {@link #numVars} will be used.).
         * @param variables the variables to use
         * @return the builder
         */
        public Builder variables(final Collection<Variable> variables) {
            this.variables = variables;
            return this;
        }

        /**
         * Sets the number of different variables which may occur in the generated formulas.
         * <p>
         * This value is ignored if also the {@link #variables} are set.
         * <p>
         * The default value is 0.
         * @param numVars the number of different variables.
         * @return the builder
         */
        public Builder numVars(final int numVars) {
            this.numVars = numVars;
            return this;
        }

        /**
         * Sets the relative weight of a constant.
         * @param weightConstant the relative weight of a constant
         * @return the builder
         */
        public Builder weightConstant(final double weightConstant) {
            this.weightConstant = weightConstant;
            return this;
        }

        /**
         * Sets the relative weight of a positive literal.
         * @param weightPositiveLiteral the relative weight of a positive literal
         * @return the builder
         */
        public Builder weightPositiveLiteral(final double weightPositiveLiteral) {
            this.weightPositiveLiteral = weightPositiveLiteral;
            return this;
        }

        /**
         * Sets the relative weight of a negative literal.
         * @param weightNegativeLiteral the relative weight of a negative literal
         * @return the builder
         */
        public Builder weightNegativeLiteral(final double weightNegativeLiteral) {
            this.weightNegativeLiteral = weightNegativeLiteral;
            return this;
        }

        /**
         * Sets the relative weight of a disjunction.
         * @param weightOr the relative weight of a disjunction
         * @return the builder
         */
        public Builder weightOr(final double weightOr) {
            this.weightOr = weightOr;
            return this;
        }

        /**
         * Sets the relative weight of a conjunction.
         * @param weightAnd the relative weight of a conjunction
         * @return the builder
         */
        public Builder weightAnd(final double weightAnd) {
            this.weightAnd = weightAnd;
            return this;
        }

        /**
         * Sets the relative weight of a negation.
         * @param weightNot the relative weight of a negation
         * @return the builder
         */
        public Builder weightNot(final double weightNot) {
            this.weightNot = weightNot;
            return this;
        }

        /**
         * Sets the relative weight of an implication.
         * @param weightImpl the relative weight of an implication
         * @return the builder
         */
        public Builder weightImpl(final double weightImpl) {
            this.weightImpl = weightImpl;
            return this;
        }

        /**
         * Sets the relative weight of an equivalence.
         * @param weightEquiv the relative weight of an equivalence
         * @return the builder
         */
        public Builder weightEquiv(final double weightEquiv) {
            this.weightEquiv = weightEquiv;
            return this;
        }

        /**
         * Sets the maximum number of operands in a conjunction.
         * @param maximumOperandsAnd the maximum number of operands in a conjunction
         * @return the builder
         */
        public Builder maximumOperandsAnd(final int maximumOperandsAnd) {
            this.maximumOperandsAnd = maximumOperandsAnd;
            return this;
        }

        /**
         * Sets the maximum number of operands in a disjunction.
         * @param maximumOperandsOr the maximum number of operands in a disjunction
         * @return the builder
         */
        public Builder maximumOperandsOr(final int maximumOperandsOr) {
            this.maximumOperandsOr = maximumOperandsOr;
            return this;
        }

        /**
         * Sets the relative weight of a pseudo boolean constraint.
         * Note that the constraint may by chance also be a cardinality constraint,
         * or even a literal or a constant.
         * @param weightPbc the relative weight of a pseudo boolean constraint
         * @return the builder
         */
        public Builder weightPbc(final double weightPbc) {
            this.weightPbc = weightPbc;
            return this;
        }

        /**
         * Sets the relative weight of a positive coefficient.
         * @param weightPbcCoeffPositive the relative weight of a positive coefficient
         * @return the builder
         */
        public Builder weightPbcCoeffPositive(final double weightPbcCoeffPositive) {
            this.weightPbcCoeffPositive = weightPbcCoeffPositive;
            return this;
        }

        /**
         * Sets the relative weight of a negative coefficient.
         * @param weightPbcCoeffNegative the relative weight of a negative coefficient
         * @return the builder
         */
        public Builder weightPbcCoeffNegative(final double weightPbcCoeffNegative) {
            this.weightPbcCoeffNegative = weightPbcCoeffNegative;
            return this;
        }

        /**
         * Sets the relative weight of a LE constraint ({@link org.logicng.formulas.CType#LE}.
         * @param weightPbcTypeLe the relative weight of a LE constraint
         * @return the builder
         */
        public Builder weightPbcTypeLe(final double weightPbcTypeLe) {
            this.weightPbcTypeLe = weightPbcTypeLe;
            return this;
        }

        /**
         * Sets the relative weight of an LT constraint ({@link org.logicng.formulas.CType#LT}.
         * @param weightPbcTypeLt the relative weight of an LT constraint
         * @return the builder
         */
        public Builder weightPbcTypeLt(final double weightPbcTypeLt) {
            this.weightPbcTypeLt = weightPbcTypeLt;
            return this;
        }

        /**
         * Sets the relative weight of a GE constraint ({@link org.logicng.formulas.CType#GE}.
         * @param weightPbcTypeGe the relative weight of a GE constraint
         * @return the builder
         */
        public Builder weightPbcTypeGe(final double weightPbcTypeGe) {
            this.weightPbcTypeGe = weightPbcTypeGe;
            return this;
        }

        /**
         * Sets the relative weight of a GT constraint ({@link org.logicng.formulas.CType#GT}.
         * @param weightPbcTypeGt the relative weight of a GT constraint
         * @return the builder
         */
        public Builder weightPbcTypeGt(final double weightPbcTypeGt) {
            this.weightPbcTypeGt = weightPbcTypeGt;
            return this;
        }

        /**
         * Sets the relative weight of a EQ constraint ({@link org.logicng.formulas.CType#EQ}.
         * @param weightPbcTypeEq the relative weight of a EQ constraint
         * @return the builder
         */
        public Builder weightPbcTypeEq(final double weightPbcTypeEq) {
            this.weightPbcTypeEq = weightPbcTypeEq;
            return this;
        }

        /**
         * Sets the maximum number of operands in a pseudo boolean constraint.
         * @param maximumOperandsPbc the maximum number of operands
         * @return the builder
         */
        public Builder maximumOperandsPbc(final int maximumOperandsPbc) {
            this.maximumOperandsPbc = maximumOperandsPbc;
            return this;
        }

        /**
         * Sets the maximum absolute value of a coefficient in a pseudo boolean constraint.
         * Whether the coefficient is positive or negative is depends on {@link #weightPbcCoeffPositive}
         * and {@link #weightPbcCoeffNegative}.
         * @param maximumCoefficientPbc the maximum absolute value of a coefficient
         * @return the builder
         */
        public Builder maximumCoefficientPbc(final int maximumCoefficientPbc) {
            this.maximumCoefficientPbc = maximumCoefficientPbc;
            return this;
        }

        /**
         * Sets the relative weight of a cardinality constraint.
         * Note that the cardinality constraint may by chance also be an AMO or EXO constraint,
         * or even a literal or a constant.
         * @param weightCc the relative weight of a cardinality constraint
         * @return the builder
         */
        public Builder weightCc(final double weightCc) {
            this.weightCc = weightCc;
            return this;
        }

        /**
         * Sets the relative weight of an at-most-one constraint.
         * @param weightAmo the relative weight of an at-most-one constraint
         * @return the builder
         */
        public Builder weightAmo(final double weightAmo) {
            this.weightAmo = weightAmo;
            return this;
        }

        /**
         * Sets the relative weight of an exactly-one constraint.
         * @param weightExo the relative weight of an exactly-one constraint
         * @return the builder
         */
        public Builder weightExo(final double weightExo) {
            this.weightExo = weightExo;
            return this;
        }

        /**
         * Sets the maximum number of operands in a cardinality, AMO, or EXO constraint.
         * @param maximumOperandsCc the maximum number of operands in a cardinality, AMO, or EXO constraint
         * @return the builder
         */
        public Builder maximumOperandsCc(final int maximumOperandsCc) {
            this.maximumOperandsCc = maximumOperandsCc;
            return this;
        }
    }
}
