mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-15 17:06:39 +00:00
Code Activity
16369 commits 43 branches 51 tags 169 MiB
Commit graph

227 commits

Author SHA1 Message Date
Nikolaj Bjorner
ef28f0e2f0 #5778 
deal with recursive calls to internalization with the same formula
 2022-04-02 01:28:58 -07:00
Nikolaj Bjorner
4392b88718 return negated literal when expression is "not" 2022-01-31 12:00:00 -08:00
Nikolaj Bjorner
7ddfc54250 shortcut negation 2022-01-31 11:58:02 -08:00
Nikolaj Bjorner
d1fb831030 relevancy overhaul 2022-01-04 16:03:31 -08:00
Nikolaj Bjorner
a086f6218b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-03 14:15:41 -08:00
Nikolaj Bjorner
8e3185ffe3 remove dual solver approach 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-03 14:08:01 -08:00
Nikolaj Bjorner
1f964eea90 na 2022-01-03 11:12:28 -08:00
Nikolaj Bjorner
2944449884 #5641 2022-01-03 11:12:09 -08:00
Nikolaj Bjorner
fc77345bec breaking change. Enforce append semantics everywhere for parameter updates #5744 
Replace semantics doesn't work with assumptions made elsewhere in code.
The remedy is to apply append (override) semantics for parameter changes.
 2021-12-30 19:11:14 -08:00
Nikolaj Bjorner
9f2b18cac5 add tactic name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-07 13:37:57 -08:00
Jamey Sharp
426306376f
CNF conversion refactoring (#5547) 
* split sat2goal out of goal2sat

These two classes need different things out of the sat::solver class,
and separating them makes it easier to fiddle with their dependencies
independently.

I also fiddled with some headers to make it possible to include
sat_solver_core.h instead of sat_solver.h.

* limit solver_core methods to those needed by goal2sat

And switch sat2goal and sat_tactic over to relying on the derived
sat::solver class instead. There were no other uses of solver_core.

I'm hoping this makes it feasible to reuse goal2sat's CNF conversion
from places like the tseitin-cnf tactic, so they can be unified into a
single implementation.
 2021-09-20 08:53:10 -07:00
Nikolaj Bjorner
e05ef8ece9 account for updating scoped state by goal2sat #5528 2021-09-02 04:20:19 -07:00
Nikolaj Bjorner
fc36fb115f format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-02 13:45:23 -07:00
Nikolaj Bjorner
d3194bb8a8 #5445 2021-08-02 11:07:28 -07:00
Nikolaj Bjorner
e3be25dad6 #5445 2021-08-01 16:48:25 -07:00
Nikolaj Bjorner
924ea6ab31 #5429 again 2021-08-01 12:00:22 -07:00
Nikolaj Bjorner
ed27ce5526 fix regression in goal2sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 11:41:55 -07:00
Nikolaj Bjorner
6a9241ff0f #5429 2021-07-31 11:00:12 -07:00
Nikolaj Bjorner
77cd82a5ca flatten if-then-else 2021-07-30 23:28:30 -07:00
Nikolaj Bjorner
442d1d28ea #5429 2021-07-27 19:11:16 -07:00
Nikolaj Bjorner
76427cd281 #5427 2021-07-22 11:33:47 -07:00
Nikolaj Bjorner
8a4b292f3e #5422 2021-07-21 06:25:30 -07:00
Nikolaj Bjorner
34fc0cdd5c #5324 2021-06-06 16:23:27 -07:00
Nikolaj Bjorner
1fd6b66ecc #fix #5328 
in-processing for "pure" PB constraints isn't model preserving and therefore removed.
 2021-06-05 12:02:33 -07:00
Nikolaj Bjorner
4d41db2920 #5223 
unreachable code in dual solver
 2021-05-29 09:49:47 -07:00
Nikolaj Bjorner
abe3ef2382 #5215 2021-05-19 10:33:23 -07:00
Nikolaj Bjorner
a61e9d6b49 #5260 2021-05-10 10:33:43 -07:00
Nikolaj Bjorner
4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
c629f09f21 fix #5139 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-29 15:46:47 -07:00
Nikolaj Bjorner
dfb696becf fix #5119 2021-03-28 16:47:56 -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
e398959732 move eq solver functionality to common place, fixes to goal2sat 2021-03-04 07:57:31 -08:00
Nikolaj Bjorner
79ababb00a force push 2021-03-03 11:38:33 -08:00
Nikolaj Bjorner
69070a7486 align translation cache with scopes and variable elimination 2021-03-03 11:22:17 -08:00
Nikolaj Bjorner
026065ff71 streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
Nikolaj Bjorner
4455f6caf8 move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail 2021-02-02 03:58:19 -08:00
Nikolaj Bjorner
bb56443e71 more #4932 2021-01-08 15:24:12 -08:00
Nikolaj Bjorner
cd77a4d9a5 fix #4909 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 11:53:19 -08:00
Nikolaj Bjorner
4d55f83654 misc 2020-12-04 16:59:13 -08:00
Nikolaj Bjorner
12198d13ac fix #4794 2020-12-02 12:24:35 -08:00
Nikolaj Bjorner
85a20791db fix relevancy tracking in new solver 2020-11-16 11:20:17 -08:00
Nikolaj Bjorner
7e68d546ba na 2020-11-11 17:37:07 -08:00
Nikolaj Bjorner
ab199dedf9 debug arith/mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-02 12:13:19 -08:00
Nikolaj Bjorner
8d76470a8a fixes to mostly solver arith/euf and backtracking scopes 2020-10-26 11:06:41 -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
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
a414480274 mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-29 15:49:48 -07:00
Nikolaj Bjorner
367e5fdd52
delay internalize (#4714) 
* adding array solver

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

* use default in model construction

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

* debug delay internalization

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

* bv

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

* arrays

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

* get rid of implied values and bounds

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

* redo egraph

* remove out

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

* remove files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-28 19:24:16 -07:00
Nikolaj Bjorner
7c2bdfe3fb
delay internalization, relevancy (#4707) 
* delay evaluation

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

* Update bv_solver.cpp

* delay internalize

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

* compiler warnings

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

* remove gc

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

* add bv delay option

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-23 17:12:01 -07:00
Nikolaj Bjorner
6f63f8761c
optimizations to bv-solver and euf-egraph (#4698) 
* additional bit-vector propagators

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

* rename restrict (not a keyword, but well) #4694, tune euf

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

* merge

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

* add pb rewriting to pb2bv #4697

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-20 06:47:27 -07:00