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

2549 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ken McMillan
4763532501 adding compile-time option to replace arrays with maps in smt (define SPARSE_MAP) 2014-09-30 11:25:47 -07:00
Ken McMillan
4c71e9479d optimizing array final check 2014-09-30 11:21:34 -07:00
Nuno Lopes
97a5e6d326 assorted compiler warnings fixes 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-28 12:21:56 +01:00
Nuno Lopes
5f59dd1644 revert usage of popcnt is MSVC 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-28 11:37:11 +01:00
Nikolaj Bjorner
e57e5328ce configuration update to SAT solver on creation time. Adding random_seed to sat parameters to enable command-line and module mode to work at the level of sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 16:42:11 -07:00
Nikolaj Bjorner
9412890c63 trace reason for undef in arithmetic, enable model generation on THEORY incompleteness, but retain undef result 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 12:58:55 -07:00
Nikolaj Bjorner
4995ce1fde disable unstable interpolation sample 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-22 22:22:26 -07:00
Nikolaj Bjorner
dca3ce6b24 update documentation on models associated with solver objects 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-22 01:16:16 -07:00
Nuno Lopes
b243ac945f hoprfully fix the build for MSVC 2010 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-21 15:20:43 +01:00
Nuno Lopes
d36cecc2f3 make use of count population intrinsincs on MSVC/gcc/clang 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-19 15:51:08 +01:00
Christoph M. Wintersteiger
bb56885147 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-18 17:10:38 +01:00
Christoph M. Wintersteiger
9949c7e31c fixed typos 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-09-18 17:09:22 +01:00
Nuno Lopes
61d67dc2de fix a few compiler warnings 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-18 14:38:40 +01:00
Nikolaj Bjorner
45bfcda16c remove typename 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-17 16:37:53 -07:00
Nuno Lopes
4717d9d1f4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-17 16:33:45 +01:00
Nuno Lopes
b95f5b0fea fix bug in the datalog compiler when using negation 
We now perform negation after filtering with interpreted constraints so that
the table reflects relevant columns which were not being added by the negation

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-17 16:33:27 +01:00
Nikolaj Bjorner
a85f1784db updated answer to binary interpolant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 23:25:39 -07:00
Nikolaj Bjorner
1636e35bf9 fix scope accounting bug in deprecated solver mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 20:11:44 -07:00
Nikolaj Bjorner
e8b9c251d5 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-16 17:13:20 -07:00
Nikolaj Bjorner
d01ca11001 reduce asymptotic overhead of asserting bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 17:13:09 -07:00
Nuno Lopes
79326e24df fix debug build.. 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-16 15:29:25 +01:00
Nuno Lopes
f7c3559c31 fix a few compiler warnings 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-16 15:26:01 +01:00
Nuno Lopes
d3570484bb Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-16 14:57:22 +01:00
Nuno Lopes
919e0a5ea2 Z3Py: fix bug in substitute() with a list of on variable 
e.g. print substitute(Int('x'), [(Int('x'), Int('y'))])

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-16 14:56:59 +01:00
Nikolaj Bjorner
67b802c9d9 fix scope accounting bug and documentation per Konrad's request 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-12 17:38:34 -07:00
Nikolaj Bjorner
c917c1c53d reset ast trail on context deletion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-12 15:54:42 -07:00
Christoph M. Wintersteiger
6b37b847a0 merge fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-09-11 00:27:37 +01:00
Christoph M. Wintersteiger
3660c617ea Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls 
Conflicts:
	src/tactic/sls/sls_tactic.cpp

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-09-11 00:19:05 +01:00
Christoph M. Wintersteiger
f8861915d2 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-10 23:54:34 +01:00
Ken McMillan
13b61d894c adding recursion bounds to duality 2014-09-09 14:02:46 -07:00
Nikolaj Bjorner
dd62ca5eb3 simplify models 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-06 20:54:16 -07:00
Nikolaj Bjorner
36816e3b2f clear cache for crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-06 19:03:37 -07:00
Nikolaj Bjorner
904ab4bf9e address race condition in cleanup methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-05 11:18:34 -07:00
Nikolaj Bjorner
19a8fa8a25 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-04 14:50:19 -07:00
Nikolaj Bjorner
3d9120c745 lifetime of expressions from model follow life-time of model, not the push/pop scope making scope based reference counting error prone 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-04 14:49:58 -07:00
Christoph M. Wintersteiger
23af977d68 Multi-threading bugfix, DLL could be used from other threads before the main thread initializes it. 
Thanks to user xor88 for reporting this one.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-09-03 17:49:10 +01:00
Christoph M. Wintersteiger
fa24d9db6f Added multi processor compilation to VS project. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-09-01 17:27:07 +01:00
Nikolaj Bjorner
d90049e9b0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-08-28 10:18:49 -07:00
Nikolaj Bjorner
8ea7109f8f update documentation to clarify reference counting policies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-28 10:18:42 -07:00
Ken McMillan
672b8e1022 merging fixes with unstable 2014-08-26 14:01:12 -07:00
Ken McMillan
9b3ef92813 merge with push/pop fixes 2014-08-26 13:50:51 -07:00
Ken McMillan
51aa10821e fixed pop issue and interpolation proof mode issue 2014-08-26 13:46:53 -07:00
Christoph M. Wintersteiger
f023b8992f Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-08-22 12:57:45 +01:00
Christoph M. Wintersteiger
38ee8cb807 .NET API: bugfix. Thanks to Konrad Jamrozik for catching this one. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-08-22 12:57:33 +01:00
Nikolaj Bjorner
9e3e52f4f6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-08-18 18:38:35 -07:00
Ken McMillan
da76a51ce6 merging with unstable 2014-08-18 17:14:49 -07:00
Ken McMillan
70a1155d71 fixed duality bug and added some code for returning bounded status (not yet used) 2014-08-18 17:13:16 -07:00
Nikolaj Bjorner
d4ec48219f Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-08-17 21:22:29 -07:00
Nikolaj Bjorner
60054ce469 fix cache bug in PDR reported by Phillip Ruemmer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-17 21:20:56 -07:00
Christoph M. Wintersteiger
37ed4b04d0 Bugfix: param_refs didn't make it through to smt::solver (smt_params) in some cases. 
Thanks to user xor88 for pointing us in the right direction!

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-08-14 12:18:00 +01:00