mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-26 18:15:37 +00:00
Code Activity
17521 commits 37 branches 58 tags 183 MiB
Commit graph

71 commits

Author SHA1 Message Date
Nikolaj Bjorner
31ffe89480 normalize more pretty printing 2022-08-17 08:24:41 -07:00
Jakob Rath
4282cfa148 Remove unused variable 2022-08-04 08:55:04 +02:00
Jakob Rath
1b370727b1 remove redundant subst_val 2022-07-21 13:15:02 +02:00
Jakob Rath
e168d8a2eb Merge branch 'master' into polysat 2022-07-21 12:56:50 +02:00
Nikolaj Bjorner
b29cdca936 integrate factorization to Grobner 2022-07-14 21:24:27 -07:00
Nikolaj Bjorner
4a192850f2 add var_factors 
Add routine to partially factor polynomials. It factors out variables.
 2022-07-14 11:06:53 -07:00
Nikolaj Bjorner
f33c933241 Add substitution routine to pdd 
For Grobner we want to preserve directions of intervals for finding sign conflicts. This means that it makes sense to have external control over linear solutions.
 2022-07-11 12:10:28 -07:00
Nikolaj Bjorner
b68af0c1e5 working on reconciling perf for arithmetic solvers 
this update integrates inferences to smt.arith.solver=6 related to grobner basis computation and handling of div/mod axioms to reconcile performance with smt.arith.solver=2.

The default of smt.arth.nl.grobner_subs_fixed is changed to 1 to make comparison with solver=2 more direct.

The selection of cluster equalities for solver=6 was reconciled with how it is done for solver=2.
 2022-07-11 07:38:51 -07:00
Jakob Rath
e5e79c1d4b Merge branch 'master' into polysat 2022-07-01 16:11:17 +02:00
Nikolaj Bjorner
3d00d1d56b prepare for equality propagation from Grobner basis 
Attempt to remedy performance regressions from the new solver core for NLA. It misses easy lemmas, presumably due to weaker bounds information.
 2022-06-14 09:51:07 -07:00
Jakob Rath
9d47d7959d helper functions to add constraints to univariate_solver 2022-03-17 14:08:00 +01:00
Jakob Rath
1de51da67e get univariate coefficients 2022-03-11 18:03:39 +01:00
Nikolaj Bjorner
8c9835bca6 smul no overflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 18:55:07 +02:00
Nikolaj Bjorner
cbbf1381f7 update to use incremental substitution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-23 03:00:25 +01:00
Jakob Rath
28864e563c First version of refine_disequal_lin 2021-12-23 18:36:27 +01:00
Nikolaj Bjorner
f1d46b58a4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-11 17:38:09 -08:00
Nikolaj Bjorner
6478e789e9 optimizations, fixes, TODO items 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 14:50:18 -07:00
Nikolaj Bjorner
1e3ff3179e handle empty clauses created as lemmas as unsat state. 
add unit tests
 2021-09-19 15:43:47 -04:00
