Added sort and const visitors

subprojects/frontends/btor2-frontend/src/main/antlr/Btor2.g4

@@ -29,50 +29,41 @@ line: ( comment | node (symbol)? (comment)? ) '\n';
 
 comment: COMMENT;
 
-nid: NUM; // TODO semantic check nid/sid for >0
-sid: NUM; // TODO semantic check nid/sid for >0
+nid: NUM;
+sid: NUM;
 
-node: ( array_sort | bitvec_sort ) // sort declaration
-    | (input | state) // input or state declaration
-    | opidx // indexed operator node
-    | op // non-indexed operator node
-    | (init | next) // init/next node
-    | property; // property node
-    // | nid 'justice' NUM (nid)+; // justice node // TODO we can not model check justice nodes (not reachability)
+node: ( array_sort | bitvec_sort ) #sort // sort declaration
+    | (input | state | init | next | property) #other
+    | (opidx | op) #operation
+    | (filled_constant | constant | constant_d | constant_h) #constantNode;
+    // | nid 'justice' NUM (nid)+; // justice node // TODO we can not modelcheck justice nodes (not reachability)
 
 opidx: ext | slice;
 
-ext: nid ('uext'|'sext') sid nid w=NUM;
-slice: nid 'slice' sid nid u=NUM l=NUM;
+ext: id=nid ('uext'|'sext') sid opd1=nid w=NUM;
+slice: id=nid 'slice' sid opd1=nid u=NUM l=NUM;
 
 op: binop | unop | terop;
 
-binop: nid BINOP sid opd1=nid opd2=nid;
-unop: nid UNARYOP sid opd1=nid;
-terop: nid TERNARYOP sid opd1=nid opd2=nid opd3=nid;
+binop: id=nid BINOP sid opd1=nid opd2=nid;
+unop: id=nid UNARYOP sid opd1=nid;
+terop: id=nid TERNARYOP sid opd1=nid opd2=nid opd3=nid;
 
-input: nid ('input' sid
-    | 'one' sid
-    | 'ones' sid
-    | 'zero' sid
-    | constant
-    | constant_d
-    | constant_h);
+input: id=nid ('input') sid;
 
-init: nid 'init' sid nid nid;
-next: nid 'next' sid nid nid;
+init: id=nid 'init' sid param1=nid param2=nid;
+next: id=nid 'next' sid param1=nid param2=nid;
 
-state: nid 'state' sid;
+state: id=nid 'state' sid;
 
-property: nid ('bad' | 'constraint' | 'fair' | 'output') nid;
+property: id=nid ('bad' | 'constraint' | 'fair' | 'output') param=nid;
 
-array_sort: sid 'sort array' sid sid;
-bitvec_sort: sid 'sort bitvec' NUM; // TODO semantic check for >0
+array_sort: id=sid 'sort array' sid1=sid sid2=sid;
+bitvec_sort: id=sid 'sort bitvec' width=NUM; // TODO semantic check for >0
 
-constant: 'const' sid bin=NUM; // TODO semantic check that really binary
-
-constant_d: 'constd' sid (MINUS)? dec=NUM; // TODO semantic check that really uint
-
-constant_h: 'consth' sid hex=SYMBOL; // TODO semantic check that really hex
+constant: id=nid 'const' sid bin=NUM; // TODO semantic check that really binary
+constant_d: id=nid 'constd' sid (MINUS)? dec=NUM; // TODO semantic check that really uint
+constant_h: id=nid 'consth' sid hex=SYMBOL; // TODO semantic check that really hex
+filled_constant: id=nid ('one' | 'ones' | 'zero') sid;
 
 symbol: SYMBOL;

subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Declarations.kt

@@ -1,14 +1,17 @@
 import hu.bme.mit.theta.frontend.model.Btor2Node
+import java.math.BigInteger
 
 // Declarations
 
+abstract class Btor2Sort(open val sid : Int) : Btor2Node(sid)
+
 // TODO start supporting arrays
-//data class Btor2ArrayDeclaration(val id: Int, val indexSort: Btor2SortDeclaration, val elementSort: Btor2SortDeclaration)
-data class Btor2BvSortDeclaration(val id: Int, val width: Int) : Btor2Node(id)
+// data class Btor2ArrayDeclaration(val id: Int, val indexSort: Btor2SortDeclaration, val elementSort: Btor2SortDeclaration)
+data class Btor2BvSort(override val sid: Int, val width: Int) : Btor2Sort(sid)
 
 // Constants
