search

dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4
GNU General Public License v3.0
48 stars 36 forks source link

dReach code generation error: undefined symbol #224

Closed mtrberzi closed 8 years ago

mtrberzi commented 8 years ago

Attached here parallel-capacitor.drh is a dReach model I've written by hand, and attempted to run using dReach -k 1 -l 1 parallel-capacitor.drh. When dReal is invoked, the solver aborts with the following error:

terminate called after throwing an instance of 'std::runtime_error'
  what():  undefined symbol 'Vsource' in the expression!
If this is a numerical constant in scientific notation please replace it by a parameter.

The same occurs if I manually run dReal with the SMT2 file that is generated by dReach. dReach's parser does not indicate that there is anything wrong with the input file, so I am not sure why I am seeing this error.

soonhokong commented 8 years ago

@mtrberzi, please add something like the following to the drh file.

  d/dt[R1] = 0;
  d/dt[C1] = 0;
  d/dt[Vsource] = 0;
  d/dt[Rcenter] = 0;

You had d/dt[VR1v] = ( (Vsource / R1) - VR1i - (VR1v / R1) ) / C1 in the file, but didn't specify the RHS of ODEs for the variables R1, C1, VSource, and Rcenter. For now, it's required to provide the RHS of each variables in a system of ODEs.

soonhokong commented 8 years ago

Does it also resolve #222? If not, please let me know.

mtrberzi commented 8 years ago

It seems to be running now. Thank you for the advice. Just to clarify, this applies to any variable that's mentioned in an ODE?

soonhokong commented 8 years ago

Just to clarify, this applies to any variable that's mentioned in an ODE?

Yes, this is the case.