Nikolaj Bjorner
fa3886136b adding Boolean propagation, watch; and factoring 2021-09-18 22:18:15 -04:00
Nikolaj Bjorner
611c28fc47 push outline of using cjust for overflow premise 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-09 09:56:00 +02:00
Nikolaj Bjorner
d8f0926620 re-adding saturation for inequalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-07 23:20:17 +02:00
Nikolaj Bjorner
04ce8ca5ef u256, separate viable_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-04 23:47:12 -07:00
Jakob Rath
d7b8ea2f7f
Polysat: minor fixes (#5364) 
* update include paths

* bdd fixes

* update/fix some tests

* work around assertion failure when constraint from clause becomes unit

* Remove old code

* use clause_builder

* Verify model when returning SAT

* log

* fix
 2021-06-22 09:27:18 -07:00
Jakob Rath
c4963f4381
Polysat: add two more prototype rules (#5355) 
* Add try_div to PDDs

* x>y is false when x==y

* First version of the other two prototype rules

* More band-aid fixes...
 2021-06-18 08:48:50 -07:00
Jakob Rath
f83705bf9f
Polysat: first pass at forbidden intervals (not yet fully integrated into solver) (#5227) 
* Add interval class

* Take dependency as const reference

* Compute forbidden intervals for ule-constraints

* Add class for evaluated interval

* We need the evaluated bounds as well

* Don't add constraint to cjust multiple times (hack, to be improved later)

* typo

* More interval helpers

* Add constraint::ult factory function

* Fix forbidden interval condition

* Add solver::has_viable

* Add conflict explanation using forbidden intervals (not yet fully integrated into solver)
 2021-04-29 10:12:54 -07:00
Jakob Rath
2fac9e6e66
Add propagate/narrow for ule_constraint (#5214) 
* Add helper to check whether pdd is univariate and linear

* Reorganize propagate/narrow of eq_constraint

* Implement propagate/narrow for ule constraints

* Also push trail instruction in push_viable
 2021-04-23 08:41:02 -07:00
Jakob Rath
324d9ed461
Add more PDD utilities (div, pow) (#5180) 
* Expose 'inv' on rationals to get reciprocal value

* Align parameter names with implementation

* Add cached operation that divides PDD by a constant

* Fix display for constant PDDs

* operator^ should probably call ^ instead of + (mk_xor instead of add)

* Add helper function 'pow' on PDDs
 2021-04-14 04:48:42 -07:00
Nikolaj Bjorner
a0d112b7b0 general form migration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-13 13:00:47 -07:00
Jakob Rath
0e9fc4762a Fix PDD factor cache in case GC happens while factoring (#5170) 
* Add method to find largest power of two that is a divisor

* Binary resolve on PDDs

* Add unit tests for binary resolve

* Fix factor cache access in case GC happens while factoring

* Coding conventions

* Change to gc_generation
 2021-04-12 11:20:40 -07:00
Jakob Rath
75c87a2869 Test and memoize pdd factoring (#5163) 
* Test and fix pdd_manager::factor

* Memoize pdd_manager::factor

* Fix Windows build (maybe)
 2021-04-12 11:20:40 -07:00
Nikolaj Bjorner
446654b680 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-12 11:20:39 -07:00
Nikolaj Bjorner
c2b353ba72 adding factorization 2021-03-26 14:58:24 -07:00
Nikolaj Bjorner
2fef6dc502 more scaffolding 2021-03-21 11:31:14 -07:00
Nikolaj Bjorner
d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Nuno Lopes
e844aef896 remove a few more copy constructors, though still not enough to enable the assertion in vector 
I give up for now; there are too many copies left for little return..
 2020-06-03 20:32:13 +01:00
Nikolaj Bjorner
b889b110ee bool_vector, some spacer tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 12:59:04 -07:00
Lev Nachmanson
06203d227e cleanup the grobner config init 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
7ad95aa5d2 Nikolaj fixes pdd_manager::reduce() to work with the changed order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
d6a246777a Nikolaj implemented lm_lt on dd::pdd 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
cca19ef1a7 unit tests for dd_pdd ordering 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
61da9a8aeb test the new order on pdd 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
407c8a60db reverse the order of vars for pdd_grobner, use pdd_grobner.reset() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
b5364b787c set level2var for m_pdd_manager of pdd_grobner 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
610a2837ea rebase with Z3Prover 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
5e19a52772 merge changes from Z3Prover 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Nikolaj Bjorner
301f9598a4 fixing leading term computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-08 12:10:23 -08:00
Nikolaj Bjorner
2acab46388 anf translation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-05 21:09:52 -08:00
Nikolaj Bjorner
d27a949ae9 add anf and aig simplifier modules, cut-set enumeration, aig_finder, hoist out xor_finder from ba_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-05 16:46:49 -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