Commit 42eeb0e3 authored by Martin Jonas's avatar Martin Jonas
Browse files

Cache BoundVars by size.

parent d7198af8
......@@ -9,8 +9,10 @@ using namespace z3;
map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e, vector<BoundVar> &boundVars, bool isPositive)
{
auto item = subformulaVariableCounts.find({e, isPositive});
if ((item != subformulaVariableCounts.end() && ((item->second).second) == boundVars))
if ((item != subformulaVariableCounts.end() && ((item->second).second) == boundVars.size()))
{
cacheHits++;
//std::cout << "Cache hit " << cacheHits << std::endl;
if (dagCounting)
{
map<string, int> varCounts;
......@@ -28,7 +30,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
Z3_ast ast = (Z3_ast)e;
int deBruijnIndex = Z3_get_index_value(*context, ast);
varCounts[std::get<0>(boundVars[boundVars.size() - deBruijnIndex - 1])] = 1;
subformulaAllConstrained[{e, boundVars}] = false;
subformulaAllConstrained[{e, boundVars.size()}] = false;
return varCounts;
}
else if (e.is_const() && !e.is_numeral())
......@@ -53,7 +55,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
varCounts[ss.str()] = 1;
}
subformulaAllConstrained[{e, boundVars}] = false;
subformulaAllConstrained[{e, boundVars.size()}] = false;
return varCounts;
}
else if (e.is_app())
......@@ -68,9 +70,9 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
if (decl_kind == Z3_OP_NOT)
{
auto result = countVariableOccurences(e.arg(0), boundVars, !isPositive);
subformulaVariableCounts.insert({{e, isPositive}, {result, boundVars}});
subformulaVariableCounts.insert({{e, isPositive}, {result, boundVars.size()}});
subformulaAllConstrained[{e, boundVars}] = subformulaAllConstrained[{e.arg(0), boundVars}];
subformulaAllConstrained[{e, boundVars.size()}] = subformulaAllConstrained[{e.arg(0), boundVars.size()}];
return result;
}
else if (decl_kind == Z3_OP_IFF || (decl_kind == Z3_OP_EQ && e.arg(0).is_bool()))
......@@ -85,7 +87,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
//addCounts(varCountsLn, varCounts);
//addCounts(varCountsRn, varCounts);
subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);
subformulaAllConstrained[{e, boundVars.size()}] = allConstrained(varCounts);
return varCounts;
}
else if (decl_kind == Z3_OP_IMPLIES)
......@@ -96,7 +98,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
addCounts(varCountsL, varCounts);
addCounts(varCountsR, varCounts);
subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);
subformulaAllConstrained[{e, boundVars.size()}] = allConstrained(varCounts);
return varCounts;
}
......@@ -119,8 +121,8 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
}
}
subformulaVariableCounts.insert({{e, isPositive}, {varCounts, boundVars}});
subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);
subformulaVariableCounts.insert({{e, isPositive}, {varCounts, boundVars.size()}});
subformulaAllConstrained[{e, boundVars.size()}] = allConstrained(varCounts);
return varCounts;
}
else if(e.is_quantifier())
......@@ -165,8 +167,8 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
}
auto result = countVariableOccurences(e.body(), newBoundVars, isPositive);
subformulaVariableCounts.insert({{e, isPositive}, {result, boundVars}});
subformulaAllConstrained[{e, boundVars}] = allConstrained(result);
subformulaVariableCounts.insert({{e, isPositive}, {result, boundVars.size()}});
subformulaAllConstrained[{e, boundVars.size()}] = allConstrained(result);
return result;
}
......@@ -180,9 +182,9 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
{
std::vector<BoundVar> boundVars;
std::cout << "Counting variables" << std::endl;
//std::cout << "Counting variables" << std::endl;
variableCounts = countVariableOccurences(expression, boundVars, true);
std::cout << "Done" << std::endl;
//std::cout << "Done" << std::endl;
bool anyUnconstrained = false;
for (auto &var : variableCounts)
......@@ -208,6 +210,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
while (oldHash != expression.hash())
{
cacheHits = 0;
//std::cout << "Simplify once" << std::endl;
//std::cout << expression << std::endl;
oldHash = expression.hash();
......@@ -222,17 +225,18 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
// std::cout << "------------------------------------" << std::endl;
//expression = simplifier.PushNegations(expression);
//subformulaVariableCounts.clear();
subformulaVariableCounts.clear();
subformulaAllConstrained.clear();
std::vector<BoundVar> boundVars;
std::cout << "Counting variables" << std::endl;
//std::cout << "Counting variables" << std::endl;
variableCounts = countVariableOccurences(expression, boundVars, true);
std::cout << "Done" << std::endl;
//std::cout << "Done" << std::endl;
//trueSimplificationCache.clear();
//falseSimplificationCache.clear();
trueSimplificationCache.clear();
falseSimplificationCache.clear();
i++;
PrintUnconstrained();
//PrintUnconstrained();
}
//PrintUnconstrained();
......@@ -240,7 +244,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<BoundVar> boundVars, bool isPositive = true)
{
if (e.is_var() || e.is_numeral() || subformulaAllConstrained[{e, boundVars}])
if (e.is_var() || e.is_numeral() || subformulaAllConstrained[{e, boundVars.size()}])
{
return e;
}
......
......@@ -72,6 +72,17 @@ namespace std
}
};
template<>
struct hash<std::pair<z3::expr, unsigned int>>
{
size_t operator () (const std::pair<z3::expr, unsigned int> &p) const {
auto h1 = p.first.hash();
auto h2 = p.second;
return h1 ^ h2;
}
};
template<>
struct hash<std::pair<z3::expr, const std::vector<BoundVar>*>>
{
......@@ -143,10 +154,10 @@ private:
z3::context* context;
z3::expr expression;
std::unordered_map<std::pair<z3::expr, bool>, std::pair<std::map<std::string, int>, std::vector<BoundVar>>> subformulaVariableCounts;
std::unordered_map<std::pair<z3::expr, bool>, std::pair<std::map<std::string, int>, unsigned int>> subformulaVariableCounts;
std::unordered_map<std::pair<z3::expr, std::vector<BoundVar>>, int> subformulaMaxDeBruijnIndices;
std::map<std::string, int> variableCounts;
std::unordered_map<std::pair<z3::expr, std::vector<BoundVar>>, bool> subformulaAllConstrained;
std::unordered_map<std::pair<z3::expr, unsigned int>, bool> subformulaAllConstrained;
typedef std::unordered_map<z3::expr, std::pair<z3::expr, const std::vector<BoundVar>>> cacheMapType;
......@@ -171,6 +182,7 @@ private:
bool dagCounting = false;
MulReplacementMode mulReplacementMode = MUL;
MulReplacement mulReplacement = ALL;
int cacheHits = 0;
};
#endif // UNCONSTRAINEDVARIABLESIMPLIFIER_H
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment