-
Notifications
You must be signed in to change notification settings - Fork 43
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
05f4293
commit b50dffd
Showing
10 changed files
with
912 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -27,3 +27,4 @@ xcfa.c | |
| xcfa.dot | ||
| xcfa.json | ||
| *.plantuml | ||
| xcfa-*.smt2 | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
| /* | ||
| * Copyright 2024 Budapest University of Technology and Economics | ||
| * | ||
| * Licensed under the Apache License, Version 2.0 (the "License"); | ||
| * you may not use this file except in compliance with the License. | ||
| * You may obtain a copy of the License at | ||
| * | ||
| * http://www.apache.org/licenses/LICENSE-2.0 | ||
| * | ||
| * Unless required by applicable law or agreed to in writing, software | ||
| * distributed under the License is distributed on an "AS IS" BASIS, | ||
| * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
| * See the License for the specific language governing permissions and | ||
| * limitations under the License. | ||
| */ | ||
| plugins { | ||
| id("kotlin-common") | ||
| } | ||
|
|
||
| dependencies { | ||
| implementation(project(":theta-common")) | ||
| implementation(project(":theta-core")) | ||
| implementation(project(":theta-xcfa")) | ||
| implementation(project(":theta-solver-smtlib")) | ||
| } |
122 changes: 122 additions & 0 deletions
122
subprojects/xcfa/xcfa2chc/src/main/java/hu/bme/mit/theta/xcfa2chc/ChcUtils.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,122 @@ | ||
| /* | ||
| * Copyright 2024 Budapest University of Technology and Economics | ||
| * | ||
| * Licensed under the Apache License, Version 2.0 (the "License"); | ||
| * you may not use this file except in compliance with the License. | ||
| * You may obtain a copy of the License at | ||
| * | ||
| * http://www.apache.org/licenses/LICENSE-2.0 | ||
| * | ||
| * Unless required by applicable law or agreed to in writing, software | ||
| * distributed under the License is distributed on an "AS IS" BASIS, | ||
| * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
| * See the License for the specific language governing permissions and | ||
| * limitations under the License. | ||
| */ | ||
|
|
||
| package hu.bme.mit.theta.xcfa2chc | ||
|
|
||
| import com.google.common.base.Preconditions.checkArgument | ||
| import hu.bme.mit.theta.core.decl.Decls.Const | ||
| import hu.bme.mit.theta.core.decl.Decls.Param | ||
| import hu.bme.mit.theta.core.decl.ParamDecl | ||
| import hu.bme.mit.theta.core.type.Expr | ||
| import hu.bme.mit.theta.core.type.Type | ||
| import hu.bme.mit.theta.core.type.booltype.BoolExprs.* | ||
| import hu.bme.mit.theta.core.type.booltype.BoolType | ||
| import hu.bme.mit.theta.core.type.functype.FuncExprs | ||
| import hu.bme.mit.theta.core.type.functype.FuncType | ||
| import hu.bme.mit.theta.core.utils.ExprUtils | ||
| import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibSymbolTable | ||
| import hu.bme.mit.theta.solver.smtlib.impl.generic.GenericSmtLibTransformationManager | ||
| import java.util.* | ||
|
|
||
| /* | ||
| We want to be able to write logical derivations in the following way: | ||
| head_name(vars) += // derivations | ||
| expr(vars). | ||
| head_name(grounds) // facts | ||
| !head_name(vars) with exprs(vars) // queries | ||
| */ | ||
|
|
||
| open class Relation(val name: String, vararg paramTypes: Type) { | ||
| companion object { | ||
| private fun funcType(params: List<Type>, finalType: Type): FuncType<*, *> { | ||
| return if(params.size == 1) { | ||
| FuncType.of(params[0], finalType) | ||
| } else if(params.size > 1) { | ||
| FuncType.of(params[0], funcType(params.subList(1, params.size), finalType)) | ||
| } else { | ||
| error("Nullary functions aren't handled here.") | ||
| } | ||
| } | ||
| } | ||
| val arity: Int = paramTypes.size | ||
| val rules: MutableList<Rule> = LinkedList() | ||
| val constDecl = if(arity == 0) Const(name, Bool()) else Const(name, funcType(paramTypes.toList(), Bool())) | ||
| open operator fun invoke(params: List<Expr<*>>) = RelationApp(this, params) | ||
| open operator fun invoke(vararg params: Expr<*>) = RelationApp(this, params.toList()) | ||
| } | ||
|
|
||
| data class RelationApp(val relation: Relation, val params: List<Expr<*>>, val constraints: List<Expr<BoolType>> = emptyList()) { | ||
| init { | ||
| checkArgument(params.size == relation.arity) | ||
| } | ||
| val expr: Expr<BoolType> by lazy { | ||
| val coreExpr = if(params.size >= 1) { | ||
| FuncExprs.App(relation.constDecl.ref as Expr<FuncType<in Type, BoolType>>, params.map { it }) | ||
| } else { | ||
| relation.constDecl.ref as Expr<BoolType> | ||
| } | ||
| if(constraints.isEmpty()) { | ||
| coreExpr | ||
| } else { | ||
| And(constraints + coreExpr) | ||
| } | ||
| } | ||
|
|
||
| operator fun plusAssign(constraints: List<Expr<BoolType>>) { relation.rules.add(Rule(expr, constraints)) } | ||
| operator fun plusAssign(constraint: Expr<BoolType>) { relation.rules.add(Rule(expr, listOf(constraint))) } | ||
|
|
||
| operator fun not() { relation.rules.add(Rule(False(), listOf(expr))) } | ||
| operator fun unaryPlus() { relation.rules.add(Rule(expr, listOf())) } | ||
| infix fun with(constraints: List<Expr<BoolType>>) = copy(constraints = this.constraints + constraints) | ||
| infix fun with(constraint: Expr<BoolType>) = copy(constraints = this.constraints + constraint) | ||
| } | ||
| data class Rule(val head: Expr<BoolType>, val constraints: List<Expr<BoolType>>) { | ||
| fun toExpr() = Forall(ExprUtils.getParams(head) + ExprUtils.getParams(constraints), Imply(And(constraints), head)) | ||
| } | ||
|
|
||
| operator fun Expr<BoolType>.plus(other: Expr<BoolType>) = listOf(this, other) | ||
|
|
||
| data class ParamHolder<T: Type>(private val type: T) { | ||
| private val lookup = LinkedHashMap<Int, ParamDecl<T>>() | ||
| operator fun get(i: Int) = lookup.getOrPut(i) { Param("P$i", type) }.ref | ||
| } | ||
|
|
||
| fun List<Relation>.toSMT2(): String { | ||
| val symbolTable = GenericSmtLibSymbolTable() | ||
| val transformationManager = GenericSmtLibTransformationManager(symbolTable) | ||
| val terms = flatMap { it.rules.map { "(assert " + transformationManager.toTerm(it.toExpr()) + ")" } } | ||
| val decls = map { symbolTable.getDeclaration(it.constDecl) } | ||
|
|
||
| return """ | ||
| ; generated by Theta | ||
| ; https://github.com/ftsrg/theta/ | ||
| (set-logic HORN) | ||
| ; declarations | ||
| ${decls.joinToString("\n")} | ||
| ; facts, rules, queries | ||
| ${terms.joinToString("\n")} | ||
| (check-sat) | ||
| (exit) | ||
| """.trimIndent() | ||
| } | ||
| fun Relation.toSMT2() = listOf(this).toSMT2() |
Oops, something went wrong.