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

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

/**
 * The configuration object for the Glucose SAT solver.
 * @version 2.0.0
 * @since 1.0
 */
public final class GlucoseConfig extends Configuration {

    final int lbLBDMinimizingClause;
    final int lbLBDFrozenClause;
    final int lbSizeMinimizingClause;
    final int firstReduceDB;
    final int specialIncReduceDB;
    final int incReduceDB;
    final double factorK;
    final double factorR;
    final int sizeLBDQueue;
    final int sizeTrailQueue;
    final boolean reduceOnSize;
    final int reduceOnSizeSize;
    final double maxVarDecay;

    /**
     * Constructs a new Glucose configuration from a given builder.
     * @param builder the builder
     */
    private GlucoseConfig(final Builder builder) {
        super(ConfigurationType.GLUCOSE);
        this.lbLBDMinimizingClause = builder.lbLBDMinimizingClause;
        this.lbLBDFrozenClause = builder.lbLBDFrozenClause;
        this.lbSizeMinimizingClause = builder.lbSizeMinimizingClause;
        this.firstReduceDB = builder.firstReduceDB;
        this.specialIncReduceDB = builder.specialIncReduceDB;
        this.incReduceDB = builder.incReduceDB;
        this.factorK = builder.factorK;
        this.factorR = builder.factorR;
        this.sizeLBDQueue = builder.sizeLBDQueue;
        this.sizeTrailQueue = builder.sizeTrailQueue;
        this.reduceOnSize = builder.reduceOnSize;
        this.reduceOnSizeSize = builder.reduceOnSizeSize;
        this.maxVarDecay = builder.maxVarDecay;
    }

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

    public int getLbLBDMinimizingClause() {
        return this.lbLBDMinimizingClause;
    }

    public int getLbLBDFrozenClause() {
        return this.lbLBDFrozenClause;
    }

    public int getLbSizeMinimizingClause() {
        return this.lbSizeMinimizingClause;
    }

    public int getFirstReduceDB() {
        return this.firstReduceDB;
    }

    public int getSpecialIncReduceDB() {
        return this.specialIncReduceDB;
    }

    public int getIncReduceDB() {
        return this.incReduceDB;
    }

    public double getFactorK() {
        return this.factorK;
    }

    public double getFactorR() {
        return this.factorR;
    }

    public int getSizeLBDQueue() {
        return this.sizeLBDQueue;
    }

    public int getSizeTrailQueue() {
        return this.sizeTrailQueue;
    }

    public boolean isReduceOnSize() {
        return this.reduceOnSize;
    }

    public int getReduceOnSizeSize() {
        return this.reduceOnSizeSize;
    }

    public double getMaxVarDecay() {
        return this.maxVarDecay;
    }

    @Override
    public String toString() {
        final StringBuilder sb = new StringBuilder("GlucoseConfig{").append(System.lineSeparator());
        sb.append("lbLBDMinimizingClause=").append(this.lbLBDMinimizingClause).append(System.lineSeparator());
        sb.append("lbLBDFrozenClause=").append(this.lbLBDFrozenClause).append(System.lineSeparator());
        sb.append("lbSizeMinimizingClause=").append(this.lbSizeMinimizingClause).append(System.lineSeparator());
        sb.append("firstReduceDB=").append(this.firstReduceDB).append(System.lineSeparator());
        sb.append("specialIncReduceDB=").append(this.specialIncReduceDB).append(System.lineSeparator());
        sb.append("incReduceDB=").append(this.incReduceDB).append(System.lineSeparator());
        sb.append("factorK=").append(this.factorK).append(System.lineSeparator());
        sb.append("factorR=").append(this.factorR).append(System.lineSeparator());
        sb.append("sizeLBDQueue=").append(this.sizeLBDQueue).append(System.lineSeparator());
        sb.append("sizeTrailQueue=").append(this.sizeTrailQueue).append(System.lineSeparator());
        sb.append("reduceOnSize=").append(this.reduceOnSize).append(System.lineSeparator());
        sb.append("reduceOnSizeSize=").append(this.reduceOnSizeSize).append(System.lineSeparator());
        sb.append("maxVarDecay=").append(this.maxVarDecay).append(System.lineSeparator());
        sb.append("}");
        return sb.toString();
    }

    /**
     * The builder for a Glucose configuration.
     */
    public static class Builder {
        private int lbLBDMinimizingClause = 6;
        private int lbLBDFrozenClause = 30;
        private int lbSizeMinimizingClause = 30;
        private int firstReduceDB = 2000;
        private int specialIncReduceDB = 1000;
        private int incReduceDB = 300;
        private double factorK = 0.8;
        private double factorR = 1.4;
        private int sizeLBDQueue = 50;
        private int sizeTrailQueue = 5000;
        private boolean reduceOnSize = false;
        private int reduceOnSizeSize = 12;
        private double maxVarDecay = 0.95;

