Jakob Rath
6e9e8999dc
fix
2021-09-09 11:00:01 +02:00
Jakob Rath
ec882d10da
add condition that degree is reduced
2021-09-09 10:54:33 +02: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
Jakob Rath
a5b7f9d77b
change to assertion
2021-09-08 18:42:08 +02:00
Jakob Rath
18411afda2
find_upper_bound
2021-09-08 18:40:29 +02:00
Jakob Rath
64ce6cb5c1
notes
2021-09-08 18:21:09 +02:00
Jakob Rath
6766c1c349
re-enable saturation engine
2021-09-08 16:57:27 +02:00
Jakob Rath
75bac21574
Re-integrate forbidden intervals
2021-09-08 16:51:16 +02:00
Jakob Rath
a0570908fb
Add support for bailout lemma
2021-09-08 16:37:47 +02:00
Jakob Rath
f2c79b851f
propagate at the right level
2021-09-08 16:00:57 +02:00
Jakob Rath
40d62af796
some fixes
2021-09-08 15:46:50 +02:00
Jakob Rath
ff1185891a
deactivate constraints when qhead is popped
2021-09-08 15:24:11 +02:00
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