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

47 commits

Author SHA1 Message Date
Nikolaj Bjorner
64dd4e1c83 fix #2659 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-25 10:42:21 -07:00
Nikolaj Bjorner
4ce6b53d95 fix #2640 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-16 20:40:03 -07:00
Nikolaj Bjorner
ca498e20d1 move value factories to model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-16 19:48:35 -07:00
Bruce Mitchener
e570940662 Prefer using empty rather than size comparisons. 2018-11-27 21:42:04 +07:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:23:04 -07:00
Nikolaj Bjorner
2456513053 sometimes comments are worth reading 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-19 10:43:51 -07:00
Nikolaj Bjorner
86c39c971d fix #1681 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-18 21:53:45 -07:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener
7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Nikolaj Bjorner
cf86e46229 check for datatype selectors when model validation fails 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-17 15:10:50 -07:00
Nikolaj Bjorner
5d17e28667 support for smtlib2.6 datatype parsing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-04 21:12:43 -07:00
Nikolaj Bjorner
a3dba5b2f9 hide new datatype plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-03 20:01:59 -07:00
Nikolaj Bjorner
7dd28781ab remove simplifier dependencies from cmakelist.txt files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-23 16:33:36 -07:00
Nikolaj Bjorner
655b3d9c19 removing dependency on simplifier in pattern_inference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-23 12:17:30 -07:00
Nikolaj Bjorner
e5826b957f fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-23 09:01:25 -07:00
Nikolaj Bjorner
ebe9db14d5 fix regression exposed by segfault2.smt2 crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-21 14:13:43 -07:00
Nikolaj Bjorner
359ee818a5 purge iterators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-20 15:35:16 -07:00
Nikolaj Bjorner
276fdd0e97 register auxiliary constants from projection operation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-20 08:51:24 -07:00
Nikolaj Bjorner
2b82fd5d0c updated include directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 10:51:47 -07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Dan Liew
4b517b96df [CMake] Move CMake files into their intended location so the 
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
 2017-06-12 11:59:00 +01:00
Nikolaj Bjorner
fcda4cee9f ensure evaluation of array equalities is enabled for external facing evaluator. Issue #917 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-09 05:29:56 +01:00
Nikolaj Bjorner
c1480b4389 handle model generation from issue #748. Deal with warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-12 00:40:52 +01:00
Nikolaj Bjorner
dea3b8ddf7 address warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 13:14:36 +01:00
Nikolaj Bjorner
5b497b6249 reduce set of mainly verbose warnings raised by -Wmaybe-uninitialized and unused variable warnings from release mode builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-22 20:25:47 -07:00
Christoph M. Wintersteiger
eb9c5b7cdb Disabled bogus assertions. 
Fixes #489
 2016-04-01 13:25:37 +01:00
Christoph M. Wintersteiger
852dc6d190 whitespace 2016-04-01 13:22:16 +01:00
Nikolaj Bjorner
ec681d7565 some of Arie's fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-23 10:19:16 -07:00
Nikolaj Bjorner
b0f65335ab update copyright year 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-17 13:07:40 -07:00
Nikolaj Bjorner
70f13ced33 make proto-model evaluation use model_evaluator instead of legacy evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-05 10:14:15 -08:00
Nikolaj Bjorner
7c6540e18f recursive function definitions; combine model-building functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-03 07:59:03 -08:00
Nikolaj Bjorner
fce286db91 Issue #354. Fix unsoundness in Array theory based on missing propagation of selects over ite expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-10 17:11:12 -08:00
Nikolaj Bjorner
85b9bb3cc6 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 08:37:47 -08:00
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
Ken McMillan
c007a5e5bd merged with unstable 2014-08-06 11:16:06 -07:00
Nikolaj Bjorner
2ee416fc8f deal with infinite loop in diagonalization attempt in datatype factory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-21 10:23:31 -07:00
Nikolaj Bjorner
3d1ca5ecc9 make eval cache sensitive to model completion. Bug 110 reported by cipher1024 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-15 21:12:16 -07:00
Nikolaj Bjorner
5be4365b47 redo edit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-15 16:53:52 -07:00
Nikolaj Bjorner
c54929e59f cycle through domain size before giving up 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-15 04:52:21 -07:00
Nikolaj Bjorner
21b27cd2d1 patching crash in data-type factory when fresh values are not produced 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-15 04:37:05 -07:00
Nikolaj Bjorner
419f99c329 fix bug found by Ethan: fresh values for bit-vectors loops if the domain of bit-vectors is truly small 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-13 15:30:56 -07:00
Leonardo de Moura
0af4384882 Fix more issues unintepreted sort tests. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-15 16:31:49 -08:00
Leonardo de Moura
d92efeb0c5 Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-18 17:14:25 -08:00
Leonardo de Moura
a07b459fdf Added is_unique_value. Its semantics is equal to the old is_value method. The contract for is_value changed. See comments at ast.h for more information. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 12:53:51 -08:00
Leonardo de Moura
589f096e6e working on new parameter framework 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-01 15:54:34 -08:00
Leonardo de Moura
c5b91aef68 Fixed bug reported by Heizmann at codeplex 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-07 07:52:07 -08:00
Leonardo de Moura
759504880a isolated proto_model obsolete code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-29 20:15:33 -07:00