mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity
17527 commits 23 branches 48 tags 156 MiB
Commit graph

215 commits

Author SHA1 Message Date
Nikolaj Bjorner 44679d8f5b
arith_solver (#4733) 
* porting arithmetic solver

* integrating arithmetic

* lp

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-16 10:49:46 -07:00
Nikolaj Bjorner fa58a36b9f
model refactor (#4723) 
* refactor model fixing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* missing cond macro

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add macros dependency

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* deps and debug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add dependency to normal forms

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* build issues

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* compile

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix leal regression

* complete model fixer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fold back private functionality to model_finder

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* avoid duplicate fixed callbacks

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-05 14:13:05 -07:00
Nikolaj Bjorner 79162b96f3 updated dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-01 08:11:55 -07:00
Nikolaj Bjorner 43db7df2b5
user solver (#4709) 
* user solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-24 04:55:34 -07:00
Nikolaj Bjorner d56dd1db7b update version' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-11 04:37:35 -07:00
Nikolaj Bjorner fe43f8df8f na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-03 08:11:43 -07:00
Nikolaj Bjorner 35e3d8425c move fpa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 11:16:21 -07:00
Nikolaj Bjorner b9cbb08858 shuffle dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 09:51:39 -07:00
Nikolaj Bjorner 86c11b9349 order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 13:05:25 -07:00
Nikolaj Bjorner b03d1c8053 deps 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 13:01:49 -07:00
Nikolaj Bjorner 0440cfeea7 add smt params dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 12:59:22 -07:00
Nikolaj Bjorner 4244ce4aad adding ack/model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 12:55:47 -07:00
Nikolaj Bjorner 4ab35a9bb5 euf model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-26 15:55:20 -07:00
Nikolaj Bjorner c21a2fcf9f sat solver setup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-26 09:40:42 -07:00
Nikolaj Bjorner ecd3315a74 add sat-euf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-25 12:16:57 -07:00
Nikolaj Bjorner 3dedc13481 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-24 02:00:37 -07:00
Nikolaj Bjorner 65e6d942ac euf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-24 01:55:13 -07:00
Nikolaj Bjorner 17b8db95c1 inc version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-08 15:05:01 -07:00
Nikolaj Bjorner 611c14844d fix #3194, remove euclidean solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-08 16:05:13 +01:00
Lev Nachmanson 8388868c27 fix the make build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 3bc67d1804 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson 6cd495979d fix the test build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Nikolaj Bjorner 40a4326ad4 add anf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-05 16:46:49 -08:00
Nikolaj Bjorner 1d0572354b add bit-matrix, avoid flattening and/or after bit-blasting, split pdd_grobner into solver/simplifier, add xlin, add smtfd option for incremental mode logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-01 20:14:20 -08:00
Nikolaj Bjorner 469f618742 build dependencies, invariant annotation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 13:48:27 -08:00
Nikolaj Bjorner 1fdde9e056 move bdd to separate space 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 10:03:01 -08:00
Nikolaj Bjorner e45bafe9bf increase version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-19 14:17:48 -08:00
Nikolaj Bjorner 22b6233e62 increment version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-22 08:31:10 -07:00
Nikolaj Bjorner 3b1a73b9e8 add smt to project.py dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-07 18:04:32 +03:00
Nikolaj Bjorner 60e4cad7f1 increase minor version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-31 17:01:42 -07:00
Nikolaj Bjorner 4d30639fd7 merge dotnetcore into dotnet 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 13:01:48 -07:00
Nikolaj Bjorner 6604aab1a2 remove dotnet as a build option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-29 17:08:45 -07:00
Nikolaj Bjorner 7e7cdf3635 update dependencies in legacy build system 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-01 12:13:50 -07:00
Nikolaj Bjorner 9dd41ba554 remove offending assert, disable assembly-info for dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 11:13:03 -08:00
Nikolaj Bjorner e1dc553228 inc version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-20 13:15:50 -08:00
Nikolaj Bjorner e83e9b02df increment version number to 4.8.4 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-19 15:17:55 -08:00
Nikolaj Bjorner becf5de872 with Mathias on nuget package generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-15 16:16:15 -08:00
Nikolaj Bjorner 0f0287d129 prepare release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-28 17:42:16 -05:00
Nikolaj Bjorner 163e1e3e55 avoid name clash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-22 11:03:41 -07:00
Nikolaj Bjorner 8a93f34b4a Merge branch 'master' of https://github.com/z3prover/z3 2018-10-22 11:00:07 -07:00
Nikolaj Bjorner 81a92edb61 prepare to retool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-22 10:59:51 -07:00
Nikolaj Bjorner 694a6a26c9 bump version, add double access 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-19 20:20:08 -07:00
Nikolaj Bjorner 016872a5e0 increment patch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-15 12:44:19 -07:00
Nikolaj Bjorner 0c4754d94b rename version.h to z3_version.h to differentiate name in install include directory. Add support for z3_version.h in python build system. #1833 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-21 20:13:58 -07:00
Nikolaj Bjorner e041ebbe80 bmc improvements, move fd_solver to self-contained directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:00:49 -07:00
Nikolaj Bjorner c247abfc65 prepare js output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-03 22:13:25 -07:00
Nikolaj Bjorner b6c43f6143 move files for build script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:13:55 -07:00
Nikolaj Bjorner 6e27ad42c8 remove pdr reference from legacy build script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:02:50 -07:00
Nikolaj Bjorner b37a5b1679 clean up python build files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-25 10:27:12 -07:00
Nikolaj Bjorner f5775f265a fix python build script dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-23 09:21:33 -07:00
Nikolaj Bjorner 78b9f0686a merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 07:43:29 -07:00
Nikolaj Bjorner f525f43e43 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-30 09:30:43 -07:00
Nikolaj Bjorner 2dc92e2b94 merge with pull request #1557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-07 17:22:49 -07:00
Nikolaj Bjorner 21a3b9c8e2 increment version number due to ABI/API breaking change #1556 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-31 05:20:47 -07:00
Nikolaj Bjorner c513f3ca09 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:57:01 -07:00
Nikolaj Bjorner 3d9139f6ef bump revision 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-10 12:07:55 -08:00
Nikolaj Bjorner ad92bfb1a1 fix python build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-01 20:19:24 -08:00
Christoph M. Wintersteiger 63951b815d Bumped version number. 2017-12-18 18:58:21 +00:00
Nikolaj Bjorner b96dacfff2 set version, fix build of test files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-30 08:42:01 -08:00
Nikolaj Bjorner 161b6a9983 increase minor version, update java/.net apis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 11:51:37 -08:00
Nikolaj Bjorner 89971e2a98 remove smtlib1 dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 10:37:30 -08:00
Nikolaj Bjorner 60b970b9ba add proofs dependency to solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:23:13 -07:00
Nikolaj Bjorner db65cc007a move more proof utils 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 10:27:48 -07:00
Nikolaj Bjorner d67f3c1466 create proofs folder, move proof-post-order utility to proofs directory, fix regression with proofs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 03:08:56 -07:00
Nikolaj Bjorner 597f77cd77 initial sketch for dominator based simplifiation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-28 20:03:31 -07:00
Nicolas Braud-Santoni 4cb7f72509 First version of the inj. tactic 2017-08-22 17:10:20 +00:00
Arie Gurfinkel 5b9bf74787 Spacer engine for HORN logic 
The algorithms implemented in the engine are described in the following papers

Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96

Nikolaj Bjørner, Arie Gurfinkel:
Property Directed Polyhedral Abstraction. VMCAI 2015: 263-281

Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki:
SMT-Based Model Checking for Recursive Programs. CAV 2014: 17-34
 2017-07-31 17:02:29 -04:00
Nikolaj Bjorner 911b24784a merge LRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-09 10:46:11 -07:00
Christoph M. Wintersteiger 889e5e9388 Bumped version number. 2016-11-07 23:19:59 +00:00
Christoph M. Wintersteiger d57a2a6dce Bumped version to 4.5.0 2016-11-07 22:02:30 +00:00
Christoph M. Wintersteiger 7f923c6a33 Include Python API files in distributions. 2016-11-07 22:00:28 +00:00
Christoph M. Wintersteiger 009af4455d Refactored and fixed model conversion for fpa2bv conversion of unspecified values via theory_fpa. 2016-10-15 18:35:39 +02:00
Andrew Dutcher cb83c42100 Make python stuff live in a python directory in the build tree 2016-09-14 01:49:16 -07:00
Christoph M. Wintersteiger 7fefe40f21 Added/improved facilities for strong name signing of the .NET assembly. 2016-07-28 18:07:34 +01:00
Nikolaj Bjorner b303fd59c0 add some version information (and date) to log file to make it easier to trap version mismatch on log files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-28 18:11:30 -07:00
Nikolaj Bjorner 20bbdfe31a moving remaining qsat functionality over 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 15:35:26 -07:00
Nikolaj Bjorner e484fc365d add outline of bv bounds tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 22:57:47 +00:00
mikolas faa620f673 Further refactoring ackermannization. 2016-02-03 17:31:19 +00:00
mikolas 2679b74543 refactoring 2016-02-03 13:53:52 +00:00
Mikolas Janota 2141a075ba Refactoring ackermannization functionality. 2016-01-28 18:24:54 +00:00
Mikolas Janota e7477e2f6a Moving things around. Adding tactic just for ackermannization. 2016-01-26 17:02:51 +00:00
Mikolas Janota 743a59254e Merge remote-tracking branch 'upstream/master' into lackr 2016-01-07 16:39:43 +00:00
Nikolaj Bjorner f414869456 add symbolic automaton 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-23 19:46:10 -08:00
Mikolas Janota c6e66ebc3a Adding ackr component. 2015-12-15 18:43:36 +00:00
Dan Liew 0a8cd3ae19 Refactor the install and uninstall commands for the python bindings 
out of ``DLLComponent`` and into ``PythonInstallComponent`` where they
belong.
 2015-12-08 23:10:48 +00:00
Nikolaj Bjorner 6c73c176b3 make dotnet optional and recover from python installation mismatch. Pull requests #338, #340 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 19:10:11 -08:00
Christoph M. Wintersteiger 00271e5531 C API cleanup. Mainly removal of ML-specific macros that are not used anymore and inline documentation fixes. 2015-12-03 17:33:25 +00: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 9cba63c31f remove deprecated iz3 example. Remove deprecated process control 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 12:32:15 -08:00
Christoph M. Wintersteiger 115187ee2b Bumped version number to 4.4.2. 2015-10-05 16:04:03 +01:00
Henning Guenther c7e96d897a Replace cone-of-influence filter with generalized dataflow-engine 
Signed-off-by: Henning Guenther <t-hennig@microsoft.com>
 2015-06-29 10:50:51 +01:00
Nikolaj Bjorner 949c21ca08 enable incremental sat for QF_BV 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-21 02:23:56 -07:00
Nikolaj Bjorner fe7c577d99 isolate inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-21 01:54:52 -07:00
Christoph M. Wintersteiger 85419ca503 Added branch into QF_NRA from QF_FP problems containing to_real terms. 2015-05-29 14:21:27 +01:00
Nikolaj Bjorner ab5022888c Merge branch 'opt' of https://github.com/Z3Prover/z3 into unstable 2015-05-14 12:11:17 +01:00
Nikolaj Bjorner 839e3fbb7c add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-09 19:40:34 -07:00
Christoph M. Wintersteiger 8c9afa423b Bumped version number to 4.4.1 in unstable. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-04-29 17:22:24 +01:00
Nikolaj Bjorner 52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
Christoph M. Wintersteiger ffd10675f4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-23 11:07:48 +00:00
Christoph M. Wintersteiger d56d63e3e8 Merge branch 'fpa-api' of https://git01.codeplex.com/z3 into unstable 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

Conflicts:
	src/tactic/portfolio/default_tactic.cpp
 2015-01-21 14:25:31 +00:00