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

A bit faster

parent 5928dbc5

UnconstrainedVariableSimplifier.cpp

+24 −62
Original line number Diff line number Diff line
@@ -28,7 +28,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e 
	Z3_ast ast = (Z3_ast)e;

	int deBruijnIndex = Z3_get_index_value(*context, ast);

	varCounts[std::get<0>(boundVars[boundVars.size() - deBruijnIndex - 1])] = 1;

	subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);

	subformulaAllConstrained[{e, boundVars}] = false;

	return varCounts;

    }

    else if (e.is_const() && !e.is_numeral())
@@ -53,7 +53,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e 
	    varCounts[ss.str()] = 1;

	}



	subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);

	subformulaAllConstrained[{e, boundVars}] = false;

	return varCounts;

    }

    else if (e.is_app())
@@ -77,13 +77,13 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e 
	    {

		auto varCountsLp = countVariableOccurences(e.arg(0), boundVars, isPositive);

		auto varCountsRp = countVariableOccurences(e.arg(1), boundVars, isPositive);

		auto varCountsLn = countVariableOccurences(e.arg(0), boundVars, !isPositive);

		auto varCountsRn = countVariableOccurences(e.arg(1), boundVars, !isPositive);

		//auto varCountsLn = countVariableOccurences(e.arg(0), boundVars, !isPositive);

		//auto varCountsRn = countVariableOccurences(e.arg(1), boundVars, !isPositive);



		addCounts(varCountsLp, varCounts);

		addCounts(varCountsRp, varCounts);

		addCounts(varCountsLn, varCounts);

		addCounts(varCountsRn, varCounts);

		//addCounts(varCountsLn, varCounts);

		//addCounts(varCountsRn, varCounts);



		subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);

		return varCounts;
@@ -104,51 +104,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e 
	    {

		auto currentVarCounts = countVariableOccurences(e.arg(i), boundVars, isPositive);



		for (auto &item : currentVarCounts)

		{

		    auto singleVarCount = varCounts.find(item.first);

		    if (singleVarCount == varCounts.end())

		    {

			varCounts[item.first] = item.second;

		    }

		    else

		    {

			if (varCounts[item.first] == 2)

			{

			    continue;

			}



			BoundType boundType = EXISTENTIAL; //not present variables are uninterpreted constants

			for (auto &boundVar : boundVars)

			{

			    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

			{

			    if (singleVarCount->second + item.second > 1)

			    {

				varCounts[item.first] = 2;

			    }

			    else

			    {

				varCounts[item.first] = singleVarCount->second + item.second;

			    }

			}

		    }

		}

		addCounts(currentVarCounts, varCounts);

	    }

	}

	else if (f.name() != NULL)
@@ -210,7 +166,8 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e 


	auto result = countVariableOccurences(e.body(), newBoundVars, isPositive);

	subformulaVariableCounts.insert({{e, isPositive}, {result, boundVars}});

	subformulaAllConstrained[{e, boundVars}] = allConstrained(varCounts);

	subformulaAllConstrained[{e, boundVars}] = allConstrained(result);



	return result;

    }
@@ -223,9 +180,9 @@ void UnconstrainedVariableSimplifier::SimplifyIte() 
{

    std::vector<BoundVar> boundVars;



    //std::cout << "Counting variables" << std::endl;

    std::cout << "Counting variables" << std::endl;

    variableCounts = countVariableOccurences(expression, boundVars, true);

    //std::cout << "Done" << std::endl;

    std::cout << "Done" << std::endl;



    bool anyUnconstrained = false;

    for (auto &var : variableCounts)
@@ -265,15 +222,17 @@ void UnconstrainedVariableSimplifier::SimplifyIte() 
	// std::cout << "------------------------------------" << std::endl;

	//expression = simplifier.PushNegations(expression);



	subformulaVariableCounts.clear();

	//std::vector<BoundVar> boundVars;

	//variableCounts = countVariableOccurences(expression, boundVars, true);

	//subformulaVariableCounts.clear();

	std::vector<BoundVar> boundVars;

	std::cout << "Counting variables" << std::endl;

	variableCounts = countVariableOccurences(expression, boundVars, true);

	std::cout << "Done" << std::endl;



	trueSimplificationCache.clear();

	falseSimplificationCache.clear();

	//trueSimplificationCache.clear();

	//falseSimplificationCache.clear();



	i++;

	break;

	PrintUnconstrained();

    }



    //PrintUnconstrained();
@@ -1099,8 +1058,11 @@ bool UnconstrainedVariableSimplifier::allConstrained(std::map<std::string, int> 
{

    for (auto &var : varCounts)

    {

	if (var.second == 1) return true;

	if (var.second == 1)

	{

	    return false;

	}

    }



    return false;

    return true;

}

main.cpp

+5 −6
Original line number Diff line number Diff line
@@ -140,9 +140,9 @@ int main(int argc, char* argv[]) 
    {

	unsigned oldHash = 0;



	do

	{

	    oldHash = e.hash();

	//do

	//{

	//    oldHash = e.hash();

	    UnconstrainedVariableSimplifier simplifier(ctx, e);

	    simplifier.SetCountVariablesLocally(countVariablesLocally);

	    simplifier.SetMulReplacementMode(mulReplacementMode);
@@ -150,9 +150,8 @@ int main(int argc, char* argv[]) 
	    simplifier.SetDagCounting(dagCounting);

	    simplifier.SimplifyIte();

	    e = simplifier.GetExpr();

	    e = e.simplify();



	    if (inprocess)

	    /*    if (inprocess)

	    {

		z3::goal g(ctx);

		g.add(e);
@@ -171,7 +170,7 @@ int main(int argc, char* argv[]) 
		z3::goal simplified = result[0];

		e = simplified.as_expr();

	    }

	} while (oldHash != e.hash());

	    } while (oldHash != e.hash()); */

    }



    e = e.simplify();