Commit 1b54d291 authored by Martin Jonáš's avatar Martin Jonáš
Browse files

Working version.

parent 7f0cae84
......@@ -13,10 +13,20 @@ file(GLOB Q3B_SRC
"*.cpp"
)
find_package(OpenMP)
if (OPENMP_FOUND)
set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${OpenMP_C_FLAGS}")
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${OpenMP_CXX_FLAGS}")
endif()
#SET(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
#SET(BUILD_SHARED_LIBRARIES OFF)
SET(CMAKE_EXE_LINKER_FLAGS "-static")
add_executable(exprsimplifier ${Q3B_SRC})
#set( CMAKE_CXX_FLAGS "-fstack-protector -fstack-protector-all" )
set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -g -Wall")
set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -g -Wall -Wextra")
set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -Wall")
find_library(LibZ3 z3 PATHS /usr/lib DOC "z3 library")
......
......@@ -598,6 +598,15 @@ expr ExprSimplifier::PushNegations(const expr &e)
func_decl dec = e.decl();
int numArgs = e.num_args();
if (dec.decl_kind() == Z3_OP_EQ && e.arg(0).get_sort().is_bool())
{
auto e0 = PushNegations(e.arg(0));
auto e1 = PushNegations(e.arg(1));
auto result = (e0 && e1) || (!e0 && !e1);
pushNegationsCache.clear();
return result;
}
expr_vector arguments(*context);
for (int i = 0; i < numArgs; i++)
{
......
This diff is collapsed.
......@@ -6,8 +6,81 @@
#include <vector>
#include <string>
#include <tuple>
#include <unordered_map>
enum BoundType { EXISTENTIAL, UNIVERSAL };
enum MulReplacementMode { MUL, SHIFT };
typedef std::tuple<std::string, BoundType, int> BoundVar;
namespace std
{
template<>
struct hash<z3::expr>
{
size_t operator() (const z3::expr& e) const
{
return e.hash();
}
};
template<>
struct hash<std::pair<z3::expr, bool>>
{
size_t operator () (const std::pair<z3::expr,bool> &p) const {
auto h1 = p.first.hash();
auto h2 = std::hash<bool>{}(p.second);
return h1 ^ h2;
}
};
template<>
struct hash<BoundVar>
{
size_t operator() (const BoundVar& p) const
{
auto h1 = std::hash<std::string>{}(std::get<0>(p));
auto h2 = 1 + std::get<1>(p);
auto h3 = std::get<2>(p);
return h1 ^ h2 ^ h3;
}
};
template<>
struct hash<std::vector<BoundVar>>
{
std::size_t operator()(const std::vector<BoundVar>& vec) const {
std::size_t seed = vec.size();
for(auto& i : vec) {
seed ^= std::hash<BoundVar>{}(i) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
}
return seed;
}
};
template<>
struct hash<std::pair<z3::expr, const std::vector<BoundVar>>>
{
size_t operator () (const std::pair<z3::expr, std::vector<BoundVar>> &p) const {
auto h1 = p.first.hash();
auto h2 = std::hash<std::vector<BoundVar>>{}(p.second);
return h1 ^ h2;
}
};
template<>
struct hash<std::pair<z3::expr, const std::vector<BoundVar>*>>
{
size_t operator () (const std::pair<z3::expr, std::vector<BoundVar>*> &p) const {
auto h1 = p.first.hash();
auto h2 = (size_t)p.second;
return h1 ^ h2;
}
};
}
class UnconstrainedVariableSimplifier
{
......@@ -15,9 +88,6 @@ public:
UnconstrainedVariableSimplifier(z3::context &ctx, z3::expr expr) : expression(expr)
{
this->context = &ctx;
std::vector<BoundVar> boundVars;
variableCounts = countVariableOccurences(expression, boundVars, true).first;
}
void PrintUnconstrained()
......@@ -26,12 +96,12 @@ public:
for (auto &item : variableCounts)
{
std::cout << "var " << item.first << " - " << item.second << " times" << std::endl;
std::cout << "var " << item.first << " - " << item.second << " times" << std::endl;
if (item.second == 1)
{
allConstrained = false;
//std::cout << "Unconstrained variable: " << item.first << std::endl;
std::cout << "Unconstrained variable: " << item.first << std::endl;
}
}
if (allConstrained) std::cout << "All variables constrained" << std::endl;
......@@ -52,33 +122,37 @@ public:
this->countVariablesLocally = countVariablesLocally;
}
void SetMulReplacementMode(MulReplacementMode mulReplacementMode)
{
this->mulReplacementMode = mulReplacementMode;
}
private:
z3::context* context;
z3::expr expression;
typedef std::tuple<std::string, BoundType, int> BoundVar;
std::map<std::pair<const Z3_ast, bool>, std::pair<std::map<std::string, int>, std::vector<BoundVar>>> subformulaVariableCounts;
std::map<const Z3_ast, 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, const std::vector<BoundVar>>, int> subformulaMaxDeBruijnIndices;
std::map<std::string, int> variableCounts;
typedef std::map<const Z3_ast, std::pair<z3::expr, const std::vector<BoundVar>>> cacheMapType;
typedef std::unordered_map<z3::expr, std::pair<z3::expr, const std::vector<BoundVar>>> cacheMapType;
cacheMapType trueSimplificationCache;
cacheMapType falseSimplificationCache;
std::pair<std::map<std::string, int>, int> countVariableOccurences(z3::expr, std::vector<BoundVar>, bool);
std::pair<std::map<std::string, int>, int> countVariableOccurences(z3::expr, std::vector<BoundVar>&, bool);
z3::expr simplifyOnce(z3::expr, std::vector<BoundVar>, bool);
bool isUnconstrained(z3::expr, const std::vector<BoundVar>&);
bool isVar(z3::expr);
bool isBefore(z3::expr, z3::expr);
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;
BoundType getBoundType(z3::expr, const std::vector<BoundVar>&);
int getNumberOfLeadingZeroes(const z3::expr&);
int lastBound = 0;
bool countVariablesLocally = false;
MulReplacementMode mulReplacementMode = MUL;
};
#endif // UNCONSTRAINEDVARIABLESIMPLIFIER_H
......@@ -26,16 +26,18 @@ int main(int argc, char* argv[])
{"run-z3", no_argument, 0, 'z' },
{"inprocess", no_argument, 0, 'i' },
{"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;
char* filename;
MulReplacementMode mulReplacementMode = SHIFT;
int opt = 0;
int long_index = 0;
while ((opt = getopt_long(argc, argv,"plzcif", long_options, &long_index )) != -1)
while ((opt = getopt_long(argc, argv,"plzcifm:", long_options, &long_index )) != -1)
{
switch (opt)
{
......@@ -57,6 +59,21 @@ int main(int argc, char* argv[])
case 'f':
full = true;
break;
case 'm':
{
string argString(optarg);
if (argString == "mul")
{
mulReplacementMode = MUL;
std::cout << "Mode: mul" << std::endl;
}
else if (argString == "shift")
{
mulReplacementMode = SHIFT;
std::cout << "Mode: shift" << std::endl;
}
break;
}
default:
std::cout << "Invalid arguments" << std::endl;
exit(1);
......@@ -81,13 +98,16 @@ int main(int argc, char* argv[])
if (canonize)
{
UnconstrainedVariableSimplifier simplifier(ctx, e);
e = simplifier.CanonizeBoundVariables(e);
ExprSimplifier simplifier(ctx);
e = simplifier.PushNegations(e);
UnconstrainedVariableSimplifier uSimplifier(ctx, e);
e = uSimplifier.CanonizeBoundVariables(e);
}
if (full)
{
ExprSimplifier simplifier(ctx, propagateUnconstrainedFlag);
ExprSimplifier simplifier(ctx, propagateUnconstrainedFlag, countVariablesLocally);
e = simplifier.Simplify(e);
}
else if (propagateUnconstrainedFlag)
......@@ -99,7 +119,7 @@ int main(int argc, char* argv[])
oldHash = e.hash();
UnconstrainedVariableSimplifier simplifier(ctx, e);
simplifier.SetCountVariablesLocally(countVariablesLocally);
//simplifier.PrintUnconstrained();
simplifier.SetMulReplacementMode(mulReplacementMode);
simplifier.SimplifyIte();
e = simplifier.GetExpr();
......@@ -112,6 +132,8 @@ int main(int argc, char* argv[])
z3::tactic(ctx, "simplify") &
z3::tactic(ctx, "elim-and") &
z3::tactic(ctx, "der") &
z3::tactic(ctx, "simplify") &
z3::tactic(ctx, "distribute-forall") &
z3::tactic(ctx, "simplify");
z3::apply_result result = derTactic(g);
......@@ -128,7 +150,7 @@ int main(int argc, char* argv[])
if (runZ3)
{
solver s(ctx);
solver s = tactic(ctx, "bv").mk_solver();
params p(ctx);
// p.set(":max_memory", 3u);
......
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