Nikolaj Bjorner
decaee83f3
move from justified_expr to dependent_expr by aligning datatypes
2025-01-22 11:46:10 -08:00
Nikolaj Bjorner
1646a41b2f
minor fixes
...
- ensure mk_extract performs simplification to distribute over extract and removing extract if the range is the entire bit-vector
- ensure bool_rewriter simplifeis disjunctions when applicable.
2022-11-02 08:44:55 -07:00
Nuno Lopes
e844aef896
remove a few more copy constructors, though still not enough to enable the assertion in vector
...
I give up for now; there are too many copies left for little return..
2020-06-03 20:32:13 +01:00
Nuno Lopes
7ac2791482
remove a bunch of constructors to avoid copies
...
still not enough to guarantee that vector::expand doesnt copy (WIP)
2020-06-03 17:09:27 +01:00
Nikolaj Bjorner
cbe52e298b
remove tracing, fix doctext
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 15:08:26 +02:00
Nikolaj Bjorner
c6722859c2
update rewriting of equalities and monomials for regressions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-09-03 14:36:03 -07:00
Nikolaj Bjorner
0d5cfe9292
separate out, add copy constructor
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-26 09:23:15 -07:00
