Commit 959fc018 authored by Martin Jonáš's avatar Martin Jonáš
Browse files

Add modifiers to limit the simplification of bvmul.

parent 6ec5f9ea
...@@ -229,7 +229,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte() ...@@ -229,7 +229,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
if (!anyUnconstrained) if (!anyUnconstrained)
{ {
//PrintUnconstrained(); //PrintUnconstrained();
return; return;
} }
...@@ -390,19 +390,22 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound ...@@ -390,19 +390,22 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
if (zeroes == 0) return e.arg(1); if (zeroes == 0) return e.arg(1);
Z3_ast returnAst; if (mulReplacement == ALL || mulReplacement == LINEAR)
if (mulReplacementMode == SHIFT)
{
returnAst = Z3_mk_bvshl(*context, (Z3_ast)e.arg(1), (Z3_ast)(context->bv_val(zeroes, e.arg(1).get_sort().bv_size())));
}
else if (mulReplacementMode == MUL)
{ {
returnAst = (Z3_ast)(context->bv_val(1 << zeroes, e.arg(1).get_sort().bv_size()) * e.arg(1)); Z3_ast returnAst;
if (mulReplacementMode == SHIFT)
{
returnAst = Z3_mk_bvshl(*context, (Z3_ast)e.arg(1), (Z3_ast)(context->bv_val(zeroes, e.arg(1).get_sort().bv_size())));
}
else if (mulReplacementMode == MUL)
{
returnAst = (Z3_ast)(context->bv_val(1 << zeroes, e.arg(1).get_sort().bv_size()) * e.arg(1));
}
return to_expr(*context, returnAst);
} }
return to_expr(*context, returnAst);
} }
else if (unconstrained0 && isBefore(e.arg(1), e.arg(0), boundVars, isPositive)) else if (mulReplacement == ALL && unconstrained0 && isBefore(e.arg(1), e.arg(0), boundVars, isPositive))
{ {
expr arg1 = simplifyOnce(e.arg(1), boundVars, isPositive); expr arg1 = simplifyOnce(e.arg(1), boundVars, isPositive);
...@@ -417,7 +420,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound ...@@ -417,7 +420,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
return returnExpr; return returnExpr;
} }
else if (unconstrained1 && isBefore(e.arg(0), e.arg(1), boundVars, isPositive)) else if (mulReplacement == ALL && unconstrained1 && isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
{ {
expr arg0 = simplifyOnce(e.arg(0), boundVars, isPositive); expr arg0 = simplifyOnce(e.arg(0), boundVars, isPositive);
...@@ -433,58 +436,74 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound ...@@ -433,58 +436,74 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
return returnExpr; return returnExpr;
} }
} }
else if (decl_kind == Z3_OP_OR && num == 2) else if (decl_kind == Z3_OP_OR)
{ {
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars, isPositive)) auto toReturn = context->bool_val(false);
std::vector<expr> toReturnVec;
bool changed = false;
for (unsigned int i = 0; i < num; i++)
{ {
auto boundType = getBoundType(e.arg(0), boundVars); if (isUnconstrained(e.arg(i), boundVars))
if (boundType == EXISTENTIAL)
{ {
return isPositive ? context->bool_val(true) : e.arg(1); auto boundType = getBoundType(e.arg(i), boundVars);
if ((boundType == EXISTENTIAL && isPositive) || (boundType == UNIVERSAL || isPositive))
{
return context->bool_val(true);
}
changed = true;
} }
else else
{ {
return isPositive ? e.arg(1) : context->bool_val(true); toReturnVec.push_back(e.arg(i));
} }
} }
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
if (changed)
{ {
auto boundType = getBoundType(e.arg(1), boundVars); for (auto const &toReturnPart : toReturnVec)
if (boundType == EXISTENTIAL)
{
return isPositive ? context->bool_val(true) : e.arg(0);
}
else
{ {
return isPositive ? e.arg(0) : context->bool_val(true);; toReturn = toReturn || toReturnPart;
} }
return toReturn;
} }
} }
else if (decl_kind == Z3_OP_AND && num == 2) else if (decl_kind == Z3_OP_AND)
{ {
if (isUnconstrained(e.arg(0), boundVars) && isBefore(e.arg(1), e.arg(0), boundVars, isPositive)) auto toReturn = context->bool_val(true);
std::vector<expr> toReturnVec;
bool changed = false;
for (unsigned int i = 0; i < num; i++)
{ {
auto boundType = getBoundType(e.arg(0), boundVars); if (isUnconstrained(e.arg(i), boundVars))
if (boundType == EXISTENTIAL)
{ {
return isPositive ? e.arg(1) : context->bool_val(false); auto boundType = getBoundType(e.arg(i), boundVars);
if ((boundType == EXISTENTIAL && !isPositive) || (boundType == UNIVERSAL && isPositive))
{
return context->bool_val(false);
}
changed = true;
} }
else else
{ {
return isPositive ? context->bool_val(false) : e.arg(1); toReturnVec.push_back(e.arg(i));
} }
} }
else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1), boundVars, isPositive))
if (changed)
{ {
auto boundType = getBoundType(e.arg(1), boundVars); for (auto const &toReturnPart : toReturnVec)
if (boundType == EXISTENTIAL)
{ {
return isPositive ? e.arg(0) : context->bool_val(false); toReturn = toReturn && toReturnPart;
}
else
{
return isPositive ? context->bool_val(false) : e.arg(0);
} }
return toReturn;
} }
} }
else if (decl_kind == Z3_OP_IFF) else if (decl_kind == Z3_OP_IFF)
...@@ -620,6 +639,16 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound ...@@ -620,6 +639,16 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
} }
else if (decl_kind == Z3_OP_ITE) else if (decl_kind == Z3_OP_ITE)
{ {
if (isUnconstrained(e.arg(0), boundVars) && isUnconstrained(e.arg(1), boundVars) && getBoundType(e.arg(0), boundVars) == getBoundType(e.arg(1), boundVars))
{
return e.arg(1);
}
if (isUnconstrained(e.arg(0), boundVars) && isUnconstrained(e.arg(2), boundVars) && getBoundType(e.arg(0), boundVars) == getBoundType(e.arg(2), boundVars))
{
return e.arg(2);
}
auto result = ite(e.arg(0), simplifyOnce(e.arg(1), boundVars, isPositive), simplifyOnce(e.arg(2), boundVars, isPositive)); auto result = ite(e.arg(0), simplifyOnce(e.arg(1), boundVars, isPositive), simplifyOnce(e.arg(2), boundVars, isPositive));
if (isPositive) if (isPositive)
{ {
......
...@@ -10,6 +10,8 @@ ...@@ -10,6 +10,8 @@
enum BoundType { EXISTENTIAL, UNIVERSAL }; enum BoundType { EXISTENTIAL, UNIVERSAL };
enum MulReplacementMode { MUL, SHIFT }; enum MulReplacementMode { MUL, SHIFT };
enum MulReplacement { ODD, LINEAR, ALL };
typedef std::tuple<std::string, BoundType, int> BoundVar; typedef std::tuple<std::string, BoundType, int> BoundVar;
namespace std namespace std
...@@ -132,6 +134,11 @@ public: ...@@ -132,6 +134,11 @@ public:
this->mulReplacementMode = mulReplacementMode; this->mulReplacementMode = mulReplacementMode;
} }
void SetMulReplacement(MulReplacement mulReplacement)
{
this->mulReplacement = mulReplacement;
}
private: private:
z3::context* context; z3::context* context;
z3::expr expression; z3::expr expression;
...@@ -161,6 +168,7 @@ private: ...@@ -161,6 +168,7 @@ private:
bool countVariablesLocally = false; bool countVariablesLocally = false;
bool dagCounting = false; bool dagCounting = false;
MulReplacementMode mulReplacementMode = MUL; MulReplacementMode mulReplacementMode = MUL;
MulReplacement mulReplacement = ALL;
}; };
#endif // UNCONSTRAINEDVARIABLESIMPLIFIER_H #endif // UNCONSTRAINEDVARIABLESIMPLIFIER_H
...@@ -27,6 +27,7 @@ int main(int argc, char* argv[]) ...@@ -27,6 +27,7 @@ int main(int argc, char* argv[])
{"inprocess", no_argument, 0, 'i' }, {"inprocess", no_argument, 0, 'i' },
{"dag-counting", no_argument, 0, 'd' }, {"dag-counting", no_argument, 0, 'd' },
{"full", no_argument, 0, 'f' }, {"full", no_argument, 0, 'f' },
{"mulReplacementMode", required_argument, 0, 'r' },
{"mulReplacement", required_argument, 0, 'm' }, {"mulReplacement", required_argument, 0, 'm' },
{0, 0, 0, 0 } {0, 0, 0, 0 }
}; };
...@@ -34,6 +35,7 @@ int main(int argc, char* argv[]) ...@@ -34,6 +35,7 @@ int main(int argc, char* argv[])
bool propagateUnconstrainedFlag = false, runZ3 = false, canonize = false, countVariablesLocally = false, inprocess = false, full = false, dagCounting = false; bool propagateUnconstrainedFlag = false, runZ3 = false, canonize = false, countVariablesLocally = false, inprocess = false, full = false, dagCounting = false;
char* filename; char* filename;
MulReplacementMode mulReplacementMode = SHIFT; MulReplacementMode mulReplacementMode = SHIFT;
MulReplacement mulReplacement = ALL;
int opt = 0; int opt = 0;
...@@ -63,18 +65,38 @@ int main(int argc, char* argv[]) ...@@ -63,18 +65,38 @@ int main(int argc, char* argv[])
case 'd': case 'd':
dagCounting = true; dagCounting = true;
break; break;
case 'm': case 'r':
{ {
string argString(optarg); string argString(optarg);
if (argString == "mul") if (argString == "mul")
{ {
mulReplacementMode = MUL; mulReplacementMode = MUL;
std::cout << "Mode: mul" << std::endl; //std::cout << "Mode: mul" << std::endl;
} }
else if (argString == "shift") else if (argString == "shift")
{ {
mulReplacementMode = SHIFT; mulReplacementMode = SHIFT;
std::cout << "Mode: shift" << std::endl; //std::cout << "Mode: shift" << std::endl;
}
break;
}
case 'm':
{
string argString(optarg);
if (argString == "odd")
{
mulReplacement = ODD;
//std::cout << "Mul: odd" << std::endl;
}
else if (argString == "linear")
{
mulReplacement = LINEAR;
//std::cout << "Mul: linear" << std::endl;
}
else if (argString == "all")
{
mulReplacement = ALL;
//std::cout << "Mul: all" << std::endl;
} }
break; break;
} }
...@@ -124,6 +146,7 @@ int main(int argc, char* argv[]) ...@@ -124,6 +146,7 @@ int main(int argc, char* argv[])
UnconstrainedVariableSimplifier simplifier(ctx, e); UnconstrainedVariableSimplifier simplifier(ctx, e);
simplifier.SetCountVariablesLocally(countVariablesLocally); simplifier.SetCountVariablesLocally(countVariablesLocally);
simplifier.SetMulReplacementMode(mulReplacementMode); simplifier.SetMulReplacementMode(mulReplacementMode);
simplifier.SetMulReplacement(mulReplacement);
simplifier.SetDagCounting(dagCounting); simplifier.SetDagCounting(dagCounting);
simplifier.SimplifyIte(); simplifier.SimplifyIte();
e = simplifier.GetExpr(); e = simplifier.GetExpr();
......
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