Merge pull request #5416 from ethereum/develop

Merge develop into release for 0.5.0

1 files changed, 16 insertions, 7 deletions

diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 16796684..af1cc8e4 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -39,7 +39,7 @@ namespace smt
 
 enum class CheckResult
 {
-	SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR
+	SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR
 };
 
 enum class Sort
@@ -171,8 +171,8 @@ public:
 		}
 	}
 
-	std::string const name;
-	std::vector<Expression> const arguments;
+	std::string name;
+	std::vector<Expression> arguments;
 	Sort sort;
 
 private:
@@ -199,8 +199,10 @@ public:
 	virtual void push() = 0;
 	virtual void pop() = 0;
 
-	virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
+	virtual void declareFunction(std::string _name, Sort _domain, Sort _codomain) = 0;
+	Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
 	{
+		declareFunction(_name, _domain, _codomain);
 		solAssert(_domain == Sort::Int, "Function sort not supported.");
 		// Subclasses should do something here
 		switch (_codomain)
@@ -214,14 +216,18 @@ public:
 			break;
 		}
 	}
-	virtual Expression newInteger(std::string _name)
+	virtual void declareInteger(std::string _name) = 0;
+	Expression newInteger(std::string _name)
 	{
 		// Subclasses should do something here
+		declareInteger(_name);
 		return Expression(std::move(_name), {}, Sort::Int);
 	}
-	virtual Expression newBool(std::string _name)
+	virtual void declareBool(std::string _name) = 0;
+	Expression newBool(std::string _name)
 	{
 		// Subclasses should do something here
+		declareBool(_name);
 		return Expression(std::move(_name), {}, Sort::Bool);
 	}
 
@@ -231,8 +237,11 @@ public:
 	/// is available. Throws SMTSolverError on error.
 	virtual std::pair<CheckResult, std::vector<std::string>>
 	check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
-};
 
+protected:
+	// SMT query timeout in milliseconds.
+	static int const queryTimeout = 10000;
+};
 
 }
 }