-data class Btor2ConstDeclaration(val id: Int, val value: Int, val type: Btor2BvSortDeclaration) : Btor2Node(id) // it can be in binary, decimal or hex in the circuit, but we extract the actual value to the int from that
+data class Btor2Const(override val nid: Int, val value: BigInteger, val type: Btor2BvSort) : Btor2Node(nid) // it can be in binary, decimal or hex in the circuit, but we extract the actual value to the int from that
 
 // Inputs and States
-data class Btor2InputDeclaration(val id: Int, val type: Btor2BvSortDeclaration) : Btor2Node(id)
-data class Btor2StateDeclaration(val id: Int, val type: Btor2BvSortDeclaration) : Btor2Node(id)
+data class Btor2Input(override val nid: Int, val type: Btor2BvSort) : Btor2Node(nid)
+data class Btor2State(override val nid: Int, val type: Btor2BvSort) : Btor2Node(nid)

subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Node.kt

@@ -1,3 +1,3 @@
 package hu.bme.mit.theta.frontend.model
 
-open class Btor2Node(val nid: Int)
+open class Btor2Node(open val nid: Int)

subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/model/Btor2Operators.kt

@@ -1,12 +1,12 @@
 package hu.bme.mit.theta.frontend.model
 
-import Btor2BvSortDeclaration
-import Btor2ConstDeclaration
-import Btor2StateDeclaration
+import Btor2BvSort
+import Btor2Const
+import Btor2State
 
 // Operator Nodes
-data class Btor2InitNode(val id: Int, val nodeType: Btor2BvSortDeclaration, val sortId: Btor2BvSortDeclaration, val state: Btor2StateDeclaration, val value: Btor2ConstDeclaration) : Btor2Node(id)
-data class Btor2NextNode(val id: Int, val nodeType: Btor2BvSortDeclaration, val sortId: Btor2BvSortDeclaration, val state: Btor2StateDeclaration, val value: Btor2Node) : Btor2Node(id)
+data class Btor2InitNode(val id: Int, val nodeType: Btor2BvSort, val sortId: Btor2BvSort, val state: Btor2State, val value: Btor2Const) : Btor2Node(id)
+data class Btor2NextNode(val id: Int, val nodeType: Btor2BvSort, val sortId: Btor2BvSort, val state: Btor2State, val value: Btor2Node) : Btor2Node(id)
 // TODO support justice nodes...? (not reachability, but an invariant)
 // data class Btor2JusticeNode(val id: Int, val num: Int, val children: List<Btor2Node>) : Btor2Node(id)
 data class Btor2BadNode(val id: Int, val operand: Btor2Node) : Btor2Node(id)

subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/Btor2Visitor.kt

@@ -0,0 +1,67 @@
+package hu.bme.mit.theta.frontend.visitor
+
+import Btor2Sort
+import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2BaseVisitor
+import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2Parser
+import hu.bme.mit.theta.frontend.model.Btor2Node
+import java.util.LinkedHashMap
+
+class Btor2Visitor : Btor2BaseVisitor<Btor2Node>() {
+    val idVisitor = IdVisitor()
+    val sortVisitor = SortVisitor(idVisitor)
+    val sorts = LinkedHashMap<Int, Btor2Sort>()
+    val constantVisitor = ConstantVisitor(idVisitor, sorts)
+
+    // Parser rules
+    override fun visitBtor2(ctx: Btor2Parser.Btor2Context): Btor2Node {
+        return visitChildren(ctx) // TODO
+    }
+
+    override fun visitLine(ctx: Btor2Parser.LineContext): Btor2Node {
+        return visitChildren(ctx) // TODO
+    }
+
+    override fun visitSort(ctx: Btor2Parser.SortContext): Btor2Node {
+        val newSort = sortVisitor.visit(ctx)
+        check(!sorts.containsKey(newSort.nid))
+        sorts[newSort.nid] = newSort
+        return newSort
+    }
+
+    override fun visitConstantNode(ctx: Btor2Parser.ConstantNodeContext): Btor2Node {
+        val newConstant = constantVisitor.visit(ctx)
+        return newConstant
+    }
+
+    ////////////////////
+
+    override fun visitInput(ctx: Btor2Parser.InputContext): Btor2Node {
+        // Implementation for visiting input rule
+        throw NotImplementedError()
+    }
+
+    override fun visitInit(ctx: Btor2Parser.InitContext): Btor2Node {
+        // Implementation for visiting init rule
+        throw NotImplementedError()
+    }
+
+    override fun visitNext(ctx: Btor2Parser.NextContext): Btor2Node {
+        // Implementation for visiting next rule
+        throw NotImplementedError()
+    }
+
+    override fun visitState(ctx: Btor2Parser.StateContext): Btor2Node {
+        // Implementation for visiting state rule
+        throw NotImplementedError()
+    }
+
+    override fun visitProperty(ctx: Btor2Parser.PropertyContext): Btor2Node {
+        // Implementation for visiting property rule
+        throw NotImplementedError()
+    }
+
+    override fun visitSymbol(ctx: Btor2Parser.SymbolContext): Btor2Node {
+        // Implementation for visiting symbol rule
+        throw NotImplementedError()
+    }
+}

subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/ConstantVisitor.kt

@@ -0,0 +1,46 @@
+package hu.bme.mit.theta.frontend.visitor
+
+import Btor2BvSort
+import Btor2Const
+import Btor2Sort
+import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2BaseVisitor
+import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2Parser
+import java.math.BigInteger
+
+class ConstantVisitor(val idVisitor : IdVisitor, val sorts : Map<Int, Btor2Sort>) : Btor2BaseVisitor<Btor2Const>() {
+    override fun visitConstantNode(ctx: Btor2Parser.ConstantNodeContext): Btor2Const {
+        check(ctx.childCount==1)
+        return ctx.children[0].accept(this)
+    }
+
+    override fun visitConstant(ctx: Btor2Parser.ConstantContext): Btor2Const {
+        val nid = idVisitor.visit(ctx.nid())
+        val sid = idVisitor.visit(ctx.sid())
+        val sort : Btor2BvSort = sorts[sid] as Btor2BvSort
+
+        val value = BigInteger(ctx.bin.text, 2)
+        val node = Btor2Const(nid, value, sort)
+        return node
+    }
+
+    override fun visitConstant_d(ctx: Btor2Parser.Constant_dContext): Btor2Const {
+        val nid = idVisitor.visit(ctx.nid())
+        val sid = idVisitor.visit(ctx.sid())
+        val sort : Btor2BvSort = sorts[sid] as Btor2BvSort
+
+        var value = BigInteger(ctx.dec.text)
+        ctx.MINUS()?.let{ value = value.multiply(BigInteger("-1")) }
+        val node = Btor2Const(nid, value, sort)
+        return node
+    }
+
+    override fun visitConstant_h(ctx: Btor2Parser.Constant_hContext): Btor2Const {
+        val nid = idVisitor.visit(ctx.nid())
+        val sid = idVisitor.visit(ctx.sid())
+        val sort : Btor2BvSort = sorts[sid] as Btor2BvSort
+
+        val value = BigInteger(ctx.hex.text, 16)
+        val node = Btor2Const(nid, value, sort)
+        return node
+    }
+}

subprojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitor/IdVisitor.kt

@@ -0,0 +1,23 @@
+package hu.bme.mit.theta.frontend.visitor
+
+import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2BaseVisitor
+import hu.bme.mit.theta.btor2.frontend.dsl.gen.Btor2Parser
+
+class IdVisitor : Btor2BaseVisitor<Int>() {
+    override fun visitNid(ctx: Btor2Parser.NidContext): Int {
+        val nid = ctx.NUM().text.toInt()
+        if (nid <= 0) {
+            throw RuntimeException("nid should be bigger than 0")
+        }
+        return nid
+    }
+
+    override fun visitSid(ctx: Btor2Parser.SidContext): Int {
+        val sid = ctx.NUM().text.toInt()
+        if (sid <= 0) {
+            throw RuntimeException("nid should be bigger than 0")
+        }
+        return sid
+    }
+
+}