<commit_before>/*
 * Kodkod -- Copyright (c) 2005-present, <NAME>
 * Pardinus -- Copyright (c) 2013-present, <NAME>, INESC TEC
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 * SOFTWARE.
 */
package kodkod.engine.unbounded;

import java.util.Collection;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Map.Entry;

import kodkod.ast.BinaryExpression;
import kodkod.ast.BinaryFormula;
import kodkod.ast.BinaryIntExpression;
import kodkod.ast.BinaryTempFormula;
import kodkod.ast.ComparisonFormula;
import kodkod.ast.Comprehension;
import kodkod.ast.ConstantExpression;
import kodkod.ast.ConstantFormula;
import kodkod.ast.Decl;
import kodkod.ast.Decls;
import kodkod.ast.ExprToIntCast;
import kodkod.ast.Expression;
import kodkod.ast.Formula;
import kodkod.ast.IfExpression;
import kodkod.ast.IfIntExpression;
import kodkod.ast.IntComparisonFormula;
import kodkod.ast.IntConstant;
import kodkod.ast.IntExpression;
import kodkod.ast.IntToExprCast;
import kodkod.ast.LeafExpression;
import kodkod.ast.MultiplicityFormula;
import kodkod.ast.NaryExpression;
import kodkod.ast.NaryFormula;
import kodkod.ast.NaryIntExpression;
import kodkod.ast.Node;
import kodkod.ast.NotFormula;
import kodkod.ast.ProjectExpression;
import kodkod.ast.QuantifiedFormula;
import kodkod.ast.Relation;
import kodkod.ast.RelationPredicate;
import kodkod.ast.RelationPredicate.Name;
import kodkod.ast.SumExpression;
import kodkod.ast.TempExpression;
import kodkod.ast.UnaryExpression;
import kodkod.ast.UnaryIntExpression;
import kodkod.ast.UnaryTempFormula;
import kodkod.ast.Variable;
import kodkod.ast.operator.ExprOperator;
import kodkod.ast.operator.FormulaOperator;
import kodkod.ast.operator.IntOperator;
import kodkod.ast.operator.Multiplicity;
import kodkod.ast.operator.TemporalOperator;
import kodkod.ast.visitor.VoidVisitor;
import kodkod.engine.config.AbstractReporter;
import kodkod.engine.config.ExtendedOptions;
import kodkod.engine.config.Options;
import kodkod.engine.config.Reporter;
import kodkod.engine.fol2sat.Translation.Whole;
import kodkod.engine.fol2sat.Translator;
import kodkod.instance.Bounds;
import kodkod.instance.PardinusBounds;
import kodkod.instance.Tuple;
import kodkod.instance.TupleSet;
import kodkod.instance.Universe;
import kodkod.util.ints.IndexedEntry;
import kodkod.util.ints.IntSet;
import kodkod.util.ints.SparseSequence;
import kodkod.util.nodes.AnnotatedNode;
import kodkod.util.nodes.PrettyPrinter;

/**
 * Translates an unbounded temporal model finding problem into an Electrod
 * problem in its concrete syntax. This includes the universe, bounds of the
 * variables, the goal as a relational formula and the symmetry breaking
 * predicate.
 * 
 * Electrod has currently limited support for integers. Although integer
 * operations and formulas over integers are supported, the conversion between
 * integer atoms and their numeric semantics is not.
 * 
 * @author <NAME> // [HASLab] unbounded temporal model finding
 */
public class ElectrodPrinter {

