1 files changed, 74 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
new file mode 100644
index 00000000..84aa521d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -0,0 +1,74 @@
+package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
+import java.util.List
+class Logic2VampireLanguageMapper_ScopeMapper {
+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
+        val Logic2VampireLanguageMapper base
+        public new(Logic2VampireLanguageMapper base) {
+                this.base = base
+        }
+        def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
+                val VLSVariable variable = createVLSVariable => [it.name = "A"]
+                
+                // 1. make a list of constants equaling the min number of specified objects
+                val List<VLSConstant> instances = newArrayList
+                for (var i = 0; i < config.typeScopes.minNewElements; i++) {
+                        val num = i + 1
+                        val cst = createVLSConstant => [
+                                it.name = "o" + num
+                        ]
+                        instances.add(cst)
+                }
+                
+                
+                // TODO: specify for the max
+                // 2. Create initial fof formula to specify the number of elems
+                val cstDec = createVLSFofFormula => [
+                        it.name = "typeScope"
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                it.variables += support.duplicate(variable)
+                                // check below
+                                it.operand = createVLSEquivalent => [
+                                        it.left = support.topLevelTypeFunc
+                                        it.right = support.unfoldOr(instances.map [ i |
+                                                createVLSEquality => [
+                                                        it.left = createVLSVariable => [it.name = variable.name]
+                                                        it.right = i
+                                                ]
+                                        ])
+                                ]
+                        ]
+                ]
+                trace.specification.formulas += cstDec
+                // TODO: specify for scope per type
+                // 3. Specify uniqueness of elements
+                val uniqueness = createVLSFofFormula => [
+                        it.name = "typeUniqueness"
+                        it.fofRole = "axiom"
+                        it.fofFormula = support.unfoldOr(instances.map [ i |
+                                createVLSEquality => [
+                                        it.left = createVLSVariable => [it.name = variable.name]
+                                        it.right = i
+                                ]
+                        ])
+                ]
+                trace.specification.formulas += cstDec
+        }
+}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend new file mode 100644 index 00000000..84aa521d --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -0,0 +1,74 @@
	1	package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
	2
	3	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
	4	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
	5	import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
	6	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
	7	import java.util.List
	8
	9	class Logic2VampireLanguageMapper_ScopeMapper {
	10	private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
	11	private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
	12	val Logic2VampireLanguageMapper base
	13
	14	public new(Logic2VampireLanguageMapper base) {
	15	this.base = base
	16	}
	17
	18	def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
	19	val VLSVariable variable = createVLSVariable => [it.name = "A"]
	20
	21
	22	// 1. make a list of constants equaling the min number of specified objects
	23	val List<VLSConstant> instances = newArrayList
	24	for (var i = 0; i < config.typeScopes.minNewElements; i++) {
	25	val num = i + 1
	26	val cst = createVLSConstant => [
	27	it.name = "o" + num
	28	]
	29	instances.add(cst)
	30	}
	31
	32
	33	// TODO: specify for the max
	34
	35
	36	// 2. Create initial fof formula to specify the number of elems
	37	val cstDec = createVLSFofFormula => [
	38	it.name = "typeScope"
	39	it.fofRole = "axiom"
	40	it.fofFormula = createVLSUniversalQuantifier => [
	41	it.variables += support.duplicate(variable)
	42	// check below
	43	it.operand = createVLSEquivalent => [
	44	it.left = support.topLevelTypeFunc
	45	it.right = support.unfoldOr(instances.map [ i \|
	46	createVLSEquality => [
	47	it.left = createVLSVariable => [it.name = variable.name]
	48	it.right = i
	49	]
	50	])
	51	]
	52	]
	53	]
	54	trace.specification.formulas += cstDec
	55
	56
	57	// TODO: specify for scope per type
	58
	59
	60
	61	// 3. Specify uniqueness of elements
	62	val uniqueness = createVLSFofFormula => [
	63	it.name = "typeUniqueness"
	64	it.fofRole = "axiom"
	65	it.fofFormula = support.unfoldOr(instances.map [ i \|
	66	createVLSEquality => [
	67	it.left = createVLSVariable => [it.name = variable.name]
	68	it.right = i
	69	]
	70	])
	71	]
	72	trace.specification.formulas += cstDec
	73	}
	74	}