aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapperTrace.xtend
blob: 69111a11069614836e0ca622d44b459966900989 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
package hu.bme.mit.inf.dslreasoner.smt.reasoner

import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration
import java.util.HashMap
import java.util.List
import java.util.Map

class Logic2SmtMapperTrace {
	public var LogicProblem problem
	public var Logic2SmtMapper forwardMapper
	public var Logic2Smt_TypeMapperTrace typeMapperTrace

	public val Map<Relation,List<Descriptor<Relation>>> relationUnfolding = new HashMap
	public val Map<Descriptor<Relation>,SMTSymbolicDeclaration> relationMap = new HashMap
	public val Map<Function,List<Descriptor<Function>>> functionUnfolding = new HashMap
	public val Map<Descriptor<Function>,SMTSymbolicDeclaration> functionMap = new HashMap
	public val Map<Function,List<Descriptor<Constant>>> constantUnfolding = new HashMap
	public val Map<Descriptor<Constant>,SMTSymbolicDeclaration> constantMap = new HashMap
}