Conversation
axic
force-pushed
the
smt-variable-types
branch
from
6c430c5 to
18ae0c3
Compare
|
Realised that z3 has the same problem so perhaps we should do this in the |
|
Yes, this should be part of the interface. Also: For now, the assertion is fine, but soon we also want to see the values for non-integer variables, e.g. bools. |
|
@chriseth current version of the Z3 code uses a map for constant/function names, which does the same assert due to duplicate key will be refused by the map. Basically Z3 part does everything this PR does for the SMT interface, i.e. this should be merged. |
| auto const& e = _expressionsToEvaluate.at(i); | ||
| // TODO they don't have to be ints... | ||
| solAssert(m_variables.count(e.name), ""); | ||
| solAssert(m_variables[e.name] == SMTVariableType::Integer, ""); |
There was a problem hiding this comment.
Most of them will actually be functions (mapping int to int or int to bool).
There was a problem hiding this comment.
Note that this code is not tested by travis.
There was a problem hiding this comment.
Ah sorry, they are of course not functions.
| std::vector<std::string> m_accumulatedOutput; | ||
|
|
||
| enum class SMTVariableType { | ||
| Function, |
There was a problem hiding this comment.
Hm, I think we also need the domain and codomain of that function, otherwise it does not make too much sense.
|
Ok, let's merge it for now, but I think we should rather pull that up into SolverInterface later. |
3 participants
No description provided.