	/**
	 * Translates and prints an unbounded temporal model finding problem into
	 * Electrod. Intercepts the symmetry breaking predicate so that it can be
	 * used by Electrod.
	 * 
	 * @param formula
	 *            the problem's formula.
	 * @param bounds
	 *            the problem's bounds.
	 * @param rep 
	 * @return the printed Electrod problem.
	 * @throws InvalidUnboundedProblem
	 *             if the problem is not supported by Electrod.
	 */
	public static String print(Formula formula, PardinusBounds bounds, Reporter rep)
			throws InvalidUnboundedProblem {
		// use a reporter to intercept the symmetry breaking predicate
		Options opt = new ExtendedOptions();
		StringBuilder temp = new StringBuilder();
		Reporter reporter = new AbstractReporter() {
			
			@Override
			public void warning(String warning) {
				rep.warning(warning);
			}
			
			@Override
			public void reportLex(List<Entry<Relation, Tuple>> _original,
					List<Entry<Relation, Tuple>> _permuted) {
				if (_original.size()+_permuted.size()==0)
					return;
				String tmp = printLexList(_original);
				temp.append(tmp.substring(0,tmp.length()-1));
				temp.append(" <= ");
				temp.append(printLexList(_permuted).substring(1));
				temp.append(";\n");
			}
			
			@Override
			public void detectedSymmetries(Set<IntSet> parts) {
				rep.detectedSymmetries(parts);
			}
			
			@Override
			public void debug(String debug) {
				rep.debug(debug);
			}

		};
		opt.setReporter(reporter);
		
//		// testing whether this is feasible
//		Map<Name, Set<RelationPredicate>> preds = AnnotatedNode.annotate(formula).predicates();
//		for (RelationPredicate pred : preds.get(Name.FUNCTION)) {
//			RelationPredicate.Function func = (RelationPredicate.Function) pred;
//			Expression upp = bounds.upperSymbBounds(func.relation());
//			if (upp != null && upp instanceof BinaryExpression && ((BinaryExpression) upp).op().equals(ExprOperator.PRODUCT) && 
//					((BinaryExpression) upp).left().equals(func.domain()) && ((BinaryExpression) upp).right().equals(func.range()))
//				System.out.println(func.relation() + " : " + func.domain() +" -> "+func.targetMult()+" "+func.range());
//		}
		

		// [HASLab] retrieve the additional formula imposed by the symbolic
		// bounds, depending on execution stage
		Formula symbForm = Formula.TRUE;
		// [HASLab] if decomposed mode, the amalgamated bounds are always considered
		if (opt.decomposed() && bounds.amalgamated() != null)
			symbForm = bounds.amalgamated().resolve(opt.reporter());
		// [HASLab] otherwise use regular bounds
		else
			symbForm = bounds.resolve(opt.reporter());


		Whole t = Translator.translate(formula.and(symbForm), bounds, opt);
		bounds = (PardinusBounds) t.bounds();

		try {
			StringBuilder sb = new StringBuilder();
			sb.append(printUniverse(bounds.universe()));
			sb.append(printBounds(bounds));
			sb.append(printSymmetries(temp.toString()));
			sb.append(printConstraint(formula.and(symbForm)));
			return sb.toString();
		} catch (Exception e) {
			throw new InvalidUnboundedProblem(e);
		}
	}

