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

1754 commits

Author SHA1 Message Date
Murphy Berzish
c44d49b625 keep track of search level ourselves 2015-12-01 14:41:11 -05:00
Murphy Berzish
dd0bc13be7 attempt to track popped variables, still segfaults, WIP 2015-11-30 19:22:01 -05:00
Nuno Lopes
5d289a8da5 fix leak in asserted_formulas::propagate_values() for proof generation mode 
continuation of issue #342

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-29 10:49:52 +00:00
Murphy Berzish
07626a1e03 remove expr_ref stuff, start tracking variables more closely 2015-11-28 23:56:30 -05:00
Nuno Lopes
d175c99542 fix ast leak in asserted_formulas::propagate_values() 
Fixes issue #342

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-11-27 20:09:17 +00:00
Murphy Berzish
9010a5c4cf honest-to-goodness working model gen, i.e. it didn't crash. more testing needed 2015-11-20 16:05:43 -05:00
Murphy Berzish
24148bafa3 fixed several AST bugs; need to load charSet now 2015-11-20 15:48:06 -05:00
Murphy Berzish
bf27d41b08 use TRACE instead of STRACE... 2015-11-20 12:27:29 -05:00
Murphy Berzish
b34fc06fe9 fix all compilation errors, now to test it 2015-11-20 12:24:23 -05:00
Nikolaj Bjorner
665af3d8b9 remove deprecated user-theory plugins and other unused functionality from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:43:27 -08:00
Nikolaj Bjorner
fd8fd40669 fix tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:00:01 -08:00
Nikolaj Bjorner
04b0e3c2f7 add checks for cancellation inside mam to agilely not ignore Rustan's soft requests for a timeout #326 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-17 18:48:52 -08:00
Nikolaj Bjorner
66fc873613 Fix for #322: PDR engine cannot falls back on fixed size arithmetic for difference logic. It would eventually overflow and cause incorrect model construction. Enable only fixed-size arithmetic when configuration allows it 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-17 09:00:16 -08:00
Murphy Berzish
9beeb09acf model gen possibly done, but I doubt it works so WIP 2015-11-15 15:18:14 -05:00
Murphy Berzish
8b538f5840 started gen_val_options() WIP 2015-11-11 15:34:11 -05:00
Nikolaj Bjorner
315dc80eb0 toggle default for bv2int decision procedure support to avoid confusing users. Issue #301 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-10 15:09:52 -05:00
Murphy Berzish
3a404c248d gen_free_var_options() WIP 2015-11-10 12:40:01 -05:00
Murphy Berzish
6374d63160 gen_len_val_options_for_free_var() WIP 2015-11-09 16:11:00 -05:00
Murphy Berzish
0178872a19 completed process_free_var(), still WIP 
working on gen_len_val_options_for_free_var()
 2015-11-09 15:33:52 -05:00
Murphy Berzish
a9b8707d48 possibly found a way to do get_parents() 2015-11-09 15:14:34 -05:00
Christoph M. Wintersteiger
5995c753d3 Bugfix for theory_fpa construction and destruction. 2015-11-09 13:54:28 +00:00
Christoph M. Wintersteiger
4e05e93ecb Bugfix for FPA model generation/conversion. 
Addresses #300
 2015-11-09 11:52:44 +00:00
Nikolaj Bjorner
4685a5f8ba add array-ext to externally exposed functions to enable interpolants with arrays to be usable in feedback loops with Z3. Addresses one issue raised in #292 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 16:42:13 -08:00
Nikolaj Bjorner
8d1fa3ae50 move mk_fresh to inside files that include smt_context.h directly to address build problem reported in #297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 11:50:06 -08:00
Nikolaj Bjorner
c1adffb6ab Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master 2015-11-07 10:00:43 -08:00
Nikolaj Bjorner
1758799ef4 add translate facility to inc_sat_solver. Limit lemma copying to unit lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 10:00:14 -08:00
Nikolaj Bjorner
396875bedf fix compilation problem, issue #297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 22:56:53 -08:00
Nikolaj Bjorner
3d993a4ee1 Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master 2015-11-06 17:29:53 -08:00
Nikolaj Bjorner
b4cb51cdb3 working on Forking/Serializing a z3 Solver #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 17:29:24 -08:00
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