<commit_before>package hu.bme.mit.inf.dslreasoner.viatra2logic;

import java.math.BigDecimal;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Random;
import java.util.Set;

import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint;
import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation;
import org.eclipse.xtext.common.types.JvmIdentifiableElement;
import org.eclipse.xtext.xbase.XBinaryOperation;
import org.eclipse.xtext.xbase.XExpression;
import org.eclipse.xtext.xbase.XFeatureCall;
import org.eclipse.xtext.xbase.XNumberLiteral;

import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
import com.microsoft.z3.IntExpr;
import com.microsoft.z3.Model;
import com.microsoft.z3.RealExpr;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Status;
import com.microsoft.z3.enumerations.Z3_ast_print_mode;

import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;


public class NumericProblemSolver {
	private static final String N_Base = "org.eclipse.xtext.xbase.lib.";
	private static final String N_PLUS = "operator_plus";
	private static final String N_MINUS = "operator_minus";
	private static final String N_POWER = "operator_power";
	private static final String N_MULTIPLY = "operator_multiply";
	private static final String N_DIVIDE = "operator_divide";
	private static final String N_MODULO = "operator_modulo";
	private static final String N_LESSTHAN = "operator_lessThan";
	private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan";
	private static final String N_GREATERTHAN = "operator_greaterThan";
	private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan";
	private static final String N_EQUALS = "operator_equals";
	private static final String N_NOTEQUALS = "operator_notEquals";
	private static final String N_EQUALS3 = "operator_tripleEquals";
	private static final String N_NOTEQUALS3 = "operator_tripleNotEquals";

	
	private Context ctx;
	private Solver s;
	private Map<Object, Expr> varMap;

