More updates to arithmetic in preparation for central equality engine (#6927)

Makes arithEqSolver more robust to propagations from multiple sources, changes the default relationship to congruence manager based on preliminary results on SMT-LIB.

7 files changed, 57 insertions, 4 deletions

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index 8766672a5..26b1cfecb 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -595,3 +595,11 @@ name   = "Arithmetic Theory"
   type       = "bool"
   default    = "false"
   help       = "whether to use the equality solver in the theory of arithmetic"
+
+[[option]]
+  name       = "arithCongMan"
+  category   = "regular"
+  long       = "arith-cong-man"
+  type       = "bool"
+  default    = "true"
+  help       = "(experimental) whether to use the congruence manager when the equality solver is enabled"
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index d5b3b7929..e12d3eb1d 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -968,6 +968,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Trace("smt") << "setting decision mode to " << opts.decision.decisionMode
                  << std::endl;
   }
+
+  // set up of central equality engine
+  if (opts.arith.arithEqSolver)
+  {
+    if (!opts.arith.arithCongManWasSetByUser)
+    {
+      // if we are using the arithmetic equality solver, do not use the
+      // arithmetic congruence manager by default
+      opts.arith.arithCongMan = false;
+    }
+  }
+
   if (options::incrementalSolving())
   {
     // disable modes not supported by incremental
diff --git a/src/theory/arith/equality_solver.cpp b/src/theory/arith/equality_solver.cpp
index 58793c654..8b4e1b8dd 100644
--- a/src/theory/arith/equality_solver.cpp
+++ b/src/theory/arith/equality_solver.cpp
@@ -80,6 +80,11 @@ TrustNode EqualitySolver::explain(TNode lit)
 }
 bool EqualitySolver::propagateLit(Node lit)
 {
+  // if we've already propagated, ignore
+  if (d_aim.hasPropagated(lit))
+  {
+    return true;
+  }
   // notice this is only used when ee-mode=distributed
   // remember that this was a literal we propagated
   Trace("arith-eq-solver-debug") << "propagate lit " << lit << std::endl;
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 90c17be4a..9cb232908 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -27,7 +27,10 @@ namespace arith {
 InferenceManager::InferenceManager(TheoryArith& ta,
                                    ArithState& astate,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::")
+    : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::"),
+      // currently must track propagated literals if using the equality solver
+      d_trackPropLits(options::arithEqSolver()),
+      d_propLits(astate.getSatContext())
 {
 }
 
@@ -146,6 +149,21 @@ bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem)
   return false;
 }
 
+bool InferenceManager::propagateLit(TNode lit)
+{
+  if (d_trackPropLits)
+  {
+    d_propLits.insert(lit);
+  }
+  return TheoryInferenceManager::propagateLit(lit);
+}
+
+bool InferenceManager::hasPropagated(TNode lit) const
+{
+  Assert(d_trackPropLits);
+  return d_propLits.find(lit) != d_propLits.end();
+}
+
 }  // namespace arith
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index 7e103797e..eeb9d096f 100644
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -97,6 +97,13 @@ class InferenceManager : public InferenceManagerBuffered
 
   /** Checks whether the given lemma is already present in the cache. */
   virtual bool hasCachedLemma(TNode lem, LemmaProperty p) override;
+  /** overrides propagateLit to track which literals have been propagated */
+  bool propagateLit(TNode lit) override;
+  /**
+   * Return true if we have propagated lit already. This call is only valid if
+   * d_trackPropLits is true.
+   */
+  bool hasPropagated(TNode lit) const;
 
  protected:
   /**
@@ -111,9 +118,12 @@ class InferenceManager : public InferenceManagerBuffered
    * conflict.
    */
   bool isEntailedFalse(const SimpleTheoryLemma& lem);
-
   /** The waiting lemmas. */
   std::vector<std::unique_ptr<SimpleTheoryLemma>> d_waitingLem;
+  /** Whether we are tracking the set of propagated literals */
+  bool d_trackPropLits;
+  /** The literals we have propagated */
+  NodeSet d_propLits;
 };
 
 }  // namespace arith
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index d7ae08379..053b91d90 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -137,7 +137,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
                           d_partialModel,
                           RaiseEqualityEngineConflict(*this),
                           d_pnm),
-      d_cmEnabled(c, true),
+      d_cmEnabled(c, options::arithCongMan()),
 
       d_dualSimplex(
           d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index c61f4311b..b11f21f1e 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -132,7 +132,7 @@ class TheoryInferenceManager
    * EqualityEngineNotify::eqNotifyTriggerPredicate and
    * EqualityEngineNotify::eqNotifyTriggerTermEquality.
    */
-  bool propagateLit(TNode lit);
+  virtual bool propagateLit(TNode lit);
   /**
    * Return an explanation for the literal represented by parameter lit
    * (which was previously propagated by this theory). By default, this