Nikolaj Bjorner
|
5e7db2e3e2
|
disable mk_array_eq as it breaks model evaluation/validation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-18 08:29:24 -07:00 |
|
|
Nikolaj Bjorner
|
99314b7252
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-05-15 11:34:55 -07:00 |
|
|
Nikolaj Bjorner
|
42726171b5
|
add limit checks in Grobner. Issue #599
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-15 11:34:48 -07:00 |
|
Arie Gurfinkel
|
d1f8b06ec4
|
bug fix in model_evaluator for array equality
|
2016-05-11 22:44:11 -04:00 |
|
|
Nikolaj Bjorner
|
0f93853a4c
|
remove labels from evaluation result
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-04-12 13:17:10 -07:00 |
|
|
Nikolaj Bjorner
|
aa7b5d80fe
|
extract array terms for evaluator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-04-12 09:41:50 -07:00 |
|
|
Nikolaj Bjorner
|
b97d694e5e
|
undo model evaluation to BR_FULL pending regression in assertion violation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-04-05 22:26:57 +02:00 |
|
|
Nikolaj Bjorner
|
ec5a4ba63d
|
add documentation comment for evaluation, Issue #536
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-04-04 12:59:18 +02:00 |
|
|
Nikolaj Bjorner
|
03336ab9f2
|
add evaluation of array equalities to model evaluator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-04-02 15:07:01 +02:00 |
|
|
Nikolaj Bjorner
|
05a784fa9e
|
fix issue #535
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-03-24 08:16:19 -07:00 |
|
Christoph M. Wintersteiger
|
778c7fcc64
|
Bugfix for model evaluator and internal, uninterpreted FPA functions.
Fixes #518
|
2016-03-16 16:17:08 +00:00 |
|
|
Nikolaj Bjorner
|
70f13ced33
|
make proto-model evaluation use model_evaluator instead of legacy evaluator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-03-05 10:14:15 -08:00 |
|
|
Nikolaj Bjorner
|
7c6540e18f
|
recursive function definitions; combine model-building functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-03-03 07:59:03 -08:00 |
|
|
Christoph M. Wintersteiger
|
7ddd2856c8
|
Added is_considered_uninterpreted() to decl_plugins.
|
2016-02-05 15:22:37 +00:00 |
|
|
Christoph M. Wintersteiger
|
bb5118acbb
|
Bugfix for bv*div0 model construction.
|
2016-02-05 13:53:35 +00:00 |
|
|
Christoph M. Wintersteiger
|
88f007e9da
|
whitespace
|
2016-02-05 13:48:47 +00:00 |
|
|
Nikolaj Bjorner
|
a295dd48dc
|
add seq_rewriter to model_evaluator, remove th_rewriter additional step in validator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-01-15 04:02:48 +05:30 |
|
|
Nikolaj Bjorner
|
baee4225a7
|
reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-11 16:21:24 -08:00 |
|
|
Nikolaj Bjorner
|
d6cb778365
|
fix rewriter for model validation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-03 07:45:42 -08:00 |
|
|
Nikolaj Bjorner
|
ec12368b54
|
Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-02 11:36:50 -08:00 |
|
|
Nikolaj Bjorner
|
77fec049a5
|
Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-02 10:27:44 -08:00 |
|
|
Nikolaj Bjorner
|
feba64b739
|
Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-02 10:18:25 -08:00 |
|
Nikolaj Bjorner
|
52619b9dbb
|
pull unstable
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
|
2015-04-01 14:57:11 -07:00 |
|
|
Christoph M. Wintersteiger
|
dd17f3c7d6
|
Renaming floats, float, Floats, Float -> FPA, fpa
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-08 13:18:56 +00:00 |
|
|
Nikolaj Bjorner
|
fe5c42c90f
|
fixes to bugs exposed by regressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-12-15 05:23:47 +02:00 |
|
Leonardo de Moura
|
a895506dac
|
Fix issue reported at http://stackoverflow.com/questions/14524316/z3-4-3-get-complete-model
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-01-25 09:29:03 -08:00 |
|
|
Leonardo de Moura
|
607fab486c
|
Fix incorrect uses of set_cancel()
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-17 18:48:10 -08:00 |
|
|
Leonardo de Moura
|
cf28cbab0a
|
saved params work
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-29 17:19:12 -08:00 |
|
|
Nikolaj Bjorner
|
93ad91d2f9
|
preparing handling of arrays/quantifiers, fix cover-related bugs reported by Arie
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2012-11-25 12:08:49 -08:00 |
|
|
Leonardo de Moura
|
f57d4b1b19
|
reorganizing the code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-25 11:28:03 -07:00 |
|
|
Leonardo de Moura
|
8b70f0b833
|
Reorganizing the code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-20 19:30:14 -07:00 |
|