Nikolaj Bjorner
|
437e83f6de
|
fixmul negative case
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-08-23 08:20:32 -07:00 |
|
Nikolaj Bjorner
|
8128ae8109
|
generalize subsumption to non-univariate
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-08-22 10:46:49 -07:00 |
|
Jakob Rath
|
058c5771b9
|
univariate solver: add_bit
|
2022-08-22 15:09:11 +02:00 |
|
Jakob Rath
|
d9a63ce786
|
fix
|
2022-08-22 15:05:29 +02:00 |
|
Jakob Rath
|
9fcea37625
|
remove constructor
|
2022-08-22 15:00:35 +02:00 |
|
Jakob Rath
|
28ddd4ad56
|
Implement unilinear subsumption as clause simplification
|
2022-08-22 14:55:02 +02:00 |
|
Jakob Rath
|
c1e2ea80f5
|
make explicit that we compare the concrete values
|
2022-08-22 14:17:47 +02:00 |
|
Jakob Rath
|
3a759c1a28
|
move fi_record
|
2022-08-22 14:14:30 +02:00 |
|
Jakob Rath
|
26fcfc6ecd
|
Add default constructor to fi_entry
|
2022-08-22 14:03:43 +02:00 |
|
Jakob Rath
|
3c093e03cf
|
log
|
2022-08-22 12:46:47 +02:00 |
|
Jakob Rath
|
53f276d225
|
apply
|
2022-08-22 12:44:56 +02:00 |
|
Jakob Rath
|
bf1a7914cd
|
Add clause simplification stub
|
2022-08-22 12:36:05 +02:00 |
|
Jakob Rath
|
3e99828c3c
|
start make_asserting for non-unit coeff
|
2022-08-19 17:06:28 +02:00 |
|
Jakob Rath
|
ee208efdc5
|
fix
|
2022-08-19 16:18:13 +02:00 |
|
Jakob Rath
|
c3e7bd34d0
|
make_asserting for unit coefficients
|
2022-08-19 16:02:56 +02:00 |
|
Jakob Rath
|
9766ad00b1
|
Revert "remove overcomplicated search_iterator"
This reverts commit 309473edad .
|
2022-08-19 14:12:57 +02:00 |
|
Nikolaj Bjorner
|
31ffe89480
|
normalize more pretty printing
|
2022-08-17 08:24:41 -07:00 |
|
Jakob Rath
|
309473edad
|
remove overcomplicated search_iterator
|
2022-08-17 09:37:43 +02:00 |
|
Jakob Rath
|
201d841a90
|
lit_pp with extra information
|
2022-08-17 09:29:00 +02:00 |
|
Jakob Rath
|
618b3945c1
|
log
|
2022-08-05 11:23:02 +02:00 |
|
Jakob Rath
|
bab8d817ef
|
Remove decisions on lemmas
|
2022-08-04 14:24:20 +02:00 |
|
Jakob Rath
|
d5f20dcf0e
|
No more boolean decisions
|
2022-08-04 14:12:12 +02:00 |
|
Jakob Rath
|
c67024d88b
|
unused for now
|
2022-08-04 13:52:29 +02:00 |
|
Jakob Rath
|
a3e8124245
|
comments; move a section
|
2022-08-04 11:52:34 +02:00 |
|
Jakob Rath
|
4282cfa148
|
Remove unused variable
|
2022-08-04 08:55:04 +02:00 |
|
Jakob Rath
|
014fe4e3fd
|
fallback stats
|
2022-08-04 08:51:24 +02:00 |
|
Jakob Rath
|
b9588af07a
|
fix output
|
2022-08-03 10:01:54 +02:00 |
|
Jakob Rath
|
a76f977f85
|
Change univariate fallback solver to one-shot mode for now
|
2022-08-02 12:42:34 +02:00 |
|
Jakob Rath
|
e105a91d4a
|
Merge branch 'master' into polysat
|
2022-08-02 11:31:01 +02:00 |
|
Jakob Rath
|
de6a0ab1a7
|
PDD operations
|
2022-08-01 18:37:11 +03:00 |
|
Jakob Rath
|
42233ab5c8
|
Additional BDD operations; BDD vectors and finite domain abstraction
|
2022-08-01 18:37:11 +03:00 |
|
Jakob Rath
|
9275d1e57a
|
sparse_matrix iterators
|
2022-08-01 18:37:11 +03:00 |
|
Bruce Mitchener
|
a89be68050
|
Use false instead of 0 .
|
2022-08-01 18:28:07 +03:00 |
|
Jakob Rath
|
220a63e8bd
|
Merge branch 'master' into polysat
|
2022-08-01 11:27:49 +02:00 |
|
Bruce Mitchener
|
5d0dea05aa
|
Remove empty leaf destructors. (#6211)
|
2022-07-30 10:07:03 +01:00 |
|
Bruce Mitchener
|
1eb84fe4b9
|
Mark override methods appropriately. (#6207)
|
2022-07-29 23:29:15 +02:00 |
|
Jakob Rath
|
d65dc82ef0
|
bailout state: add premises of assignment
|
2022-07-25 13:49:21 +02:00 |
|
Bruce Mitchener
|
3e38bbb009
|
Make sure all headers do #pragma once . (#6188)
|
2022-07-23 10:41:14 -07:00 |
|
Jakob Rath
|
1b370727b1
|
remove redundant subst_val
|
2022-07-21 13:15:02 +02:00 |
|
Jakob Rath
|
4a3fe8ab82
|
fix
|
2022-07-21 13:00:36 +02:00 |
|
Jakob Rath
|
e168d8a2eb
|
Merge branch 'master' into polysat
|
2022-07-21 12:56:50 +02:00 |
|
Jakob Rath
|
48c6bea331
|
umul 2
|
2022-07-21 12:38:00 +02:00 |
|
Jakob Rath
|
d4592f2abf
|
umul
|
2022-07-21 11:57:27 +02:00 |
|
Jakob Rath
|
8d871bf8b5
|
dead code
|
2022-07-21 11:48:41 +02:00 |
|
Nikolaj Bjorner
|
6c5747a80e
|
guard against lemmas that are already true
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-07-15 10:03:31 -07:00 |
|
Nikolaj Bjorner
|
4ecb61aeaa
|
neatify
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-07-15 09:53:56 -07:00 |
|
Nikolaj Bjorner
|
2696775088
|
remove stale assertion
with support for substitutions we allow the simplifier to change the state of equations.
|
2022-07-15 04:03:25 -07:00 |
|
Nikolaj Bjorner
|
b29cdca936
|
integrate factorization to Grobner
|
2022-07-14 21:24:27 -07:00 |
|
Nikolaj Bjorner
|
7c177584f3
|
add propagators to grobner
|
2022-07-14 15:45:07 -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 |
|