Skip to content

Commit

Permalink
don't show projection variables
Browse files Browse the repository at this point in the history
  • Loading branch information
arijitsh committed Nov 29, 2024
1 parent 9e3a210 commit 6ba1172
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions lib/ToSat/ToCNFAIG.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -155,9 +156,9 @@ void ToCNFAIG::fill_node_to_var(Cnf_Dat_t* cnfData,
const vector<BBNodeAIG>& 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.
Expand All @@ -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

0 comments on commit 6ba1172

Please sign in to comment.