	/**
	 * Print the universe of atoms.
	 * 
	 * @param universe the universe of atoms.
	 * @return the universe in Electrod's concrete syntax.
	 */
	private static String printUniverse(Universe universe) {
		StringBuilder sb = new StringBuilder("univ : { ");
		Iterator<Object> it = universe.iterator();<commit_msg>documentation<commit_after>/*
 * Kodkod -- Copyright (c) 2005-present, <NAME>
 * Pardinus -- Copyright (c) 2013-present, <NAME>, INESC TEC
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 * SOFTWARE.
 */
package kodkod.engine.unbounded;

import java.util.Collection;
import java.util.Iterator;
import java.util.List;
import java.util.Set;
import java.util.Map.Entry;

import kodkod.ast.BinaryExpression;
import kodkod.ast.BinaryFormula;
import kodkod.ast.BinaryIntExpression;
import kodkod.ast.BinaryTempFormula;
import kodkod.ast.ComparisonFormula;
import kodkod.ast.Comprehension;
import kodkod.ast.ConstantExpression;
import kodkod.ast.ConstantFormula;
import kodkod.ast.Decl;
import kodkod.ast.Decls;
import kodkod.ast.ExprToIntCast;
import kodkod.ast.Expression;
import kodkod.ast.Formula;
import kodkod.ast.IfExpression;
import kodkod.ast.IfIntExpression;
import kodkod.ast.IntComparisonFormula;
import kodkod.ast.IntConstant;
import kodkod.ast.IntExpression;
import kodkod.ast.IntToExprCast;
import kodkod.ast.LeafExpression;
import kodkod.ast.MultiplicityFormula;
import kodkod.ast.NaryExpression;
import kodkod.ast.NaryFormula;
import kodkod.ast.NaryIntExpression;
import kodkod.ast.Node;
import kodkod.ast.NotFormula;
import kodkod.ast.ProjectExpression;
import kodkod.ast.QuantifiedFormula;
import kodkod.ast.Relation;
import kodkod.ast.RelationPredicate;
import kodkod.ast.SumExpression;
import kodkod.ast.TempExpression;
import kodkod.ast.UnaryExpression;
import kodkod.ast.UnaryIntExpression;
import kodkod.ast.UnaryTempFormula;
import kodkod.ast.Variable;
import kodkod.ast.operator.ExprOperator;
import kodkod.ast.operator.FormulaOperator;
import kodkod.ast.operator.IntOperator;
import kodkod.ast.operator.Multiplicity;
import kodkod.ast.operator.TemporalOperator;
import kodkod.ast.visitor.VoidVisitor;
import kodkod.engine.config.AbstractReporter;
import kodkod.engine.config.ExtendedOptions;
import kodkod.engine.config.Options;
import kodkod.engine.config.Reporter;
import kodkod.engine.fol2sat.Translation.Whole;
import kodkod.engine.fol2sat.Translator;
import kodkod.instance.Bounds;
import kodkod.instance.PardinusBounds;
import kodkod.instance.Tuple;
import kodkod.instance.TupleSet;
import kodkod.instance.Universe;
import kodkod.util.ints.IndexedEntry;
import kodkod.util.ints.IntSet;
import kodkod.util.ints.SparseSequence;
import kodkod.util.nodes.PrettyPrinter;

/**
 * Translates an unbounded temporal model finding problem into an Electrod
 * problem in its concrete syntax. This includes the universe, bounds of the
 * variables, the goal as a relational formula and the symmetry breaking
 * predicate.
 * 
 * Electrod has currently limited support for integers. Although integer
 * operations and formulas over integers are supported, the conversion between
 * integer atoms and their numeric semantics is not.
 * 
 * @author <NAME> // [HASLab] unbounded temporal model finding
 */
public class ElectrodPrinter {

	/**
	 * Translates and prints an unbounded temporal model finding problem into
	 * Electrod. Intercepts the symmetry breaking predicate so that it can be
	 * used by Electrod.
	 * 
	 * @param formula
	 *            the problem's formula.
	 * @param bounds
	 *            the problem's bounds.
	 * @param rep 
	 * @return the printed Electrod problem.
	 * @throws InvalidUnboundedProblem
	 *             if the problem is not supported by Electrod.
	 */
	public static String print(Formula formula, PardinusBounds bounds, Reporter rep)
			throws InvalidUnboundedProblem {
		// use a reporter to intercept the symmetry breaking predicate
		Options opt = new ExtendedOptions();
		StringBuilder temp = new StringBuilder();
		Reporter reporter = new AbstractReporter() {
			
			@Override
			public void warning(String warning) {
				rep.warning(warning);
			}
			
			@Override
			public void reportLex(List<Entry<Relation, Tuple>> _original,
					List<Entry<Relation, Tuple>> _permuted) {
				if (_original.size()+_permuted.size()==0)
					return;
				String tmp = printLexList(_original);
				temp.append(tmp.substring(0,tmp.length()-1));
				temp.append(" <= ");
				temp.append(printLexList(_permuted).substring(1));
				temp.append(";\n");
			}
			
			@Override
			public void detectedSymmetries(Set<IntSet> parts) {
				rep.detectedSymmetries(parts);
			}
			
			@Override
			public void debug(String debug) {
				rep.debug(debug);
			}

		};
		opt.setReporter(reporter);
		
//		Map<Name, Set<RelationPredicate>> preds = AnnotatedNode.annotate(formula).predicates();
//		for (RelationPredicate pred : preds.get(Name.FUNCTION)) {
//			RelationPredicate.Function func = (RelationPredicate.Function) pred;
//			Expression upp = bounds.upperSymbBounds(func.relation());
//			if (upp != null && upp instanceof BinaryExpression && ((BinaryExpression) upp).op().equals(ExprOperator.PRODUCT) && 
//					((BinaryExpression) upp).left().equals(func.domain()) && ((BinaryExpression) upp).right().equals(func.range()))
//				System.out.println(func.relation() + " : " + func.domain() +" -> "+func.targetMult()+" "+func.range());
//		}
		

		// retrieve the additional formula imposed by the symbolic
		// bounds, depending on execution stage
		Formula symbForm = Formula.TRUE;
		// if decomposed mode, the amalgamated bounds are always considered
		if (opt.decomposed() && bounds.amalgamated() != null)
			symbForm = bounds.amalgamated().resolve(opt.reporter());
		// otherwise use regular bounds
		else
			symbForm = bounds.resolve(opt.reporter());


		Whole t = Translator.translate(formula.and(symbForm), bounds, opt);
		bounds = (PardinusBounds) t.bounds();

		try {
			StringBuilder sb = new StringBuilder();
			sb.append(printUniverse(bounds.universe()));
			sb.append(printBounds(bounds));
			sb.append(printSymmetries(temp.toString()));
			sb.append(printConstraint(formula.and(symbForm)));
			return sb.toString();
		} catch (Exception e) {
			throw new InvalidUnboundedProblem(e);
		}
	}

	/**
	 * Print the universe of atoms.
	 * 
	 * @param universe the universe of atoms.
	 * @return the universe in Electrod's concrete syntax.
	 */
	private static String printUniverse(Universe universe) {
		StringBuilder sb = new StringBuilder("univ : { ");
		Iterator<Object> it = universe.iterator();
{'fraction_non_alphanumeric': 0.10292214426810163, 'fraction_numerical': 0.0019072270281315987, 'mean_word_length': 4.5071267816954235, 'pattern_counts': {'":': 0, '<': 27, '<?xml version=': 0, '>': 27, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3747802', 'n_tokens_mistral': 4866, 'n_tokens_neox': 4390, 'n_words': 1247}