Add full simplifier

ExprSimplifier.h

+#ifndef EXPRSIMPLIFIER_H
+#define EXPRSIMPLIFIER_H
+#include "z3++.h"
+#include <map>
+#include <set>
+
+class ExprSimplifier
+{
+public:
+ExprSimplifier(z3::context &ctx) : propagateUnconstrained(false), countUnconstrainedLocally(false)
+    {
+	this->context = &ctx;
+    }
+
+ExprSimplifier(z3::context &ctx, bool propagateUnconstrained) : propagateUnconstrained(propagateUnconstrained)
+    {
+	this->context = &ctx;
+    }
+
+ExprSimplifier(z3::context &ctx, bool propagateUnconstrained, bool countUnconstrainedLocally) : propagateUnconstrained(propagateUnconstrained), countUnconstrainedLocally(countUnconstrainedLocally)
+    {
+	this->context = &ctx;
+    }
+
+    z3::expr Simplify (z3::expr);
+    z3::expr ApplyConstantEqualities(const z3::expr&);
+    z3::expr PushQuantifierIrrelevantSubformulas(const z3::expr&);
+    z3::expr RefinedPushQuantifierIrrelevantSubformulas(const z3::expr&);
+    z3::expr negate(const z3::expr&);
+    z3::expr PushNegations(const z3::expr&);
+    z3::expr PropagateInequalities(z3::expr);
+    z3::expr UnflattenAddition(const z3::expr&);
+    z3::expr CanonizeBoundVariables(const z3::expr&);
+
+private:
+    std::map<const Z3_ast, z3::expr> refinedPushIrrelevantCache;
+    std::map<const Z3_ast, z3::expr> pushIrrelevantCache;
+    std::map<std::tuple<const Z3_ast, int, int>, z3::expr> decreaseDeBruijnCache;
+    std::map<std::tuple<const Z3_ast, int, int>, bool> isRelevantCache;
+    std::map<const Z3_ast, z3::expr> pushNegationsCache;
+    std::map<const Z3_ast, z3::expr> unflattenAdditionCache;
+    std::set<Z3_ast> seenAddends;
+    void clearCaches();
+
+    z3::context* context;
+    bool getSubstitutableEquality(const z3::expr&, z3::expr*, z3::expr*);
+    z3::expr decreaseDeBruijnIndices(const z3::expr&, int, int);
+    bool isRelevant(const z3::expr&, int, int);
+    z3::expr mk_or(z3::expr_vector&);
+    z3::expr mk_and(z3::expr_vector&);
+    z3::expr applyDer(const z3::expr&);
+    bool isVar(z3::expr);
+    bool propagateUnconstrained;
+    bool countUnconstrainedLocally;
+
+    int lastBound = 0;
+};
+
+
+#endif // EXPRSIMPLIFIER_H

UnconstrainedVariableSimplifier.cpp

@@ -384,7 +384,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 	    else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1)))
 	    {
 //		std::cout << "unconstrained" << e << std::endl;
-		auto boundType = getBoundType(e.arg(0), boundVars);
+		auto boundType = getBoundType(e.arg(1), boundVars);
 		if (boundType == EXISTENTIAL)
 		{
 		    return isPositive ? context->bool_val(true) : e.arg(0);
@@ -413,7 +413,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 	    else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1)))
 	    {
 //		std::cout << "unconstrained" << e << std::endl;
-		auto boundType = getBoundType(e.arg(0), boundVars);
+		auto boundType = getBoundType(e.arg(1), boundVars);
 		if (boundType == EXISTENTIAL)
 		{
 		    return isPositive ? e.arg(1) : context->bool_val(false);
@@ -924,6 +924,7 @@ BoundType UnconstrainedVariableSimplifier::getBoundType(expr e, const std::vecto
 	}
     }
 
+    std::cout << e << std::endl;
     assert(false);
 }
 

main.cpp

@@ -9,6 +9,7 @@
 #include <chrono>
 
 #include "UnconstrainedVariableSimplifier.h"
+#include "ExprSimplifier.h"
 
 using namespace std;
 using namespace z3;
@@ -24,16 +25,17 @@ int main(int argc, char* argv[])
 	{"canonize", no_argument, 0, 'c' },
 	{"run-z3", no_argument, 0, 'z' },
 	{"inprocess", no_argument, 0, 'i' },
+	{"full", no_argument, 0, 'f' },
 	{0,           0,                 0,  0   }
     };
 
-    bool propagateUnconstrainedFlag = false, runZ3 = false, canonize = false, countVariablesLocally = false, inprocess = false;
+    bool propagateUnconstrainedFlag = false, runZ3 = false, canonize = false, countVariablesLocally = false, inprocess = false, full = false;
     char* filename;
 
     int opt = 0;
 
     int long_index = 0;
-    while ((opt = getopt_long(argc, argv,"plzci", long_options, &long_index )) != -1)
+    while ((opt = getopt_long(argc, argv,"plzcif", long_options, &long_index )) != -1)
     {
 	switch (opt)
 	{
@@ -52,6 +54,9 @@ int main(int argc, char* argv[])
 	case 'c':
 	    canonize = true;
 	    break;
+	case 'f':
+	    full = true;
+	    break;
 	default:
 	    std::cout << "Invalid arguments" << std::endl;
 	    exit(1);
@@ -80,7 +85,12 @@ int main(int argc, char* argv[])
 	e = simplifier.CanonizeBoundVariables(e);
     }
 
-    if (propagateUnconstrainedFlag)
+    if (full)
+    {
+	ExprSimplifier simplifier(ctx, propagateUnconstrainedFlag);
+	e = simplifier.Simplify(e);
+    }
+    else if (propagateUnconstrainedFlag)
     {
 	unsigned oldHash = 0;