mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
11940 commits 49 branches 53 tags 182 MiB
Commit graph

172 commits

Author SHA1 Message Date
Nikolaj Bjorner
be9d5c7088 fix evaluator for array store expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-02 21:33:24 +00:00
Christoph M. Wintersteiger
ab4bb8194e Added unregister_decl to model_core 2016-10-15 18:35:39 +02:00
Nikolaj Bjorner
b66d457b19 move arithmetical mbp functionality to model_based_opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-26 16:12:14 -07:00
Nikolaj Bjorner
5b497b6249 reduce set of mainly verbose warnings raised by -Wmaybe-uninitialized and unused variable warnings from release mode builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-22 20:25:47 -07:00
Nikolaj Bjorner
b8716b3339 avoid use-before-def crashes fp-operations.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 14:32:39 -07:00
Nikolaj Bjorner
a07381ac19 fix regression in evaluator exposed by build failure on fp-array-6.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 14:23:07 -07:00
Nikolaj Bjorner
cd441c318e add compare utility to compress common cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 09:03:24 -07:00
Nikolaj Bjorner
af3cc7e578 tune array evaluation, still disabled 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 08:57:59 -07:00
Nikolaj Bjorner
1aa3fdab8a remove min/max, use qmax; disable cancellation during model evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-19 13:04:20 -07:00
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
b512212d41 update func_interp code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 17:31:36 -07:00
Nikolaj Bjorner
3a6218ac21 update func_interp code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 17:30:52 -07:00
Nikolaj Bjorner
c3f4124a9f trace down recent exposed regression in goal2sat, incorporate Scott's suggestion on making vector<std::string inaccessible 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 14:50:10 -07: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
Christoph M. Wintersteiger
3a532c08a6 Bugfix for func_interp else-case compression 2016-04-06 19:24:08 +01:00
Christoph M. Wintersteiger
e527aca296 Bugfix for unspecified else-case in func_interps. 2016-04-06 15:39:32 +01:00
Christoph M. Wintersteiger
7534b53bae Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-06 14:51:25 +01: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
Christoph M. Wintersteiger
ccd18283e7 Moved extension_converter func_interp entry compression to func_interp. 
Relates to #547
 2016-04-01 15:38:38 +01:00
Christoph M. Wintersteiger
3b82604590 whitespace 2016-04-01 15:37:40 +01:00
Christoph M. Wintersteiger
eb9c5b7cdb Disabled bogus assertions. 
Fixes #489
 2016-04-01 13:25:37 +01:00
Christoph M. Wintersteiger
852dc6d190 whitespace 2016-04-01 13:22:16 +01:00
Nikolaj Bjorner
05a784fa9e fix issue #535 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-24 08:16:19 -07:00
Nikolaj Bjorner
b0f65335ab update copyright year 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-17 13:07:40 -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
e2d54940b4 revert mixed integer/real handling pending fix to equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 12:11:27 -08:00
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
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
52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
Christoph M. Wintersteiger
858ce1158d Bugfix in model translation (ast_manager mismatch after par-or). Thanks to stackoverflow user user297886 for reporting this issue. 
http://stackoverflow.com/questions/28852722/segmentation-fault-while-using-par-or-tactic
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 18:30:06 +00: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
960e8ea1d5 working on hitting sets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-08 14:12:54 +01:00
Nikolaj Bjorner
6f0155ce94 avoid compiler warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-20 10:14:40 -07:00
Nikolaj Bjorner
3d1ca5ecc9 make eval cache sensitive to model completion. Bug 110 reported by cipher1024 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-15 21:12:16 -07:00