// Path: src/main/java/jhilbert/data/DVConstraints.java
// public interface DVConstraints extends Iterable<Variable[]>, Serializable {
// 
// 	/**
// 	 * Adds the specified variables to these <code>DVConstraints</code>
// 	 * by adding each non-diagonal pair.
// 	 *
// 	 * @param vars variables to be added.
// 	 *
// 	 * @throws DataException if the same variable appears twice in the
// 	 * 	specified array.
// 	 */
// 	public void add(Variable... vars) throws ConstraintException;
// 
// 	/**
// 	 * Adds the entire DV constraints specified to these
// 	 * <code>DVConstraints</code>.
// 	 *
// 	 * @param dvConstraints DV constraints to add
// 	 */
// 	public void add(DVConstraints dvConstraints);
// 
// 	/**
// 	 * Adds the cartesian product of the two specified sets of variables.
// 	 *
// 	 * @param varSet1 first set.
// 	 * @param varSet2 second set.
// 	 *
// 	 * @throws ConstraintException if the two sets are not disjoint.
// 	 */
// 	public void addProduct(Set<Variable> varSet1, Set<Variable> varSet2) throws ConstraintException;
// 
// 	/**
// 	 * Checks whether the specified variable pair is contained in these
// 	 * <code>DVConstraints</code>.
// 	 *
// 	 * @param var1 first variable.
// 	 * @param var2 second variable.
// 	 *
// 	 * @return <code>true</code> if {<code>var1</code>, <code>var2</code>}
// 	 * 	is contained in these constraints, <code>false</code>
// 	 * 	otherwise.
// 	 */
// 	public boolean contains(Variable var1, Variable var2);
// 
// 	/**
// 	 * Checks whther the specified DV constraints are contained in these
// 	 * DV constraints.
// 	 *
// 	 * @param dv other disjoint variable constraints.
// 	 *
// 	 * @return <code>true</code> if <code>dv</code> is contained in these
// 	 * 	constraints, <code>false</code> otherwise.
// 	 */
// 	public boolean contains(DVConstraints dv);
// 
// 	/**
// 	 * Removes all variable pairs from these <code>DVConstraints</code>
// 	 * whose elements are not both contained in the specified set.
// 	 *
// 	 * @param varSet variable set to restrict these constraints to.
// 	 */
// 	public void restrict(Set<Variable> varSet);
// 
// }
// 
// Path: src/main/java/jhilbert/data/Variable.java
// public interface Variable extends Symbol, Term {
// 
// 	/**
// 	 * Reimplemented from {@link Name#getOriginalName}, this method always
// 	 * returns <code>null</code> as variables are always local.
// 	 *
// 	 * @return <code>null</code>.
// 	 */
// 	public Name getOriginalName();
// 
// 	/**
// 	 * Returns whether this <code>Variable</code> is a dummy variable.
// 	 *
// 	 * @return <code>true</code> if this <code>Variable</code> is a dummy
// 	 * 	variable, <code>false</code> otherwise.
// 	 */
// 	public boolean isDummy();
// 
// }


import java.util.Set;
import jhilbert.data.DVConstraints;
import jhilbert.data.Variable;
/*
    JHilbert, a verifier for collaborative theorem proving

    Copyright © 2008, 2009, 2011 The JHilbert Authors
      See the AUTHORS file for the list of JHilbert authors.
      See the commit logs ("git log") for a list of individual contributions.

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.

    You may contact the author on this Wiki page:
    http://www.wikiproofs.de/w/index.php?title=User_talk:GrafZahl
*/

package jhilbert.expressions;



/**
 * An <code>Anonymiser</code> replaces {@link Variable}s in {@link Expression}s
 * with unnamed variables according to a replacement set which must be
 * provided to constructors of implementing classes.
 */
public interface Anonymiser {

	/**
	 * Returns an anonymised version of the specified variable.
	 * If the variable is not from the set of variables inherent to this
	 * <code>Anonymiser</code>, a dummy variable will be returned.
	 * Repeated calls to this method will result in consistent assignments
	 * of variables.
	 *
	 * @param var variable to anonymise.
	 *
	 * @return the anonymised variable.
	 */
	public Variable anonymise(Variable var);

