theory-specific simplifications in the ClauseInliner

uuverifiers · Aug 27, 2024 · e88e9b4 · e88e9b4
1 parent e8d4044
commit e88e9b4
Show file tree

Hide file tree

Showing 2 changed files with 27 additions and 5 deletions.
diff --git a/src/main/scala/lazabs/horn/bottomup/HornClauses.scala b/src/main/scala/lazabs/horn/bottomup/HornClauses.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2011-2021 Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2011-2024 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:
@@ -57,6 +57,12 @@ object HornClauses {
     (for (clause <- clauses.iterator;
           p <- clause.predicates.iterator) yield p).toSet - HornClauses.FALSE
 
+  def allTheories(clauses : Iterable[Clause]) : Seq[Theory] = {
+    val coll = new TheoryCollector
+    clauses.foreach(_.collectTheories(coll))
+    coll.theories
+  }
+
   def allTermsSimple(terms : Iterable[ITerm]) : Boolean =
     terms forall {
       case SimpleTerm(_) => true
@@ -84,12 +90,16 @@ object HornClauses {
     lazy val predicates =
       (for (IAtom(p, _) <- (Iterator single head) ++ body.iterator) yield p).toSet
 
-    lazy val theories : Seq[Theory] = {
-      val coll = new TheoryCollector
+    def collectTheories(coll : TheoryCollector) : Unit = {
       coll(head)
       for (a <- body)
         coll(a)
       coll(constraint)
+    }
+
+    lazy val theories : Seq[Theory] = {
+      val coll = new TheoryCollector
+      collectTheories(coll)
       coll.theories
     }
 

diff --git a/src/main/scala/lazabs/horn/preprocessor/ClauseInliner.scala b/src/main/scala/lazabs/horn/preprocessor/ClauseInliner.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2011-2023 Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2011-2024 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:
@@ -36,6 +36,7 @@ import lazabs.horn.Util.{Dag, DagNode, DagEmpty}
 
 import ap.basetypes.IdealInt
 import ap.parser._
+import ap.theories.Theory
 import IExpression._
 import ap.SimpleAPI
 import SimpleAPI.ProverStatus
@@ -82,6 +83,17 @@ class ClauseInliner extends HornPreprocessor {
       // solutions
 
       def translate(solution : Solution) = {
+        val clauseTheories = HornClauses.allTheories(clauses)
+
+        // theory-specific simplification of solutions
+        val rewritings =
+          Rewriter.combineRewritings(Theory.postSimplifiers(clauseTheories))
+        val simplifier =
+          new Simplifier {
+            protected override def furtherSimplifications(expr : IExpression) =
+              rewritings(expr)
+          }
+
         // augment solution to also satisfy inlined clauses
         var remaining =
           (for ((p, c) <- inlinedClauses.iterator;
@@ -117,7 +129,7 @@ class ClauseInliner extends HornPreprocessor {
                       yield subst(curSolution(pred), args.toList, 0)) &
                   (head.args === headVars)
 
-                val simpSol = (new Simplifier)(projectEx(completeConstraint, headVars))
+                val simpSol = simplifier(projectEx(completeConstraint, headVars))
                 val simpSolVar =
                   ConstantSubstVisitor(simpSol,
                                        (for ((IConstant(c), n) <-