	public NumericProblemSolver() {
		HashMap<String, String> cfg = new HashMap<String, String>();
		cfg.put("model", "true");
		ctx = new Context(cfg);	
		ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL);
		s = ctx.mkSolver();
		varMap = new HashMap<Object, Expr>();
	}

	public Context getNumericProblemContext() {
		return ctx;
	}
	
	
	private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) {
		ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>();
		XExpression left = ((XBinaryOperation) expression).getLeftOperand();
		XExpression right = ((XBinaryOperation) expression).getRightOperand();
		
		getJvmIdentifiableElementsHelper(left, allElem);
		getJvmIdentifiableElementsHelper(right, allElem);
		return allElem;
	}
	
	private void getJvmIdentifiableElementsHelper(XExpression e, List<JvmIdentifiableElement> allElem) {
		if (e instanceof XFeatureCall) {
			allElem.add(((XFeatureCall) e).getFeature());
		} else if (e instanceof XBinaryOperation) {
			getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem);
			getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem);
		}
	}
	
	public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
		BoolExpr problemInstance = formNumericProblemInstance(matches);
		s.add(problemInstance);
		boolean result = (s.check() == Status.SATISFIABLE);
		this.ctx.close();
		return result;
	}
	
	public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {		
		Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>();
		long startformingProblem = System.currentTimeMillis();
		BoolExpr problemInstance = formNumericProblemInstance(matches);
		long endformingProblem = System.currentTimeMillis();
		System.out.println("Forming problem: " + (endformingProblem - startformingProblem));
		s.add(problemInstance);
		long startSolvingProblem = System.currentTimeMillis();
		if (s.check() == Status.SATISFIABLE) {
			Model m = s.getModel();
			long endSolvingProblem = System.currentTimeMillis();
			System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem));
			long startFormingSolution = System.currentTimeMillis();
			for (PrimitiveElement o: objs) {
				if(varMap.containsKey(o)) {
					if (o instanceof IntegerElement) {
						IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false);
						Integer oSol = Integer.parseInt(val.toString());
						sol.put(o, oSol);
					} else {
						RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false);
						Long oSol = Long.parseLong(val.toString());
						sol.put(o, oSol);
					}
					//System.out.println("Solution:" + o + "->" + oSol);
					
				} else {
					//System.out.println("not used var:" + o);
				}
			}
			long endFormingSolution = System.currentTimeMillis();
			System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution));
		} else {
			System.out.println("Unsatisfiable");
		}
		this.ctx.close();
		return sol;
	}

	private BoolExpr formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception {
		if (!(e instanceof XBinaryOperation)) {
			throw new Exception ("error in check expression!!!");
		}

		String name = ((XBinaryOperation) e).getFeature().getQualifiedName();

		BoolExpr constraint = null;
				<commit_msg>precise time measurements for the numeric solver<commit_after>package hu.bme.mit.inf.dslreasoner.viatra2logic;

import java.math.BigDecimal;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Random;
import java.util.Set;

import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint;
import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation;
import org.eclipse.xtext.common.types.JvmIdentifiableElement;
import org.eclipse.xtext.xbase.XBinaryOperation;
import org.eclipse.xtext.xbase.XExpression;
import org.eclipse.xtext.xbase.XFeatureCall;
import org.eclipse.xtext.xbase.XNumberLiteral;

import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
import com.microsoft.z3.IntExpr;
import com.microsoft.z3.Model;
import com.microsoft.z3.RealExpr;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Status;
import com.microsoft.z3.enumerations.Z3_ast_print_mode;

import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;


public class NumericProblemSolver {
	private static final String N_Base = "org.eclipse.xtext.xbase.lib.";
	private static final String N_PLUS = "operator_plus";
	private static final String N_MINUS = "operator_minus";
	private static final String N_POWER = "operator_power";
	private static final String N_MULTIPLY = "operator_multiply";
	private static final String N_DIVIDE = "operator_divide";
	private static final String N_MODULO = "operator_modulo";
	private static final String N_LESSTHAN = "operator_lessThan";
	private static final String N_LESSEQUALSTHAN = "operator_lessEqualsThan";
	private static final String N_GREATERTHAN = "operator_greaterThan";
	private static final String N_GREATEREQUALTHAN = "operator_greaterEqualsThan";
	private static final String N_EQUALS = "operator_equals";
	private static final String N_NOTEQUALS = "operator_notEquals";
	private static final String N_EQUALS3 = "operator_tripleEquals";
	private static final String N_NOTEQUALS3 = "operator_tripleNotEquals";

	
	private Context ctx;
	private Solver s;
	private Map<Object, Expr> varMap;
	
	long endformingProblem=0;
	long endSolvingProblem=0;
	long endFormingSolution=0;

	public NumericProblemSolver() {
		HashMap<String, String> cfg = new HashMap<String, String>();
		cfg.put("model", "true");
		ctx = new Context(cfg);	
		ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL);
		s = ctx.mkSolver();
		varMap = new HashMap<Object, Expr>();
	}

	public Context getNumericProblemContext() {
		return ctx;
	}
	
	public long getEndformingProblem() {
		return endformingProblem;
	}

	public long getEndSolvingProblem() {
		return endSolvingProblem;
	}

	public long getEndFormingSolution() {
		return endFormingSolution;
	}

	private ArrayList<JvmIdentifiableElement> getJvmIdentifiableElements(XExpression expression) {
		ArrayList<JvmIdentifiableElement> allElem = new ArrayList<JvmIdentifiableElement>();
		XExpression left = ((XBinaryOperation) expression).getLeftOperand();
		XExpression right = ((XBinaryOperation) expression).getRightOperand();
		
		getJvmIdentifiableElementsHelper(left, allElem);
		getJvmIdentifiableElementsHelper(right, allElem);
		return allElem;
	}
	
	private void getJvmIdentifiableElementsHelper(XExpression e, List<JvmIdentifiableElement> allElem) {
		if (e instanceof XFeatureCall) {
			allElem.add(((XFeatureCall) e).getFeature());
		} else if (e instanceof XBinaryOperation) {
			getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getLeftOperand(), allElem);
			getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem);
		}
	}
	
	public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {
		long startformingProblem = System.nanoTime();
		BoolExpr problemInstance = formNumericProblemInstance(matches);
		s.add(problemInstance);
		endformingProblem = System.nanoTime()-startformingProblem;
		long startSolvingProblem = System.nanoTime();
		boolean result = (s.check() == Status.SATISFIABLE);
		endSolvingProblem = System.nanoTime()-startSolvingProblem;
		this.ctx.close();
		return result;
	}
	
	public Map<PrimitiveElement,Number> getOneSolution(List<PrimitiveElement> objs, Map<XExpression, Iterable<Map<JvmIdentifiableElement,PrimitiveElement>>> matches) throws Exception {		
		Map<PrimitiveElement,Number> sol = new HashMap<PrimitiveElement, Number>();
		long startformingProblem = System.nanoTime();
		BoolExpr problemInstance = formNumericProblemInstance(matches);
		endformingProblem = System.nanoTime()-startformingProblem;
		//System.out.println("Forming problem: " + (endformingProblem - startformingProblem));
		s.add(problemInstance);
		long startSolvingProblem = System.nanoTime();
		if (s.check() == Status.SATISFIABLE) {
			Model m = s.getModel();
			endSolvingProblem = System.nanoTime()-startSolvingProblem;
			System.out.println("Solving problem: " + (endSolvingProblem - startSolvingProblem));
			long startFormingSolution = System.nanoTime();
			for (PrimitiveElement o: objs) {
				if(varMap.containsKey(o)) {
					if (o instanceof IntegerElement) {
						IntExpr val =(IntExpr) m.evaluate(varMap.get(o), false);
						Integer oSol = Integer.parseInt(val.toString());
						sol.put(o, oSol);
					} else {
						RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false);
						Long oSol = Long.parseLong(val.toString());
						sol.put(o, oSol);
					}
					//System.out.println("Solution:" + o + "->" + oSol);
					
				} else {
					//System.out.println("not used var:" + o);
				}
			}
			endFormingSolution = System.nanoTime()-startFormingSolution;
			//System.out.println("Forming solution: " + (endFormingSolution - startFormingSolution));
		} else {
			System.out.println("Unsatisfiable numerical problem");
		}
		this.ctx.close();
		return sol;
	}

	private BoolExpr formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception {
		if (!(e instanceof XBinaryOperation)) {
			throw new Exception ("error in check expression!!!");
		}

		String name = ((XBinaryOperation) e).getFeature().getQualifiedName();

		BoolExpr constraint = null;
				
{'fraction_non_alphanumeric': 0.10831963684746028, 'fraction_numerical': 0.0027392971746106284, 'mean_word_length': 5.704092339979014, 'pattern_counts': {'":': 0, '<': 41, '<?xml version=': 0, '>': 43, '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': '3116338', 'n_tokens_mistral': 4312, 'n_tokens_neox': 3913, 'n_words': 790}