	/**
	 * Anonymises the specified {@link DVConstraints} by calling
	 * {@link #anonymise(Variable)} on each variable in the constraints.
	 *
	 * @param dv disjoint variable constraints.
	 *
	 * @return anonymised disjoint variable constraints.
	 */
// Path: src/main/java/jhilbert/data/DVConstraints.java
// public interface DVConstraints extends Iterable<Variable[]>, Serializable {
// 
// 	/**
// 	 * Adds the specified variables to these <code>DVConstraints</code>
// 	 * by adding each non-diagonal pair.
// 	 *
// 	 * @param vars variables to be added.
// 	 *
// 	 * @throws DataException if the same variable appears twice in the
// 	 * 	specified array.
// 	 */
// 	public void add(Variable... vars) throws ConstraintException;
// 
// 	/**
// 	 * Adds the entire DV constraints specified to these
// 	 * <code>DVConstraints</code>.
// 	 *
// 	 * @param dvConstraints DV constraints to add
// 	 */
// 	public void add(DVConstraints dvConstraints);
// 
// 	/**
// 	 * Adds the cartesian product of the two specified sets of variables.
// 	 *
// 	 * @param varSet1 first set.
// 	 * @param varSet2 second set.
// 	 *
// 	 * @throws ConstraintException if the two sets are not disjoint.
// 	 */
// 	public void addProduct(Set<Variable> varSet1, Set<Variable> varSet2) throws ConstraintException;
// 
// 	/**
// 	 * Checks whether the specified variable pair is contained in these
// 	 * <code>DVConstraints</code>.
// 	 *
// 	 * @param var1 first variable.
// 	 * @param var2 second variable.
// 	 *
// 	 * @return <code>true</code> if {<code>var1</code>, <code>var2</code>}
// 	 * 	is contained in these constraints, <code>false</code>
// 	 * 	otherwise.
// 	 */
// 	public boolean contains(Variable var1, Variable var2);
// 
// 	/**
// 	 * Checks whther the specified DV constraints are contained in these
// 	 * DV constraints.
// 	 *
// 	 * @param dv other disjoint variable constraints.
// 	 *
// 	 * @return <code>true</code> if <code>dv</code> is contained in these
// 	 * 	constraints, <code>false</code> otherwise.
// 	 */
// 	public boolean contains(DVConstraints dv);
// 
// 	/**
// 	 * Removes all variable pairs from these <code>DVConstraints</code>
// 	 * whose elements are not both contained in the specified set.
// 	 *
// 	 * @param varSet variable set to restrict these constraints to.
// 	 */
// 	public void restrict(Set<Variable> varSet);
// 
// }
// 
// Path: src/main/java/jhilbert/data/Variable.java
// public interface Variable extends Symbol, Term {
// 
// 	/**
// 	 * Reimplemented from {@link Name#getOriginalName}, this method always
// 	 * returns <code>null</code> as variables are always local.
// 	 *
// 	 * @return <code>null</code>.
// 	 */
// 	public Name getOriginalName();
// 
// 	/**
// 	 * Returns whether this <code>Variable</code> is a dummy variable.
// 	 *
// 	 * @return <code>true</code> if this <code>Variable</code> is a dummy
// 	 * 	variable, <code>false</code> otherwise.
// 	 */
// 	public boolean isDummy();
// 
// }


// Path: src/main/java/jhilbert/expressions/Anonymiser.java
import java.util.Set;
import jhilbert.data.DVConstraints;
import jhilbert.data.Variable;

/*
    JHilbert, a verifier for collaborative theorem proving

    Copyright © 2008, 2009, 2011 The JHilbert Authors
      See the AUTHORS file for the list of JHilbert authors.
      See the commit logs ("git log") for a list of individual contributions.

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.

    You may contact the author on this Wiki page:
    http://www.wikiproofs.de/w/index.php?title=User_talk:GrafZahl
*/

package jhilbert.expressions;



/**
 * An <code>Anonymiser</code> replaces {@link Variable}s in {@link Expression}s
 * with unnamed variables according to a replacement set which must be
 * provided to constructors of implementing classes.
 */
public interface Anonymiser {

	/**
	 * Returns an anonymised version of the specified variable.
	 * If the variable is not from the set of variables inherent to this
	 * <code>Anonymiser</code>, a dummy variable will be returned.
	 * Repeated calls to this method will result in consistent assignments
	 * of variables.
	 *
	 * @param var variable to anonymise.
	 *
	 * @return the anonymised variable.
	 */
	public Variable anonymise(Variable var);

	/**
	 * Anonymises the specified {@link DVConstraints} by calling
	 * {@link #anonymise(Variable)} on each variable in the constraints.
	 *
	 * @param dv disjoint variable constraints.
	 *
	 * @return anonymised disjoint variable constraints.
	 */
	public DVConstraints anonymise(DVConstraints dv);