Nikolaj Bjorner
4b1419261f
#5778
2022-03-21 16:23:43 -07:00
Nikolaj Bjorner
20bd59bb20
#5778 - missed tracking literal assignment justification
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-21 10:15:00 -07:00
Nikolaj Bjorner
6d836e7e2f
expose model update
2022-03-19 09:23:08 -07:00
Nikolaj Bjorner
580012e19f
fix #5894
...
expp is not implemented. This is the second time a fuzz bug reports it. Instead of closing the bug, just disable code path as fuzzers are not considering the comment from previous bug.
2022-03-10 09:45:09 -08:00
Nikolaj Bjorner
1d224d1bcd
na
2022-03-08 08:51:00 -08:00
Nikolaj Bjorner
c6f8ee33d4
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-08 08:36:19 -08:00
Nikolaj Bjorner
3293aeb7c7
na
2022-03-08 08:36:19 -08:00
Nikolaj Bjorner
7b4f1ed530
missing initialization of m_user_propagator, disable unsound in-processing in pb_solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-23 04:49:42 -08:00
Nikolaj Bjorner
10b611b3ba
fix #5850
2022-02-20 10:30:52 +02:00
Nikolaj Bjorner
2e00f2f32d
Propagator ( #5845 )
...
* user propagator without ids
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* user propagator without ids
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix signature
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* references #5818
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix c++ build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch to vs 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update propagator example (I) (#5835 )
* fix #5829
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch to vs 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Adapted the example to the changes in the propagator
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* context goes out of scope in stack allocation, so can't used scoped context when passing objects around
* parameter check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Fixed bug in user-propagator "created" (#5843 )
Co-authored-by: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
2022-02-17 09:21:41 +02:00
Qix
9cf50766a6
fix compiler warnings under clang ( #5839 )
2022-02-16 23:36:34 +02:00
Nikolaj Bjorner
1e0d49512b
call mux finder
2022-01-31 12:00:16 -08: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
6422b783b2
fix mux extraction to check for top-level assertion
2022-01-31 11:57:16 -08:00
Nikolaj Bjorner
62bb234251
expose extract roots as separate
2022-01-31 11:56:44 -08:00
Nikolaj Bjorner
9e5b6e0c9c
#5778
2022-01-27 12:12:58 -08:00
Nikolaj Bjorner
9969809745
#5778
2022-01-21 09:40:06 +01:00
Nikolaj Bjorner
a3d4e9a4e8
adding created to sat/smt
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-20 11:48:27 +01:00
Nikolaj Bjorner
c00591daaf
finish is-fixed
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-19 16:28:34 +01:00
Nikolaj Bjorner
e5767bf2b8
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-19 15:19:07 +01:00
Nikolaj Bjorner
06feb71eb1
fix bug in root setting exposed by incremental mode pb_solver
2022-01-18 10:55:27 +01:00
Nikolaj Bjorner
d777306bb6
#5778
2022-01-17 10:43:15 -08:00
Nikolaj Bjorner
fcc9f379e7
#5778
2022-01-16 19:36:00 -08:00
Nikolaj Bjorner
a15da8f9ba
#5778
2022-01-16 19:11:55 -08:00
Nikolaj Bjorner
637ddf9397
fix #5777
...
latest issue
2022-01-16 18:09:38 -08:00
Nikolaj Bjorner
0dd5a5e576
#5777
2022-01-16 17:46:08 -08:00
Nikolaj Bjorner
a48d3fdbb1
#5777
2022-01-16 14:01:49 -08:00
Nikolaj Bjorner
ea93345b75
#5777
2022-01-16 10:52:25 -08:00
Nikolaj Bjorner
cd56d55e34
#5753
2022-01-16 09:31:16 -08:00
Nikolaj Bjorner
bc9c6ad93d
#5753
2022-01-15 18:01:31 -08:00
Nikolaj Bjorner
1b5f7cd9e5
na
2022-01-15 10:05:26 -08:00
Nikolaj Bjorner
17cfc1d034
#5753
2022-01-15 10:03:03 -08:00
Nikolaj Bjorner
74824ac901
#5753
...
get_antecedent has to be well-founded. It got broken when using eval during propagation and egraph explain during conflict resolution.
2022-01-15 09:35:25 -08:00
Nikolaj Bjorner
d09abdf58e
fix #5771
...
Missing congruence closure enforcement on auxiliary guard predicates.
It diverges but is sound.
2022-01-14 15:46:40 -08:00
Nikolaj Bjorner
d5cc162fa7
bug in bounds
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-13 15:42:23 -08:00
Nikolaj Bjorner
2363bfc132
internalize arithmetic sub-terms #5753
2022-01-13 15:34:04 -08:00
Nikolaj Bjorner
e816946ddc
handling unsimplified input
2022-01-13 14:40:46 -08:00
Nikolaj Bjorner
b259f46f85
dependencies
2022-01-13 12:34:58 -08:00
Nikolaj Bjorner
4b6679e8e0
#5753
2022-01-13 12:19:54 -08:00
Nikolaj Bjorner
366cd9b16d
missing pb cases
2022-01-12 14:50:40 -08:00
Nikolaj Bjorner
0720998bac
#5753
2022-01-12 13:12:10 -08:00
Nikolaj Bjorner
10dc8d7313
#5753
2022-01-12 12:49:06 -08:00
Nikolaj Bjorner
56d3718cde
add simplification with qe-lite as an option #5767
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-12 03:41:21 -08:00
Nikolaj Bjorner
e5eaea46aa
ensure m_true is assigned #5753
2022-01-11 10:42:05 -08:00
Nikolaj Bjorner
f1bf660adc
add case for abs (normally simplified, but not with default_tactic=smt).
2022-01-09 11:55:21 -08:00
Nikolaj Bjorner
671d071e54
#5753
2022-01-09 11:39:21 -08:00
Nikolaj Bjorner
bf3c213fd3
#5753
2022-01-09 11:03:29 -08:00
Nikolaj Bjorner
90fd3d82fc
enable propagation
2022-01-08 19:00:56 -08:00
Nadav Rotem
9f9543ef69
Fix unused variable warnings. ( #5760 )
...
This commit fixes a few cases of unused variables in release builds.
The commit uses the (void)xxx; syntax which is used in other parts of
the code.
2022-01-08 18:18:30 -08:00
