From b7ecb57e7240844886759c0f483b67319a80bb40 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Thu, 13 Nov 2025 16:39:00 +0100 Subject: [PATCH 1/3] Allowed retrieving internal terms from PartitionManager and also single terms --- src/api/PartitionManager.cc | 22 ++++++++++++++ src/api/PartitionManager.h | 6 ++++ src/cnfizers/TermMapper.h | 1 + src/common/FlaPartitionMap.cc | 48 ++++++++++++++++++++---------- src/common/FlaPartitionMap.h | 56 +++++++++++++++++++++++++++++------ src/common/PartitionInfo.cc | 2 +- src/common/PartitionInfo.h | 5 +++- 7 files changed, 114 insertions(+), 26 deletions(-) diff --git a/src/api/PartitionManager.cc b/src/api/PartitionManager.cc index 2d7e43e70..6d1958a69 100644 --- a/src/api/PartitionManager.cc +++ b/src/api/PartitionManager.cc @@ -90,6 +90,28 @@ vec PartitionManager::getPartitions(ipartitions_t const & mask) const { return res; } +PTRef PartitionManager::getPartition(int partitionIndex) const { + if (partitionIndex < 0) { return PTRef_Undef; } + return partitionInfo.getTopLevelFormula(static_cast(partitionIndex)); +} + +PTRef PartitionManager::getPartitionForInternal(PTRef term) const { + // we ignore if the term is actually top-level .. + int const partitionIndex = getPartitionIndex(term); + return getPartition(partitionIndex); +} + +PTRef PartitionManager::getInternalPartition(int partitionIndex) const { + if (partitionIndex < 0) { return PTRef_Undef; } + return partitionInfo.getInternalFormula(static_cast(partitionIndex)); +} + +PTRef PartitionManager::getInternalPartitionFor(PTRef term) const { + // we ignore if the term is actually internal .. + int const partitionIndex = getPartitionIndex(term); + return getInternalPartition(partitionIndex); +} + void PartitionManager::addClauseClassMask(CRef c, ipartitions_t const & toadd) { partitionInfo.addClausePartition(c, toadd); } diff --git a/src/api/PartitionManager.h b/src/api/PartitionManager.h index bd62e7a67..9c2bb345b 100644 --- a/src/api/PartitionManager.h +++ b/src/api/PartitionManager.h @@ -49,11 +49,17 @@ class PartitionManager { void invalidatePartitions(ipartitions_t const & toinvalidate); inline std::vector getPartitions() const { return partitionInfo.getTopLevelFormulas(); } + inline std::vector getInternalPartitions() const { return partitionInfo.getInternalFormulas(); } vec getPartitions(ipartitions_t const &) const; unsigned getNofPartitions() const { return partitionInfo.getNoOfPartitions(); } + PTRef getPartition(int partitionIndex) const; + PTRef getPartitionForInternal(PTRef) const; + PTRef getInternalPartition(int partitionIndex) const; + PTRef getInternalPartitionFor(PTRef) const; + void transferPartitionMembership(PTRef old, PTRef new_ptref) { if (new_ptref == old) { return; } this->addIPartitions(new_ptref, getIPartitions(old)); diff --git a/src/cnfizers/TermMapper.h b/src/cnfizers/TermMapper.h index 6d21d7ef5..e5d69a219 100644 --- a/src/cnfizers/TermMapper.h +++ b/src/cnfizers/TermMapper.h @@ -51,6 +51,7 @@ class TermMapper { // Returns the literal corresponding to the term. The connection must already exist. Lit getLit(PTRef) const; // Test if the given term already has an assigned SAT variable + // Only *internal* terms that were given to the SMT solver are tracked, not necessarily top-level formulas! bool hasLit(PTRef tr) const { Var v = var_Undef; peekVar(toPositive(tr), v); diff --git a/src/common/FlaPartitionMap.cc b/src/common/FlaPartitionMap.cc index 8d24f8645..a79045abf 100644 --- a/src/common/FlaPartitionMap.cc +++ b/src/common/FlaPartitionMap.cc @@ -1,34 +1,52 @@ -// -// Created by Martin Blicha on 06.10.18. -// +/* + * Copyright (c) 2018, Martin Blicha + * 2025, Tomas Kolarik + * + * SPDX-License-Identifier: MIT + * + */ #include "FlaPartitionMap.h" namespace opensmt { -std::vector FlaPartitionMap::get_top_level_flas() const { +std::vector FlaPartitionMap::getTopLevelFlas() const { std::vector res; - res.reserve(top_level_flas.size()); - for (auto entry : top_level_flas) { + res.reserve(topLevelFlaToIdxMap.size()); + for (auto entry : topLevelFlaToIdxMap) { + res.push_back(entry.first); + } + return res; +} + +std::vector FlaPartitionMap::getInternalFlas() const { + std::vector res; + res.reserve(topLevelFlaToIdxMap.size()); + for (auto entry : topLevelFlaToIdxMap) { res.push_back(entry.first); } return res; } void FlaPartitionMap::transferPartitionMembership(PTRef old, PTRef new_ptref) { - auto it = top_level_flas.find(old); - if (it != top_level_flas.end()) { - store_other_fla_index(new_ptref, it->second); + if (auto it = internalFlaToIdxMap.find(old); it != internalFlaToIdxMap.end()) { + storeInternalFlaIndex(new_ptref, it->second); + internalFlaToIdxMap.erase(it); + assert(internalIdxToFlaMap.contains(it->second) and internalIdxToFlaMap.at(it->second) == new_ptref); return; } - auto other_it = other_flas.find(old); - if (other_it != other_flas.end()) { store_other_fla_index(new_ptref, other_it->second); } + + if (auto it = topLevelFlaToIdxMap.find(old); it != topLevelFlaToIdxMap.end()) { + storeInternalFlaIndex(new_ptref, it->second); + } } int FlaPartitionMap::getPartitionIndex(PTRef ref) const { - auto it = top_level_flas.find(ref); - if (it != top_level_flas.end()) { return static_cast(it->second); } - auto other_it = other_flas.find(ref); - if (other_it != other_flas.end()) { return static_cast(other_it->second); } + if (auto it = topLevelFlaToIdxMap.find(ref); it != topLevelFlaToIdxMap.end()) { + return static_cast(it->second); + } + if (auto it = internalFlaToIdxMap.find(ref); it != internalFlaToIdxMap.end()) { + return static_cast(it->second); + } return -1; } } // namespace opensmt diff --git a/src/common/FlaPartitionMap.h b/src/common/FlaPartitionMap.h index 9c9fa61f5..f33ba0876 100644 --- a/src/common/FlaPartitionMap.h +++ b/src/common/FlaPartitionMap.h @@ -1,29 +1,67 @@ -// -// Created by Martin Blicha on 06.10.18. -// +/* + * Copyright (c) 2018, Martin Blicha + * 2025, Tomas Kolarik + * + * SPDX-License-Identifier: MIT + * + */ #ifndef OPENSMT_FLAPARTITIONMAP_H #define OPENSMT_FLAPARTITIONMAP_H #include +#include #include +#include #include namespace opensmt { class FlaPartitionMap { public: - void store_top_level_fla_index(PTRef fla, unsigned int idx) { top_level_flas[fla] = idx; } - void store_other_fla_index(PTRef fla, unsigned int idx) { other_flas[fla] = idx; } - std::vector get_top_level_flas() const; - unsigned getNoOfPartitions() const { return get_top_level_flas().size(); } + inline void storeTopLevelFlaIndex(PTRef fla, unsigned int idx); + inline void storeInternalFlaIndex(PTRef fla, unsigned int idx); + std::vector getTopLevelFlas() const; + std::vector getInternalFlas() const; + inline PTRef getTopLevelFla(unsigned int idx) const noexcept; + inline PTRef getInternalFla(unsigned int idx) const noexcept; + inline unsigned getNoOfPartitions() const; void transferPartitionMembership(PTRef old, PTRef new_ptref); int getPartitionIndex(PTRef ref) const; private: - std::map top_level_flas; - std::map other_flas; + std::map topLevelFlaToIdxMap; + std::map internalFlaToIdxMap; + std::unordered_map topLevelIdxToFlaMap; + std::unordered_map internalIdxToFlaMap; }; + +void FlaPartitionMap::storeTopLevelFlaIndex(PTRef fla, unsigned int idx) { + topLevelFlaToIdxMap[fla] = idx; + topLevelIdxToFlaMap[idx] = fla; +} + +void FlaPartitionMap::storeInternalFlaIndex(PTRef fla, unsigned int idx) { + internalFlaToIdxMap[fla] = idx; + internalIdxToFlaMap[idx] = fla; +} + +PTRef FlaPartitionMap::getTopLevelFla(unsigned int idx) const noexcept { + if (auto it = topLevelIdxToFlaMap.find(idx); it != topLevelIdxToFlaMap.end()) { return it->second; } + return PTRef_Undef; +} + +PTRef FlaPartitionMap::getInternalFla(unsigned int idx) const noexcept { + if (auto it = internalIdxToFlaMap.find(idx); it != internalIdxToFlaMap.end()) { return it->second; } + return PTRef_Undef; +} + +unsigned FlaPartitionMap::getNoOfPartitions() const { + assert(getTopLevelFlas().size() == topLevelFlaToIdxMap.size()); + assert(topLevelFlaToIdxMap.size() <= topLevelIdxToFlaMap.size()); + return topLevelFlaToIdxMap.size(); +} + } // namespace opensmt #endif // OPENSMT_FLAPARTITIONMAP_H diff --git a/src/common/PartitionInfo.cc b/src/common/PartitionInfo.cc index 2cd6bccb7..c7b236b9a 100644 --- a/src/common/PartitionInfo.cc +++ b/src/common/PartitionInfo.cc @@ -6,7 +6,7 @@ namespace opensmt { void PartitionInfo::assignTopLevelPartitionIndex(unsigned int n, PTRef tr) { - flaPartitionMap.store_top_level_fla_index(tr, n); + flaPartitionMap.storeTopLevelFlaIndex(tr, n); ipartitions_t p = 0; setbit(p, n); addIPartitions(tr, p); diff --git a/src/common/PartitionInfo.h b/src/common/PartitionInfo.h index 18906d722..3d2bc395a 100644 --- a/src/common/PartitionInfo.h +++ b/src/common/PartitionInfo.h @@ -28,7 +28,10 @@ class PartitionInfo { ipartitions_t const & getClausePartitions(CRef) const; void addClausePartition(CRef c, ipartitions_t const & p); - inline std::vector getTopLevelFormulas() const { return flaPartitionMap.get_top_level_flas(); } + inline std::vector getTopLevelFormulas() const { return flaPartitionMap.getTopLevelFlas(); } + inline std::vector getInternalFormulas() const { return flaPartitionMap.getInternalFlas(); } + inline PTRef getTopLevelFormula(unsigned int idx) const { return flaPartitionMap.getTopLevelFla(idx); } + inline PTRef getInternalFormula(unsigned int idx) const { return flaPartitionMap.getInternalFla(idx); } inline unsigned int getNoOfPartitions() const { return flaPartitionMap.getNoOfPartitions(); } inline void transferPartitionMembership(PTRef o, PTRef n) { return flaPartitionMap.transferPartitionMembership(o, n); From 04db7ab08f5cdc161ce63f9a9f43ee92d61625d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Thu, 13 Nov 2025 16:49:05 +0100 Subject: [PATCH 2/3] [[WIP]] --- src/api/MainSolver.cc | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 781602091..210bdbb41 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -289,6 +289,11 @@ std::unique_ptr MainSolver::getUnsatCore() const { lbool MainSolver::getTermValue(PTRef tr) const { if (logic.getSortRef(tr) != logic.getSort_bool()) { return l_Undef; } + + assert(trackPartitions()); + if (PTRef new_tr = pmanager.getInternalPartitionFor(tr); new_tr != PTRef_Undef) { + tr = new_tr; + } if (not term_mapper->hasLit(tr)) { return l_Undef; } Lit l = term_mapper->getLit(tr); From 8a48cc7c7394326924304fff51188903cb7efae3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Thu, 13 Nov 2025 16:49:58 +0100 Subject: [PATCH 3/3] [[stash]] --- src/api/MainSolver.cc | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 210bdbb41..2a476f69f 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -117,6 +117,7 @@ void MainSolver::insertFormula(PTRef fla) { // easily unsigned int partition_index = insertedFormulasCount++; pmanager.assignTopLevelPartitionIndex(partition_index, fla); + std::cerr << logic.termToSMT2String(fla) << " [" << fla.x << "] : " << pmanager.getPartitionIndex(fla) << std::endl; assert(pmanager.getPartitionIndex(fla) != -1); } else { ++insertedFormulasCount; @@ -148,7 +149,10 @@ sstat MainSolver::simplifyFormulas() { vec frameFormulas; for (PTRef fla : frames[i].formulas) { PTRef processed = theory->preprocessAfterSubstitutions(fla, context); + std::cerr << logic.termToSMT2String(fla) << " [" << fla.x << "] -> " << logic.termToSMT2String(processed) << " [" << processed.x << "]" << std::endl; pmanager.transferPartitionMembership(fla, processed); + std::cerr << logic.termToSMT2String(fla) << " [" << fla.x << "] : " << pmanager.getPartitionIndex(fla) << std::endl; + std::cerr << logic.termToSMT2String(processed) << " [" << processed.x << "] : " << pmanager.getPartitionIndex(processed) << std::endl; frameFormulas.push(processed); preprocessor.addPreprocessedFormula(processed); } @@ -158,6 +162,7 @@ sstat MainSolver::simplifyFormulas() { } theory->afterPreprocessing(preprocessor.getPreprocessedFormulas()); for (PTRef fla : frameFormulas) { + std::cerr << ">> " << logic.termToSMT2String(fla) << " [" << fla.x << "] : " << pmanager.getPartitionIndex(fla) << std::endl; if (fla == logic.getTerm_true()) { continue; } assert(pmanager.getPartitionIndex(fla) != -1); // Optimize the dag for cnfization @@ -168,6 +173,7 @@ sstat MainSolver::simplifyFormulas() { } assert(pmanager.getPartitionIndex(fla) != -1); pmanager.propagatePartitionMask(fla); + std::cerr << ">>> " << logic.termToSMT2String(fla) << " [" << fla.x << "] : " << pmanager.getPartitionIndex(fla) << std::endl; status = giveToSolver(fla, frames[i].getId()); if (status == s_False) { break; } } @@ -291,9 +297,13 @@ lbool MainSolver::getTermValue(PTRef tr) const { if (logic.getSortRef(tr) != logic.getSort_bool()) { return l_Undef; } assert(trackPartitions()); + std::cerr << logic.termToSMT2String(tr) << " [" << tr.x << "]" << std::endl; + assert(pmanager.getPartitionIndex(tr) != -1); if (PTRef new_tr = pmanager.getInternalPartitionFor(tr); new_tr != PTRef_Undef) { tr = new_tr; + std::cerr << "-> " << logic.termToSMT2String(tr) << " [" << tr.x << "]" << std::endl; } + assert(term_mapper->hasLit(tr)); if (not term_mapper->hasLit(tr)) { return l_Undef; } Lit l = term_mapper->getLit(tr); @@ -318,11 +328,26 @@ sstat MainSolver::giveToSolver(PTRef root, FrameId push_id) { void operator()(vec && c) override { clauses.push_back(std::move(c)); } }; ClauseCallBack callBack; + std::cerr << "adding " << logic.termToSMT2String(root) << " [" << root.x << "] : " << pmanager.getPartitionIndex(root) << std::endl; ts.setClauseCallBack(&callBack); ts.Cnfizer::cnfize(root, push_id); bool const keepPartitionsSeparate = trackPartitions(); Lit frameLit = push_id == 0 ? Lit{} : term_mapper->getOrCreateLit(frameTerms[push_id]); - int partitionIndex = keepPartitionsSeparate ? pmanager.getPartitionIndex(root) : -1; + int partitionIndex; + if (keepPartitionsSeparate) { + partitionIndex = pmanager.getPartitionIndex(root); + PTRef topLevelFla = pmanager.getPartitionForInternal(root); + assert(topLevelFla != PTRef_Undef); + if (termNames.contains(topLevelFla) and not term_mapper->hasLit(root)) { + PTRef varTerm = logic.mkBoolVar(".eq" + std::to_string(root.x)); + PTRef eq = logic.mkEq(varTerm, root); + Lit l = term_mapper->getOrCreateLit(root); + smt_solver->addVar(var(l)); + term_mapper->setFrozen(var(l)); + } + } else { + partitionIndex = -1; + } for (auto & clause : callBack.clauses) { if (push_id != 0) { clause.push(frameLit); } pair iorefs{CRef_Undef, CRef_Undef};