From b95e90dfb2c7f0a57cf02c2313d03521ca94b2e7 Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@gmail.com>
Date: Sat, 24 Feb 2024 10:11:47 +0100
Subject: [PATCH] Rewriting: Do not collect rewritten arithmetic inequalities

The information about which inequalities originated from arithmetic
equalities were recorded during preprocessing. However, this makes it
difficult to separate preprocessing passes and make them more
independent, i.e., so we can run them on single formula as well as on
group of formulas.
If this information is needed, it should be obtain in a different way.
At the moment, this information is only used by the lookahead solver for
partitioning, where the strategy is to not split on such inequalities.
However, I do not see benefit in such strategy.
Since the need to record this information is blocking further
refactoring that has the potential to unlock performance improvements in
incremental solving, I propose to just not record this information
anymore.
---
 src/logics/LATheory.h                      |  3 ---
 src/logics/Theory.h                        |  1 -
 src/rewriters/ArithmeticEqualityRewriter.h | 14 ++------------
 src/smtsolvers/LookaheadSMTSolver.h        |  2 +-
 4 files changed, 3 insertions(+), 17 deletions(-)

diff --git a/src/logics/LATheory.h b/src/logics/LATheory.h
index 1e0803465..c961c55f7 100644
--- a/src/logics/LATheory.h
+++ b/src/logics/LATheory.h
@@ -15,7 +15,6 @@ class LATheory : public Theory
 protected:
     LinAlgLogic& lalogic;
     LinAlgTHandler  latshandler;
-    std::unique_ptr<Map<PTRef,bool,PTRefHash>> notOkToPartition;
 public:
     LATheory(SMTConfig & c, LinAlgLogic & logic)
             : Theory(c)
@@ -26,7 +25,6 @@ class LATheory : public Theory
     virtual const LinAlgLogic&    getLogic() const override { return lalogic; }
     virtual LinAlgTHandler&       getTSolverHandler() override { return latshandler; }
     virtual bool               simplify(const vec<PFRef>&, PartitionManager& pmanager, int) override; // Theory specific simplifications
-    virtual bool               okToPartition(PTRef tr) const override { return !notOkToPartition->has(tr); }
 };
 
 namespace {
@@ -69,7 +67,6 @@ bool LATheory<LinAlgLogic,LinAlgTSHandler>::simplify(const vec<PFRef>& formulas,
         finalFla = rewriteDivMod<LinAlgLogic>(lalogic, finalFla);
         currentFrame.root = equalityRewriter.rewrite(finalFla);
     }
-    notOkToPartition = equalityRewriter.getAndClearNotOkToPartition();
     return true;
 }
 
diff --git a/src/logics/Theory.h b/src/logics/Theory.h
index 6d3ed0dcb..5bede3f29 100644
--- a/src/logics/Theory.h
+++ b/src/logics/Theory.h
@@ -170,7 +170,6 @@ class Theory
     virtual bool            simplify(const vec<PFRef>&, PartitionManager& pmanager, int) = 0; // Simplify a vector of PushFrames in an incrementality-aware manner
     SubstitutionResult      computeSubstitutions(PTRef fla);
     void                    printFramesAsQuery(const vec<PFRef> & frames, std::ostream & s) const;
-    virtual bool            okToPartition(PTRef) const { return true; }
     virtual                ~Theory() = default;
 };
 
diff --git a/src/rewriters/ArithmeticEqualityRewriter.h b/src/rewriters/ArithmeticEqualityRewriter.h
index fda1ea650..4157f85ec 100644
--- a/src/rewriters/ArithmeticEqualityRewriter.h
+++ b/src/rewriters/ArithmeticEqualityRewriter.h
@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2021-2023, Martin Blicha <martin.blicha@gmail.com>
+ * Copyright (c) 2021-2024, Martin Blicha <martin.blicha@gmail.com>
  *
  *  SPDX-License-Identifier: MIT
  *
@@ -12,14 +12,9 @@
 
 class EqualityRewriterConfig : public DefaultRewriterConfig {
     ArithLogic & logic;
-    std::unique_ptr<Map<PTRef, bool, PTRefHash>> notOkToPartition;
 
 public:
-    EqualityRewriterConfig(ArithLogic & logic) : logic(logic), notOkToPartition(new Map<PTRef, bool, PTRefHash>()) {}
-
-    std::unique_ptr<Map<PTRef, bool, PTRefHash>> getAndClearNotOkToPartition() {
-        return std::exchange(notOkToPartition, std::make_unique<Map<PTRef, bool, PTRefHash>>());
-    }
+    explicit EqualityRewriterConfig(ArithLogic & logic) : logic(logic) {}
 
     bool previsit(PTRef term) override { return logic.hasSortBool(term) and not logic.isIte(term); }
 
@@ -30,8 +25,6 @@ class EqualityRewriterConfig : public DefaultRewriterConfig {
             PTRef a2 = p[1];
             PTRef i1 = logic.mkLeq(a1, a2);
             PTRef i2 = logic.mkGeq(a1, a2);
-            notOkToPartition->insert(i1, true);
-            notOkToPartition->insert(i2, true);
             term = logic.mkAnd(i1, i2);
         }
         return term;
@@ -44,9 +37,6 @@ class ArithmeticEqualityRewriter : public Rewriter<EqualityRewriterConfig> {
 public:
     explicit ArithmeticEqualityRewriter(ArithLogic & logic)
         : Rewriter<EqualityRewriterConfig>(logic, config), config(logic) {}
-    std::unique_ptr<Map<PTRef, bool, PTRefHash>> getAndClearNotOkToPartition() {
-        return config.getAndClearNotOkToPartition();
-    }
 };
 
 #endif // OPENSMT_ARITHMETICEQUALITYREWRITER_H
diff --git a/src/smtsolvers/LookaheadSMTSolver.h b/src/smtsolvers/LookaheadSMTSolver.h
index b17fb6046..ae8ed3ca5 100644
--- a/src/smtsolvers/LookaheadSMTSolver.h
+++ b/src/smtsolvers/LookaheadSMTSolver.h
@@ -72,7 +72,7 @@ class LookaheadSMTSolver : public SimpSMTSolver {
     laresult expandTree(LANode & n, std::unique_ptr<LANode> c1,
                         std::unique_ptr<LANode> c2); // Do lookahead.  On success write the new children to c1 and c2
     std::unique_ptr<LookaheadScore> score;
-    bool okToPartition(Var v) const { return theory_handler.getTheory().okToPartition(theory_handler.varToTerm(v)); };
+    bool okToPartition(Var) const { return true; }
 
 public:
     LookaheadSMTSolver(SMTConfig &, THandler &);