        private Builder() {
            // Initialize only via factory
        }

        /**
         * Sets the minimal LBD required to minimize a clause to a given value.  The default value is 6.
         * @param lbLBDMinimizingClause the value (should be at least 3)
         * @return the builder
         */
        public Builder lbLBDMinimizingClause(final int lbLBDMinimizingClause) {
            this.lbLBDMinimizingClause = lbLBDMinimizingClause;
            return this;
        }

        /**
         * Sets the value to protect clauses if their LBD decrease and is lower than it (for one turn).  The default value
         * is 30.
         * @param lbLBDFrozenClause the value
         * @return the builder
         */
        public Builder lbLBDFrozenClause(final int lbLBDFrozenClause) {
            this.lbLBDFrozenClause = lbLBDFrozenClause;
            return this;
        }

        /**
         * Sets the minimal size required to minimize a clause to a given value.  The default value is 30.
         * @param lbSizeMinimizingClause the value (should be at least 3)
         * @return the builder
         */
        public Builder lbSizeMinimizingClause(final int lbSizeMinimizingClause) {
            this.lbSizeMinimizingClause = lbSizeMinimizingClause;
            return this;
        }

        /**
         * Sets the number of conflicts before the first DB reduction to a given value.  The default value is 2000.
         * @param firstReduceDB the value
         * @return the builder
         */
        public Builder firstReduceDB(final int firstReduceDB) {
            this.firstReduceDB = firstReduceDB;
            return this;
        }

        /**
         * Sets the special increment for the DB reduction to a given value.  The default value is 1000.
         * @param specialIncReduceDB the value
         * @return the builder
         */
        public Builder specialIncReduceDB(final int specialIncReduceDB) {
            this.specialIncReduceDB = specialIncReduceDB;
            return this;
        }

        /**
         * Sets the increment for the DB reduction to a given value. The default value is 300.
         * @param incReduceDB the value
         * @return the builder
         */
        public Builder incReduceDB(final int incReduceDB) {
            this.incReduceDB = incReduceDB;
            return this;
        }

        /**
         * Sets the constant used to force restart to a given value.  The default value is 0.8.
         * @param factorK the value (should be in the range 0..1)
         * @return the builder
         */
        public Builder factorK(final double factorK) {
            this.factorK = factorK;
            return this;
        }

        /**
         * Sets the constant used to block restart to a given value.  The default value is 1.4.
         * @param factorR the value (should be in the range 1..5)
         * @return the builder
         */
        public Builder factorR(final double factorR) {
            this.factorR = factorR;
            return this;
        }

        /**
         * Sets the size of moving average for LBD (restarts) to a given value.  The default value is 50.
         * @param sizeLBDQueue the value (should be at least 10)
         * @return the builder
         */
        public Builder sizeLBDQueue(final int sizeLBDQueue) {
            this.sizeLBDQueue = sizeLBDQueue;
            return this;
        }

        /**
         * Sets the size of moving average for trail (block restarts) to a given value.  The default value is 5000.
         * @param sizeTrailQueue the value (should be at least 10)
         * @return the builder
         */
        public Builder sizeTrailQueue(final int sizeTrailQueue) {
            this.sizeTrailQueue = sizeTrailQueue;
            return this;
        }

        /**
         * Turns on the size reduction during LBD computation like described in the XMinisat paper.  The default value is
         * {@code false}.
         * @param reduceOnSize {@code true} if the size reduction is turned on, {@code false} otherwise
         * @return the builder
         */
        public Builder reduceOnSize(final boolean reduceOnSize) {
            this.reduceOnSize = reduceOnSize;
            return this;
        }

        /**
         * Sets the constant used during size reduction like described in the XMinisat paper to a given value.  The default
         * value is 12.
         * @param reduceOnSizeSize the value
         * @return the builder
         */
        public Builder reduceOnSizeSize(final int reduceOnSizeSize) {
            this.reduceOnSizeSize = reduceOnSizeSize;
            return this;
        }

        /**
         * Sets the maximal variable activity decay factor to a given value.  The default value is 0.95.
         * @param maxVarDecay the value (should be in the range 0..1)
         * @return the builder
         */
        public Builder maxVarDecay(final double maxVarDecay) {
            this.maxVarDecay = maxVarDecay;
            return this;
        }

        /**
         * Builds the Glucose configuration.
         * @return the configuration
         */
        public GlucoseConfig build() {
            return new GlucoseConfig(this);
        }
    }
}
