Commit 6ec5f9ea authored Apr 16, 2017 by Martin Jonas

Change the output format.

parent cec68bcd

ExprSimplifier.cpp

+1 −1

Original line number	Diff line number	Diff line
		@@ -98,7 +98,7 @@ expr ExprSimplifier::Simplify(expr expression)
		if (DEBUG)
		{
		UnconstrainedVariableSimplifier unconstrainedSimplifier(*context, expression);
		unconstrainedSimplifier.PrintUnconstrained();
		//unconstrainedSimplifier.PrintUnconstrained();
		}

		pushNegationsCache.clear();

UnconstrainedVariableSimplifier.cpp

+2 −2

Original line number	Diff line number	Diff line
		@@ -229,7 +229,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte()

		if (!anyUnconstrained)
		{
		PrintUnconstrained();
		//PrintUnconstrained();
		return;
		}

		@@ -265,7 +265,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
		i++;
		}

		PrintUnconstrained();
		//PrintUnconstrained();
		}

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

main.cpp

+1 −0

Original line number	Diff line number	Diff line
		@@ -169,5 +169,6 @@ 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;
		}
		}