Egraph: Avoid unnecessary mkNot calls

This is just a tiny optimization to avoid some calls to Logic::mkNot.
Instead of storing information for the negated terms, we can store the
same information for the positive term and then we do not need to lookup
the negated term first.

src/tsolvers/egraph/Egraph.h

@@ -182,7 +182,7 @@ class Egraph : public TSolver {
     bool childDuplicatesClass(ERef parent, uint32_t childIndex);
 
     //***************************************************************************************************************
-    Map<PTRef, ERef, PTRefHash> negatedTermToERef;
+    Map<PTRef, ERef, PTRefHash> termToNegatedERef;
 
     ELAllocator forbid_allocator;
 

src/tsolvers/egraph/EgraphSolver.cc

@@ -270,7 +270,7 @@ void Egraph::declareTerm(PTRef tr) {
     if (logic.hasSortBool(tr) and not logic.isDisequality(tr) and PTRefERefPairVec.size() == 2) {
         auto [negated_tr, negated_er] = PTRefERefPairVec[1];
         assert(logic.isNot(negated_tr));
-        negatedTermToERef.insert(negated_tr, negated_er);
+        termToNegatedERef.insert(tr, negated_er);
         assert(PTRefERefPairVec[0].tr == logic.mkNot(PTRefERefPairVec[1].tr));
         assertNEq(PTRefERefPairVec[0].er, PTRefERefPairVec[1].er, Expl(Expl::Type::pol, PtAsgn_Undef, PTRefERefPairVec[0].tr));
     }
@@ -349,8 +349,8 @@ bool Egraph::addTrue(PTRef term) {
     assert(logic.hasSortBool(term));
     assert(not logic.isNot(term));
     bool res = assertEq(term, logic.getTerm_true(), PtAsgn(term, l_True));
-    if (res and negatedTermToERef.has(logic.mkNot(term))) {
-        res = assertEq(logic.mkNot(term), logic.getTerm_false(), PtAsgn(term, l_True));
+    if (res and termToNegatedERef.has(term)) {
+        res = assertEq(termToNegatedERef[term], termToERef(logic.getTerm_false()), PtAsgn(term, l_True));
     }
 #ifdef STATISTICS
     if (res == false)
@@ -366,8 +366,8 @@ bool Egraph::addFalse(PTRef term) {
     assert(logic.hasSortBool(term));
     assert(not logic.isNot(term));
     bool res = assertEq(term, logic.getTerm_false(), PtAsgn(term, l_False));
-    if (res and negatedTermToERef.has(logic.mkNot(term))) {
-        res = assertEq(logic.mkNot(term), logic.getTerm_true(), PtAsgn(term, l_False));
+    if (res and termToNegatedERef.has(term)) {
+        res = assertEq(termToNegatedERef[term], termToERef(logic.getTerm_true()), PtAsgn(term, l_False));
     }
 #ifdef STATISTICS
     if (res == false)