6 commits

Author	SHA1	Message	Date
Simon Cruanes	3fdb07b533	feat: handle get-model/get-value from smtlib inputs	2022-02-02 15:51:44 -05:00
Simon Cruanes	d4cf722d32	wip: LIA: just relax to LRA for now	2022-01-31 15:12:55 -05:00
Simon Cruanes	f713106514	lia: use branch and bound a bit ... this should be removed when we use the intsolver, alongside a pure real relaxation of int constraints…	2022-01-14 13:34:23 -05:00
Simon Cruanes	4b2afd7a05	wip: LIA theory	2022-01-13 12:55:36 -05:00
Simon Cruanes	44af0afd59	fix(lia): problems with only integer constants are not incomplete	2022-01-11 14:00:05 -05:00
Simon Cruanes	8410a57f1a	wip: feat(LIA): LIA solver, will rely on LRA solver ... we want to reuse the simplex, but do branch and bound + cutting planes	2022-01-11 14:00:04 -05:00