mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

weed out some bugs, add more bv op support in intblast and polysat solvers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-14 12:12:11 -08:00
parent e251b5e9d0
commit b220cb4b63
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/polysat_internalize.cpp
View file

@ -152,8 +152,11 @@ namespace polysat {
case OP_BREDAND: // x == 2^K - 1 unary, return single bit, 1 if all input bits are set.
case OP_BREDOR: // x > 0 unary, return single bit, 1 if at least one input bit is set.
case OP_BCOMP: // x == y binary, return single bit, 1 if the arguments are equal.
case OP_BCOMP: // x == y ? 1 : 0 binary, return single bit, 1 if the arguments are equal.
case OP_ROTATE_LEFT:
case OP_ROTATE_RIGHT:
case OP_EXT_ROTATE_LEFT:
case OP_EXT_ROTATE_RIGHT:
default:
IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n");
NOT_IMPLEMENTED_YET();