From 7021a4d1f2805ebf3145cbc3893761d12f23361f Mon Sep 17 00:00:00 2001
From: Kristóf Marussy <kris7topher@gmail.com>
Date: Thu, 1 Aug 2019 01:00:12 +0200
Subject: Configurability and better statistics for measurements

---
 .../ModelGenerationMethodProvider.xtend            | 54 +++++++++++++++++-----
 1 file changed, 42 insertions(+), 12 deletions(-)

(limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend')

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
index 4b278188..8e061b63 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
@@ -27,6 +27,7 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
 import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
 import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
 import org.eclipse.xtend.lib.annotations.Data
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
 
 class ModelGenerationStatistics {
 	public var long transformationExecutionTime = 0
@@ -35,7 +36,25 @@ class ModelGenerationStatistics {
 		transformationExecutionTime += amount
 	}
 
-	public var long PreliminaryTypeAnalisisTime = 0
+	public var long scopePropagationTime = 0
+
+	synchronized def addScopePropagationTime(long amount) {
+		scopePropagationTime += amount
+	}
+
+	public var long preliminaryTypeAnalisisTime = 0
+
+	public var int decisionsTried = 0
+	
+	synchronized def incrementDecisionCount() {
+		decisionsTried++
+	}
+	
+	public var int scopePropagatorInvocations
+	
+	synchronized def incrementScopePropagationCount() {
+		scopePropagatorInvocations++
+	}
 }
 
 @Data class ModelGenerationMethod {
@@ -84,12 +103,12 @@ class ModelGenerationMethodProvider {
 		val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem)
 		val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries,
 			workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles)
-		val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries)
+		val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries, statistics)
 		scopePropagator.propagateAllScopeConstraints
-		val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>>
-		objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator,
+		val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator,
 			nameNewElements, statistics)
-		val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, statistics)
+		val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator,
+			statistics)
 
 		val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries)
 		val unfinishedWF = queries.getUnfinishedWFQueries.values
@@ -118,15 +137,26 @@ class ModelGenerationMethodProvider {
 	}
 
 	private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy,
-		PartialInterpretation emptySolution, GeneratedPatterns queries) {
+		PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) {
 		switch (scopePropagatorStrategy) {
-			case BasicTypeHierarchy:
-				new ScopePropagator(emptySolution)
-			case PolyhedralTypeHierarchy,
-			case PolyhedralRelations: {
+			case ScopePropagatorStrategy.BasicTypeHierarchy:
+				new ScopePropagator(emptySolution, statistics)
+			ScopePropagatorStrategy.Polyhedral: {
 				val types = queries.refineObjectQueries.keySet.map[newType].toSet
-				val solver = new CbcPolyhedronSolver
-				new PolyhedronScopePropagator(emptySolution, types, queries.multiplicityConstraintQueries,
+				val solver = switch (scopePropagatorStrategy.solver) {
+					case Z3Integer:
+						new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds)
+					case Z3Real:
+						new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds)
+					case Cbc:
+						new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true)
+					case Clp:
+						new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true)
+					default:
+						throw new IllegalArgumentException("Unknown polyhedron solver: " +
+							scopePropagatorStrategy.solver)
+				}
+				new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries,
 					queries.hasElementInContainmentQuery, solver, scopePropagatorStrategy.requiresUpperBoundIndexing)
 			}
 			default:
-- 
cgit v1.2.3-54-g00ecf