Skip to content
GitLab
Commit 120878ac authored by Martin Jonáš's avatar Martin Jonáš
Browse files

Fixes.

parent 1b54d291
Hide whitespace changes
Inline Side-by-side
UnconstrainedVariableSimplifier.cpp
View file @ 120878ac
......@@ -6,35 +6,29 @@
using namespace std;
using namespace z3;
pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccurences(z3::expr e, vector<BoundVar> &boundVars, bool isPositive=true)
map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e, vector<BoundVar> &boundVars, bool isPositive=true)
{
map<string, int> varCounts;
auto item = subformulaVariableCounts.find({e, isPositive});
auto mdb = subformulaMaxDeBruijnIndices.find({e, boundVars});
if (item != subformulaVariableCounts.end() && (item->second).second == &boundVars && mdb != subformulaMaxDeBruijnIndices.end())
if ((item != subformulaVariableCounts.end() && ((item->second).second) == boundVars))
{
//probably can be return {varCounts, subformulaMaxDeBruijnIndices[(Z3_ast)e]};
if (countVariablesLocally)
{
return {(item->second).first, subformulaMaxDeBruijnIndices.at({e, boundVars})};
}
else
{
return {varCounts, subformulaMaxDeBruijnIndices[{e, boundVars}]};
}
//if (countVariablesLocally)
//{
return (item->second).first;
//}
//else
//{
//map<string, int> varCounts;
//return varCounts;
//}
}
map<string, int> varCounts;
if (e.is_var())
{
Z3_ast ast = (Z3_ast)e;
int deBruijnIndex = Z3_get_index_value(*context, ast);
varCounts[std::get<0>(boundVars[boundVars.size() - deBruijnIndex - 1])] = 1;
int level = std::get<2>(boundVars[boundVars.size() - deBruijnIndex - 1]);
subformulaMaxDeBruijnIndices.insert({{e, boundVars}, level});
//subformulaVariableCounts.insert({{(Z3_ast)e, isPositive}, {varCounts, boundVars}});
return {varCounts, level};
return varCounts;
}
else if (e.is_const() && !e.is_numeral())
{
......@@ -45,7 +39,7 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
if (ss.str() == "true" || ss.str() == "false")
{
return {varCounts, -1};
return varCounts;
}
varCounts[ss.str()] = 1;
......@@ -58,17 +52,13 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
varCounts[ss.str()] = 1;
}
subformulaMaxDeBruijnIndices.insert({{e, boundVars}, -1});
//subformulaVariableCounts.insert({{(Z3_ast)e, isPositive}, {varCounts, boundVars}});
return {varCounts, -1};
return varCounts;
}
else if (e.is_app())
{
func_decl f = e.decl();
unsigned num = e.num_args();
int maxDeBruijnIndex = -1;
if (num != 0)
{
auto decl_kind = e.decl().decl_kind();
......@@ -76,8 +66,7 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
if (decl_kind == Z3_OP_NOT)
{
auto result = countVariableOccurences(e.arg(0), boundVars, !isPositive);
subformulaVariableCounts.insert({{e, isPositive}, {result.first, &boundVars}});
subformulaMaxDeBruijnIndices.insert({{e, boundVars}, result.second});
subformulaVariableCounts.insert({{e, isPositive}, {result, boundVars}});
return result;
}
......@@ -86,7 +75,7 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
{
auto currentVarCounts = countVariableOccurences(e.arg(i), boundVars);
for (auto &item : currentVarCounts.first)
for (auto &item : currentVarCounts)
{
auto singleVarCount = varCounts.find(item.first);
if (singleVarCount == varCounts.end())
......@@ -95,6 +84,11 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
}
else
{
if (varCounts[item.first] == 2)
{
continue;
}
BoundType boundType = EXISTENTIAL; //not present variables are uninterpreted constants
for (auto &boundVar : boundVars)
{
......@@ -126,11 +120,6 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
}
}
}
if (currentVarCounts.second > maxDeBruijnIndex)
{
maxDeBruijnIndex = currentVarCounts.second;
}
}
}
else if (f.name() != NULL)
......@@ -145,10 +134,8 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
}
}
subformulaMaxDeBruijnIndices.insert({{e, boundVars}, maxDeBruijnIndex});
subformulaVariableCounts.insert({{e, isPositive}, {varCounts, &boundVars}});
return {varCounts, maxDeBruijnIndex};
subformulaVariableCounts.insert({{e, isPositive}, {varCounts, boundVars}});
return varCounts;
}
else if(e.is_quantifier())
{
......@@ -192,25 +179,20 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
}
auto result = countVariableOccurences(e.body(), newBoundVars, isPositive);
subformulaVariableCounts.insert({{e, isPositive}, {result.first, &boundVars}});
subformulaMaxDeBruijnIndices.insert({{e, boundVars}, result.second});
subformulaVariableCounts.insert({{e, isPositive}, {result, boundVars}});
return result;
}
std::cout << e << std::endl;
assert(false);
return {varCounts, -1};
return varCounts;
}
void UnconstrainedVariableSimplifier::SimplifyIte()
{
std::vector<BoundVar> boundVars;
std::cout << "Counting variables" << std::endl;
variableCounts = countVariableOccurences(expression, boundVars, true).first;
std::cout << "Simplifying" << std::endl;
std::cout << "Cache size: " << subformulaVariableCounts.size() << std::endl;
variableCounts = countVariableOccurences(expression, boundVars, true);
//PrintUnconstrained();
......@@ -237,7 +219,6 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
while (oldHash != expression.hash())
{
std::cout << i << std::endl;
//std::cout << expression << std::endl;
oldHash = expression.hash();
......@@ -251,13 +232,9 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
// std::cout << "------------------------------------" << std::endl;
//expression = simplifier.PushNegations(expression);
return;
//subformulaVariableCounts.clear();
subformulaMaxDeBruijnIndices.clear();
subformulaVariableCounts.clear();
std::vector<BoundVar> boundVars;
variableCounts = countVariableOccurences(expression, boundVars).first;
variableCounts = countVariableOccurences(expression, boundVars);
trueSimplificationCache.clear();
falseSimplificationCache.clear();
......@@ -318,11 +295,11 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
if (decl_kind == Z3_OP_BADD && num == 2)
{
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars))
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars, isPositive))
{
return e.arg(0);
}
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars))
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
{
return e.arg(1);
}
......@@ -338,7 +315,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
{
if (isUnconstrained(e.arg(0), boundVars) && isUnconstrained(e.arg(1), boundVars))
{
if (isBefore(e.arg(0), e.arg(1), boundVars))
if (isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
{
return e.arg(1);
}
......@@ -355,7 +332,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
if (unconstrained0 && unconstrained1)
{
if (isBefore(e.arg(0), e.arg(1), boundVars))
if (isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
{
return e.arg(1);
}
......@@ -408,7 +385,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
}
return to_expr(*context, returnAst);
}
else if (unconstrained0)
else if (unconstrained0 && isBefore(e.arg(1), e.arg(0), boundVars, isPositive))
{
expr arg1 = simplifyOnce(e.arg(1), boundVars, isPositive);
......@@ -423,7 +400,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
return returnExpr;
}
else if (unconstrained1)
else if (unconstrained1 && isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
{
expr arg0 = simplifyOnce(e.arg(0), boundVars, isPositive);
......@@ -441,7 +418,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
}
else if (decl_kind == Z3_OP_OR && num == 2)
{
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars))
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars, isPositive))
{
auto boundType = getBoundType(e.arg(0), boundVars);
if (boundType == EXISTENTIAL)
......@@ -453,7 +430,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
return isPositive ? e.arg(1) : context->bool_val(true);
}
}
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars))
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
{
auto boundType = getBoundType(e.arg(1), boundVars);
if (boundType == EXISTENTIAL)
......@@ -468,7 +445,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
}
else if (decl_kind == Z3_OP_AND && num == 2)
{
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars))
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars, isPositive))
{
auto boundType = getBoundType(e.arg(0), boundVars);
if (boundType == EXISTENTIAL)
......@@ -480,7 +457,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
return isPositive ? context->bool_val(false) : e.arg(1);
}
}
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars))
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
{
auto boundType = getBoundType(e.arg(1), boundVars);
if (boundType == EXISTENTIAL)
......@@ -508,7 +485,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
}
else if (decl_kind == Z3_OP_EQ)
{
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars))
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars, isPositive))
{
auto boundType = getBoundType(e.arg(0), boundVars);
if (boundType == EXISTENTIAL)
......@@ -520,7 +497,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
return isPositive ? context->bool_val(false) : context->bool_val(true);
}
}
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars))
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
{
auto boundType = getBoundType(e.arg(1), boundVars);
......@@ -540,7 +517,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
}
else if (decl_kind == Z3_OP_SLEQ || decl_kind == Z3_OP_ULEQ )
{
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars))
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars, isPositive))
{
auto boundType = getBoundType(e.arg(0), boundVars);
auto bvSize = e.arg(1).get_sort().bv_size();
......@@ -558,7 +535,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
return isPositive ? e.arg(1) == maxValue : context->bool_val(true);
}
}
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars))
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
{
auto boundType = getBoundType(e.arg(1), boundVars);
auto bvSize = e.arg(1).get_sort().bv_size();
......@@ -580,7 +557,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
}
else if (decl_kind == Z3_OP_SLT || decl_kind == Z3_OP_ULT)
{
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars))
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars, isPositive))
{
auto boundType = getBoundType(e.arg(0), boundVars);
auto bvSize = e.arg(1).get_sort().bv_size();
......@@ -598,7 +575,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
return isPositive ? context->bool_val(false) : !(e.arg(1) == minValue);
}
}
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars))
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
{
auto boundType = getBoundType(e.arg(1), boundVars);
auto bvSize = e.arg(1).get_sort().bv_size();
......@@ -756,7 +733,6 @@ bool UnconstrainedVariableSimplifier::isUnconstrained(expr e, const vector<Bound
if (ss.str() != "true" && ss.str() != "false")
{
//std::cout << "isUnconstrained " << ss.str() << std::endl;
//std::cout << "result: " << (variableCounts.at(ss.str()) == 1) << std::endl;
return (variableCounts.at(ss.str()) == 1);
}
......@@ -786,11 +762,106 @@ bool UnconstrainedVariableSimplifier::isVar(expr e) const
return false;
}
int UnconstrainedVariableSimplifier::getMaxLevel(expr e, const std::vector<BoundVar> &boundVars, bool isPositive = true)
{
auto item = subformulaMaxDeBruijnIndices.find({e, boundVars});
if (item != subformulaMaxDeBruijnIndices.end())
{
return item->second;
}
if (e.is_var())
{
Z3_ast ast = (Z3_ast)e;
int deBruijnIndex = Z3_get_index_value(*context, ast);
return std::get<2>(boundVars[boundVars.size() - deBruijnIndex - 1]);
}
else if (e.is_const() && !e.is_numeral())
{
return -1;
}
else if (e.is_app())
{
func_decl f = e.decl();
unsigned num = e.num_args();
int maxLevel = -1;
if (num != 0)
{
for (unsigned i = 0; i < num; i++)
{
auto currentMaxLevel = getMaxLevel(e.arg(i), boundVars, isPositive);
if (currentMaxLevel > maxLevel)
{
maxLevel = currentMaxLevel;
}
}
subformulaMaxDeBruijnIndices.insert({{e, boundVars}, maxLevel});
return maxLevel;
}
else if (f.name() != NULL)
{
return -1;
}
}
else if(e.is_quantifier())
{
Z3_ast ast = (Z3_ast)e;
int numBound = Z3_get_quantifier_num_bound(*context, ast);
BoundType boundType;
if (isPositive)
{
boundType = Z3_is_quantifier_forall(*context, ast) ? UNIVERSAL : EXISTENTIAL;
}
else
{
boundType = Z3_is_quantifier_forall(*context, ast) ? EXISTENTIAL : UNIVERSAL;
}
int level;
if (boundVars.size() == 0)
{
level = 1;
}
else
{
auto previousVar = boundVars.back();
level = std::get<2>(previousVar);
if (boundType != std::get<1>(previousVar))
{
level++;
}
}
vector<BoundVar> newBoundVars = boundVars;
for (int i = 0; i < numBound; i++)
{
Z3_symbol z3_symbol = Z3_get_quantifier_bound_name(*context, ast, i);
symbol current_symbol(*context, z3_symbol);
newBoundVars.push_back(make_tuple(current_symbol.str(), boundType, level));
}
return getMaxLevel(e.body(), newBoundVars, isPositive);
}
assert(false);
return -1;
}
//should be true if all variables in "a" are quantified before a variable "b"
bool UnconstrainedVariableSimplifier::isBefore(expr a, expr b, const std::vector<BoundVar> &boundVars) const
bool UnconstrainedVariableSimplifier::isBefore(expr a, expr b, const std::vector<BoundVar> &boundVars, bool isPositive)
{
bool result = (subformulaMaxDeBruijnIndices.at({a, boundVars}) <= subformulaMaxDeBruijnIndices.at({b, boundVars})) || (subformulaMaxDeBruijnIndices.at({a, boundVars}) == -1);
return result;
int aLevel = getMaxLevel(a, boundVars, isPositive);
int bLevel = getMaxLevel(b, boundVars, isPositive);
return (aLevel <= bLevel);
}
BoundType UnconstrainedVariableSimplifier::getBoundType(expr e, const std::vector<BoundVar> &boundVars)
......
UnconstrainedVariableSimplifier.h
View file @ 120878ac
......@@ -60,7 +60,7 @@ namespace std
};
template<>
struct hash<std::pair<z3::expr, const std::vector<BoundVar>>>
struct hash<std::pair<z3::expr, std::vector<BoundVar>>>
{
size_t operator () (const std::pair<z3::expr, std::vector<BoundVar>> &p) const {
auto h1 = p.first.hash();
......@@ -131,8 +131,8 @@ 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, const std::vector<BoundVar>>, int> subformulaMaxDeBruijnIndices;
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;
typedef std::unordered_map<z3::expr, std::pair<z3::expr, const std::vector<BoundVar>>> cacheMapType;
......@@ -140,12 +140,13 @@ private:
cacheMapType trueSimplificationCache;
cacheMapType falseSimplificationCache;
std::pair<std::map<std::string, int>, int> countVariableOccurences(z3::expr, std::vector<BoundVar>&, bool);
std::map<std::string, int> countVariableOccurences(z3::expr, std::vector<BoundVar>&, bool);
int getMaxLevel(z3::expr, const std::vector<BoundVar>&, bool);
z3::expr simplifyOnce(z3::expr, std::vector<BoundVar>, bool);
bool isUnconstrained(z3::expr, const std::vector<BoundVar>&) const;
bool isVar(z3::expr) const;
bool isBefore(z3::expr, z3::expr, const std::vector<BoundVar>&) const;
bool isBefore(z3::expr, z3::expr, const std::vector<BoundVar>&, bool);
BoundType getBoundType(z3::expr, const std::vector<BoundVar>&);
int getNumberOfLeadingZeroes(const z3::expr&);
......
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