Only allow bv2nat/int2bv with BV and integer logic (#4118)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 19 Mar 2020 06:46:50 +0000 (23:46 -0700)
committerGitHub <noreply@github.com>
Thu, 19 Mar 2020 06:46:50 +0000 (23:46 -0700)
commitd862942f821ea14973207ef538be3326fb11c17c
tree80a6b809f84019d9bcd1e0552cea778b10a1e8c8
parent9c960866c9e71e543c5688aac826a8150c899ca6
Only allow bv2nat/int2bv with BV and integer logic (#4118)

CVC4 supports `bv2nat` and `int2bv` to convert bit-vectors to/from
integers. Those operators are not standard. This commit only enables
those operators when parsing is non-strict and both bit-vectors and
integers are enabled in the logic. To achieve this, the commit
simplifies the handling of logics in the parser: Instead of defining a
separate `Logic` enum in the `Smt2` class, we simply use `LogicInfo`
directly.
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
test/regress/CMakeLists.txt
test/regress/regress0/parser/bv_nat.smt2 [new file with mode: 0644]
test/unit/parser/parser_black.h