Local counting & early break

UnconstrainedVariableSimplifier.cpp

@@ -4,11 +4,11 @@
 using namespace std;
 using namespace z3;
 
-pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccurences(z3::expr e, vector<BoundVar> boundVars)
+pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccurences(z3::expr e, vector<BoundVar> boundVars, bool isPositive=true)
 {
     map<string, int> varCounts;
 
-    auto item = subformulaVariableCounts.find((Z3_ast)e);
+    auto item = subformulaVariableCounts.find({(Z3_ast)e, isPositive});
     if (item != subformulaVariableCounts.end() && (subformulaMaxDeBruijnIndices[(Z3_ast)e] == -1 || (item->second).second == boundVars))
     {
 	//probably can be return {varCounts, subformulaMaxDeBruijnIndices[(Z3_ast)e]};
@@ -57,6 +57,13 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
 
 	if (num != 0)
 	{
+	    auto decl_kind = e.decl().decl_kind();
+
+	    if (decl_kind == Z3_OP_NOT)
+	    {
+		return countVariableOccurences(e.arg(0), boundVars, !isPositive);
+	    }
+
 	    for (unsigned i = 0; i < num; i++)
 	    {
 		auto currentVarCounts = countVariableOccurences(e.arg(i), boundVars);
@@ -70,13 +77,34 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
 		    }
 		    else
 		    {
-			if (singleVarCount->second + item.second > 1)
+			BoundType boundType;
+			for (auto &boundVar : boundVars)
 			{
-			    varCounts[item.first] = 2;
+			    if (std::get<0>(boundVar) == item.first)
+			    {
+				boundType = std::get<1>(boundVar);
+				break;
+			    }
+			}
+
+			if (countVariablesLocally &&
+			    ((boundType == EXISTENTIAL && decl_kind == Z3_OP_OR && isPositive) ||
+			     (boundType == EXISTENTIAL && decl_kind == Z3_OP_AND && !isPositive) ||
+			     (boundType == UNIVERSAL && decl_kind == Z3_OP_AND && isPositive) ||
+			     (boundType == UNIVERSAL && decl_kind == Z3_OP_OR && !isPositive)))
+			{
+			    varCounts[item.first] = max(singleVarCount->second, item.second);
 			}
 			else
 			{
-			    varCounts[item.first] = singleVarCount->second + item.second;
+			    if (singleVarCount->second + item.second > 1)
+			    {
+				varCounts[item.first] = 2;
+			    }
+			    else
+			    {
+				varCounts[item.first] = singleVarCount->second + item.second;
+			    }
 			}
 		    }
 		}
@@ -105,7 +133,6 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
 	    }
 	}
 
-	subformulaVariableCounts.insert({(Z3_ast)e, {varCounts, boundVars}});
 	subformulaMaxDeBruijnIndices.insert({(Z3_ast)e, maxDeBruijnIndex});
 	return {varCounts, maxDeBruijnIndex};
     }
@@ -115,7 +142,7 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
 	int numBound = Z3_get_quantifier_num_bound(*context, ast);
 	BoundType boundType;
 
-	if (true) //isPositive
+	if (isPositive)
 	{
 	    boundType = Z3_is_quantifier_forall(*context, ast) ? UNIVERSAL : EXISTENTIAL;
 	}
@@ -149,7 +176,7 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
 	}
 
 	auto result = countVariableOccurences(e.body(), boundVars);
-	subformulaVariableCounts.insert({(Z3_ast)e, {result.first, boundVars}});
+	subformulaVariableCounts.insert({{(Z3_ast)e, isPositive}, {result.first, boundVars}});
 	subformulaMaxDeBruijnIndices.insert({(Z3_ast)e, result.second});
 	return result;
     }
@@ -160,6 +187,20 @@ pair<map<string, int>, int> UnconstrainedVariableSimplifier::countVariableOccure
 
 void UnconstrainedVariableSimplifier::SimplifyIte()
 {
+    bool anyUnconstrained = false;
+    for (auto &var : variableCounts)
+    {
+	if (var.second == 1)
+	{
+	    anyUnconstrained = true;
+	}
+    }
+
+    if (!anyUnconstrained)
+    {
+	return;
+    }
+
     unsigned oldHash = 0;
 
     //expression = expression.simplify();

UnconstrainedVariableSimplifier.h

@@ -17,7 +17,7 @@ public:
       this->context = &ctx;
 
       std::vector<BoundVar> boundVars;
-      variableCounts = countVariableOccurences(expression, boundVars).first;
+      variableCounts = countVariableOccurences(expression, boundVars, true).first;
     }
 
     void PrintUnconstrained()
@@ -47,13 +47,18 @@ public:
     void SimplifyIte();
     z3::expr CanonizeBoundVariables(const z3::expr&);
 
+    void SetCountVariablesLocally(bool countVariablesLocally)
+    {
+	this->countVariablesLocally = countVariablesLocally;
+    }
+
 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<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::map<std::string, int> variableCounts;
 
@@ -62,7 +67,7 @@ private:
     cacheMapType trueSimplificationCache;
     cacheMapType falseSimplificationCache;
 
-    std::pair<std::map<std::string, int>, int> countVariableOccurences(z3::expr, std::vector<BoundVar>);
+    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>&);
@@ -72,6 +77,8 @@ private:
 
     int getNumberOfLeadingZeroes(const z3::expr&);
     int lastBound = 0;
+
+    bool countVariablesLocally = false;
 };
 
 #endif // UNCONSTRAINEDVARIABLESIMPLIFIER_H

main.cpp

@@ -20,24 +20,28 @@ int main(int argc, char* argv[])
 {
     static struct option long_options[] = {
 	{"propagate-unconstrained", no_argument, 0, 'p' },
+	{"count-locally", no_argument, 0, 'l' },
 	{"canonize", no_argument, 0, 'c' },
 	{"run-z3", no_argument, 0, 'z' },
 	{0,           0,                 0,  0   }
     };
 
-    bool propagateUnconstrainedFlag = false, runZ3 = false, canonize = false;
+    bool propagateUnconstrainedFlag = false, runZ3 = false, canonize = false, countVariablesLocally = false;
     char* filename;
 
     int opt = 0;
 
     int long_index = 0;
-    while ((opt = getopt_long(argc, argv,"pzc", long_options, &long_index )) != -1)
+    while ((opt = getopt_long(argc, argv,"plzc", long_options, &long_index )) != -1)
     {
 	switch (opt)
 	{
 	case 'p':
 	    propagateUnconstrainedFlag = true;
 	    break;
+	case 'l':
+	    countVariablesLocally = true;
+	    break;
 	case 'z':
 	    runZ3 = true;
 	    break;
@@ -75,6 +79,7 @@ int main(int argc, char* argv[])
     if (propagateUnconstrainedFlag)
     {
 	UnconstrainedVariableSimplifier simplifier(ctx, e);
+	simplifier.SetCountVariablesLocally(countVariablesLocally);
 	//simplifier.PrintUnconstrained();
 	simplifier.SimplifyIte();
 	e = simplifier.GetExpr();