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

dump_dr_file() handles some inequalities wrongly #299

Closed scungao closed 8 years ago

scungao commented 8 years ago

Most likely missing polarity.

soonho-tri commented 8 years ago

can you give me 1-2 examples?

scungao commented 8 years ago

sicun-> cat wrong.cpp

#include "dreal.h"
using namespace dreal;
int main() {
    solver s;
    expr x = s.var("x",-1,1);
    s.add(x+sin(x)<0);
    s.dump_dr_file("wrong"); //it writes to wrongdumped.dr
    return 0;
}
sicun-> cat wrongdumped.dr
var:
[-1,1] x;
ctr:
(0.000000000000000000000000000000)<=(x+sin(x)); //note how the inequality is reversed
1>0;
soonho-tri commented 8 years ago

I'm on it.