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

Merge branch 'master' of gitlab.fi.muni.cz:xjonas/BVExprSimplifier

parents 959fc018 6f21aca5

UnconstrainedVariableSimplifier.cpp

+24 −3
Original line number Diff line number Diff line
@@ -28,6 +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);

	return varCounts;

    }

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

	}



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

	return varCounts;

    }

    else if (e.is_app())
@@ -68,6 +70,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e 
		auto result = countVariableOccurences(e.arg(0), boundVars, !isPositive);

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



		subformulaAllConstrained[{e, boundVars}] = subformulaAllConstrained[{e.arg(0), boundVars}];

		return result;

	    }

	    else if (decl_kind == Z3_OP_IFF || (decl_kind == Z3_OP_EQ && e.arg(0).is_bool()))
@@ -82,6 +85,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e 
		addCounts(varCountsLn, varCounts);

		addCounts(varCountsRn, varCounts);



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

		return varCounts;

	    }

	    else if (decl_kind == Z3_OP_IMPLIES)
@@ -92,6 +96,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e 
		addCounts(varCountsL, varCounts);

		addCounts(varCountsR, varCounts);



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

		return varCounts;

	    }
@@ -159,6 +164,7 @@ map<string, int> UnconstrainedVariableSimplifier::countVariableOccurences(expr e 
	}



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

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

	return varCounts;

    }

    else if(e.is_quantifier())
@@ -204,6 +210,7 @@ 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);

	return result;

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

    std::vector<BoundVar> boundVars;



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

    variableCounts = countVariableOccurences(expression, boundVars, true);

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



    bool anyUnconstrained = false;

    for (auto &var : variableCounts)
@@ -242,6 +251,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte() 


    while (oldHash != expression.hash())

    {

	//std::cout << "Simplify once" << std::endl;

	//std::cout << expression << std::endl;

	oldHash = expression.hash();
@@ -256,13 +266,14 @@ void UnconstrainedVariableSimplifier::SimplifyIte() 
	//expression = simplifier.PushNegations(expression);



	subformulaVariableCounts.clear();

	std::vector<BoundVar> boundVars;

	variableCounts = countVariableOccurences(expression, boundVars, true);

	//std::vector<BoundVar> boundVars;

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



	trueSimplificationCache.clear();

	falseSimplificationCache.clear();



	i++;

	break;

    }



    //PrintUnconstrained();
@@ -270,7 +281,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte() 


z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<BoundVar> boundVars, bool isPositive = true)

{

    if (e.is_var() || e.is_numeral())

    if (e.is_var() || e.is_numeral() || subformulaAllConstrained[{e, boundVars}])

    {

	return e;

    }
@@ -1083,3 +1094,13 @@ void UnconstrainedVariableSimplifier::addCounts(std::map<std::string, int> &from 
	}

    }

}



bool UnconstrainedVariableSimplifier::allConstrained(std::map<std::string, int> &varCounts)

{

    for (auto &var : varCounts)

    {

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

    }



    return false;

}

UnconstrainedVariableSimplifier.h

+2 −0
Original line number Diff line number Diff line
@@ -146,6 +146,7 @@ private: 
    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, std::vector<BoundVar>>, int> subformulaMaxDeBruijnIndices;

    std::map<std::string, int> variableCounts;

    std::unordered_map<std::pair<z3::expr, std::vector<BoundVar>>, bool> subformulaAllConstrained;



    typedef std::unordered_map<z3::expr, std::pair<z3::expr, const std::vector<BoundVar>>> cacheMapType;
@@ -154,6 +155,7 @@ private: 


    std::map<std::string, int> countVariableOccurences(z3::expr, std::vector<BoundVar>&, bool);

    void addCounts(std::map<std::string, int>&, std::map<std::string, int>&);

    bool allConstrained(std::map<std::string, int>&);

    int getMaxLevel(z3::expr, const std::vector<BoundVar>&, bool);



    z3::expr simplifyOnce(z3::expr, std::vector<BoundVar>, bool);

main.cpp

+2 −0
Original line number Diff line number Diff line
@@ -150,6 +150,7 @@ int main(int argc, char* argv[]) 
	    simplifier.SetDagCounting(dagCounting);

	    simplifier.SimplifyIte();

	    e = simplifier.GetExpr();

	    e = e.simplify();



	    if (inprocess)

	    {
@@ -191,6 +192,7 @@ int main(int argc, char* argv[]) 
    {

        std::cout << "(set-logic BV)" << std::endl;

	//std::cout << s.to_smt2() << std::endl;



	std::cout << s << std::endl;

	std::cout << "(check-sat)" << std::endl;

    }