Nikolaj Bjorner
33c35b0c31
fix #6851
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-13 14:49:25 -07:00
Lev Nachmanson
eb817f779d
small change in factor to support TRACE
2023-08-11 12:04:08 -10:00
Lev Nachmanson
a932e596eb
add a constructor from a variable to factor
2023-08-10 08:34:53 -10:00
Lev Nachmanson
e091a2e775
remove the line with clang-format off
2023-07-10 12:05:59 -07:00
Lev Nachmanson
5ed2a82893
set clang format off for lp files ( #6795 )
...
* adding // clang-format off
* set clang-format off at the beginning of lp files
* set clang-format off
* remove dead code
2023-07-03 17:35:16 -07:00
Henrich Lauko
96671cfc73
Add and fix a few general compiler warnings. ( #5628 )
...
* rewriter: fix unused variable warnings
* cmake: make missing non-virtual dtors error
* treewide: add missing virtual destructors
* cmake: add a few more checks
* api: add missing virtual destructor to user_propagator_base
* examples: compile cpp example with compiler warnings
* model: fix unused variable warnings
* rewriter: fix logical-op-parentheses warnings
* sat: fix unused variable warnings
* smt: fix unused variable warnings
2021-10-29 15:42:32 +02:00
Nikolaj Bjorner
d67919373e
add bailout option for code review #5208
...
@levnach
Could you review and maybe make this much more streamlined?
The patch is to simply bail out the iterator if it fails to find canonical monics.
If m_ff could produce the existing canonical monics up front this kind of bail-out could maybe avoided.
2021-04-22 11:30:11 -07:00
Nikolaj Bjorner
b889b110ee
bool_vector, some spacer tidy
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-05 12:59:04 -07:00
Nikolaj Bjorner
031b3a55ef
fix #3733 persist uninterpreted atoms across calls to incremental sat solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-04 13:11:39 -07:00
Nikolaj Bjorner
8a665e25ed
reverting signed mon_eq, try to rely on canonization state during add/pop
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
cc74dd6373
emonics
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-25 19:43:55 -07:00
Lev Nachmanson
a0bdb8135d
rename monomial to monic
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
33cbd29ed0
mv util/lp to math/lp
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
