Jakob Rath
e7894873c8
fix
2021-09-08 15:06:23 +02:00
Nikolaj Bjorner
0fd583f5d2
idea w/o implementation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-08 14:48:54 +02:00
Nikolaj Bjorner
f0984a0736
Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat
2021-09-08 14:06:53 +02:00
Nikolaj Bjorner
c894efd777
nit
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-08 14:06:46 +02:00
Jakob Rath
ba8fa1f072
update polynomial superposition
2021-09-08 14:01:41 +02:00
Jakob Rath
2de443c74f
disable conflict_var handling for now
2021-09-08 14:01:41 +02:00
Jakob Rath
c0f51eacf8
conflict_core helpers
2021-09-08 14:01:41 +02:00
Jakob Rath
05b846a472
Activate constraints when their boolean literal is propagated
2021-09-08 14:01:41 +02:00
Jakob Rath
3f15bf5963
assign conflict_var
2021-09-08 14:01:41 +02:00
Nikolaj Bjorner
c7129d2537
more on saturation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-08 14:00:36 +02:00
Nikolaj Bjorner
58276e2569
reorg notes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-08 10:50:30 +02:00
Nikolaj Bjorner
7980b05cc1
forbidden intervals create a lemma
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-08 06:54:36 +02:00
Nikolaj Bjorner
8bcec83ee8
we have to replay in order, otherwise dependencies could become shuffled
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-08 00:06:22 +02:00
Nikolaj Bjorner
efdab0cd4c
add more todo note
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-07 23:56:40 +02:00
Nikolaj Bjorner
eddc03b2eb
add some validation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-07 23:44:30 +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
e6e5621366
Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat
2021-09-07 17:04:36 +02:00
Nikolaj Bjorner
146d107961
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-07 17:04:32 +02:00
Jakob Rath
e74cf72cef
fix cjust update when backtracking over boolean decision
2021-09-07 17:03:47 +02:00
Nikolaj Bjorner
a6643955e6
forbidden interval update
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-07 17:00:46 +02:00
Nikolaj Bjorner
e6c4ae19c6
stab at forbidden intervals
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-07 15:49:29 +02:00
Nikolaj Bjorner
9450ac0d18
Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat
2021-09-07 15:09:28 +02:00
Nikolaj Bjorner
f48e0498d0
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-07 15:09:25 +02:00
Jakob Rath
c7562114ef
Merge
2021-09-07 15:04:28 +02:00
Jakob Rath
24f96acf4f
build_lemma returns clause_builder; adjust reason in revert_bool_decision
2021-09-07 15:02:29 +02:00
Nikolaj Bjorner
4c7ec75868
add replay
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-07 14:58:56 +02:00
Jakob Rath
733c21bb20
update
2021-09-07 14:06:32 +02:00
Jakob Rath
7d58296ad2
Begin reorganizing resolve_value
2021-09-07 11:40:50 +02:00
Jakob Rath
b4e14c31d0
comment
2021-09-07 11:36:45 +02:00
Jakob Rath
eed79df481
resolve_bool should work normally also in bailout mode
2021-09-07 11:35:38 +02:00
Jakob Rath
15c094fa32
Add fallback lemma
2021-09-06 18:00:21 +02:00
Jakob Rath
381d13993c
Add TODO notes from discussion
2021-09-06 16:45:20 +02:00
Jakob Rath
ec1e6725de
Merge resolve_bailout into resolve_conflict
2021-09-06 16:44:47 +02:00
Jakob Rath
39d42913cf
bailout
2021-09-06 15:16:13 +02:00
Jakob Rath
56b33b1b3e
resolve_bailout etc.
2021-09-06 14:08:07 +02:00
Nikolaj Bjorner
ed200f4214
na ( #5536 )
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-05 12:13:08 +02:00
Jakob Rath
9f387f5738
Polysat: conflict resolution updates ( #5534 )
...
* variable elimination / saturation sketch
* conflict resolution updates
2021-09-03 10:17:06 -07:00
Jakob Rath
dc547510db
Polysat: conflict resolution wip ( #5529 )
...
* conflict_core doesn't need gc() anymore
* update comments, ensure_bvar for new constraints
* Make sure constraints can only be created through constraint_manager
* fix constraint::display if no boolean variable is assigned
* Move clause into separate file
* Add conflict_core binary resolution
* conflict_core additions
* reactivate conflict resolution outer loop
* wip
* seems commented includes break CI build
2021-09-01 09:10:10 -07:00
Jakob Rath
8b374c3745
Merge pull request #5525 from Z3Prover/polysat-pull
...
remove scoped
2021-09-01 09:37:50 +02:00
Nikolaj Bjorner
2348667304
build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-31 11:31:14 -07:00
Nikolaj Bjorner
475ac77897
na
2021-08-31 11:27:06 -07:00
Nikolaj Bjorner
22b5b63743
Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat
2021-08-31 11:26:51 -07:00
Nikolaj Bjorner
05d564e828
bug fixes
...
values cannot change on basic variables from inequalities
arithmetic modulo can produce 0 coefficients
2021-08-31 11:26:44 -07:00
Nikolaj Bjorner
978bd9e560
remove scoped
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-31 08:55:48 -07:00
Jakob Rath
dde8fb0c37
Polysat updates ( #5524 )
...
* Move boolean resolution into conflict_core
* Move store() into dedup functionality
* comments
* Call gc()
* Add inference_engine sketch
2021-08-31 08:16:45 -07:00
Nikolaj Bjorner
d1118cb178
cc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-30 11:45:41 -07:00
Nikolaj Bjorner
7cff3d4236
more code review
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-30 11:37:08 -07:00
Nikolaj Bjorner
7ea1bf12b6
add code review to constraint
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-30 11:11:55 -07:00
Nikolaj Bjorner
ef297ced13
merge current master
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-30 10:01:11 -07:00
Nikolaj Bjorner
39f50d46cc
Merge branch 'master' of https://github.com/z3prover/z3 into polysat
2021-08-30 10:00:58 -07:00
