Improved bookkeeping on UF appearances of boolean terms (#189)

* Do not mark PTRefs as declared to EnodeStore if not actually declaerd

* Keep count on Boolean terms appearing in the UF terms

* Cleaning commented prints

* Added regression tests

* Implemented correct handling of conflicts when egraph reasoning results in p and (not p) being in the same eq class.

* Do not distinguish between UF appearances of negated and pure literals

* Made uf appearance tracking into ternary: unseen, removed, or appearing

Co-authored-by: Martin Blicha <blichm@usi.ch>

regression/QF_UF/issue185c.smt2

@@ -0,0 +1,14 @@
+(set-logic QF_UF)
+(declare-fun uf7 (Bool Bool Bool Bool Bool Bool Bool) Bool)
+(declare-fun v0 () Bool)
+(declare-fun v2 () Bool)
+(declare-fun v7 () Bool)
+(declare-fun v11 () Bool)
+(declare-fun v13 () Bool)
+(declare-fun v16 () Bool)
+(declare-fun v17 () Bool)
+(declare-fun v19 () Bool)
+(assert (uf7 v2 v19 (= v11 (not v17)) v13 (=> v16 v0) v7 v17))
+(check-sat)
+(assert v16)
+(check-sat)

regression/QF_UF/issue185c.smt2.expected.out

@@ -0,0 +1,2 @@
+sat
+sat

regression/QF_UF/issue188.smt2

@@ -0,0 +1,33 @@
+(set-logic QF_UF)
+(declare-fun uf3 (Bool Bool Bool) Bool)
+(declare-fun v0 () Bool)
+(declare-fun v1 () Bool)
+(declare-fun v2 () Bool)
+(declare-fun v3 () Bool)
+(declare-fun v4 () Bool)
+(declare-fun v5 () Bool)
+(push 1)
+(declare-fun v6 () Bool)
+(declare-fun v7 () Bool)
+(push 1)
+(declare-fun v8 () Bool)
+(assert v0)
+(push 1)
+(declare-sort S0 0)
+(declare-fun v9 () Bool)
+(declare-fun v10 () Bool)
+(declare-fun v11 () Bool)
+(assert v6)
+(assert (distinct v10 (not v3)))
+(assert (uf3 v8 (not v3) (distinct v10 (not v3))))
+(declare-fun S0-0 () S0)
+(push 1)
+(push 1)
+(assert (not v7))
+(check-sat)
+(declare-sort S1 0)
+(declare-fun v12 () Bool)
+(assert (=> v1 v7))
+(assert (uf3 v11 v2 v10))
+(assert (not (not v3)))
+(check-sat)

regression/QF_UF/issue188.smt2.expected.out

@@ -0,0 +1,2 @@
+sat
+sat

regression/QF_UF/issue190.smt2

@@ -0,0 +1,23 @@
+(set-logic QF_UF)
+(declare-fun uf3 (Bool) Bool)
+(declare-fun uf7 (Bool Bool Bool Bool) Bool)
+(declare-fun v0 () Bool)
+(declare-fun v1 () Bool)
+(declare-fun v2 () Bool)
+(declare-fun v3 () Bool)
+(declare-fun v4 () Bool)
+(declare-fun v5 () Bool)
+(declare-fun v6 () Bool)
+(declare-fun v7 () Bool)
+(assert (= v6 v1))
+(push 1)
+(assert
+ (uf7 true
+      (uf7 v3 v5 v4 v5)
+      (or v3 (= (not v5) (uf3 v7)))
+      (= (not v5) (uf3 v7))
+ )
+)
+(check-sat)
+(pop 1)
+(check-sat)

regression/QF_UF/issue190.smt2.expected.out

@@ -0,0 +1,2 @@
+sat
+sat

regression/QF_UF/issue190b.smt2

@@ -0,0 +1,34 @@
+(set-logic QF_UF)
+(declare-fun uf4 (Bool Bool Bool Bool) Bool)
+(declare-fun uf7 (Bool Bool Bool Bool Bool Bool Bool) Bool)
+(declare-fun v3 () Bool)
+(declare-fun v8 () Bool)
+(declare-fun v11 () Bool)
+(declare-fun v17 () Bool)
+(check-sat)
+(check-sat)
+(assert (uf7 (=> v3 v11) true true true true v8 true))
+(push 1)
+(declare-sort S2 0)
+(declare-sort S3 0)
+(assert (= v3 v17))
+(declare-sort S4 0)
+(push 1)
+(assert false)
+(check-sat)
+(pop 1)
+(check-sat)
+(check-sat)
+(pop 1)
+(push 1)
+(declare-sort S2 0)
+(assert (uf4 (= (=> v3 v11) (not v8)) true true true))
+(check-sat)
+(declare-sort S2 0)
+(declare-sort S3 0)
+(declare-sort S4 0)
+(declare-sort S2 0)
+(check-sat)
+(pop 1)
+(assert (=> v3 v11))
+(check-sat)

regression/QF_UF/issue190b.smt2.expected.out

@@ -0,0 +1,18 @@
+sat
+sat
+unsat
+sat
+sat
+(error "sort S2 already declared")
+
+sat
+(error "sort S2 already declared")
+
+(error "sort S3 already declared")
+
+(error "sort S4 already declared")
+
+(error "sort S2 already declared")
+
+sat
+sat

src/logics/Logic.cc

@@ -397,22 +397,32 @@ bool Logic::isTheorySymbol(SymRef tr) const {
     return !(isBooleanOperator(tr));
 }
 
+void Logic::unsetAppearsInUF(PTRef tr) {
+    tr = isNot(tr) ? getPterm(tr)[0]: tr;
+    uint32_t id = Idx(getPterm(tr).getId());
+    appears_in_uf[id] = UFAppearanceStatus::removed;
+}
+
 void Logic::setAppearsInUF(PTRef tr) {
+    assert(not isNot(tr));
     int id = static_cast<int>(Idx(getPterm(tr).getId()));
-
-    if (appears_in_uf.size() <= id || appears_in_uf[id] == false)
+    if (appears_in_uf.size() <= id || appears_in_uf[id] == UFAppearanceStatus::unseen) {
         propFormulasAppearingInUF.push(tr);
+    }
 
-    while (id >= appears_in_uf.size())
-        appears_in_uf.push(false);
+    while (id >= appears_in_uf.size()) {
+        appears_in_uf.push(UFAppearanceStatus::unseen);
+    }
 
-    appears_in_uf[id] = true;
+    appears_in_uf[id] = UFAppearanceStatus::appears;
 }
 
 bool Logic::appearsInUF(PTRef tr) const {
+    tr = isNot(tr) ? getPterm(tr)[0] : tr;
+
     uint32_t id = Idx(getPterm(tr).getId());
     if (id < static_cast<unsigned int>(appears_in_uf.size()))
-        return appears_in_uf[id];
+        return appears_in_uf[id] == UFAppearanceStatus::appears;
     else
         return false;
 }
@@ -982,8 +992,7 @@ PTRef Logic::mkUninterpFun(SymRef f, const vec<PTRef> & args) {
     if (isUFTerm(tr) || isUP(tr)) {
         for (int i = 0; i < args.size(); i++) {
             if (hasSortBool(args[i])) {
-                setAppearsInUF(args[i]);
-                setAppearsInUF(mkNot(args[i]));
+                setAppearsInUF(isNot(args[i]) ? getPterm(args[i])[0] : args[i]);
             }
         }
     }
@@ -1356,8 +1365,10 @@ bool Logic::varsubstitute(PTRef root, const Map<PTRef, PtAsgn, PTRefHash> & subs
 #ifdef SIMPLIFY_DEBUG
                     printf("  %s -> %s\n", printTerm(t[i]), printTerm(gen_sub[t[i]]));
 #endif
+                    if (hasSub and appearsInUF(t[i]) and isUF(tr)) {
+                        unsetAppearsInUF(t[i]);
+                    }
                 }
-
                 result = changed ? insertTerm(t.symb(), args_mapped) : tr;
 #ifdef SIMPLIFY_DEBUG
                 printf("  -> %s\n", printTerm(result));

src/logics/Logic.h

@@ -164,7 +164,12 @@ class Logic {
     void dumpFunction(ostream &, const TFun&);
 
   private:
-    vec<bool> appears_in_uf;
+    enum class UFAppearanceStatus {
+        unseen, removed, appears
+    };
+    vec<UFAppearanceStatus> appears_in_uf;
+    void unsetAppearsInUF(PTRef tr);
+
   public:
     vec<PTRef> propFormulasAppearingInUF;
     std::size_t getNumberOfTerms() const { return term_store.getNumberOfTerms(); }

src/tsolvers/egraph/Egraph.h

@@ -334,22 +334,24 @@ class Egraph : public TSolver {
     void      declareTerm         (PTRef);
 
 private:
+
     std::unordered_set<PTRef, PTRefHash> declared;
     void declareTermRecursively(PTRef);
 
-    bool    assertEq        ( PTRef, PTRef, PtAsgn );               // Asserts an equality
-    bool    assertEq        ( ERef, ERef, PtAsgn );                 // Called by the above
-    bool    assertNEq       ( PTRef, PTRef, PtAsgn );               // Asserts a negated equality
-    bool    assertNEq       ( ERef, ERef, PtAsgn );                 // Called by the above
-    bool    assertDist      ( PTRef, PtAsgn );                      // Asserts a distinction
+    bool    assertEq        (PTRef, PTRef, PtAsgn);               // Asserts an equality
+    bool    assertEq        (ERef, ERef, PtAsgn);                 // Called by the above
+    bool    assertNEq       (PTRef, PTRef, const Expl &r);        // Asserts a negated equality
+    bool    assertNEq       (ERef, ERef, const Expl &r);          // Called by the above
+    bool    assertDist      ( PTRef, PtAsgn);                     // Asserts a distinction
     //
     // Backtracking
     //
     void    backtrackToStackSize ( size_t );                      // Backtrack to a certain operation
     //
     // Congruence closure main routines
     //
-    bool    unmergeable     ( ERef, ERef, PtAsgn& ) const;        // Can two nodes be merged ?
+
+    bool    unmergeable     ( ERef, ERef, Expl& ) const;        // Can two nodes be merged ?
     void    merge           ( ERef, ERef, PtAsgn );               // Merge two nodes
     bool    mergeLoop       ( PtAsgn reason );                    // Merge loop
     void    deduce          ( ERef, ERef, PtAsgn );               // Deduce from merging of two nodes (record the reason)

src/tsolvers/egraph/EgraphDebug.cc

@@ -314,7 +314,7 @@ const string Egraph::printDistinctionList( ELRef x, ELAllocator& ela, bool detai
               << "| ELRef: " << x.x << endl
               << "| id: " << ela[x].getId() << endl
               << "| dirty: " << ela[x].isDirty() << endl
-              << "| reason: " << (ela[x].reason.sgn == l_True ? "" : "not " ) << logic.printTerm(ela[x].reason.tr) << endl;
+              << "| reason: " << (ela[x].reason.pta.sgn == l_True ? "" : "not " ) << logic.printTerm(ela[x].reason.pta.tr) << endl;
 
             if (ela[x].reloced())
                 os << "| reloced to: " << ela[x].rel_e.x << endl;
@@ -328,7 +328,7 @@ const string Egraph::printDistinctionList( ELRef x, ELAllocator& ela, bool detai
             os << "+-----------------------------------------------------------+" << endl
                << "| Forbid list node                                          |" << endl
                << "+-----------------------------------------------------------+" << endl
-               << "| reason: " << (ela[x].reason.sgn == l_True ? "" : "not " ) << logic.printTerm(ela[x].reason.tr) << endl;
+               << "| reason: " << (ela[x].reason.pta.sgn == l_True ? "" : "not " ) << logic.printTerm(ela[x].reason.pta.tr) << endl;
 
             os << "| different from enode " << ela[x].e.x << endl;
             if (enode_store[ela[x].e].isTerm())