Jakob Rath
6e72a97727
Refactor assignment and search state
2022-11-21 17:25:15 +01:00
Jakob Rath
eec8e8ebe4
Fix name: value propagation -> evaluation (for boolean literals)
2022-11-14 14:58:20 +01:00
Jakob Rath
3d27ec41d0
Bring back boolean decisions (wip)
...
The backtracking code doesn't know about boolean decisions yet
2022-10-03 18:36:16 +02:00
Jakob Rath
0a0953ae78
Reduce log output
2022-09-23 16:12:39 +02:00
Jakob Rath
d5f20dcf0e
No more boolean decisions
2022-08-04 14:12:12 +02:00
Jakob Rath
d98a93bcc8
Remove bdecide
2022-04-11 15:55:41 +02:00
Jakob Rath
613b0db4cc
fix refcount issue
2022-03-19 04:19:16 +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
4c4f916917
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-02 08:24:58 -08:00
Nikolaj Bjorner
c48f14e537
updated conflict state
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-01 11:47:33 -08:00
Jakob Rath
5ee02ec5df
Merge remote-tracking branch 'origin/polysat' into polysat
2022-01-31 15:36:22 +01:00
Nikolaj Bjorner
60248d0981
resolution is still wrong
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-29 09:32:14 -08:00
Jakob Rath
67647433ba
log justifications during conflict resolution
2022-01-28 15:52:52 +01:00
Nikolaj Bjorner
0677eb1c05
fixing up missing dependencies during resolution
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-27 16:58:16 -08:00
Nikolaj Bjorner
ff4b471f93
resurrect Booelan decisions to deal with quot-rem and similar axioms
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-27 14:26:41 -08:00
Jakob Rath
645f190e35
Add wrapper for external dependencies to prevent accidental conversions
2022-01-26 11:44:01 +01: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
c4c9c84aeb
Treat eval'd literals as propagations (not as decisions)
2022-01-21 15:56:16 +01:00
Nikolaj Bjorner
caef8d026f
add unsat core, activity, quick pass for viable
2021-11-24 13:23:28 +01:00
Nikolaj Bjorner
57c40e480b
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-08 05:08:57 -08:00
Nikolaj Bjorner
8ee54c665a
removing unit clauses and dependency manager, use minisat approach by tracking assumption literals directly also in clauses
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-20 15:10:03 -07:00
Nikolaj Bjorner
fa3886136b
adding Boolean propagation, watch; and factoring
2021-09-18 22:18:15 -04:00
Nikolaj Bjorner
f01da40e49
adding watches on Booleans
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-16 22:01:34 +01:00
Jakob Rath
71e97a4098
don't need marks in bool_var_manager anymore
2021-09-13 04:35:37 +02:00
Nikolaj Bjorner
ed60cdc403
finish sketch of special case interval propagation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-09 12:23:03 +02:00
Jakob Rath
f2c79b851f
propagate at the right level
2021-09-08 16:00:57 +02:00
Jakob Rath
ba8fa1f072
update polynomial superposition
2021-09-08 14:01:41 +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
8757f04d20
Polysat: disjunctive lemmas ( #5311 )
...
* Add macro to disable linear solver for development
* Move new_* and add_* to header
* Add ref_vector_core::push_back(ref<T>&&)
* Attempt to simplify lifetime handling
* Make operator bool() explicit
* clause improvements
* display boolean assignment
* clause::resolve
* bug fixes
* more fixes
* final case of backtrack
2021-05-28 13:53:08 -07:00
Jakob Rath
28996429df
Polysat disjunctive lemmas (WIP) ( #5275 )
...
* Extend search state by boolean literals
* Only resolve against positive equality
* mk_dep_ref
* Make clause non-owning
* scoped_clause
* Use scoped_clause
* minor
* scoped_ptr move assignment
* WIP: internal handling of disjunctive constraints
* leaf_value
* disjunctive constraints continued
* Fix bool_lit
* Actually add constraints to storage
* Some fixes
* more fixes
* constraint should have a bool_lit instead of a bool_var
* propagate(bool_lit)
* updates
* interface changes
* small fixes
* Make sat::dimacs_lit's constructor explicit
(otherwise, calling operator<< with sat::literal is ambiguous)
* Use sat::literal
* Print test name at the beginning
* Convention: constraint corresponds to the positive boolean literal
* Make constraint ownership more explicit
* clause stores literals
2021-05-21 13:50:25 -07:00
