From 2de63b89c520b0d751d594000b0048e0cab79791 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Dec 2023 12:12:11 -0800 Subject: [PATCH] weed out some bugs, add more bv op support in intblast and polysat solvers Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat_internalize.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 0ba59de0a..68e5e4cc6 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -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();