Commit 81b9d81f authored by lonca's avatar lonca
Browse files

Added license header and comments ; renamed XmlCommentPrintWriter to fit the...

Added license header and comments ; renamed XmlCommentPrintWriter to fit the case convention used until now.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2542 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent f2aa026f
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp;
import java.io.PrintStream;
......@@ -18,6 +36,12 @@ import org.sat4j.specs.SearchListener;
import org.sat4j.specs.TimeoutException;
import org.sat4j.specs.UnitClauseProvider;
/**
* A simple decorator allowing to use an {@link IPBSolver} as an {@link ICspPBSatSolver}.
* It provides two methods allowing to set/retrieve whether the associated CSP to SAT encoding must be displayed or not.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public class CspSatSolverDecorator implements ICspPBSatSolver {
private static final long serialVersionUID = 1L;
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp;
import org.sat4j.pb.IPBSolver;
/**
* An extension of the {@link IPBSolver} interface allowing to know if a solver used for CSP should display the encoding used.
* This is particularly useful since the encoding must be displayed for DIMACS output solvers but might not be for "real" solvers, as it may be huge.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public interface ICspPBSatSolver extends IPBSolver {
/**
* Tells whether the CSP to SAT encoding should be displayed.
*
* @return true iff the encoding must be displayed
*/
boolean shouldOnlyDisplayEncoding();
/**
* Sets the flag indicating whether the CSP to SAT encoding should be displayed.
*
* @param b the flag value (true for display)
*/
void setShouldOnlyDisplayEncoding(boolean b);
}
......@@ -32,7 +32,7 @@ import org.xcsp.common.Types.TypeOperator;
import org.xcsp.parser.entries.XVariables.XVarInteger;
/**
* A utility class for XCSP3 constraint builders.
* Utility class for XCSP3 constraint builders.
*
* @author Emmanuel Lonca - lonca@cril.fr
*
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.constraints3;
import org.sat4j.csp.intension.ICspToSatEncoder;
import org.sat4j.csp.intension.IIntensionCtrEncoder;
import org.sat4j.reader.XMLCSP3Reader;
import org.xcsp.parser.entries.XVariables.XVarInteger;
/**
* @author Emmanuel Lonca - lonca@cril.fr
*/
/**
* A constraint builder for XCSP3 instance format.
* Used by {@link XMLCSP3Reader}.
* This class is dedicated to elementary (clauses, terms) constraints.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public class ElementaryCtrBuilder {
private final IIntensionCtrEncoder intensionEncoder;
......
......@@ -42,7 +42,6 @@ import org.xcsp.parser.entries.XVariables.XVarInteger;
* This class is dedicated to intension (including "primitive" special cases) constraints.
*
* @author Emmanuel Lonca - lonca@cril.fr
*
*/
public class GenericCtrBuilder {
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.constraints3;
import java.util.ArrayList;
......@@ -6,11 +24,17 @@ import java.util.List;
import java.util.Map;
import org.sat4j.csp.intension.ICspToSatEncoder;
import org.sat4j.reader.XMLCSP3Reader;
import org.sat4j.specs.ContradictionException;
import org.xcsp.parser.entries.XVariables.XVarInteger;
/**
/**
* A constraint builder for XCSP3 instance format.
* Used by {@link XMLCSP3Reader}.
* This class is dedicated to language (regular, MDD) constraints.
*
* @author Emmanuel Lonca - lonca@cril.fr
*
*/
public class LanguageCtrBuilder {
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.constraints3;
import java.util.ArrayList;
......@@ -9,9 +27,11 @@ import org.xcsp.common.Condition.ConditionIntvl;
import org.xcsp.common.Condition.ConditionVal;
import org.xcsp.common.Condition.ConditionVar;
/**
* @author Emmanuel Lonca - lonca@cril.fr
*/
/**
* A class which aims at representing any constraint of xcsp3parser as a string.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public class StringCondition {
public static final String LEFT_OPERAND = "__LEFT_OPERAND__";
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.intension;
import java.util.Arrays;
......@@ -15,6 +33,11 @@ import org.sat4j.pb.IPBSolver;
import org.sat4j.specs.ContradictionException;
import org.xcsp.parser.entries.XVariables.XVarInteger;
/**
* A simple decorator of {@link IPBSolver} that implements {@link ICspToSatEncoder}.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public class CspToPBSolverDecorator implements ICspToSatEncoder {
private final IPBSolver solver;
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.intension;
/**
* Enumerates the kinds of (sub)expression types that may be found in an intension constraint.
*
* @author Emmanuel Lonca - lonca@cril.fr>-
*/
public enum EExpressionType {
VAR,
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.intension;
import java.util.HashMap;
import java.util.Map;
/**
* Enumerates the operators that may be found in an intension constraint.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public enum EOperator {
OPPOSITE("neg", EExpressionType.INTEGER, 1, 1, EAssociativityState.NONE),
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.intension;
import java.util.Map;
import org.xcsp.parser.entries.XVariables.XVarInteger;
/**
* A SAT solver with the ability to build a mapping between bollean variables and CSP variables.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public interface ICspToSatEncoder {
int[] getCspVarDomain(String var);
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.intension;
import java.util.Set;
/**
* An expresiion in an intension constraint.
* It may be a constant, a variable, a composed expression rooted by an operator, ...
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public interface IExpression extends Comparable<IExpression> {
String typeAsString();
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.intension;
/**
* An interfacer to be implemented by classes able to encode intension constraints and store them in a solver.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public interface IIntensionCtrEncoder {
public boolean encode(String strExpression);
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.intension;
import java.util.HashSet;
import java.util.Set;
/**
* An {@link IExpression} equal to an integer constant.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public class IntegerExpression implements IExpression {
private final Integer value;
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.intension;
/**
* A factory for intension constraints encoders.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public class IntensionCtrEncoderFactory {
private static IntensionCtrEncoderFactory instance = null;
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.intension;
import java.lang.reflect.InvocationTargetException;
......@@ -7,6 +25,12 @@ import java.util.Iterator;
import java.util.Map;
import java.util.Set;
/**
* Encodes {@link IExpression} expressions into an {@link ICspToSatEncoder}.
* Given the expression, generates all nogoods and store them in the solver.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public class NogoodBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
private final ICspToSatEncoder solver;
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.intension;
import java.util.Arrays;
import java.util.HashSet;
import java.util.Set;
/**
* An {@link IExpression} equal to an operator-rooted expression.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public class OperatorExpression implements IExpression {
private EOperator op;
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*******************************************************************************/
package org.sat4j.csp.intension;
import java.util.ArrayList;
import java.util.List;
/** ICE stands for Intension Constraint Encoder */
/**
* Parses an intension constraint given as a string and returns it as a tree of {@link IExpression}.
*
* @author Emmanuel Lonca - lonca@cril.fr
*/
public class Parser {
private static final String NULL_LENGTH_EXPR_MSG_PREFIX = "null length expression at index ";
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2016 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions