mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-08 00:05:46 +00:00
Code Activity
16916 commits 25 branches 48 tags 158 MiB
Commit graph

46 commits

Author SHA1 Message Date
Bruce Mitchener
42f5047463 cmake: Cleanup remnants of workaround for USES_TERMINAL. 
In older versions, this was dependent upon the version of cmake,
but when it was updated for newer cmake, these remnants were
left.
 2022-08-02 17:39:10 +03:00
Nikolaj Bjorner
08294d62e5 separate dependencies for qe_lite 2022-01-12 03:26:22 -08:00
Nikolaj Bjorner
8ba0fb5b58 rounding mode sort removed for incompatibility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-21 16:18:43 -07:00
Nikolaj Bjorner
731cf9b885 ensure compilation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-19 15:37:05 -07:00
Nikolaj Bjorner
ab0735fde2 separate component for asserted_formulas to break dependency cycles 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-17 15:51:38 -07:00
Nikolaj Bjorner
ddbcd08d46 move asserted_formulas to solver scope 2021-03-17 15:02:16 -07:00
Nikolaj Bjorner
8412ecbdbf fixes to new solver, add mode for using nlsat solver eagerly from nla_core 2021-03-14 13:57:04 -07:00
Nikolaj Bjorner
72d407a49f
mbp (#4741) 
* adding dt-solver

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

* dt

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

* move mbp to self-contained module

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

* files

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

* Create CMakeLists.txt

* dt

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

* rename to bool_var2expr to indicate type class

* mbp

* na

* add projection

* na

* na

* na

* na

* na

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

* deps

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

* testing arith/q

* na

* newline for model printing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-21 15:48:40 -07:00
Nikolaj Bjorner
2f756da294
adding dt-solver (#4739) 
* adding dt-solver

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

* dt

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

* move mbp to self-contained module

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

* files

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

* Create CMakeLists.txt

* dt

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

* rename to bool_var2expr to indicate type class

* mbp

* na
 2020-10-18 15:28:21 -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
b9cbb08858 shuffle dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 09:51:39 -07:00
Nikolaj Bjorner
4e6476c90a fix cmake build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 09:22:04 -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
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
65e6d942ac euf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-24 01:55:13 -07:00
Nikolaj Bjorner
becf423c77
remove level of indirection for context and ast_manager in smt_theory (#4253) 
* remove level of indirection for context and ast_manager in smt_theory

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

* add request by #4252

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

* move to def

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

* int

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-08 16:46:03 -07:00
ahumenberger
df1b308dd0
Julia bindings (#3228) 
* First steps toward adding Julia bindings

* Simplifications

* Streamlining

* Friends of tactic and probe

* Add missing functions

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Changes for CxxWrap v0.9.0

* Wrap enumeration and tuple sort

* Wrap z3::fixedpoint

* Wrap z3::optimize

* Wrap missing functions

* Fix aux types

* Add some missing functions

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit 5aab9f9240.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit cfccd7ca2c.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit f24740c595.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit 592499eaa0.

* Checkout current version of pipeline

* Build Julia bindings on macOS
 2020-03-10 09:16:34 -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
976f10c613 rebase with Z3Prover 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9c62b431e4 address the NB's comments 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
b6f07e2a23 roll back changes in get_model 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Nikolaj Bjorner
12e727e49a na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-05 16:46:49 -08:00
Nikolaj Bjorner
f090abce9f add deps 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 11:33:16 -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
a0dcad0221 fix #2708 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-19 21:36:13 -08:00
Nikolaj Bjorner
53a01a07bd rename additional build options #2709 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-18 21:32:35 -08:00
Julien Schueller
c93a265b0b Install dlls in prefix/bin 
Static/Import libraries usually go to prefix/lib and exe/dlls into prefix/bin
 2019-10-13 05:28:16 -07:00
Charlie Barto
167f968fa8 Change from BINARY_DIR to PROJECT_BINARY_DIR 2019-05-15 11:25:40 -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
39ed27101e include version.h in install include directory for cmake build #1833 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-20 19:56:55 -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
6adaed718f remove pdr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Nikolaj Bjorner
4f5775c531 remove interpolation and duality dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-24 08:33:48 -07:00
Nikolaj Bjorner
e4d24fd2c3 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 09:39:19 -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
89971e2a98 remove smtlib1 dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 10:37:30 -08:00
Nikolaj Bjorner
df6b1a707e remove proof_converter from tactic application, removing nlsat_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 23:32:29 -08:00
Nikolaj Bjorner
fd49a0c89c added facility to persist model transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 00:05:52 -05: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
651587ce01 merge with master branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-19 09:39:22 -07:00
Nikolaj Bjorner
f20e95184e remove old_simplify dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-28 13:29:51 -07:00
Arie Gurfinkel
d080c146a2 public API for spacer 2017-07-31 17:03:18 -04: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
a28a8304b7 Dev (#56) 
* introduce int_solver.h

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add int_solver class

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* track which var is an integer

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* add queries for integrality of vars

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* resurrect lp_tst in its own director lp

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* add file

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* add_constraint has got a body

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* fix add_constraint and substitute_terms_in_linear_expression

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* after merge with Z3Prover

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* adding stub check_int_feasibility()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Dev (#50)

* initial skeletons for nra solver

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

* initial skeletons for nra solver

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

* small fix in lar_solver.cpp

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* adding some content to the new check_int_feasibility()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Dev (#51)

* initial skeletons for nra solver

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

* initial skeletons for nra solver

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

* adding more nlsat

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

* nlsat integration

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

* adding constraints

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

* adding nra solver

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

* add missing initialization

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

* adding nra solver

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

* test

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* Dev (#53)

* change in a comment

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Disabled debug output

* removing FOCI2 interface from interp

* remove foci reference from cmakelist.txt

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

* initial skeletons for nra solver

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

* initial skeletons for nra solver

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

* adding more nlsat

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

* nlsat integration

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

* adding constraints

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

* adding nra solver

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

* add missing initialization

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

* adding nra solver

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

* adding nra

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

* debugging nra

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

* updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver

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

* n/a

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

* integrate nlsat

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

* tidy

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

* preserve is_int flag

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove a debug printout

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Dev (#54)

* change in a comment

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Disabled debug output

* removing FOCI2 interface from interp

* remove foci reference from cmakelist.txt

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

* initial skeletons for nra solver

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

* initial skeletons for nra solver

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

* adding more nlsat

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

* nlsat integration

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

* adding constraints

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

* adding nra solver

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

* add missing initialization

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

* adding nra solver

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

* adding nra

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

* debugging nra

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

* updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver

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

* n/a

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

* integrate nlsat

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

* tidy

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

* use integer test from lra solver, updated it to work on term variables

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

* fix equality check in assume-eq

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

* fix model_is_int_feasible

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* untested gcd_test()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* call fill_explanation_from_fixed_columns()

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* add the call to pivot_fixed_vars_from_basis() to int_solver.cpp::check()

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* port more of theory_arith_int.h

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* use statistics of lar_solver by theory_lra.cpp

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* port more code to int_solver.cpp

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* add an assert

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* more int porting

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix a bug in pivot_fixed_vars_from_basis

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* small change

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* implement find_inf_int_base_column()

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* catch unregistered vars in add_var_bound

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* add a file

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* compile for vs2012

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* fix asserts in add_var_bound

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* fix the lp_solver init when workig on an mps file

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* towards int_solver::check()

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* change in int_solver::check() signature

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>

* add handlers for lia moves

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

* spacing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-28 13:12:12 -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
Renamed from contrib/cmake/src/CMakeLists.txt (Browse further)