This is work towards having the linear arithmetic solver not impose restrictions on equalities.
The linear arithmetic solver using a CongruenceManager which involves many non-standard uses of the equality engine.
The responsibilities of the CongruenceManager should be migrated to the arithmetic EqSolver, which manages the equality engine in the default way.
This PR is the first step. It makes it so that the memory management and notifications of the equality engine are now solely the responsibility of the EqSolver.
All relevant notifications from the EqSolver are directly forwarded to CongruenceManager. Thus there are no significant behavior changes in this PR.
This PR required removing the experimental option arithCongMan, which forces having the CongruenceManager and the EqSolver both use equality engines.
type = "bool"
default = "false"
help = "whether to use the equality solver in the theory of arithmetic"
-
-[[option]]
- name = "arithCongMan"
- category = "expert"
- long = "arith-cong-man"
- type = "bool"
- default = "true"
- help = "(experimental) whether to use the congruence manager when the equality solver is enabled"
opts.arith.arithEqSolver = true;
}
}
- 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 (logic.isHigherOrder())
{
#include "theory/arith/equality_solver.h"
#include "theory/arith/inference_manager.h"
+#include "theory/arith/linear/congruence_manager.h"
using namespace cvc5::internal::kind;
d_aim(aim),
d_notify(*this),
d_ee(nullptr),
- d_propLits(context())
+ d_propLits(context()),
+ d_acm(nullptr)
{
}
// if we did, explain with the arithmetic inference manager
return d_aim.explainLit(lit);
}
+
+void EqualitySolver::setCongruenceManager(linear::ArithCongruenceManager* acm)
+{
+ d_acm = acm;
+}
+
bool EqualitySolver::propagateLit(Node lit)
{
+ if (d_acm != nullptr)
+ {
+ // if we are using the congruence manager, notify it
+ return d_acm->propagate(lit);
+ }
// if we've already propagated, ignore
if (d_aim.hasPropagated(lit))
{
}
void EqualitySolver::conflictEqConstantMerge(TNode a, TNode b)
{
+ if (d_acm != nullptr)
+ {
+ // if we are using the congruence manager, notify it
+ Node eq = a.eqNode(b);
+ d_acm->propagate(eq);
+ return;
+ }
d_aim.conflictEqConstantMerge(a, b);
}
class InferenceManager;
+namespace linear {
+class ArithCongruenceManager;
+}
+
/**
* The arithmetic equality solver. This class manages arithmetic equalities
- * in the default way via an equality engine.
+ * in the default way via an equality engine, or defers to the congruence
+ * manager of linear arithmetic if setCongruenceManager is called on a
+ * non-null congruence manager.
*
* Since arithmetic has multiple ways of propagating literals, it tracks
* the literals that it propagates and only explains the literals that
*/
TrustNode explain(TNode lit);
+ /** Set the congruence manager, which will be notified of propagations */
+ void setCongruenceManager(linear::ArithCongruenceManager* acm);
+
private:
/** Notification class from the equality engine */
class EqualitySolverNotify : public eq::EqualityEngineNotify
eq::EqualityEngine* d_ee;
/** The literals we have propagated */
NodeSet d_propLits;
+ /** Pointer to the congruence manager, for notifications of propagations */
+ linear::ArithCongruenceManager* d_acm;
};
} // namespace arith
: EnvObj(env),
d_inConflict(context()),
d_raiseConflict(raiseConflict),
- d_notify(*this),
d_keepAlive(context()),
d_propagatations(context()),
d_explanationMap(context()),
ArithCongruenceManager::~ArithCongruenceManager() {}
-bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi)
-{
- Assert(!options().arith.arithEqSolver);
- esi.d_notify = &d_notify;
- esi.d_name = "arithCong::ee";
- return true;
-}
-
void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee)
{
- if (options().arith.arithEqSolver)
- {
- // use our own copy
- d_allocEe = std::make_unique<eq::EqualityEngine>(
- d_env, context(), d_notify, "arithCong::ee", true);
- d_ee = d_allocEe.get();
- if (d_pnm != nullptr)
- {
- // allocate an internal proof equality engine
- d_allocPfee = std::make_unique<eq::ProofEqEngine>(d_env, *d_ee);
- d_ee->setProofEqualityEngine(d_allocPfee.get());
- }
- }
- else
- {
- Assert(ee != nullptr);
- // otherwise, we use the official one
- d_ee = ee;
- }
- // set the congruence kinds on the separate equality engine
- d_ee->addFunctionKind(kind::NONLINEAR_MULT);
- d_ee->addFunctionKind(kind::EXPONENTIAL);
- d_ee->addFunctionKind(kind::SINE);
- d_ee->addFunctionKind(kind::IAND);
- d_ee->addFunctionKind(kind::POW2);
+ Assert(ee != nullptr);
+ // otherwise, we use the official one
+ d_ee = ee;
+ // the congruence kinds are already set up
// the proof equality engine is the one from the equality engine
d_pfee = d_ee->getProofEqualityEngine();
// have proof equality engine only if proofs are enabled
{
}
-ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongruenceManager& acm)
- : d_acm(acm)
-{}
-
-bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerPredicate(
- TNode predicate, bool value)
-{
- Assert(predicate.getKind() == kind::EQUAL);
- Trace("arith::congruences")
- << "ArithCongruenceNotify::eqNotifyTriggerPredicate(" << predicate << ", "
- << (value ? "true" : "false") << ")" << std::endl;
- if (value) {
- return d_acm.propagate(predicate);
- }
- return d_acm.propagate(predicate.notNode());
-}
-
-bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
- Trace("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
- if (value) {
- return d_acm.propagate(t1.eqNode(t2));
- } else {
- return d_acm.propagate(t1.eqNode(t2).notNode());
- }
-}
-void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
- Trace("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
- d_acm.propagate(t1.eqNode(t2));
-}
-void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyNewClass(TNode t) {
-}
-void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyMerge(TNode t1,
- TNode t2)
-{
-}
-void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
-}
-
void ArithCongruenceManager::raiseConflict(Node conflict,
std::shared_ptr<ProofNode> pf)
{
/** d_watchedVariables |-> (= x y) */
ArithVarToNodeMap d_watchedEqualities;
-
- class ArithCongruenceNotify : public eq::EqualityEngineNotify {
- private:
- ArithCongruenceManager& d_acm;
- public:
- ArithCongruenceNotify(ArithCongruenceManager& acm);
-
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
-
- bool eqNotifyTriggerTermEquality(TheoryId tag,
- TNode t1,
- TNode t2,
- bool value) override;
-
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
- void eqNotifyNewClass(TNode t) override;
- void eqNotifyMerge(TNode t1, TNode t2) override;
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
- };
- ArithCongruenceNotify d_notify;
-
context::CDList<Node> d_keepAlive;
/** Store the propagations. */
/** The equality engine being used by this class */
eq::EqualityEngine* d_ee;
- /** The equality engine we allocated */
- std::unique_ptr<eq::EqualityEngine> d_allocEe;
/** proof manager */
ProofNodeManager* d_pnm;
/** A proof generator for storing proofs of facts that are asserted to the EQ
bool canExplain(TNode n) const;
-private:
+ /**
+ * Propagate. Called when the equality engine has inferred literal x.
+ */
+ bool propagate(TNode x);
+
+ private:
Node externalToInternal(TNode n) const;
void pushBack(TNode n);
void pushBack(TNode n, TNode r, TNode w);
- bool propagate(TNode x);
void explain(TNode literal, std::vector<TNode>& assumptions);
/** Assert this literal to the eq engine. Common functionality for
~ArithCongruenceManager();
//--------------------------------- initialization
- /**
- * Returns true if we need an equality engine, see
- * Theory::needsEqualityEngine.
- */
- bool needsEqualityEngine(EeSetupInfo& esi);
/**
* Finish initialize. This class is instructed by TheoryArithPrivate to use
* the equality engine ee.
SetupLiteralCallBack(*this),
d_partialModel,
RaiseEqualityEngineConflict(*this)),
- d_cmEnabled(context(), options().arith.arithCongMan),
+ d_cmEnabled(context(), !options().arith.arithEqSolver),
d_dualSimplex(
env, d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
if(d_approxStats != NULL) { delete d_approxStats; }
}
-bool TheoryArithPrivate::needsEqualityEngine(EeSetupInfo& esi)
-{
- if (!d_cmEnabled)
- {
- return false;
- }
- return d_congruenceManager.needsEqualityEngine(esi);
-}
void TheoryArithPrivate::finishInit()
{
if (d_cmEnabled)
return &d_checker;
}
+ArithCongruenceManager* TheoryArithPrivate::getCongruenceManager()
+{
+ return d_cmEnabled.get() ? &d_congruenceManager : nullptr;
+}
+
} // namespace arith
} // namespace theory
} // namespace cvc5::internal
~TheoryArithPrivate();
//--------------------------------- initialization
- /**
- * Returns true if we need an equality engine, see
- * Theory::needsEqualityEngine.
- */
- bool needsEqualityEngine(EeSetupInfo& esi);
/** finish initialize */
void finishInit();
//--------------------------------- end initialization
/** get the proof checker of this theory */
ArithProofRuleChecker* getProofChecker();
+ /** get the congruence manager, if we are using one */
+ ArithCongruenceManager* getCongruenceManager();
private:
/** The constant zero. */
d_theoryState = &d_astate;
d_inferManager = &d_im;
- if (options().arith.arithEqSolver)
- {
- d_eqSolver.reset(new EqualitySolver(env, d_astate, d_im));
- }
+ // construct the equality solver
+ d_eqSolver.reset(new EqualitySolver(env, d_astate, d_im));
}
TheoryArith::~TheoryArith(){
{
// if the equality solver is enabled, then it is responsible for setting
// up the equality engine
- if (d_eqSolver != nullptr)
- {
- return d_eqSolver->needsEqualityEngine(esi);
- }
- // otherwise, the linear arithmetic solver is responsible for setting up
- // the equality engine
- return d_internal->needsEqualityEngine(esi);
+ return d_eqSolver->needsEqualityEngine(esi);
}
void TheoryArith::finishInit()
{
d_nonlinearExtension.reset(
new nl::NonlinearExtension(d_env, *this, d_astate));
}
- if (d_eqSolver != nullptr)
- {
- d_eqSolver->finishInit();
- }
+ d_eqSolver->finishInit();
// finish initialize in the old linear solver
d_internal->finishInit();
+
+ // Set the congruence manager on the equality solver. If the congruence
+ // manager exists, it is responsible for managing the notifications from
+ // the equality engine, which the equality solver forwards to it.
+ d_eqSolver->setCongruenceManager(d_internal->getCongruenceManager());
}
void TheoryArith::preRegisterTerm(TNode n)
// We do not assert to the equality engine of arithmetic in the standard way,
// hence we return "true" to indicate we are finished with this fact.
bool ret = true;
- if (d_eqSolver != nullptr)
+ if (options().arith.arithEqSolver)
{
// the equality solver may indicate ret = false, after which the assertion
// will be asserted to the equality engine in the default way.
TrustNode TheoryArith::explain(TNode n)
{
- if (d_eqSolver != nullptr)
+ if (options().arith.arithEqSolver)
{
// if the equality solver has an explanation for it, use it
TrustNode texp = d_eqSolver->explain(n);
projects / cvc5.git / commitdiff