From 6ba1172155a93eea0d5d3796c31d3b74de7378d4 Mon Sep 17 00:00:00 2001 From: Arijit Shaw Date: Fri, 29 Nov 2024 18:24:34 -0500 Subject: [PATCH 1/2] don't show projection variables --- lib/ToSat/ToCNFAIG.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/lib/ToSat/ToCNFAIG.cpp b/lib/ToSat/ToCNFAIG.cpp index ba512068..1bc2d4f2 100644 --- a/lib/ToSat/ToCNFAIG.cpp +++ b/lib/ToSat/ToCNFAIG.cpp @@ -146,6 +146,7 @@ void ToCNFAIG::fill_node_to_var(Cnf_Dat_t* cnfData, { BBNodeManagerAIG::SymbolToBBNode::const_iterator it; assert(nodeToVars.size() == 0); + uint32_t proj_var_num = 0, non_proj_var_num = 0; // todo. cf. with addvariables above... // Each symbol maps to a vector of CNF variables. @@ -155,9 +156,9 @@ void ToCNFAIG::fill_node_to_var(Cnf_Dat_t* cnfData, const vector& b = it->second; assert(nodeToVars.find(n) == nodeToVars.end()); if (bm->isProjSymbol(n)) - std::cout << "proj symbol" << n.GetName() << std::endl; + proj_var_num++; else - std::cout << "not proj symbol" << n.GetName() << std::endl; + non_proj_var_num++; const int width = (n.GetType() == BOOLEAN_TYPE) ? 1 : n.GetValueWidth(); // INT_MAX for parts of symbols that didn't get encoded. @@ -181,5 +182,7 @@ void ToCNFAIG::fill_node_to_var(Cnf_Dat_t* cnfData, nodeToVars.insert(make_pair(n, v)); } + std::cout << "c Projection variables: " << proj_var_num + << " Other variables: " << non_proj_var_num << std::endl; } } // namespace stp From fe4289809cd938baec36b05c40c7cdaf5ede251f Mon Sep 17 00:00:00 2001 From: Arijit Shaw Date: Fri, 29 Nov 2024 18:57:18 -0500 Subject: [PATCH 2/2] if no projvar declared, move to non-projection mode --- include/stp/STPManager/STPManager.h | 8 ++++++++ lib/ToSat/ToCNFAIG.cpp | 6 ++++++ 2 files changed, 14 insertions(+) diff --git a/include/stp/STPManager/STPManager.h b/include/stp/STPManager/STPManager.h index 67d71af6..65625088 100644 --- a/include/stp/STPManager/STPManager.h +++ b/include/stp/STPManager/STPManager.h @@ -402,9 +402,17 @@ class STPMgr bool isProjSymbol(ASTNode& s) { + if (_proj_symbol_list.size() == 0) + return true; return _proj_symbol_list.find(s) != _proj_symbol_list.end(); } + bool isAnyProjSymbolDeclared() + { + if (_proj_symbol_list.size() == 0) + return false; + return true; + } bool FoundIntroducedSymbolSet(const ASTNode& in) { diff --git a/lib/ToSat/ToCNFAIG.cpp b/lib/ToSat/ToCNFAIG.cpp index 1bc2d4f2..83a71920 100644 --- a/lib/ToSat/ToCNFAIG.cpp +++ b/lib/ToSat/ToCNFAIG.cpp @@ -182,6 +182,12 @@ void ToCNFAIG::fill_node_to_var(Cnf_Dat_t* cnfData, nodeToVars.insert(make_pair(n, v)); } + if (!bm->isAnyProjSymbolDeclared()) + { + std::cout << "c No variables declared as projection var, moving to " + "non-projection mode" + << std::endl; + } std::cout << "c Projection variables: " << proj_var_num << " Other variables: " << non_proj_var_num << std::endl; }