diff options
| author |  Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-02-07 04:54:42 +0100 |
|---|---|---|
| committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-02-07 04:54:42 +0100 |
| commit | 9f02e7e2fe8b3e347f3d05e8d0751dec016842cd (patch) | |
| tree | 6d0c34c617ed51c9c9715f3ec18552425656b3a5 /Solvers | |
| parent | Remove dreal (diff) | |
| download | VIATRA-Generator-9f02e7e2fe8b3e347f3d05e8d0751dec016842cd.tar.gz VIATRA-Generator-9f02e7e2fe8b3e347f3d05e8d0751dec016842cd.tar.zst VIATRA-Generator-9f02e7e2fe8b3e347f3d05e8d0751dec016842cd.zip | |
measurement setup is ready for server
Diffstat (limited to 'Solvers')
3 files changed, 13 insertions, 2 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend index 1e2bbe6d..381823b3 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend | |||
| @@ -195,6 +195,7 @@ class InstanceModel2PartialInterpretation { | |||
| 195 | EAttribute attribute, | 195 | EAttribute attribute, |
| 196 | Map<String, Map<String, String>> ignoredAttribs | 196 | Map<String, Map<String, String>> ignoredAttribs |
| 197 | ) { | 197 | ) { |
| 198 | if (ignoredAttribs === null || ignoredAttribs.isEmpty) return false; | ||
| 198 | val classInIgnored = ignoredAttribs.get(object.eClass.name) | 199 | val classInIgnored = ignoredAttribs.get(object.eClass.name) |
| 199 | val mayIgnored = ( | 200 | val mayIgnored = ( |
| 200 | classInIgnored !== null && classInIgnored.containsKey("*") | 201 | classInIgnored !== null && classInIgnored.containsKey("*") |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index fbcd6e1d..61a2ac41 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend | |||
| @@ -77,7 +77,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
| 77 | public var nonContainmentWeight = 1 | 77 | public var nonContainmentWeight = 1 |
| 78 | public var unfinishedWFWeight = 1 | 78 | public var unfinishedWFWeight = 1 |
| 79 | public var calculateObjectCreationCosts = false | 79 | public var calculateObjectCreationCosts = false |
| 80 | public NumericSolverSelection numericSolverSelection = NumericSolverSelection.DREAL_DOCKER //currently defaulted to DREAL | 80 | public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3 |
| 81 | public var drealLocalPath = "<path-to-dreal>"; | 81 | public var drealLocalPath = "<path-to-dreal>"; |
| 82 | public var Map<String, Map<String, String>> ignoredAttributesMap = null; | 82 | public var Map<String, Map<String, String>> ignoredAttributesMap = null; |
| 83 | 83 | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index fc1a616b..b8ea25e5 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | |||
| @@ -53,7 +53,17 @@ class NumericSolver { | |||
| 53 | return new NumericDrealProblemSolver(true, null) | 53 | return new NumericDrealProblemSolver(true, null) |
| 54 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) | 54 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) |
| 55 | return new NumericDrealProblemSolver(false, drealLocalPath) | 55 | return new NumericDrealProblemSolver(false, drealLocalPath) |
| 56 | if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver | 56 | if (solverSelection == NumericSolverSelection.Z3) { |
| 57 | //TODO THIS IS HARD-CODED for now | ||
| 58 | val root = "/data/viatra/VIATRA-Generator"; | ||
| 59 | //END HARD-CODED | ||
| 60 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); | ||
| 61 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); | ||
| 62 | System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | ||
| 63 | // System.load("libz3.so"); | ||
| 64 | // System.load("libz3java.so"); | ||
| 65 | return new NumericZ3ProblemSolver | ||
| 66 | } | ||
| 57 | } | 67 | } |
| 58 | 68 | ||
| 59 | def init(ThreadContext context) { | 69 | def init(ThreadContext context) { |