From e4e19cd62b3eebed2de5b9b627509df0ffec23e1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 26 Jul 2021 13:26:55 -0500 Subject: 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. --- src/options/arith_options.toml | 8 ++++++++ src/smt/set_defaults.cpp | 12 ++++++++++++ src/theory/arith/equality_solver.cpp | 5 +++++ src/theory/arith/inference_manager.cpp | 20 +++++++++++++++++++- src/theory/arith/inference_manager.h | 12 +++++++++++- src/theory/arith/theory_arith_private.cpp | 2 +- src/theory/theory_inference_manager.h | 2 +- 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> 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 -- cgit v1.2.3