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

@@ -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;
 }
 

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;
 };
 

src/rewriters/ArithmeticEqualityRewriter.h

@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2021-2023, Martin Blicha <[email protected]>
+ * Copyright (c) 2021-2024, Martin Blicha <[email protected]>
  *
  *  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

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 &);