Working version

CMakeLists.txt

+#specify the version being used aswell as the language
+cmake_minimum_required(VERSION 2.6)
+#Name your project here
+project(ExprSimplifier)
+
+#set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules/")
+
+#Sends the -std=c99 flag to the gcc compiler
+add_definitions(-std=c++0x)
+#This tells CMake to fib.c and name it fibonacci
+file(GLOB Q3B_SRC
+    "*.h"
+    "*.cpp"
+)
+
+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_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -Wall")
+
+find_library(LibZ3 z3 PATHS /usr/lib DOC "z3 library")
+
+if(NOT LibZ3)
+  message(FATAL_ERROR "Library libz3 required, but not found!")
+endif(NOT LibZ3)
+
+include_directories(${LibZ3_INCLUDE_DIRS})
+set(LIBS ${LIBS} ${LibZ3})
+
+target_link_libraries(exprsimplifier ${LIBS})

UnconstrainedVariableSimplifier.h

+#ifndef UNCONSTRAINEDVARIABLESIMPLIFIER_H
+#define UNCONSTRAINEDVARIABLESIMPLIFIER_H
+
+#include "z3++.h"
+#include <map>
+#include <vector>
+#include <string>
+#include <tuple>
+
+enum BoundType { EXISTENTIAL, UNIVERSAL };
+
+class UnconstrainedVariableSimplifier
+{
+public:
+    UnconstrainedVariableSimplifier(z3::context &ctx, z3::expr expr) : expression(expr)
+    {
+      this->context = &ctx;
+
+      std::vector<BoundVar> boundVars;
+      variableCounts = countVariableOccurences(expression, boundVars).first;
+    }
+
+    void PrintUnconstrained()
+    {
+        bool allConstrained = true;
+
+        for (auto &item : variableCounts)
+        {
+            std::cout << "var " << item.first << " - " << item.second << " times" << std::endl;
+
+            if (item.second == 1)
+            {
+                allConstrained = false;
+                //std::cout << "Unconstrained variable: " << item.first << std::endl;
+            }
+        }
+        if (allConstrained) std::cout << "All variables constrained" << std::endl;
+    }
+
+    void SimplifyOnce()
+    {
+        expression = simplifyOnce(expression, {}, true);
+    }
+
+    z3::expr GetExpr() const { return expression; }
+
+    void SimplifyIte();
+
+private:
+    z3::context* context;
+    z3::expr expression;
+
+    typedef std::tuple<std::string, BoundType, int> BoundVar;
+
+    std::map<const Z3_ast, std::pair<std::map<std::string, int>, std::vector<BoundVar>>> subformulaVariableCounts;
+    std::map<const Z3_ast, int> subformulaMaxDeBruijnIndices;
+    std::map<std::string, int> variableCounts;
+
+    typedef std::map<const Z3_ast, 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>);
+
+    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);
+    BoundType getBoundType(z3::expr, const std::vector<BoundVar>&);
+
+    int getNumberOfLeadingZeroes(const z3::expr&);
+};
+
+#endif // UNCONSTRAINEDVARIABLESIMPLIFIER_H

main.cpp

+
+#include <iostream>
+#include <string>
+#include <z3++.h>
+#include <cmath>
+#include <fstream>
+#include <getopt.h>
+
+#include <chrono>
+
+#include "UnconstrainedVariableSimplifier.h"
+
+using namespace std;
+using namespace z3;
+
+using std::chrono::high_resolution_clock;
+using std::chrono::milliseconds;
+
+int main(int argc, char* argv[])
+{
+    static struct option long_options[] = {
+	{"propagate-unconstrained", no_argument, 0, 'p' },
+	{"run-z3", no_argument, 0, 'z' },
+	{0,           0,                 0,  0   }
+    };
+
+    bool propagateUnconstrainedFlag = false, runZ3 = false;
+    char* filename;
+
+    int opt = 0;
+
+    int long_index = 0;
+    while ((opt = getopt_long(argc, argv,"pz", long_options, &long_index )) != -1)
+    {
+	switch (opt)
+	{
+	case 'p':
+	    propagateUnconstrainedFlag = true;
+	    break;
+	case 'z':
+	    runZ3 = true;
+	    break;
+	default:
+	    std::cout << "Invalid arguments" << std::endl;
+	    exit(1);
+	}
+    }
+
+    if (optind < argc)
+    {
+	filename = argv[optind];
+    }
+    else
+    {
+	std::cout << "Filename required" << std::endl;
+	return 1;
+    }
+
+    z3::context ctx;
+    Z3_ast ast = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
+    expr e = to_expr(ctx, ast);
+
+    e = e.simplify();
+
+    if (propagateUnconstrainedFlag)
+    {
+	UnconstrainedVariableSimplifier simplifier(ctx, e);
+
+	//simplifier.PrintUnconstrained();
+	simplifier.SimplifyIte();
+	e = simplifier.GetExpr();
+    }
+
+    e = e.simplify();
+    //std::cout << e << std::endl;
+
+    if (runZ3)
+    {
+	solver s(ctx);
+	s.add(e);
+	std::cout << s.check() << std::endl;
+    }
+    else
+    {
+	std::cout << e << std::endl;
+    }
+}