mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-06 16:01:55 +00:00
Code Activity
5560 commits 28 branches 52 tags 171 MiB
Commit graph

975 commits

Author SHA1 Message Date
Murphy Berzish
e9b31f2995 temporarily patched in a get_eqc_allUnroll() implementation 2015-11-06 14:13:38 -05:00
Murphy Berzish
ac8b5e6eae free variable WIP 2015-11-06 14:10:18 -05:00
Murphy Berzish
4a8ee88461 ctx_dep_analysis() done, final_check() WIP 2015-11-06 13:43:54 -05:00
Nikolaj Bjorner
5ea2c22153 fix build break - by renaming tout to out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 10:21:02 -08:00
Nikolaj Bjorner
aeedb931f3 fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 10:20:21 -08:00
Christoph M. Wintersteiger
a6b3fba038 Build fix, hide debug code in release mode. 2015-11-06 18:06:23 +00:00
Nikolaj Bjorner
7b72486644 Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master 2015-11-05 17:32:35 -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
Murphy Berzish
9f01b9dc92 more progress on model gen (WIP) 2015-11-04 16:22:06 -05:00
Nikolaj Bjorner
2efd5bf9d1 Fix bug exposed in #281 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-02 14:18:49 -08:00
Nikolaj Bjorner
f78c769b3b Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-02 13:49:48 -08:00
Christoph M. Wintersteiger
14d2356a32 Code simplification 2015-11-02 19:25:11 +00:00
Christoph M. Wintersteiger
ba70ab9ad2 Bugfix for theory_fpa 2015-11-02 19:08:52 +00: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
7169fc469e Merge branch 'master' of https://github.com/NikolajBjorner/z3 2015-11-02 08:19:35 -08:00
Nikolaj Bjorner
32f3bd17fb adding translation routine to context to address enhancement request #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-31 14:30:54 -07:00
Nikolaj Bjorner
9acaa49a05 adding translation routine to context to address enhancement request #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-31 14:28:21 -07:00
Nikolaj Bjorner
4b1a730f46 API method for translating context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-31 12:47:16 -07:00
Nikolaj Bjorner
fb624780d5 add checks in internalizer for issues of the form #227 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-31 12:41:57 -07:00
Christoph M. Wintersteiger
88064fc172 minor theory_fpa refactoring 2015-10-31 19:16:09 +00:00
Christoph M. Wintersteiger
1d7aa9ba2f Fixed rewriter bug in theory_fpa. 2015-10-31 18:53:40 +00:00
Christoph M. Wintersteiger
8491b3bebe Revert "Fixed use of mk_th_axiom in theory_fpa." 
This reverts commit 89e99c7b4b.
 2015-10-31 18:51:32 +00:00
Nikolaj Bjorner
4fd1f4a65c add handler for abuse of OP_IMPLIES 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-31 11:34:55 -07:00
Christoph M. Wintersteiger
89e99c7b4b Fixed use of mk_th_axiom in theory_fpa. 
Relates to #227
 2015-10-31 13:57:17 +00:00
Nikolaj Bjorner
ac3edbbaaa add line/position information to unsupported command reports per zeph pull request 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-30 19:23:31 -07:00
Nikolaj Bjorner
b19fbe4429 make sure to bring constraints into clausal form before using the th_axiom assertion. Old version should not have been used as a template for copying, as in issue #227 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-30 15:55:18 -07:00
Christoph M. Wintersteiger
8fffa9f188 Removed trailing whitespace. 2015-10-30 12:20:41 +00: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
2a95a77706 fix issues #240, #250 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 09:47:17 -07:00
Nikolaj Bjorner
b197e590a4 fix coercion regression. Issue #263 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-27 19:25:38 -07:00
Nikolaj Bjorner
47cb1058b2 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-27 18:11:35 -07:00
Nikolaj Bjorner
357a92dfef n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-27 18:11:31 -07:00
Murphy Berzish
1f3c5cebbf variable classification (WIP) 2015-10-26 15:43:31 -04:00
Christoph M. Wintersteiger
9b5abcd55a Improved support for FPA unspecified min/max values, model validation, and proof generation. 2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger
ca496f20cb Partial refactoring of fpa2bv conversion to support proofs. 2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger
e3ed0159a8 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-25 13:09:59 +00:00
Christoph M. Wintersteiger
21ad1fb623 Bugfix for proof production in asserted_formulas::propagate_values() 
Fixes #259
 2015-10-25 13:09:18 +00:00
Nikolaj Bjorner
05c6ed1698 fixing issue #254 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-22 09:54:05 -07:00
Nikolaj Bjorner
ac902dad1a fix another regression and missing detection of bounds, Issue #254 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-22 08:53:12 -07:00
Murphy Berzish
c08f4371f4 begin model generation, wip 2015-10-21 21:32:38 -04:00
Nikolaj Bjorner
ffa78b95ab fix unbounded, issue #252 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-21 14:38:47 -07:00
Christoph M. Wintersteiger
6749c19ab1 Merge branch 'static_analysis' of https://github.com/daniel-j-h/z3 
# Conflicts:
#	src/ast/ast.h
#	src/interp/iz3foci.cpp
#	src/muz/duality/duality_dl_interface.cpp
#	src/util/hwf.h
 2015-10-19 15:14:45 +01:00
Murphy Berzish
3ee8f27588 possibly fix internalization bug mentioned in #2 
(this leads to a not-implemented-yet in final_check_eh()
due to missing code surrounding free variable production)
 2015-10-18 20:20:09 -04:00
Murphy Berzish
e521ab2c3a fix concat_axiom loop in propagate(): compare against size()...... 2015-10-18 19:40:03 -04:00
Nikolaj Bjorner
f4954e9d7f fix for fixed size rational difference logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-13 09:24:02 -07:00
Nuno Lopes
0e387b2abe use Z3_fallthrough instead of __falthrough directly to avoid messing with reserved identifiers 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-10-09 18:06:49 +01:00
Christoph M. Wintersteiger
a951ff0769 Fix for FP UFs and conversion functions. 2015-10-08 16:04:17 +01:00
Christoph M. Wintersteiger
a2503af585 Bugfixes for UFs and conversion functions in theory_fpa 2015-10-08 11:54:35 +01:00
Christoph M. Wintersteiger
de39173f6f Corrected unspecified behavior of fp.min/fp.max corner cases in fpa2bv_converter and in theory_fpa. 
Fixes #68
 2015-10-07 20:44:08 +01:00
Nikolaj Bjorner
6e852762ba patch for issue #232 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-06 19:07:47 -07:00