Fixed TermNames to also consider mapping of internal terms to original user terms

Author: Tomaqa

src/api/MainSolver.cc

@@ -9,6 +9,7 @@
 #include "MainSolver.h"
 
 #include <common/ApiException.h>
+#include <common/InternalToUserTermMap.h>
 #include <itehandler/IteHandler.h>
 #include <logics/ArrayTheory.h>
 #include <logics/LATheory.h>
@@ -30,7 +31,7 @@ MainSolver::MainSolver(Logic & logic, SMTConfig & conf, std::string name)
       term_mapper(new TermMapper(logic)),
       thandler(new THandler(getTheory(), *term_mapper)),
       smt_solver(createInnerSolver(conf, *thandler)),
-      termNames(conf),
+      termNames(conf, internalToUserTermMap),
       logic(thandler->getLogic()),
       pmanager(logic),
       config(conf),
@@ -46,7 +47,7 @@ MainSolver::MainSolver(std::unique_ptr<Theory> th, std::unique_ptr<TermMapper> t
       term_mapper(std::move(tm)),
       thandler(std::move(thd)),
       smt_solver(std::move(ss)),
-      termNames(conf),
+      termNames(conf, internalToUserTermMap),
       logic(thandler->getLogic()),
       pmanager(logic),
       config(conf),
@@ -108,7 +109,11 @@ void MainSolver::insertFormula(PTRef fla) {
         throw ApiException("Top-level assertion sort must be Bool, got " + logic.printSort(logic.getSortRef(fla)));
     }
     // TODO: Move this to preprocessing of the formulas
-    fla = IteHandler(logic, getPartitionManager().getNofPartitions()).rewrite(fla);
+    {
+        PTRef newFla = IteHandler(logic, getPartitionManager().getNofPartitions()).rewrite(fla);
+        internalToUserTermMap.maybeAddMapping(newFla, fla);
+        fla = newFla;
+    }
 
     if (trackPartitions()) {
         // MB: Important for HiFrog! partition index is the index of the formula in an virtual array of inserted

src/api/MainSolver.h

@@ -23,6 +23,7 @@
 
 namespace opensmt {
 class Logic;
+class InternalToUserTermMap;
 
 class sstat {
 public:
@@ -139,7 +140,7 @@ class MainSolver {
     // Returns interpolation context for the last query (must be in UNSAT state)
     std::unique_ptr<InterpolationContext> getInterpolationContext();
 
-    [[deprecated("Use tryAddNamedAssertion or tryAddTermName")]]
+    [[deprecated("Use tryAddNamedAssertion or tryAddTermNameFor")]]
     TermNames & getTermNames() {
         return termNames;
     }
@@ -310,6 +311,7 @@ class MainSolver {
     std::unique_ptr<TermMapper> term_mapper;
     std::unique_ptr<THandler> thandler;
     std::unique_ptr<SimpSMTSolver> smt_solver;
+    InternalToUserTermMap internalToUserTermMap;
     TermNames termNames;
     Logic & logic;
     PartitionManager pmanager;

src/common/CMakeLists.txt

@@ -7,16 +7,17 @@ PUBLIC
     "${CMAKE_CURRENT_LIST_DIR}/Partitions.h"
     "${CMAKE_CURRENT_LIST_DIR}/TermNames.h"
 PRIVATE
-    "${CMAKE_CURRENT_LIST_DIR}/SystemQueries.h"
     "${CMAKE_CURRENT_LIST_DIR}/inttypes.h"
+    "${CMAKE_CURRENT_LIST_DIR}/InternalToUserTermMap.h"
+    "${CMAKE_CURRENT_LIST_DIR}/NatSet.h"
+    "${CMAKE_CURRENT_LIST_DIR}/PartitionInfo.cc"
+    "${CMAKE_CURRENT_LIST_DIR}/ReportUtils.h"
     "${CMAKE_CURRENT_LIST_DIR}/StringMap.h"
     "${CMAKE_CURRENT_LIST_DIR}/StringConv.h"
+    "${CMAKE_CURRENT_LIST_DIR}/SystemQueries.h"
     "${CMAKE_CURRENT_LIST_DIR}/Timer.h"
     "${CMAKE_CURRENT_LIST_DIR}/TreeOps.h"
-    "${CMAKE_CURRENT_LIST_DIR}/NatSet.h"
-    "${CMAKE_CURRENT_LIST_DIR}/PartitionInfo.cc"
     "${CMAKE_CURRENT_LIST_DIR}/VerificationUtils.cc"
-    "${CMAKE_CURRENT_LIST_DIR}/ReportUtils.h"
     "${CMAKE_CURRENT_LIST_DIR}/polynomials/Translations.cc"
 )
 
@@ -25,5 +26,5 @@ include(numbers/CMakeLists.txt)
 install(FILES
         StringMap.h Timer.h inttypes.h IColor.h
         TreeOps.h FlaPartitionMap.h PartitionInfo.h Partitions.h ApiException.h TypeUtils.h
-        NatSet.h ScopedVector.h TermNames.h
+        NatSet.h ScopedVector.h TermNames.h InternalToUserTermMap.h
 DESTINATION ${INSTALL_HEADERS_DIR}/common)

src/common/InternalToUserTermMap.h

@@ -0,0 +1,32 @@
+#ifndef OPENSMT_USERTERMMAP_H
+#define OPENSMT_USERTERMMAP_H
+
+#include <pterms/PTRef.h>
+
+#include <unordered_map>
+
+namespace opensmt {
+class InternalToUserTermMap {
+public:
+    bool maybeAddMapping(PTRef newTerm, PTRef userTerm) {
+        if (newTerm == userTerm) { return false; }
+
+        // overwrite any previous mappings
+        map.insert_or_assign(newTerm, userTerm);
+        return true;
+    }
+
+    PTRef getUserTerm(PTRef term) const {
+        auto it = map.find(term);
+        if (it == map.end()) { return term; }
+
+        assert(it->first.x == term.x);
+        return it->second;
+    }
+
+private:
+    std::unordered_map<PTRef, PTRef, PTRefHash> map;
+};
+} // namespace opensmt
+
+#endif // OPENSMT_USERTERMMAP_H

src/common/TermNames.h

@@ -1,6 +1,7 @@
 #ifndef OPENSMT_TERMNAMES_H
 #define OPENSMT_TERMNAMES_H
 
+#include "InternalToUserTermMap.h"
 #include "ScopedVector.h"
 #include "TypeUtils.h"
 
@@ -19,12 +20,15 @@ using TermName = std::string;
 
 class TermNames {
 public:
-    TermNames(SMTConfig const & conf) : config{conf} {}
+    TermNames(SMTConfig const & conf, InternalToUserTermMap const & map) : config{conf}, internalToUserTermMap{map} {}
 
     bool isGlobal() const { return config.declarations_are_global(); }
 
     bool contains(TermName const & name) const { return nameToTerm.contains(name); }
-    bool contains(PTRef term) const { return termToNames.contains(term); }
+    bool contains(PTRef term) const {
+        term = internalToUserTermMap.getUserTerm(term);
+        return termToNames.contains(term);
+    }
 
     [[deprecated("Use tryInsert")]]
     void insert(TermName const & name, PTRef term) {
@@ -48,6 +52,8 @@ class TermNames {
     }
 
     std::vector<TermName> const & namesForTerm(PTRef term) const {
+        assert(contains(term));
+        term = internalToUserTermMap.getUserTerm(term);
         assert(contains(term));
         return termToNames.at(term);
     }
@@ -72,6 +78,7 @@ class TermNames {
 
     // std::optional does not work with references so we must use pointers
     std::vector<TermName> const * tryGetNamesForTerm(PTRef term) const {
+        term = internalToUserTermMap.getUserTerm(term);
         if (auto it = termToNames.find(term); it != termToNames.end()) { return &it->second; }
 
         return nullptr;
@@ -121,16 +128,26 @@ class TermNames {
         if (isGlobal()) { return; }
         scopedNamesAndTerms.popScope([this](auto const & p) {
             auto const & [name, term] = p;
-            auto it = nameToTerm.find(name);
-            if (it == nameToTerm.end()) { return; }
-            auto & names_ = _namesForTerm(term);
-            names_.erase(std::find(names_.begin(), names_.end(), name));
-            nameToTerm.erase(it);
+            assert(not contains(term) or nameToTerm.find(name)->second.x == term.x);
+            eraseTermName(name);
         });
     }
 
+    bool eraseTermName(TermName const & name) {
+        auto termIt = nameToTerm.find(name);
+        if (termIt == nameToTerm.end()) { return false; }
+
+        auto const & term = termIt->second;
+        auto & names_ = _namesForTerm(term);
+        names_.erase(std::find(names_.begin(), names_.end(), name));
+        nameToTerm.erase(termIt);
+        return true;
+    }
+
     SMTConfig const & config;
 
+    InternalToUserTermMap const & internalToUserTermMap;
+
     ScopedNamesAndTerms scopedNamesAndTerms;
     NameToTermMap nameToTerm;
     TermToNamesMap termToNames;