aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/SMTChecker.cpp87
-rw-r--r--libsolidity/formal/SMTChecker.h15
-rw-r--r--libsolidity/formal/SSAVariable.cpp73
-rw-r--r--libsolidity/formal/SSAVariable.h88
-rw-r--r--libsolidity/formal/SymbolicIntVariable.cpp56
-rw-r--r--libsolidity/formal/SymbolicIntVariable.h50
-rw-r--r--libsolidity/formal/SymbolicVariable.cpp40
-rw-r--r--libsolidity/formal/SymbolicVariable.h69
8 files changed, 414 insertions, 64 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index a64024b3..1da5b291 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -23,6 +23,8 @@
#include <libsolidity/formal/SMTLib2Interface.h>
#endif
+#include <libsolidity/formal/SSAVariable.h>
+#include <libsolidity/formal/SymbolicIntVariable.h>
#include <libsolidity/formal/VariableUsage.h>
#include <libsolidity/interface/ErrorReporter.h>
@@ -69,8 +71,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
// We only handle local variables, so we clear at the beginning of the function.
// If we add storage variables, those should be cleared differently.
m_interface->reset();
- m_currentSequenceCounter.clear();
- m_nextFreeSequenceCounter.clear();
+ m_variables.clear();
m_pathConditions.clear();
m_conditionalExecutionHappened = false;
initializeLocalVariables(_function);
@@ -91,14 +92,18 @@ bool SMTChecker::visit(IfStatement const& _node)
checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
- auto countersEndFalse = m_currentSequenceCounter;
auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
+ decltype(countersEndTrue) countersEndFalse;
if (_node.falseStatement())
{
countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
}
+ else
+ {
+ countersEndFalse = m_variables;
+ }
mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse);
@@ -152,7 +157,7 @@ bool SMTChecker::visit(ForStatement const& _node)
checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
}
- VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
+ VariableSequenceCounters sequenceCountersStart = m_variables;
m_interface->push();
if (_node.condition())
m_interface->addAssertion(expr(*_node.condition()));
@@ -163,7 +168,7 @@ bool SMTChecker::visit(ForStatement const& _node)
m_interface->pop();
m_conditionalExecutionHappened = true;
- m_currentSequenceCounter = sequenceCountersStart;
+ std::swap(sequenceCountersStart, m_variables);
resetVariables(touchedVariables);
@@ -240,14 +245,14 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location)
{
checkCondition(
- _value < minValue(_type),
+ _value < SymbolicIntVariable::minValue(_type),
_location,
"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
"value",
&_value
);
checkCondition(
- _value > maxValue(_type),
+ _value > SymbolicIntVariable::maxValue(_type),
_location,
"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
"value",
@@ -365,7 +370,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{
// Will be translated as part of the node that requested the lvalue.
}
- else if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+ else if (SSAVariable::supportedType(_identifier.annotation().type.get()))
defineExpr(_identifier, currentValue(*decl));
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{
@@ -514,7 +519,7 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s
SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
{
- VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
+ VariableSequenceCounters beforeVars = m_variables;
if (_condition)
pushPathCondition(*_condition);
@@ -523,8 +528,9 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s
popPathCondition();
m_conditionalExecutionHappened = true;
- std::swap(sequenceCountersStart, m_currentSequenceCounter);
- return sequenceCountersStart;
+ std::swap(m_variables, beforeVars);
+
+ return beforeVars;
}
void SMTChecker::checkCondition(
@@ -709,8 +715,8 @@ void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, sm
set<Declaration const*> uniqueVars(_variables.begin(), _variables.end());
for (auto const* decl: uniqueVars)
{
- int trueCounter = _countersEndTrue.at(decl);
- int falseCounter = _countersEndFalse.at(decl);
+ int trueCounter = _countersEndTrue.at(decl).index();
+ int falseCounter = _countersEndFalse.at(decl).index();
solAssert(trueCounter != falseCounter, "");
m_interface->addAssertion(newValue(*decl) == smt::Expression::ite(
_condition,
@@ -722,14 +728,10 @@ void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, sm
bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
{
- if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
+ if (SSAVariable::supportedType(_varDecl.type().get()))
{
- solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
- solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
solAssert(m_variables.count(&_varDecl) == 0, "");
- m_currentSequenceCounter[&_varDecl] = 0;
- m_nextFreeSequenceCounter[&_varDecl] = 1;
- m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
+ m_variables.emplace(&_varDecl, SSAVariable(&_varDecl, *m_interface));
return true;
}
else
@@ -742,11 +744,6 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
}
}
-string SMTChecker::uniqueSymbol(Declaration const& _decl)
-{
- return _decl.name() + "_" + to_string(_decl.id());
-}
-
string SMTChecker::uniqueSymbol(Expression const& _expr)
{
return "expr_" + to_string(_expr.id());
@@ -754,48 +751,38 @@ string SMTChecker::uniqueSymbol(Expression const& _expr)
bool SMTChecker::knownVariable(Declaration const& _decl)
{
- return m_currentSequenceCounter.count(&_decl);
+ return m_variables.count(&_decl);
}
smt::Expression SMTChecker::currentValue(Declaration const& _decl)
{
- solAssert(m_currentSequenceCounter.count(&_decl), "");
- return valueAtSequence(_decl, m_currentSequenceCounter.at(&_decl));
+ solAssert(knownVariable(_decl), "");
+ return m_variables.at(&_decl)();
}
-smt::Expression SMTChecker::valueAtSequence(const Declaration& _decl, int _sequence)
+smt::Expression SMTChecker::valueAtSequence(Declaration const& _decl, int _sequence)
{
- return var(_decl)(_sequence);
+ solAssert(knownVariable(_decl), "");
+ return m_variables.at(&_decl)(_sequence);
}
smt::Expression SMTChecker::newValue(Declaration const& _decl)
{
- solAssert(m_nextFreeSequenceCounter.count(&_decl), "");
- m_currentSequenceCounter[&_decl] = m_nextFreeSequenceCounter[&_decl]++;
- return currentValue(_decl);
+ solAssert(knownVariable(_decl), "");
+ ++m_variables.at(&_decl);
+ return m_variables.at(&_decl)();
}
void SMTChecker::setZeroValue(Declaration const& _decl)
{
- solAssert(_decl.type()->category() == Type::Category::Integer, "");
- m_interface->addAssertion(currentValue(_decl) == 0);
+ solAssert(knownVariable(_decl), "");
+ m_variables.at(&_decl).setZeroValue();
}
void SMTChecker::setUnknownValue(Declaration const& _decl)
{
- auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
- m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
- m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
-}
-
-smt::Expression SMTChecker::minValue(IntegerType const& _t)
-{
- return smt::Expression(_t.minValue());
-}
-
-smt::Expression SMTChecker::maxValue(IntegerType const& _t)
-{
- return smt::Expression(_t.maxValue());
+ solAssert(knownVariable(_decl), "");
+ m_variables.at(&_decl).setUnknownValue();
}
smt::Expression SMTChecker::expr(Expression const& _e)
@@ -842,12 +829,6 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
m_interface->addAssertion(expr(_e) == _value);
}
-smt::Expression SMTChecker::var(Declaration const& _decl)
-{
- solAssert(m_variables.count(&_decl), "");
- return m_variables.at(&_decl);
-}
-
void SMTChecker::popPathCondition()
{
solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty.");
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index b57f0f96..7e7996cf 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -20,6 +20,8 @@
#include <libsolidity/formal/SolverInterface.h>
+#include <libsolidity/formal/SSAVariable.h>
+
#include <libsolidity/ast/ASTVisitor.h>
#include <libsolidity/interface/ReadFile.h>
@@ -76,7 +78,7 @@ private:
void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
/// Maps a variable to an SSA index.
- using VariableSequenceCounters = std::map<Declaration const*, int>;
+ using VariableSequenceCounters = std::map<Declaration const*, SSAVariable>;
/// Visits the branch given by the statement, pushes and pops the current path conditions.
/// @param _condition if present, asserts that this condition is true within the branch.
@@ -118,7 +120,6 @@ private:
/// This fails if the type is not supported.
bool createVariable(VariableDeclaration const& _varDecl);
- static std::string uniqueSymbol(Declaration const& _decl);
static std::string uniqueSymbol(Expression const& _expr);
/// @returns true if _delc is a variable that is known at the current point, i.e.
@@ -139,18 +140,12 @@ private:
/// Resets the variable to an unknown value (in its range).
void setUnknownValue(Declaration const& decl);
- static smt::Expression minValue(IntegerType const& _t);
- static smt::Expression maxValue(IntegerType const& _t);
-
/// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
smt::Expression expr(Expression const& _e);
/// Creates the expression (value can be arbitrary)
void createExpr(Expression const& _e);
/// Creates the expression and sets its value.
void defineExpr(Expression const& _e, smt::Expression _value);
- /// Returns the function declaration corresponding to the given variable.
- /// The function takes one argument which is the "sequence number".
- smt::Expression var(Declaration const& _decl);
/// Adds a new path condition
void pushPathCondition(smt::Expression const& _e);
@@ -166,10 +161,8 @@ private:
std::shared_ptr<smt::SolverInterface> m_interface;
std::shared_ptr<VariableUsage> m_variableUsage;
bool m_conditionalExecutionHappened = false;
- std::map<Declaration const*, int> m_currentSequenceCounter;
- std::map<Declaration const*, int> m_nextFreeSequenceCounter;
std::map<Expression const*, smt::Expression> m_expressions;
- std::map<Declaration const*, smt::Expression> m_variables;
+ std::map<Declaration const*, SSAVariable> m_variables;
std::vector<smt::Expression> m_pathConditions;
ErrorReporter& m_errorReporter;
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
new file mode 100644
index 00000000..4e6bcbcb
--- /dev/null
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -0,0 +1,73 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/SSAVariable.h>
+
+#include <libsolidity/formal/SymbolicIntVariable.h>
+
+#include <libsolidity/ast/AST.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SSAVariable::SSAVariable(
+ Declaration const* _decl,
+ smt::SolverInterface& _interface
+)
+{
+ resetIndex();
+
+ if (dynamic_cast<IntegerType const*>(_decl->type().get()))
+ m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
+ else
+ {
+ solAssert(false, "");
+ }
+}
+
+bool SSAVariable::supportedType(Type const* _decl)
+{
+ return dynamic_cast<IntegerType const*>(_decl);
+}
+
+void SSAVariable::resetIndex()
+{
+ m_currentSequenceCounter = 0;
+ m_nextFreeSequenceCounter.reset (new int);
+ *m_nextFreeSequenceCounter = 1;
+}
+
+int SSAVariable::index() const
+{
+ return m_currentSequenceCounter;
+}
+
+int SSAVariable::next() const
+{
+ return *m_nextFreeSequenceCounter;
+}
+
+void SSAVariable::setZeroValue()
+{
+ m_symbolicVar->setZeroValue(index());
+}
+
+void SSAVariable::setUnknownValue()
+{
+ m_symbolicVar->setUnknownValue(index());
+}
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
new file mode 100644
index 00000000..275e8590
--- /dev/null
+++ b/libsolidity/formal/SSAVariable.h
@@ -0,0 +1,88 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libsolidity/formal/SymbolicVariable.h>
+
+#include <memory>
+
+namespace dev
+{
+namespace solidity
+{
+
+class Declaration;
+
+/**
+ * This class represents the SSA representation of a program variable.
+ */
+class SSAVariable
+{
+public:
+ /// @param _decl Used to determine the type and forwarded to the symbolic var.
+ /// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver.
+ SSAVariable(
+ Declaration const* _decl,
+ smt::SolverInterface& _interface
+ );
+
+ void resetIndex();
+
+ /// This function returns the current index of this SSA variable.
+ int index() const;
+ /// This function returns the next free index of this SSA variable.
+ int next() const;
+
+ int operator++()
+ {
+ return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++;
+ }
+
+ smt::Expression operator()() const
+ {
+ return valueAtSequence(index());
+ }
+
+ smt::Expression operator()(int _seq) const
+ {
+ return valueAtSequence(_seq);
+ }
+
+ /// These two functions forward the call to the symbolic var
+ /// which generates the constraints according to the type.
+ void setZeroValue();
+ void setUnknownValue();
+
+ /// So far Int is supported.
+ static bool supportedType(Type const* _decl);
+
+private:
+ smt::Expression valueAtSequence(int _seq) const
+ {
+ return (*m_symbolicVar)(_seq);
+ }
+
+ std::shared_ptr<SymbolicVariable> m_symbolicVar = nullptr;
+ int m_currentSequenceCounter;
+ /// The next free sequence counter is a shared pointer because we want
+ /// the copy and the copied to share it.
+ std::shared_ptr<int> m_nextFreeSequenceCounter;
+};
+
+}
+}
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
new file mode 100644
index 00000000..d08dc155
--- /dev/null
+++ b/libsolidity/formal/SymbolicIntVariable.cpp
@@ -0,0 +1,56 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/SymbolicIntVariable.h>
+
+#include <libsolidity/ast/AST.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SymbolicIntVariable::SymbolicIntVariable(
+ Declaration const* _decl,
+ smt::SolverInterface& _interface
+):
+ SymbolicVariable(_decl, _interface)
+{
+ solAssert(m_declaration->type()->category() == Type::Category::Integer, "");
+ m_expression = make_shared<smt::Expression>(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Int));
+}
+
+void SymbolicIntVariable::setZeroValue(int _seq)
+{
+ m_interface.addAssertion(valueAtSequence(_seq) == 0);
+}
+
+void SymbolicIntVariable::setUnknownValue(int _seq)
+{
+ auto const& intType = dynamic_cast<IntegerType const&>(*m_declaration->type());
+ m_interface.addAssertion(valueAtSequence(_seq) >= minValue(intType));
+ m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(intType));
+}
+
+smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t)
+{
+ return smt::Expression(_t.minValue());
+}
+
+smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t)
+{
+ return smt::Expression(_t.maxValue());
+}
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
new file mode 100644
index 00000000..afa25f1b
--- /dev/null
+++ b/libsolidity/formal/SymbolicIntVariable.h
@@ -0,0 +1,50 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libsolidity/formal/SymbolicVariable.h>
+
+#include <libsolidity/ast/Types.h>
+
+namespace dev
+{
+namespace solidity
+{
+
+/**
+ * Specialization of SymbolicVariable for Integers
+ */
+class SymbolicIntVariable: public SymbolicVariable
+{
+public:
+ SymbolicIntVariable(
+ Declaration const* _decl,
+ smt::SolverInterface& _interface
+ );
+
+ /// Sets the var to 0.
+ void setZeroValue(int _seq);
+ /// Sets the variable to the full valid value range.
+ void setUnknownValue(int _seq);
+
+ static smt::Expression minValue(IntegerType const& _t);
+ static smt::Expression maxValue(IntegerType const& _t);
+};
+
+}
+}
diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp
new file mode 100644
index 00000000..629049ea
--- /dev/null
+++ b/libsolidity/formal/SymbolicVariable.cpp
@@ -0,0 +1,40 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/SymbolicVariable.h>
+
+#include <libsolidity/ast/AST.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SymbolicVariable::SymbolicVariable(
+ Declaration const* _decl,
+ smt::SolverInterface& _interface
+):
+ m_declaration(_decl),
+ m_interface(_interface)
+{
+}
+
+string SymbolicVariable::uniqueSymbol() const
+{
+ return m_declaration->name() + "_" + to_string(m_declaration->id());
+}
+
+
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
new file mode 100644
index 00000000..93258250
--- /dev/null
+++ b/libsolidity/formal/SymbolicVariable.h
@@ -0,0 +1,69 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libsolidity/formal/SolverInterface.h>
+
+#include <libsolidity/ast/AST.h>
+
+#include <memory>
+
+namespace dev
+{
+namespace solidity
+{
+
+class Declaration;
+
+/**
+ * This class represents the symbolic version of a program variable.
+ */
+class SymbolicVariable
+{
+public:
+ SymbolicVariable(
+ Declaration const* _decl,
+ smt::SolverInterface& _interface
+ );
+
+ smt::Expression operator()(int _seq) const
+ {
+ return valueAtSequence(_seq);
+ }
+
+ std::string uniqueSymbol() const;
+
+ /// Sets the var to the default value of its type.
+ virtual void setZeroValue(int _seq) = 0;
+ /// The unknown value is the full range of valid values,
+ /// and that's sub-type dependent.
+ virtual void setUnknownValue(int _seq) = 0;
+
+protected:
+ smt::Expression valueAtSequence(int _seq) const
+ {
+ return (*m_expression)(_seq);
+ }
+
+ Declaration const* m_declaration;
+ std::shared_ptr<smt::Expression> m_expression = nullptr;
+ smt::SolverInterface& m_interface;
+};
+
+}
+}