From a3f999a13e075f639dda30362a6ed37d4caa2dec Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Sun, 20 Mar 2022 22:33:22 +0100
Subject: [PATCH] temp

---
 libsolutil/BooleanLP.cpp                      | 10 ++++++++--
 libsolutil/CDCL.cpp                           |  4 ++--
 libyul/optimiser/ReasoningBasedSimplifier.cpp |  2 ++
 test/libsolutil/BooleanLP.cpp                 |  8 ++++++++
 4 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index 99c54d734..295d7d3c9 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -207,7 +207,10 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 	cout << "--------------" << endl;
 
 	if (state().infeasible)
+	{
+		cout << "----->>>>> unsatisfiable" << endl;
 		return make_pair(CheckResult::UNSATISFIABLE, vector<string>{});
+	}
 
 	std::vector<std::string> booleanVariables;
 	std::vector<Clause> clauses = state().clauses;
@@ -227,7 +230,10 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 	//cout << "Boolean variables:" << joinHumanReadable(booleanVariables) << endl;
 	//cout << "Running LP solver on fixed constraints." << endl;
 	if (m_lpSolver.check(lpState).first == LPResult::Infeasible)
+	{
+		cout << "----->>>>> unsatisfiable" << endl;
 		return {CheckResult::UNSATISFIABLE, {}};
+	}
 
 	auto theorySolver = [&](map<size_t, bool> const& _booleanAssignment) -> optional<Clause>
 	{
@@ -263,12 +269,12 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 	auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver}.solve();
 	if (!optionalModel)
 	{
-		//cout << "==============> CDCL final result: unsatisfiable." << endl;
+		cout << "==============> CDCL final result: unsatisfiable." << endl;
 		return {CheckResult::UNSATISFIABLE, {}};
 	}
 	else
 	{
-		//cout << "==============> CDCL final result: SATisfiable / UNKNOWN." << endl;
+		cout << "==============> CDCL final result: SATisfiable / UNKNOWN." << endl;
 		// TODO should be "unknown" later on
 		//return {CheckResult::SATISFIABLE, {}};
 		return {CheckResult::UNKNOWN, {}};
diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp
index f72b53e05..d58224247 100644
--- a/libsolutil/CDCL.cpp
+++ b/libsolutil/CDCL.cpp
@@ -69,8 +69,8 @@ optional<CDCL::Model> CDCL::solve()
 			cancelUntil(backtrackLevel);
 			solAssert(!learntClause.empty());
 			solAssert(!isAssigned(learntClause.front()));
-			for (size_t i = 1; i < learntClause.size(); i++)
-				solAssert(isAssignedFalse(learntClause.at(i)));
+//			for (size_t i = 1; i < learntClause.size(); i++)
+//				solAssert(value(learntClause[i]) == TriState{false});
 
 			addClause(move(learntClause));
 			enqueue(m_clauses.back()->front(), &(*m_clauses.back()));
diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp
index a420b2020..189140ba9 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.cpp
+++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp
@@ -85,6 +85,7 @@ void ReasoningBasedSimplifier::operator()(If& _if)
 	{
 		cout << "Checking if condition  can be true" << endl;
 		m_solver->push();
+		// TODO change this to >= 1 for simplicity?
 		m_solver->addAssertion(condition != constantValue(0));
 		cout << "  running check" << endl;
 		CheckResult result2 = m_solver->check({}).first;
@@ -99,6 +100,7 @@ void ReasoningBasedSimplifier::operator()(If& _if)
 			// Nothing left to be done.
 			return;
 		}
+		cout << " unknown :(" << endl;
 	}
 
 	m_solver->push();
diff --git a/test/libsolutil/BooleanLP.cpp b/test/libsolutil/BooleanLP.cpp
index eae7b2818..927212ef4 100644
--- a/test/libsolutil/BooleanLP.cpp
+++ b/test/libsolutil/BooleanLP.cpp
@@ -344,6 +344,14 @@ BOOST_AUTO_TEST_CASE(pure_boolean)
 	infeasible();
 }
 
+BOOST_AUTO_TEST_CASE(more_test)
+{
+	Expression x = variable("x");
+	solver.addAssertion(x == 0);
+	solver.addAssertion(x != 0);
+	infeasible();
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }