Fix CHCSmtLib2Interface

libsmtutil/CHCSmtLib2Interface.cpp

@@ -53,8 +53,7 @@ void CHCSmtLib2Interface::reset()
 	m_accumulatedOutput.clear();
 	m_variables.clear();
 	m_unhandledQueries.clear();
-	if (m_queryTimeout)
+	m_sortNames.clear();
-		write("(set-option :timeout " + to_string(*m_queryTimeout) + ")");
 }
 
 void CHCSmtLib2Interface::registerRelation(Expression const& _expr)
@@ -64,27 +63,25 @@ void CHCSmtLib2Interface::registerRelation(Expression const& _expr)
 	if (!m_variables.count(_expr.name))
 	{
 		auto fSort = dynamic_pointer_cast<FunctionSort>(_expr.sort);
-		string domain = m_smtlib2->toSmtLibSort(fSort->domain);
+		string domain = toSmtLibSort(fSort->domain);
 		// Relations are predicates which have implicit codomain Bool.
 		m_variables.insert(_expr.name);
 		write(
-			"(declare-rel |" +
+			"(declare-fun |" +
 			_expr.name +
 			"| " +
 			domain +
-			")"
+			" Bool)"
 		);
 	}
 }
 
-void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& _name)
+void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /*_name*/)
 {
 	write(
-		"(rule (! " +
+		"(assert\n(forall " + forall() + "\n" +
 		m_smtlib2->toSExpr(_expr) +
-		" :named " +
+		"))\n\n"
-		_name +
-		"))"
 	);
 }
 
@@ -92,22 +89,29 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expre
 {
 	string accumulated{};
 	swap(m_accumulatedOutput, accumulated);
-	for (auto const& var: m_smtlib2->variables())
+	solAssert(m_smtlib2, "");
-		declareVariable(var.first, var.second);
+	writeHeader();
+	for (auto const& [type, decl]: m_smtlib2->userSorts())
+		write(decl);
 	m_accumulatedOutput += accumulated;
 
+	string queryRule = "(assert\n(forall " + forall() + "\n" +
+		"(=> " + _block.name + " false)"
+		"))";
 	string response = querySolver(
 		m_accumulatedOutput +
-		"\n(query " + _block.name + " :print-certificate true)"
+		queryRule +
+		"\n(check-sat)"
 	);
+	swap(m_accumulatedOutput, accumulated);
 
 	CheckResult result;
 	// TODO proper parsing
-	if (boost::starts_with(response, "sat\n"))
+	if (boost::starts_with(response, "sat"))
-		result = CheckResult::SATISFIABLE;
-	else if (boost::starts_with(response, "unsat\n"))
 		result = CheckResult::UNSATISFIABLE;
-	else if (boost::starts_with(response, "unknown\n"))
+	else if (boost::starts_with(response, "unsat"))
+		result = CheckResult::SATISFIABLE;
+	else if (boost::starts_with(response, "unknown"))
 		result = CheckResult::UNKNOWN;
 	else
 		result = CheckResult::ERROR;
@@ -124,10 +128,46 @@ void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const
 	else if (!m_variables.count(_name))
 	{
 		m_variables.insert(_name);
-		write("(declare-var |" + _name + "| " + m_smtlib2->toSmtLibSort(*_sort) + ')');
+		write("(declare-var |" + _name + "| " + toSmtLibSort(*_sort) + ')');
 	}
 }
 
+string CHCSmtLib2Interface::toSmtLibSort(Sort const& _sort)
+{
+	if (!m_sortNames.count(&_sort))
+		m_sortNames[&_sort] = m_smtlib2->toSmtLibSort(_sort);
+	return m_sortNames.at(&_sort);
+}
+
+string CHCSmtLib2Interface::toSmtLibSort(vector<SortPointer> const& _sorts)
+{
+	string ssort("(");
+	for (auto const& sort: _sorts)
+		ssort += toSmtLibSort(*sort) + " ";
+	ssort += ")";
+	return ssort;
+}
+
+void CHCSmtLib2Interface::writeHeader()
+{
+	if (m_queryTimeout)
+		write("(set-option :timeout " + to_string(*m_queryTimeout) + ")");
+	write("(set-logic HORN)\n");
+}
+
+string CHCSmtLib2Interface::forall()
+{
+	string vars("(");
+	for (auto const& [name, sort]: m_smtlib2->variables())
+	{
+		solAssert(sort, "");
+		if (sort->kind != Kind::Function)
+			vars += " (" + name + " " + toSmtLibSort(*sort) + ")";
+	}
+	vars += ")";
+	return vars;
+}
+
 void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
 {
 	smtAssert(_sort, "");
@@ -137,8 +177,8 @@ void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const
 	{
 		auto fSort = dynamic_pointer_cast<FunctionSort>(_sort);
 		smtAssert(fSort->codomain, "");
-		string domain = m_smtlib2->toSmtLibSort(fSort->domain);
+		string domain = toSmtLibSort(fSort->domain);
-		string codomain = m_smtlib2->toSmtLibSort(*fSort->codomain);
+		string codomain = toSmtLibSort(*fSort->codomain);
 		m_variables.insert(_name);
 		write(
 			"(declare-fun |" +

libsmtutil/CHCSmtLib2Interface.h

@@ -53,6 +53,12 @@ public:
 	SMTLib2Interface* smtlib2Interface() const { return m_smtlib2.get(); }
 
 private:
+	std::string toSmtLibSort(Sort const& _sort);
+	std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
+
+	void writeHeader();
+	std::string forall();
+
 	void declareFunction(std::string const& _name, SortPointer const& _sort);
 
 	void write(std::string _data);
@@ -70,6 +76,8 @@ private:
 	std::vector<std::string> m_unhandledQueries;
 
 	frontend::ReadCallback::Callback m_smtCallback;
+
+	std::map<Sort const*, std::string> m_sortNames;
 };
 
 }

libsmtutil/SMTLib2Interface.cpp

@@ -23,6 +23,8 @@
 #include <boost/algorithm/string/join.hpp>
 #include <boost/algorithm/string/predicate.hpp>
 
+#include <range/v3/algorithm/find_if.hpp>
+
 #include <array>
 #include <fstream>
 #include <iostream>
@@ -231,14 +233,15 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 	{
 		auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
 		string tupleName = "|" + tupleSort.name + "|";
-		if (!m_userSorts.count(tupleName))
+		auto isName = [&](auto entry) { return entry.first == tupleName; };
+		if (ranges::find_if(m_userSorts, isName) == m_userSorts.end())
 		{
-			m_userSorts.insert(tupleName);
 			string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName);
 			smtAssert(tupleSort.members.size() == tupleSort.components.size(), "");
 			for (unsigned i = 0; i < tupleSort.members.size(); ++i)
 				decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")";
 			decl += "))))";
+			m_userSorts.emplace_back(tupleName, decl);
 			write(decl);
 		}
 

libsmtutil/SMTLib2Interface.h

@@ -66,6 +66,8 @@ public:
 
 	std::map<std::string, SortPointer> variables() { return m_variables; }
 
+	std::vector<std::pair<std::string, std::string>>const& userSorts() const { return m_userSorts; }
+
 private:
 	void declareFunction(std::string const& _name, SortPointer const& _sort);
 
@@ -79,7 +81,7 @@ private:
 
 	std::vector<std::string> m_accumulatedOutput;
 	std::map<std::string, SortPointer> m_variables;
-	std::set<std::string> m_userSorts;
+	std::vector<std::pair<std::string, std::string>> m_userSorts;
 
 	std::map<util::h256, std::string> m_queryResponses;
 	std::vector<std::string> m_unhandledQueries;

libsolidity/formal/CHC.cpp

@@ -946,7 +946,6 @@ void CHC::resetSourceAnalysis()
 	if (!usesZ3)
 	{
 		auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
-		smtlib2Interface->reset();
 		solAssert(smtlib2Interface, "");
 		m_context.setSolver(smtlib2Interface->smtlib2Interface());
 	}

libsolidity/formal/SymbolicTypes.cpp

@@ -118,7 +118,7 @@ SortPointer smtSort(frontend::Type const& _type)
 			else
 				tupleName = arrayType->baseType()->toString(true);
 
-			tupleName += "[]";
+			tupleName += "_array";
 		}
 		else
 			tupleName = _type.toString(true);