correctly typed terms with constant propagation

Author: pruemmer

regression-tests/horn-bv/constants.smt2

@@ -0,0 +1,18 @@
+(set-logic HORN)
+
+(declare-fun I1 ((_ BitVec 32)) Bool)
+(declare-fun I2 ((_ BitVec 32)) Bool)
+(declare-fun I3 ((_ BitVec 32)) Bool)
+(declare-fun I4 ((_ BitVec 32)) Bool)
+
+(assert (I1 (_ bv10 32)))
+
+(assert (forall ((x (_ BitVec 32))) (=> (I1 x) (I2 x))))
+(assert (forall ((x (_ BitVec 32))) (=> (I1 x) (I3 x))))
+(assert (forall ((x (_ BitVec 32))) (=> (I2 x) (I4 x))))
+(assert (forall ((x (_ BitVec 32))) (=> (I3 x) (I4 x))))
+
+(assert (forall ((x (_ BitVec 32))) (=> (I4 x) (= x (_ bv10 32)))))
+
+(check-sat)
+

regression-tests/horn-bv/runtests

@@ -25,6 +25,14 @@ for name in $TESTS; do
     $LAZABS -cex -abstract:off "$@" $name 2>&1 | grep -v 'at '
 done
 
+TESTS="constants.smt2"
+
+for name in $TESTS; do
+    echo
+    echo $name
+    $LAZABS -scex -ssol -abstract:off "$@" $name 2>&1 | grep -v 'at '
+done
+
 TESTS="int2bv.smt2"
 
 for name in $TESTS; do

src/main/scala/lazabs/horn/preprocessor/ConstantPropagator.scala

@@ -143,7 +143,12 @@ object SimplePropagators {
           val subst =
             (for (((arg, sort), ind) <-
                     (constantArgs.iterator zip sorts.iterator).zipWithIndex)
-             yield (arg getOrElse v(ind, sort))).toList
+             yield {
+               arg match {
+                case Some(c) => SymbolSplitter.toCtorTerm(c, sort)
+                case None => v(ind, sort)
+               }
+             }).toList
           val simpSol = SimplifyingVariableSubstVisitor(sol, (subst, 0))
 
           and(for ((Some(t), ind) <- constantArgs.iterator.zipWithIndex)

src/main/scala/lazabs/horn/preprocessor/SymbolSplitter.scala

@@ -40,6 +40,7 @@ import ap.types.MonoSortedPredicate
 import ap.types.Sort
 import IExpression._
 import ap.util.Seqs
+import ap.theories.ModuloArithmetic
 
 import scala.collection.mutable.{HashSet => MHashSet, HashMap => MHashMap,
                                  LinkedHashSet, ArrayBuffer}
@@ -231,16 +232,30 @@ object SymbolSplitter extends HornPreprocessor {
 
   //////////////////////////////////////////////////////////////////////////////
 
+  import ModuloArithmetic.{mod_cast, evalModCast, ModSort}
+
   protected[preprocessor] def solutionEquation(argNum : Int,
                                                argSort : Sort,
                                                t : ITerm) : IFormula =
-    t match {
+    (t, argSort) match {
       // don't introduce a simple equation in case of
       // False, this would be too strong
-      case Sort.MultipleValueBool.False =>
+      case (Sort.MultipleValueBool.False, Sort.MultipleValueBool) =>
         (v(argNum, argSort) =/= Sort.MultipleValueBool.True)
-      case arg =>
-        (v(argNum, argSort) === arg)
+      case (Const(value), ModSort(lower, upper)) =>
+        (v(argNum, argSort) === mod_cast(lower, upper, value))
+      case (t, argSort) =>
+        (v(argNum, argSort) === t)
+    }
+
+  protected[preprocessor] def toCtorTerm(arg : ITerm, sort : Sort) : ITerm =
+    (arg, sort) match {
+      case (IIntLit(value), ModSort(lower, upper)) => {
+        assert(evalModCast(lower, upper, value) == value)
+        mod_cast(lower, upper, value)
+      }
+      case (t, _) =>
+        t
     }
 
   //////////////////////////////////////////////////////////////////////////////
@@ -274,6 +289,8 @@ object SymbolSplitter extends HornPreprocessor {
     object ConcreteTerm {
       def unapply(t : ITerm) : Option[ITerm] = t match {
         case t : IIntLit                  => Some(t)
+        case IFunApp(`mod_cast`, Seq(Const(l), Const(u), Const(v)))
+                                          => Some(IIntLit(evalModCast(l, u, v)))
         case IConstant(c)                 => constValue get c
         case True | False                 => Some(t)
         case _                            => None

src/main/scala/lazabs/horn/preprocessor/UniqueConstructorExpander.scala

@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2020-2025 Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2020-2026 Philipp Ruemmer. All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -233,7 +233,7 @@ class UniqueConstructorExpander extends ArgumentExpander {
                adtSort = sort.asInstanceOf[ADT.ADTProxySort];
                adt = adtSort.adtTheory;
                if adt.ctorIdsPerSort(adtSort.sortNum).size > 1) yield {
-            adt.hasCtor(v(argInd), ctorInd)
+            adt.hasCtor(v(argInd, sort), ctorInd)
           }
         f &&& and(ctorConstraints)
       }