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

7194 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
cb140011bc add missing rewrite rule. Issue #731 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 09:42:36 -07:00
Nikolaj Bjorner
2f67665c7e ensure stoi axiom even when no value is present for argument. Issue #731 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 09:40:21 -07:00
Murphy Berzish
82e07aae8c disable deferred eqc check in theory_str 2016-09-08 19:55:08 -04:00
Nikolaj Bjorner
d74e618565 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-08 13:59:22 -07:00
Nikolaj Bjorner
e485d1889c update replace semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-08 13:59:13 -07:00
Nikolaj Bjorner
76cf28d48b move from uint_set to hashtable over unsigned to save memory overhead in consequence generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-08 13:34:59 -07:00
Nikolaj Bjorner
94b67412ec Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-07 11:59:06 -07:00
Nikolaj Bjorner
c5dd441947 fixes to consequence generation and cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-07 11:50:26 -07:00
Nikolaj Bjorner
2d9dced1c7 fix spacing, cast to Bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-06 20:18:31 -07:00
Nikolaj Bjorner
520f8fc60e Merge pull request #730 from cttghc/patch-1 
Fix omission of Z3_model_has_interp in z3++.h
 2016-09-07 11:13:24 +08:00
cttghc
758266b952 Fix omission of Z3_model_has_interp in z3++.h 2016-09-06 18:32:41 -05:00
Nikolaj Bjorner
0e9758a211 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-06 14:39:19 -07:00
Nikolaj Bjorner
3b70dd6678 tuning by using get_consequences2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-06 14:29:40 +08:00
Murphy Berzish
c83e39d3b8 fix incorrect axiom in theory_str for Contains check 
this partially fixes a regression in contains-034.smt2, which now
is at least not a SAT-as-UNSAT
 2016-09-05 17:45:10 -04:00
Christoph M. Wintersteiger
e7ae60893c Merge pull request #728 from AlexVonB/patch-1 
Fix VisualStudio 2010 compiler warning C4100
 2016-09-05 10:29:22 -04:00
AlexVonB
c6b0fc444c Fix VisualStudio 2010 compiler warning C4100 
When compiling with Visual Studio 2010 the buildlog warns of the following: `z3++.h: warning C4100: 'e' : unreferenced formal parameter` and `z3++.h: warning C4100: 'c' : unreferenced formal parameter`. This merge request removes this warning.
 2016-09-05 16:22:00 +02:00
Murphy Berzish
7b34efada7 add aggressive unroll test option to theory_str 2016-09-04 18:48:15 -04:00
Murphy Berzish
347f441517 add a check for variable scope to theory_str 2016-09-02 20:44:14 -04:00
Murphy Berzish
2b8f165cc4 patch UNSAT to UNKNOWN in cmd_context for theory_str 2016-09-02 19:04:20 -04:00
Murphy Berzish
d3062a8eff omit out-of-scope length testers from axiom premise in theory_str::gen_len_test_options 
this fixes a regression in charAt-007.smt2
 2016-09-02 18:23:41 -04:00
Nikolaj Bjorner
424a8c69bd Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-02 03:05:23 -07:00
Nikolaj Bjorner
dc48008d46 fixestoconsequences 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-02 11:00:40 +08:00
Nikolaj Bjorner
c746d46d80 add validation code, fix bugs in consequence finder 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-01 16:21:23 +08:00
Murphy Berzish
f9b4f21683 add rewrite for theory_str rewriter RegexPlus 
fixes regex-013.smt2
 2016-08-31 19:22:04 -04:00
Murphy Berzish
5e22bc57c8 theory_str cleanup 2016-08-31 19:19:23 -04:00
Nikolaj Bjorner
4d9aadde35 updated consequence finder to fix bug in processing enumeration types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-31 16:15:36 +08:00
Nikolaj Bjorner
237fde1f76 fix crash during shutdown. Issue #719 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-31 09:57:46 +08:00
Nikolaj Bjorner
310c0f31a1 use type constrsaints for co-variant subtying to enable .net 3.5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-30 12:07:06 +08:00
Nikolaj Bjorner
d4539b8887 fix dt2bv transformation to only work with constants, issue #725 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-30 11:42:14 +08:00
Nikolaj Bjorner
882c3bd0cd fix unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-23 18:18:11 -03:00
Nikolaj Bjorner
510231df42 fix to #717. The bottom-up COI filter can only use positive facts for filtering 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-23 12:26:38 -03:00
Nikolaj Bjorner
b5c521e4b2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-23 11:44:48 -03:00
Nikolaj Bjorner
0a09d5ff52 check for non-nullness when handling optional info fields for marking. Fixes issue #719 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-23 11:33:40 -03:00
Murphy Berzish
89d5f4ffb4 add compute_contains check to theory_str 
this may cause a crash in indexof-002.smt2 but
I cannot reproduce it
 2016-08-21 21:37:46 -04:00
Murphy Berzish
2a199294a1 remove incorrect null pointer check from theory_str::gen_len_val_options_for_free_var 
everything that calls this method knows that it can legally return null
 2016-08-21 00:43:00 -04:00
Murphy Berzish
7b3203b48e disable aggressive length/value testing in theory_str, it seems to be detrimental 2016-08-21 00:30:29 -04:00
Murphy Berzish
1a75781a3c add experimental option to defer new_eq_check to final_check in theory_str 2016-08-20 23:09:08 -04:00
Christoph M. Wintersteiger
b03dc0af3b fixed memory leaks 2016-08-20 17:57:00 -04:00
Christoph M. Wintersteiger
47e95f8676 Fixed binding substitution in macro_util 2016-08-20 17:56:52 -04:00
Nikolaj Bjorner
879f792125 fix axiomatization of str.replace. Fixes issue #703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 06:13:52 -07:00
Nikolaj Bjorner
2d8325ed43 fix axiomatization of str.replace. Fixes issue #703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 06:05:13 -07:00
Nikolaj Bjorner
439e8e6b04 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-20 03:53:55 -07:00
Nikolaj Bjorner
f2b5c11d1c add option for prettier proof printing, Issue #706 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 03:52:45 -07:00
Murphy Berzish
481e97a274 propagate early in theory_str to set up contains/regex maps 
this fixes an unsat-as-sat error in a regex test and flips around some timeouts
so more work will be required to track this down
 2016-08-19 22:53:36 -04:00
Nikolaj Bjorner
5069da62a3 safe sat clause_offset in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-19 08:45:06 -07:00
Nikolaj Bjorner
e132c5eae8 safe sat clause_offset in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-19 08:42:40 -07:00
Nikolaj Bjorner
b2383a481a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-18 18:02:22 -07:00
Nikolaj Bjorner
665fccf07a addressing max-segment issue for AMD64 + Debug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-18 18:01:29 -07:00
Murphy Berzish
8598a48e3b fix weird Contains rewriter behaviour in theory_str 2016-08-18 19:14:50 -04:00
Murphy Berzish
3c8b833eeb fix expression dereference error in theory_str::gen_assign_unroll_Str2Reg 2016-08-18 17:03:32 -04:00