3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-07 05:06:26 +00:00
Commit graph

11 commits

Author SHA1 Message Date
Nikolaj Bjorner
fc4260e018 enable Horner evaluation also for mixed-integer constraints now that ast-manger inserts coercions on the fly. Avoids loop for issue #399, but with this alone results in unknown status
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-09 10:01:44 -08:00
Nikolaj Bjorner
fc592fc856 fix for #291. The root issue is that the set of antecedents is recycled as a fixed object between routines. Antecedents that were already allocated for a Gomory cut got reset by the internalizer. This causes unsound bounds axioms to be created
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-05 15:08:42 -08:00
Nikolaj Bjorner
6b82b949cf Make Groebner basis computation interruptable. Exponsed in issue #269
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-28 11:39:59 -07:00
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-08 23:18:40 -07:00
Nikolaj Bjorner
d815cf9b7b fix bug in optimization where a variable is updated twice
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-07 16:01:48 -07:00
Nikolaj Bjorner
e8811748d3 fix regressions in nl/smt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-16 19:08:37 +01:00
Nikolaj Bjorner
d45c7ce082 prepare revised primal phase
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-01-18 04:11:40 +05:30
Nikolaj Bjorner
41ad1d50f9 fix java compilation bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-01-16 08:08:51 +05:30
Nikolaj Bjorner
9412890c63 trace reason for undef in arithmetic, enable model generation on THEORY incompleteness, but retain undef result
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-26 12:58:55 -07:00
Nikolaj Bjorner
3d995648ee partial fix to model generation bug for non-linear constraints: avoid epsilon refinment for non-shared variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-08-07 20:39:20 +09:00
Leonardo de Moura
add684d8e9 checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-21 13:32:12 -07:00
Renamed from lib/theory_arith_nl.h (Browse further)