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

more methods in api #227

Closed scungao closed 8 years ago

soonhokong commented 8 years ago

what's "weird result in example"?

scungao commented 8 years ago

No problem there anymore.

soonhokong commented 8 years ago

OK. I'll take a closer look at them and possibly change the commit messages then :-)

soonhokong commented 8 years ago

Closed by 6c8e624ff6df453e8ed3b45d92195709389052c3.

soonhokong commented 8 years ago

@scungao: It seems that something is wrong here. I ran ./tests/cpp_api/cpp_api_example and it failed to pass three tests:

-------------------------------------------------------------------------------
basic1
-------------------------------------------------------------------------------
/Users/soonhok/work/dreal3/src/tests/cpp_api/example.cpp:34
...............................................................................

/Users/soonhok/work/dreal3/src/tests/cpp_api/example.cpp:44: FAILED:
  REQUIRE( s.check() )
with expansion:
  false

-------------------------------------------------------------------------------
basic2
-------------------------------------------------------------------------------
/Users/soonhok/work/dreal3/src/tests/cpp_api/example.cpp:47
...............................................................................

/Users/soonhok/work/dreal3/src/tests/cpp_api/example.cpp:61: FAILED:
  REQUIRE( s.check() )
with expansion:
  false

(= (+ (+ x x) x) 0)
-------------------------------------------------------------------------------
basic3
-------------------------------------------------------------------------------
/Users/soonhok/work/dreal3/src/tests/cpp_api/example.cpp:64
...............................................................................

/Users/soonhok/work/dreal3/src/tests/cpp_api/example.cpp:70: FAILED:
  REQUIRE( s.check() )
with expansion:
  false

===============================================================================
test cases: 11 | 8 passed | 3 failed
assertions: 12 | 9 passed | 3 failed
soonhokong commented 8 years ago

Later, I'll add some code for expr class so that you can use unordered_set<expr> instead of set<expr>.