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

2430 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ken McMillan
c3eae9bf2a working on incremental stratified inlining in duality 2013-06-05 17:02:13 -07:00
Leonardo de Moura
110fa0b7fb Fix issue http://z3.codeplex.com/workitem/45 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-05 13:50:22 -07:00
Christoph M. Wintersteiger
d301bd35a9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-05 14:36:18 +01:00
Ken McMillan
418f148ecf working on incremental stratified inlining in duality 2013-06-04 18:22:54 -07:00
Nikolaj Bjorner
b6d9d8a601 fix bugs reported by Nuno Lopes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-04 12:55:35 -07:00
Nikolaj Bjorner
aa0d921240 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-03 11:48:21 -07:00
Nikolaj Bjorner
bd064bf5d0 enable UTVPI by default 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-03 11:46:13 -07:00
Christoph M. Wintersteiger
093fe945bc FPA: min/max/fma bugfixes + partial quantifier support 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-03 18:19:45 +01:00
Christoph M. Wintersteiger
7c32df93a4 SLS tactic: compilation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-03 18:17:41 +01:00
Nikolaj Bjorner
56bfc06c4f fix reference count bugs in overflow/underflow APIs for bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-02 20:55:15 -07:00
Nikolaj Bjorner
d569027e36 fix reference count bugs in overflow/underflow APIs for bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-02 20:54:01 -07:00
Nikolaj Bjorner
89d8970d41 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-02 12:03:01 -07:00
Nikolaj Bjorner
ec121db5c1 addressing race condition on interrupts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-02 12:02:35 -07:00
Nikolaj Bjorner
76a269c85a clean up parity computation 
Signed-off-by: unknown <nbjorner@NIKOLAJ-ZEN.redmond.corp.microsoft.com>
 2013-06-01 17:14:18 -07:00
Ken McMillan
9890b3bb5c changing model format in duality to support boogie 2013-05-31 18:00:50 -07:00
Ken McMillan
ca38158966 fix bug in getting decision count in duality 2013-05-31 17:52:51 -07:00
Nikolaj Bjorner
c0895e5548 remove hassel table from unstable: does not compile under other plantforms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-31 17:48:19 -07:00
Leonardo de Moura
b670f0bb69 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-05-30 10:55:19 -07:00
Leonardo de Moura
37215b03bc Remove redundant register_on_timeout_proc 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-05-29 18:18:24 -07:00
Nikolaj Bjorner
60c4973c1d fix crash in proof generation in BMC 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-29 17:56:23 -07:00
Ken McMillan
dfae0c5109 output background model in duality counterexamples 2013-05-29 16:40:47 -07:00
Nuno Lopes
9a66696639 merge hassel table code from branch 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-29 14:35:32 -07:00
Ken McMillan
ee4b9d46f1 fix labels bug in duality 2013-05-27 19:22:47 -07:00
Ken McMillan
b27abc501e set proof mode by default to avoid crash on pop if we set it later in duality 2013-05-27 19:22:19 -07:00
Leonardo de Moura
fbbbfad564 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-05-27 17:49:29 -07:00
Leonardo de Moura
c6f4cdab0f Fix bug reported at https://z3.codeplex.com/workitem/41 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-05-27 17:49:03 -07:00
Leonardo de Moura
edb2f8554d Add new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-05-27 17:45:56 -07:00
Nikolaj Bjorner
7c12ab4716 fix some compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-25 14:40:57 -07:00
Nikolaj Bjorner
ccf10d0abe fix crash in PDR engine when transformations don't produce output predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-25 14:38:02 -07:00
Leonardo de Moura
09945dc2cb Fix compilation error with gcc 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-05-23 08:07:19 -07:00
Ken McMillan
058c8d2083 fixing labels in duality 2013-05-22 15:42:25 -07:00
Ken McMillan
9d611997b3 fixing labels in duality 2013-05-22 15:18:50 -07:00
Ken McMillan
193e255387 Merge /home/mcmillan/pc/Code/z3_interp into interp 2013-05-22 13:31:24 -07:00
Ken McMillan
7905f48e88 status reporting issue 2013-05-22 13:23:37 -07:00
Nuno Lopes
dc91a754dd improve clp solver 
- run default rule transformations
 - sort a predicate's rules by number of queries in the body to bias search

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-21 10:48:55 -07:00
Nikolaj Bjorner
56dedec740 fix build break include uint_set.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-18 10:02:53 -07:00
Nuno Lopes
aea667d09b fix a one-too-many in my previous commit 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-17 12:17:35 -07:00
Nuno Lopes
d1999b3424 AIG exporter: create latches lazily 
properly check for constants

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-17 09:46:30 -07:00
Christoph M. Wintersteiger
5d1339beec .NET/Java: API doc update for Context constructor. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-05-17 13:43:32 +01:00
Nikolaj Bjorner
ef2a9994a9 fix UTVPI model generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-16 19:58:14 -07:00
Nikolaj Bjorner
69b7c3ede7 fixing parity bug in model generation for UTVPI 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-16 15:36:27 -07:00
Nuno Lopes
6560fc0a2c add experimental Horn clause to AIG (AAG format) converter. 
Clauses should be over booleans only (or bit-blasted with fixedpoint.bit_blast=true).
We will crash if that's not the case.
Only linear clauses supported for now

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-16 09:58:31 -07:00
Nuno Lopes
100e396618 fix typo in my previous commit 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-15 13:33:42 -07:00
Nuno Lopes
5efdc58194 horn clause bit blasting: propagate output predicates for predicates without rules (most likely an UNSAT prog) 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-15 13:17:00 -07:00
Nuno Lopes
e6c8149873 horn rule bit blaster: fix propagation of output predicates when arity == 0 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-15 10:50:46 -07:00
Nuno Lopes
878d57d139 minor code simplification 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-15 09:23:57 -07:00
Nuno Lopes
7fc93b94f5 remove unimplemented method 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-05-14 08:54:04 -07:00
Nikolaj Bjorner
ac6488a195 relax pre-processing to untangle non-horn formulas, based on Eldarica/linear benchmarks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-13 13:21:45 -07:00
Nikolaj Bjorner
e35fd58968 add rewriting option to simplify store equalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-13 11:43:30 -07:00
Nikolaj Bjorner
5eed106ffe fix parameters in utvpi and make Karr invariants use backward propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-12 17:02:25 -07:00