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

Changes

parent 5e14a0fb
Hide whitespace changes
Inline Side-by-side
UnconstrainedVariableSimplifier.cpp
View file @ cec68bcd
......@@ -6,20 +6,20 @@
using namespace std;
using namespace z3;
map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e, vector<BoundVar> &boundVars, bool isPositive=true)
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 (countVariablesLocally)
//{
return (item->second).first;
//}
//else
//{
//map<string, int> varCounts;
//return varCounts;
//}
if (dagCounting)
{
map<string, int> varCounts;
return varCounts;
}
else
{
return (item->second).first;
}
}
map<string, int> varCounts;
......@@ -70,10 +70,34 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e
return result;
}
else if (decl_kind == Z3_OP_IFF || (decl_kind == Z3_OP_EQ && e.arg(0).is_bool()))
{
auto varCountsLp = countVariableOccurences(e.arg(0), boundVars, isPositive);
auto varCountsRp = countVariableOccurences(e.arg(1), boundVars, isPositive);
auto varCountsLn = countVariableOccurences(e.arg(0), boundVars, !isPositive);
auto varCountsRn = countVariableOccurences(e.arg(1), boundVars, !isPositive);
addCounts(varCountsLp, varCounts);
addCounts(varCountsRp, varCounts);
addCounts(varCountsLn, varCounts);
addCounts(varCountsRn, varCounts);
return varCounts;
}
else if (decl_kind == Z3_OP_IMPLIES)
{
auto varCountsL = countVariableOccurences(e.arg(0), boundVars, !isPositive);
auto varCountsR = countVariableOccurences(e.arg(1), boundVars, isPositive);
addCounts(varCountsL, varCounts);
addCounts(varCountsR, varCounts);
return varCounts;
}
for (unsigned i = 0; i < num; i++)
{
auto currentVarCounts = countVariableOccurences(e.arg(i), boundVars);
auto currentVarCounts = countVariableOccurences(e.arg(i), boundVars, isPositive);
for (auto &item : currentVarCounts)
{
......@@ -194,8 +218,6 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
variableCounts = countVariableOccurences(expression, boundVars, true);
//PrintUnconstrained();
bool anyUnconstrained = false;
for (auto &var : variableCounts)
{
......@@ -207,6 +229,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
if (!anyUnconstrained)
{
PrintUnconstrained();
return;
}
......@@ -234,13 +257,15 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
subformulaVariableCounts.clear();
std::vector<BoundVar> boundVars;
variableCounts = countVariableOccurences(expression, boundVars);
variableCounts = countVariableOccurences(expression, boundVars, true);
trueSimplificationCache.clear();
falseSimplificationCache.clear();
i++;
}
PrintUnconstrained();
}
z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<BoundVar> boundVars, bool isPositive = true)
......@@ -351,12 +376,10 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
if (mulReplacementMode == SHIFT)
{
std::cout << "Replacing SHFIT" << std::endl;
returnAst = Z3_mk_bvshl(*context, (Z3_ast)e.arg(0), (Z3_ast)(context->bv_val(zeroes, e.arg(0).get_sort().bv_size())));
}
else if (mulReplacementMode == MUL)
{
std::cout << "Replacing MUL" << std::endl;
returnAst = (Z3_ast)(context->bv_val(1 << zeroes, e.arg(0).get_sort().bv_size()) * e.arg(0));
}
return to_expr(*context, returnAst);
......@@ -371,17 +394,11 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
if (mulReplacementMode == SHIFT)
{
std::cout << "Replacing SHFIT" << std::endl;
returnAst = Z3_mk_bvshl(*context, (Z3_ast)e.arg(1), (Z3_ast)(context->bv_val(zeroes, e.arg(1).get_sort().bv_size())));
std::cout << "Replacing " << e << " by " << to_expr(*context, returnAst) << std::endl;
}
else if (mulReplacementMode == MUL)
{
std::cout << "Replacing MUL" << std::endl;
returnAst = (Z3_ast)(context->bv_val(1 << zeroes, e.arg(1).get_sort().bv_size()) * e.arg(1));
std::cout << "Replacing " << e << " by " << to_expr(*context, returnAst) << std::endl;
}
return to_expr(*context, returnAst);
}
......@@ -512,7 +529,14 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
}
else
{
return e;
if (e.arg(0).is_bool())
{
return e; //or split into implications
}
else
{
return simplifyOnce(e.arg(0), boundVars, isPositive) == simplifyOnce(e.arg(1), boundVars, isPositive);
}
}
}
else if (decl_kind == Z3_OP_SLEQ || decl_kind == Z3_OP_ULEQ )
......@@ -1002,3 +1026,31 @@ expr UnconstrainedVariableSimplifier::CanonizeBoundVariables(const expr &e)
return e;
}
}
void UnconstrainedVariableSimplifier::addCounts(std::map<std::string, int> &from, std::map<std::string, int> &to)
{
for (auto &item : from)
{
auto singleVarCount = to.find(item.first);
if (singleVarCount == to.end())
{
to[item.first] = item.second;
}
else
{
if (to[item.first] == 2)
{
continue;
}
if (singleVarCount->second + item.second > 1)
{
to[item.first] = 2;
}
else
{
to[item.first] = singleVarCount->second + item.second;
}
}
}
}
UnconstrainedVariableSimplifier.h
View file @ cec68bcd
......@@ -92,12 +92,11 @@ public:
void PrintUnconstrained()
{
std::cout << "------" << std::endl;
bool allConstrained = true;
for (auto &item : variableCounts)
{
std::cout << "var " << item.first << " - " << item.second << " times" << std::endl;
if (item.second == 1)
{
allConstrained = false;
......@@ -105,6 +104,7 @@ public:
}
}
if (allConstrained) std::cout << "All variables constrained" << std::endl;
std::cout << "------" << std::endl;
}
void SimplifyOnce()
......@@ -122,6 +122,11 @@ public:
this->countVariablesLocally = countVariablesLocally;
}
void SetDagCounting(bool dagCounting)
{
this->dagCounting = dagCounting;
}
void SetMulReplacementMode(MulReplacementMode mulReplacementMode)
{
this->mulReplacementMode = mulReplacementMode;
......@@ -141,6 +146,7 @@ private:
cacheMapType falseSimplificationCache;
std::map<std::string, int> countVariableOccurences(z3::expr, std::vector<BoundVar>&, bool);
void addCounts(std::map<std::string, int>&, std::map<std::string, int>&);
int getMaxLevel(z3::expr, const std::vector<BoundVar>&, bool);
z3::expr simplifyOnce(z3::expr, std::vector<BoundVar>, bool);
......@@ -153,6 +159,7 @@ private:
int lastBound = 0;
bool countVariablesLocally = false;
bool dagCounting = false;
MulReplacementMode mulReplacementMode = MUL;
};
......
main.cpp
View file @ cec68bcd
......@@ -25,19 +25,20 @@ int main(int argc, char* argv[])
{"canonize", no_argument, 0, 'c' },
{"run-z3", no_argument, 0, 'z' },
{"inprocess", no_argument, 0, 'i' },
{"dag-counting", no_argument, 0, 'd' },
{"full", no_argument, 0, 'f' },
{"mulReplacement", required_argument, 0, 'm' },
{0, 0, 0, 0 }
};
bool propagateUnconstrainedFlag = false, runZ3 = false, canonize = false, countVariablesLocally = false, inprocess = false, full = false;
bool propagateUnconstrainedFlag = false, runZ3 = false, canonize = false, countVariablesLocally = false, inprocess = false, full = false, dagCounting = false;
char* filename;
MulReplacementMode mulReplacementMode = SHIFT;
int opt = 0;
int long_index = 0;
while ((opt = getopt_long(argc, argv,"plzcifm:", long_options, &long_index )) != -1)
while ((opt = getopt_long(argc, argv,"plzcifdm:", long_options, &long_index )) != -1)
{
switch (opt)
{
......@@ -59,6 +60,9 @@ int main(int argc, char* argv[])
case 'f':
full = true;
break;
case 'd':
dagCounting = true;
break;
case 'm':
{
string argString(optarg);
......@@ -98,8 +102,8 @@ int main(int argc, char* argv[])
if (canonize)
{
ExprSimplifier simplifier(ctx);
e = simplifier.PushNegations(e);
ExprSimplifier simplifier(ctx);
e = simplifier.PushNegations(e);
UnconstrainedVariableSimplifier uSimplifier(ctx, e);
e = uSimplifier.CanonizeBoundVariables(e);
......@@ -120,6 +124,7 @@ int main(int argc, char* argv[])
UnconstrainedVariableSimplifier simplifier(ctx, e);
simplifier.SetCountVariablesLocally(countVariablesLocally);
simplifier.SetMulReplacementMode(mulReplacementMode);
simplifier.SetDagCounting(dagCounting);
simplifier.SimplifyIte();
e = simplifier.GetExpr();
......@@ -161,6 +166,8 @@ int main(int argc, char* argv[])
}
else
{
std::cout << s.to_smt2() << std::endl;
std::cout << "(set-logic BV)" << std::endl;
//std::cout << s.to_smt2() << std::endl;
std::cout << s << 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