Merge pull request #275 from ftsrg/chc-out

This PR adds support for CHC solving via dedicated CHC solvers (including Z3)

.github/workflows/linux-build-test-deploy.yml

@@ -101,7 +101,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-latest, ubuntu-22.04, ubuntu-20.04]
+        os: [ubuntu-latest, ubuntu-22.04]
     needs: build
     runs-on: ${{ matrix.os }}
     steps:

.gitignore

@@ -27,3 +27,4 @@ xcfa.c
 xcfa.dot
 xcfa.json
 *.plantuml
+xcfa-*.smt2

build.gradle.kts

@@ -28,7 +28,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "5.3.0"
+    version = "5.4.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

settings.gradle.kts

@@ -39,6 +39,7 @@ include(
     "xcfa/c2xcfa",
     "xcfa/litmus2xcfa",
     "xcfa/llvm2xcfa",
+    "xcfa/xcfa2chc",
     "xcfa/xcfa-analysis",
     "xcfa/xcfa-cli",
 

subprojects/common/core/src/main/java/hu/bme/mit/theta/core/ChcUtils.kt

@@ -0,0 +1,115 @@
+/*
+ *  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.core
+
+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 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
+}

subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/functype/FuncExprs.java

@@ -22,6 +22,7 @@
 import java.util.List;
 
 import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkState;
 
 public final class FuncExprs {
 
@@ -62,4 +63,16 @@ public static <ParamType extends Type, ResultType extends Type> FuncAppExpr<Para
         return App(func, paramHead, paramTail);
     }
 
+    public static <T1 extends Type, T2 extends Type> Expr<?> UnsafeApp(final Expr<?> func, final Expr<?> param) {
+        checkState(func.getType() instanceof FuncType<?, ?> fFunc && fFunc.getParamType().equals(param.getType()), "Parameter of type " + param.getType() + " is not suitable for function of type " + func.getType());
+        final Expr<FuncType<T1, T2>> funcTyped = (Expr<FuncType<T1, T2>>) func;
+        final Expr<T1> paramTyped = (Expr<T1>) param;
+        return App(funcTyped, paramTyped);
+    }
+
+    public static <T1 extends Type, T2 extends Type> Expr<?> UnsafeApp(final Expr<?> func, final List<Expr<?>> param) {
+        checkState(func.getType() instanceof FuncType<?, ?> fFunc, "Supposed function is of type " + func.getType());
+        final Expr<FuncType<T1, T2>> funcTyped = (Expr<FuncType<T1, T2>>) func;
+        return App(funcTyped, param.stream().map(it -> (Expr) it).toList());
+    }
 }

subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprUtils.java

@@ -15,9 +15,12 @@
  */
 package hu.bme.mit.theta.core.utils;
 
+import com.google.common.collect.ImmutableList;
+import hu.bme.mit.theta.common.Tuple2;
 import hu.bme.mit.theta.common.container.Containers;
 import hu.bme.mit.theta.core.decl.ConstDecl;
 import hu.bme.mit.theta.core.decl.Decl;
+import hu.bme.mit.theta.core.decl.IndexedConstDecl;
 import hu.bme.mit.theta.core.decl.ParamDecl;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.model.ImmutableValuation;
@@ -27,20 +30,26 @@
 import hu.bme.mit.theta.core.type.anytype.RefExpr;
 import hu.bme.mit.theta.core.type.booltype.AndExpr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.type.booltype.ExistsExpr;
+import hu.bme.mit.theta.core.type.booltype.ForallExpr;
 import hu.bme.mit.theta.core.type.booltype.NotExpr;
+import hu.bme.mit.theta.core.type.functype.FuncAppExpr;
 import hu.bme.mit.theta.core.utils.IndexedVars.Builder;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
 
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Collections;
 import java.util.HashSet;
+import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Map;
+import java.util.Map.Entry;
 import java.util.Set;
 import java.util.stream.Collectors;
 
 import static com.google.common.base.Preconditions.checkNotNull;
+import static hu.bme.mit.theta.core.utils.TypeUtils.cast;
 
 /**
  * Utility functions related to expressions.
@@ -112,6 +121,69 @@ public static Collection<Expr<BoolType>> getConjuncts(final Expr<BoolType> expr)
         }
     }
 
+    /**
+     * Collect params of an expression into a given collection.
+     *
+     * @param expr      Expression
+     * @param collectTo Collection where the params should be put
+     */
+    public static void collectParams(final Expr<?> expr, final Collection<ParamDecl<?>> collectTo) {
+        if (expr instanceof RefExpr<?> refExpr) {
+            final Decl<?> decl = refExpr.getDecl();
+            if (decl instanceof ParamDecl<?> param) {
+                collectTo.add(param);
+                return;
+            }
+        }
+
+        if (expr instanceof ForallExpr forall) {
+            Set<ParamDecl<?>> params = new LinkedHashSet<>(getParams(forall.getOp()));
+            forall.getParamDecls().forEach(params::remove);
+            collectTo.addAll(params);
+        } else if (expr instanceof ExistsExpr exists) {
+            Set<ParamDecl<?>> params = new LinkedHashSet<>(getParams(exists.getOp()));
+            exists.getParamDecls().forEach(params::remove);
+            collectTo.addAll(params);
+        } else {
+            expr.getOps().forEach(op -> collectParams(op, collectTo));
+        }
+    }
+
+    /**
+     * Collect params from expressions into a given collection.
+     *
+     * @param exprs     Expressions
+     * @param collectTo Collection where the variables should be put
+     */
+    public static void collectParams(final Iterable<? extends Expr<?>> exprs, final Collection<ParamDecl<?>> collectTo) {
+        exprs.forEach(e -> collectParams(e, collectTo));
+    }
+
+    /**
+     * Get variables of an expression.
+     *
+     * @param expr Expression
+     * @return Set of variables appearing in the expression
+     */
+    public static Set<ParamDecl<?>> getParams(final Expr<?> expr) {
+        final Set<ParamDecl<?>> vars = Containers.createSet();
+        collectParams(expr, vars);
+        return vars;
+    }
+
+    /**
+     * Get variables of expressions.
+     *
+     * @param exprs Expressions
+     * @return Set of variables appearing in the expressions
+     */
+    public static Set<ParamDecl<?>> getParams(final Iterable<? extends Expr<?>> exprs) {
+        final Set<ParamDecl<?>> vars = Containers.createSet();
+        collectParams(exprs, vars);
+        return vars;
+    }
+
+
     /**
      * Collect variables of an expression into a given collection.
      *
@@ -165,6 +237,59 @@ public static Set<VarDecl<?>> getVars(final Iterable<? extends Expr<?>> exprs) {
         return vars;
     }
 
+    /**
+     * Collect indexed constants of an expression into a given collection.
+     *
+     * @param expr      Expression
+     * @param collectTo Collection where the constants should be put
+     */
+    public static void collectIndexedConstants(final Expr<?> expr, final Collection<IndexedConstDecl<?>> collectTo) {
+        if (expr instanceof RefExpr) {
+            final RefExpr<?> refExpr = (RefExpr<?>) expr;
+            final Decl<?> decl = refExpr.getDecl();
+            if (decl instanceof IndexedConstDecl<?>) {
+                final IndexedConstDecl<?> constDecl = (IndexedConstDecl<?>) decl;
+                collectTo.add(constDecl);
+                return;
+            }
+        }
+        expr.getOps().forEach(op -> collectIndexedConstants(op, collectTo));
+    }
+
+    /**
+     * Collect indexed constants from expressions into a given collection.
+     *
+     * @param exprs     Expressions
+     * @param collectTo Collection where the constants should be put
+     */
+    public static void collectIndexedConstants(final Iterable<? extends Expr<?>> exprs, final Collection<IndexedConstDecl<?>> collectTo) {
+        exprs.forEach(e -> collectIndexedConstants(e, collectTo));
+    }
+
+    /**
+     * Get indexed constants of an expression.
+     *
+     * @param expr Expression
+     * @return Set of constants appearing in the expression
+     */
+    public static Set<IndexedConstDecl<?>> getIndexedConstants(final Expr<?> expr) {
+        final Set<IndexedConstDecl<?>> consts = new HashSet<>();
+        collectIndexedConstants(expr, consts);
+        return consts;
+    }
+
+    /**
+     * Get indexed constants of expressions.
+     *
+     * @param exprs Expressions
+     * @return Set of constants appearing in the expressions
+     */
+    public static Set<IndexedConstDecl<?>> getIndexedConstants(final Iterable<? extends Expr<?>> exprs) {
+        final Set<IndexedConstDecl<?>> consts = new HashSet<>();
+        collectIndexedConstants(exprs, consts);
+        return consts;
+    }
+
     /**
      * Collect constants of an expression into a given collection.
      *
@@ -363,4 +488,41 @@ public static int nodeCountSize(final Expr<?> expr) {
         return 1 + expr.getOps().stream().map(ExprUtils::nodeCountSize).reduce(0, (x, y) -> x + y);
     }
 
+    /**
+     * Change fixed subexpressions using a lookup
+     *
+     * @param expr   the expr to change subexpressions in
+     * @param lookup the lookup mapping subexpression to replacements
+     * @return the changed expression
+     */
+    public static <T extends Type> Expr<T> changeSubexpr(Expr<T> expr, Map<Expr<?>, Expr<?>> lookup) {
+        if (lookup.containsKey(expr)) {
+            return cast(lookup.get(expr), expr.getType());
+        } else {
+            return expr.map(e -> changeSubexpr(e, lookup));
+        }
+    }
+
+    public static <T extends Type> Expr<T> changeDecls(Expr<T> expr, Map<? extends Decl<?>, ? extends Decl<?>> lookup) {
+        return changeSubexpr(expr, lookup.entrySet().stream().map(entry -> Map.entry(entry.getKey().getRef(), entry.getValue().getRef())).collect(Collectors.toMap(Entry::getKey, Entry::getValue)));
+    }
+
+    /**
+     * Extracts function and its arguments from a nested expression
+     */
+    public static Tuple2<Expr<?>, List<Expr<?>>> extractFuncAndArgs(final FuncAppExpr<?, ?> expr) {
+        final Expr<?> func = expr.getFunc();
+        final Expr<?> arg = expr.getParam();
+        if (func instanceof FuncAppExpr) {
+            final FuncAppExpr<?, ?> funcApp = (FuncAppExpr<?, ?>) func;
+            final Tuple2<Expr<?>, List<Expr<?>>> funcAndArgs = extractFuncAndArgs(funcApp);
+            final Expr<?> resFunc = funcAndArgs.get1();
+            final List<Expr<?>> args = funcAndArgs.get2();
+            final List<Expr<?>> resArgs = ImmutableList.<Expr<?>>builder().addAll(args).add(arg)
+                    .build();
+            return Tuple2.of(resFunc, resArgs);
+        } else {
+            return Tuple2.of(func, ImmutableList.of(arg));
+        }
+    }
 }