New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

BV: Simplifier testing #534

Merged
merged 16 commits into from Oct 29, 2018

Conversation

Projects
None yet
3 participants
@marcogario
Contributor

marcogario commented Oct 27, 2018

Merge the changes from #531, with additional checks to ensure the same semantics for the simplifications across solvers. This highlighted a bug in the converter for Btor for logical shift when the shift leads to an overflow. The issue is also fixed in this PR.

hzzhang and others added some commits Oct 21, 2018

simplifier: simplify BVAdd if one operand is 0
Simplify `0 + x` and `x + 0` to `x`.
simplifier: simplify BVMul if one operand is 0 or 1
1. Simplify `0 * x` and `x * 0` to `0`.
2. Simplify `1 * x` and `x * 1` to `x`
simplifier: simplify BVUDiv if one operand is 0 or 1
1. Simplify `x / 1` to `x`, where `x` can be constant or symbol.
2. Simplify `x / 0` to `2**width - 1`, where `x` can be constant or
   symbol, and `width` is the bit width of the formula.
simplifier: simplify BVURem if one operand is 0 or 1
1. Simplify `0 % x` to `0`.
2. Simplify `x % 0` to `x`.
3. Simplify `x % 1` to `0`.
simplifier: simplify BVULT in some special cases
1. Simplify the irreflexive case to false.
2. Simplify `x < 0` to false.
simplifier: simplify BVULE in some special cases
1. Simplify the reflexive case to true.
2. Simplify `0 <= x` to true.
simplifier: simplify BVAnd in some special cases
1. Given a bit vector `x` of `n` bits, simplify `x & (2**width - 1)`
   and `(2**width - 1) & x` to `x`.
2. Simplify `x & 0` and `0 & x` to `0`.
simplifier: simplify BVOr in some special cases
1. Given a bit vector `x` of `n` bits, simplify `x | (2**n - 1)` to
   the bit vector constant `2**n - 1`.
2. Simplify `x | 0` to `x`.
simplifier: simplify BVSub in some special cases
1. Simplify `x - x` to `0`.
2. Simplify `x - 0` to `x`.
simplifier: simplify BVLShl in some special cases
1. Simplify `x << 0` to `x`.
2. Simplify `0 << n` to `0`.
3. Given a bit vector `x` of `n` bits, simplify `x << m` to `0` if m >= n.
simplifier: simplify BVLShr in some special cases
1. Simplify `x >> 0` to `x`.
2. Simplify `0 >> n` to `0`.
3. Given a bit vector `x` of `n` bits, simplify `x >> m` to `0` if m >= n.
simplifier: simplify the reflexive case of BVSLE
Simplify `x <= x` to True.
Merge pull request #531 from hzzhang/hzzhang/simpl_improvements
Trivial improvements for bit vector simplification

@marcogario marcogario added this to the 0.7.6 milestone Oct 27, 2018

@marcogario marcogario self-assigned this Oct 27, 2018

@marcogario

This comment has been minimized.

Contributor

marcogario commented Oct 27, 2018

Boolector does not agree with the simplification done for lshl_overflow and lshr_overflow.

======================================================================
FAIL: test_bv_lshl_overflow (pysmt.test.test_bv_simplification.TestBvSimplification)
----------------------------------------------------------------------
Traceback (most recent call last):
  File "/home/travis/build/pysmt/pysmt/pysmt/test/test_bv_simplification.py", line 371, in test_bv_lshl_overflow
    self.check_equal_and_valid(f, BVZero(32))
  File "/home/travis/build/pysmt/pysmt/pysmt/test/test_bv_simplification.py", line 109, in check_equal_and_valid
    self.assertValid(EqualsOrIff(simplified, formula), logic=QF_BV)
  File "/home/travis/build/pysmt/pysmt/pysmt/test/__init__.py", line 52, in assertValid
    msg=msg)
AssertionError: False is not true
======================================================================
FAIL: test_bv_lshr_underflow (pysmt.test.test_bv_simplification.TestBvSimplification)
----------------------------------------------------------------------
Traceback (most recent call last):
  File "/home/travis/build/pysmt/pysmt/pysmt/test/test_bv_simplification.py", line 395, in test_bv_lshr_underflow
    self.check_equal_and_valid(f, BVZero(32))
  File "/home/travis/build/pysmt/pysmt/pysmt/test/test_bv_simplification.py", line 109, in check_equal_and_valid
    self.assertValid(EqualsOrIff(simplified, formula), logic=QF_BV)
  File "/home/travis/build/pysmt/pysmt/pysmt/test/__init__.py", line 52, in assertValid
    msg=msg)
AssertionError: False is not true
----------------------------------------------------------------------
@marcogario

This comment has been minimized.

Contributor

marcogario commented Oct 28, 2018

This seems to be a bug in our converter. The same problem in SMT-LIB is declared unsat by boolector 3.0.0

(set-logic QF_BV)
(declare-fun x () (_ BitVec 32))
(assert (let ((.def_0 (bvshl x #b00000000000000000000000000100001))) (let ((.def_1 (= .def_0 #b00000000000000000000000000000000))) (let ((.def_2 (not .def_1))) .def_2))))
(check-sat)

@marcogario marcogario requested a review from mikand Oct 28, 2018

@marcogario marcogario assigned mikand and unassigned marcogario Oct 28, 2018

@mikand

mikand approved these changes Oct 29, 2018

Looks great to me!

@mikand mikand merged commit 6be9413 into master Oct 29, 2018

5 checks passed

clahub All contributors have signed the Contributor License Agreement.
Details
continuous-integration/appveyor/branch AppVeyor build succeeded
Details
continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
continuous-integration/travis-ci/push The Travis CI build passed
Details

@mikand mikand deleted the pr531/edits branch Oct 29, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment