Function inlineLetExpressions

libsmtutil/CHCSmtLib2Interface.cpp:534–597

};

void inlineLetExpressions(SMTLib2Expression& _expr, LetBindings& _bindings)
{
	if (isAtom(_expr))
	{
		auto const& atom = asAtom(_expr);
		if (_bindings.has(atom))
			_expr = _bindings[atom];
		return;
	}
	auto& subexprs = asSubExpressions(_expr);
	smtSolverInteractionRequire(!subexprs.empty(), "Invalid let expression");
	auto const& first = subexprs.at(0);
	if (isAtom(first) && asAtom(first) == "let")
	{
		smtSolverInteractionRequire(subexprs.size() == 3, "Invalid let expression");
		smtSolverInteractionRequire(!isAtom(subexprs[1]), "Invalid let expression");
		auto& bindingExpressions = asSubExpressions(subexprs[1]);
		// process new bindings
		std::vector<std::pair<std::string, SMTLib2Expression>> newBindings;
		for (auto& binding: bindingExpressions)
		{
			smtSolverInteractionRequire(!isAtom(binding), "Invalid let expression");
			auto& bindingPair = asSubExpressions(binding);
			smtSolverInteractionRequire(bindingPair.size() == 2, "Invalid let expression");
			smtSolverInteractionRequire(isAtom(bindingPair.at(0)), "Invalid let expression");
			inlineLetExpressions(bindingPair.at(1), _bindings);
			newBindings.emplace_back(asAtom(bindingPair.at(0)), bindingPair.at(1));
		}
		_bindings.pushScope();
		for (auto&& [name, expr]: newBindings)
			_bindings.addBinding(std::move(name), std::move(expr));

		newBindings.clear();

		// get new subexpression
		inlineLetExpressions(subexprs.at(2), _bindings);
		// remove the new bindings
		_bindings.popScope();

		// update the expression
		auto tmp = std::move(subexprs.at(2));
		_expr = std::move(tmp);
		return;
	}
	else if (isAtom(first) && (asAtom(first) == "forall" || asAtom(first) == "exists"))
	{
		// A little hack to ensure quantified variables are not substituted because of some outer let definition:
		// We define the current binding of the variable to itself, before we recurse in to subterm
		smtSolverInteractionRequire(subexprs.size() == 3, "Invalid let expression");
		_bindings.pushScope();
		for (auto const& sortedVar: asSubExpressions(subexprs.at(1)))
		{
			auto const& varNameExpr = asSubExpressions(sortedVar).at(0);
			_bindings.addBinding(asAtom(varNameExpr), varNameExpr);
		}
		inlineLetExpressions(subexprs.at(2), _bindings);
		_bindings.popScope();
		return;