mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-04 23:13:57 +00:00
Code Activity
13872 commits 26 branches 52 tags 171 MiB
Commit graph

876 commits

Author SHA1 Message Date
Nikolaj Bjorner
fff54d5d08 fix perf regression with negative polynomial normalization, adding new datatype plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-03 03:56:10 -07:00
Nikolaj Bjorner
009e94d188 update to theory_seq following examples from PJLJ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-30 14:00:01 -07:00
Nikolaj Bjorner
9e4b2a6795 port simplifications on bv2int 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-28 02:55:50 -07:00
Nikolaj Bjorner
f76815a009 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-27 12:55:55 -07:00
Nikolaj Bjorner
3bfc3437f1 purify 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-27 11:57:13 -07:00
Nikolaj Bjorner
2ede4b2c80 fixes based on regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-27 09:31:16 -07:00
Nikolaj Bjorner
809a4efc6b removing dependencies on simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-26 11:24:19 -07:00
Nikolaj Bjorner
bcf229dcfd removing dependencies on simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-26 11:23:41 -07:00
Nikolaj Bjorner
82a937d1af enforce arithmetic normalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-26 10:41:25 -07:00
Nikolaj Bjorner
14e6b5b500 mising files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-26 01:38:55 -07:00
Nikolaj Bjorner
b16a4ac452 remove simplify dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-25 23:57:10 -07:00
Nikolaj Bjorner
d3c00181ba remove simplify dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-25 23:56:31 -07:00
Nikolaj Bjorner
ac0bb6a3d0 remove simplify dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-25 23:56:09 -07:00
Nikolaj Bjorner
9438ff848f moved files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-25 17:44:57 -07:00
Nikolaj Bjorner
ebcacaa26d update new assertions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-25 17:44:33 -07:00
Christoph M. Wintersteiger
799fb4a0d1 Revert "Eliminated the dependency of the macro-finder on the simplifier." 
This reverts commit 8310b24c52.
 2017-08-24 21:26:09 +01:00
Christoph M. Wintersteiger
8310b24c52 Eliminated the dependency of the macro-finder on the simplifier. 2017-08-24 20:34:11 +01:00
Nikolaj Bjorner
5141477809 remove dead code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-24 11:16:48 -07:00
Nikolaj Bjorner
23d1c0a9a8 move pull/push files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-24 11:13:01 -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
e5826b957f fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-23 09:01:25 -07:00
Nikolaj Bjorner
ce04c18a7a trying to get rid of last simplifier dependency in macros 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-22 22:14:13 -07:00
Nikolaj Bjorner
e2b46257d6 reducing dependencies on simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-22 15:09:34 -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
07bc19b489 add documentation to string rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-14 07:19:04 -07:00
Nikolaj Bjorner
a39b0b201a another fix to str.to.int/int.to.str semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 17:27:34 -07:00
Nikolaj Bjorner
fb17362dff fix string rewriting according to definition. Relates to examples in #1202 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 17:21:38 -07:00
Nikolaj Bjorner
ead704f52f handle undefined constant cases for int.to.str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-13 17:13:10 -07:00
Nikolaj Bjorner
c4083c367a update handling of contains constraints taking string literals into account 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 19:14:55 -07:00
Nikolaj Bjorner
50e9b371d9 inc version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 17:52:58 -07:00
Nikolaj Bjorner
85cdfd885f address bug reported in #1196 and include additional ad-hoc rewrites to handle some string cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 17:41:18 -07:00
Nikolaj Bjorner
f99048f3e7 rewrite to address some cases like #1203, updates to division handling in NRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-12 13:24:54 -07:00
Nikolaj Bjorner
7b47b0380e update Ackerman reduction for division to make Andre and Nathan happy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-10 23:43:21 +02: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
063b6e9ea5 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 13:24:57 -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
Arie Gurfinkel
15451ae858 extra flags to control quant_hoist 2017-07-31 14:13:45 -04:00
Nikolaj Bjorner
b482dbd589 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 17:02:27 -07:00
Nikolaj Bjorner
30b0d5ba13 Merge branch 'master' of https://github.com/z3prover/z3 2017-07-24 10:49:54 -07:00
Nikolaj Bjorner
08524a2d90 cleanup for warning message 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 11:47:17 -07: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
Nikolaj Bjorner
244cbc2638 ensure that auxiliary PB booleans are recognized during rewriting. Fixes segementation fault #1113, but does not address performance issues with quantifiers and optimization combinations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-26 10:04:50 -07:00
Nikolaj Bjorner
5752830f71 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-22 15:01: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
Nikolaj Bjorner
19d4b0a97a resolve conflicts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-02 10:38:37 -07:00
Nikolaj Bjorner
3ce82ea8ce merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-02 10:37:22 -07:00
Christoph M. Wintersteiger
596652ed36 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-31 18:35:52 +01:00
Christoph M. Wintersteiger
a7d5bb7b36 Tabs 2017-05-31 12:18:00 +01:00
Nikolaj Bjorner
7d245be4e1 enable exposing internal solver state on interrupted solvers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-30 17:33:27 -07:00
Nikolaj Bjorner
e0a86ccc1a add lrb/chb and experiment with them 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-28 10:48:31 -07:00