mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity
8810 commits 24 branches 48 tags 158 MiB
Commit graph

7261 commits

Author SHA1 Message Date
Nikolaj Bjorner
a0a8bc2a62 fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-24 09:12:43 -07:00
Fábio Ferreira
2e2782577b pretty printer: fix typo with ReSort sort name 2017-07-23 02:32:35 +01:00
Lev Nachmanson
bd4fb22665 track the set of integer variables that are not set to integer values 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-21 21:09:51 -07:00
Christoph M. Wintersteiger
0f1583309d Bugfix for fp.fma. One piece of puzzle #872. 2017-07-21 21:12:45 +01:00
Christoph M. Wintersteiger
faa19117e4 Fixed inconsistent state upon solver interruption. Partially fixes #951. 2017-07-21 17:42:48 +01:00
Lev Nachmanson
64e542bd70 fix term indices for the time being when exiting from check() 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-20 19:13:13 -07:00
Lev Nachmanson
04824e7372 add a check in gomory cut 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-20 18:12:16 -07:00
Christoph M. Wintersteiger
943dc8118a Improved collect-statistics tactic 2017-07-20 13:44:47 +01:00
Lev Nachmanson
1490b7a15f a cleaner version of subs_term_columns 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-19 22:14:05 -07:00
Lev Nachmanson
4d1b0d8026 gomory cut worked on a toy example 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-19 16:50:23 -07:00
Murphy Berzish
7ddb940f77 add e_internalized() check in theory_str::get_arith_value() 2017-07-19 10:15:38 -04:00
Murphy Berzish
69f0ed9b1f remove disabled code block in get_arith_value() 2017-07-18 13:13:12 -04:00
Murphy Berzish
c6707688ba improved get_arith_value() in theory_str 
Since the root of the eqc of an integer term should be a constant
if there is a constant in that eqc, we can ask for it directly
without either iterating over the entire eqc or
asking the arithmetic solver (and receiving potentially stale info).
 2017-07-18 13:11:03 -04:00
Lev Nachmanson
94b3fee6ac rename a function 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-17 16:41:02 -07:00
Lev Nachmanson
729644a2b6 fix term_is_int 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-17 16:08:20 -07:00
Lev Nachmanson
77171f4af8 the first version of Gomory cut, probably broken 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-17 15:17:46 -07:00
Nikolaj Bjorner
8c67e958ff n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-16 18:51:01 +02:00
Christoph M. Wintersteiger
da34de340d Fixed bug in sat model converter. Fixes #1148. 2017-07-15 20:25:13 +01:00
Lev Nachmanson
1931adcb74 add a file 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-13 09:48:29 -07:00
Lev Nachmanson
8750da1da7 progress in gomory cut 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-12 16:43:10 -07:00
Christoph M. Wintersteiger
680f342247 Merge pull request #1145 from delcypher/fix_doc_typo 
Fix minor typo in C API documentation
 2017-07-12 15:47:44 +01:00
Dan Liew
5b511f12b3 Fix minor typo in C API documentation 2017-07-12 13:07:19 +01:00
Dan Liew
89c8f1722f Fix typo that prevented uses of bvsmod_i being parsed. 2017-07-12 12:53:10 +01:00
Lev Nachmanson
2056404ed4 branch on a free variable before trying Gomory cuts 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-11 16:44:04 -07:00
Lev Nachmanson
bac16bac85 start gomory cut 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-11 13:46:46 -07:00
Lev Nachmanson
fc6a876845 start gomory cut 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-11 13:38:59 -07:00
Jack Feser
0e45777104 add get_num_scopes to python solver api 2017-07-11 14:42:34 -04:00
Murphy Berzish
86e7f83e06 proper theory_arith integration in theory_str::get_arith_value() 2017-07-11 13:24:48 -04:00
Lev Nachmanson
69d6b022b8 speed up in get_model and fix in git_model_do_not_care_... 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-10 22:14:56 -07:00
Lev Nachmanson
2fe846d9fc fix a bug in the lar_solver::m_status update during push/pop 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-10 16:34:23 -07:00
Lev Nachmanson
581098299b change the order of initializations in the constructor of imp in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-10 12:04:58 -07:00
Lev Nachmanson
9dc7ba73eb use a faster version of get_model in debug checks 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-10 11:57:33 -07:00
Lev Nachmanson
86ed01a63b replace clp to clean 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-10 11:30:08 -07:00
Lev Nachmanson
cc32e45471 replace lean to lp 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-10 11:06:37 -07:00
Nikolaj Bjorner
2b0106c199 doc fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-09 11:26:27 +02:00
Nikolaj Bjorner
2af08a378d avoid complaining about division by 0 as unhandled in theory-lra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-08 18:21:47 -07:00
Nikolaj Bjorner
5714f830b0 fix check for finite sorts #1122 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-08 13:37:24 -07:00
Lev Nachmanson
f6a75600c2 solve all smt2 from QF_LIA/calypto with int_solver 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-07 22:15:47 -07:00
Nikolaj Bjorner
55f54b4fdc fixing overflow checking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-07 13:53:26 -07:00
Lev Nachmanson
3abc793876 solve more integer smt problems 2017-07-07 11:47:52 -07:00
Nikolaj Bjorner
ea331ebfbe revert update to #1134 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-07 08:29:16 -07:00
Nikolaj Bjorner
d06e48a361 detect overlapping signatures #1134 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-07 08:13:14 -07:00
Nikolaj Bjorner
49cf3f8008 update documentation according to #1058 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-07 07:44:55 -07:00
Nikolaj Bjorner
53c38f02d5 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-06 22:12:18 -07:00
Lev Nachmanson
2cd81851e7 solve more ilp smt 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-07-06 21:29:09 -07:00
Lev Nachmanson
7cd6dc1b5a Merge branch 'master' of https://github.com/levnach/z3 2017-07-06 20:47:19 -07:00
Nikolaj Bjorner
055593469a Dev (#64) 
* 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>

* return branch from int_solver::check()

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

* add a stub for mk_gomory_cut

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

* Dev (#59)

* add handlers for lia moves

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

* spacing

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

* loops

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

* Dev (#60)

* add handlers for lia moves

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

* spacing

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

* loops

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

* loops

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

* Dev (#61)

* add handlers for lia moves

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

* spacing

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

* loops

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

* loops

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

* more TRACE(arith_int)

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

* fix the build

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

* loops

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

* Dev (#62)

* add handlers for lia moves

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

* spacing

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

* loops

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

* loops

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

* loops

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

* build fix

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-06 20:47:07 -07:00
Lev Nachmanson
9b1b096a16 fix in init_int_int_set 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-07-06 20:46:17 -07:00
Lev Nachmanson
0e0e9c7041 correct handling of integer vars by NB 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-06 14:06:33 -07:00
Lev Nachmanson
2e95a9d6b2 return a value from pivot_column_general 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-07-06 10:59:20 -07:00