Commit 6f21aca5 authored by Martin Jonas's avatar Martin Jonas
Browse files

Make the simplification a bit faster.

parent 6ec5f9ea
......@@ -28,6 +28,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}] = allConstrained(varCounts);
return varCounts;
}
else if (e.is_const() && !e.is_numeral())
......@@ -52,6 +53,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
varCounts[ss.str()] = 1;
}
subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);
return varCounts;
}
else if (e.is_app())
......@@ -68,6 +70,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
auto result = countVariableOccurences(e.arg(0), boundVars, !isPositive);
subformulaVariableCounts.insert({{e, isPositive}, {result, boundVars}});
subformulaAllConstrained[{e, boundVars}] = subformulaAllConstrained[{e.arg(0), boundVars}];
return result;
}
else if (decl_kind == Z3_OP_IFF || (decl_kind == Z3_OP_EQ && e.arg(0).is_bool()))
......@@ -82,6 +85,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
addCounts(varCountsLn, varCounts);
addCounts(varCountsRn, varCounts);
subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);
return varCounts;
}
else if (decl_kind == Z3_OP_IMPLIES)
......@@ -92,6 +96,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
addCounts(varCountsL, varCounts);
addCounts(varCountsR, varCounts);
subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);
return varCounts;
}
......@@ -159,6 +164,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
}
subformulaVariableCounts.insert({{e, isPositive}, {varCounts, boundVars}});
subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);
return varCounts;
}
else if(e.is_quantifier())
......@@ -204,6 +210,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
auto result = countVariableOccurences(e.body(), newBoundVars, isPositive);
subformulaVariableCounts.insert({{e, isPositive}, {result, boundVars}});
subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);
return result;
}
......@@ -216,7 +223,9 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
{
std::vector<BoundVar> boundVars;
//std::cout << "Counting variables" << std::endl;
variableCounts = countVariableOccurences(expression, boundVars, true);
//std::cout << "Done" << std::endl;
bool anyUnconstrained = false;
for (auto &var : variableCounts)
......@@ -242,6 +251,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
while (oldHash != expression.hash())
{
//std::cout << "Simplify once" << std::endl;
//std::cout << expression << std::endl;
oldHash = expression.hash();
......@@ -256,13 +266,14 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
//expression = simplifier.PushNegations(expression);
subformulaVariableCounts.clear();
std::vector<BoundVar> boundVars;
variableCounts = countVariableOccurences(expression, boundVars, true);
//std::vector<BoundVar> boundVars;
//variableCounts = countVariableOccurences(expression, boundVars, true);
trueSimplificationCache.clear();
falseSimplificationCache.clear();
i++;
break;
}
//PrintUnconstrained();
......@@ -270,7 +281,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<BoundVar> boundVars, bool isPositive = true)
{
if (e.is_var() || e.is_numeral())
if (e.is_var() || e.is_numeral() || subformulaAllConstrained[{e, boundVars}])
{
return e;
}
......@@ -1054,3 +1065,13 @@ void UnconstrainedVariableSimplifier::addCounts(std::map<std::string, int> &from
}
}
}
bool UnconstrainedVariableSimplifier::allConstrained(std::map<std::string, int> &varCounts)
{
for (auto &var : varCounts)
{
if (var.second == 1) return true;
}
return false;
}
......@@ -139,6 +139,7 @@ private:
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, std::vector<BoundVar>>, int> subformulaMaxDeBruijnIndices;
std::map<std::string, int> variableCounts;
std::unordered_map<std::pair<z3::expr, std::vector<BoundVar>>, bool> subformulaAllConstrained;
typedef std::unordered_map<z3::expr, std::pair<z3::expr, const std::vector<BoundVar>>> cacheMapType;
......@@ -147,6 +148,7 @@ private:
std::map<std::string, int> countVariableOccurences(z3::expr, std::vector<BoundVar>&, bool);
void addCounts(std::map<std::string, int>&, std::map<std::string, int>&);
bool allConstrained(std::map<std::string, int>&);
int getMaxLevel(z3::expr, const std::vector<BoundVar>&, bool);
z3::expr simplifyOnce(z3::expr, std::vector<BoundVar>, bool);
......
......@@ -127,6 +127,7 @@ int main(int argc, char* argv[])
simplifier.SetDagCounting(dagCounting);
simplifier.SimplifyIte();
e = simplifier.GetExpr();
e = e.simplify();
if (inprocess)
{
......@@ -168,6 +169,7 @@ int main(int argc, char* argv[])
{
std::cout << "(set-logic BV)" << std::endl;
//std::cout << s.to_smt2() << std::endl;
std::cout << s << std::endl;
std::cout << "(check-sat)" << std::endl;
}
......
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