Adding support for bool-to-bv
authorClark Barrett <barrett@cs.stanford.edu>
Mon, 6 Mar 2017 08:25:26 +0000 (00:25 -0800)
committerClark Barrett <barrett@cs.stanford.edu>
Mon, 6 Mar 2017 08:25:26 +0000 (00:25 -0800)
commit5f096cbd59afa98e8b3c7e7e7aa0b6df3c7e01b0
treef7897714f42c89eac1547039de37fa25a730537a
parentf81c51ca8af1c38126336f0c31a33fba72614dc1
Adding support for bool-to-bv

Squashed commit of the following:

commit 5197a663eb262afbeb7740f53b5bd27479dccea0
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Mon Mar 6 00:16:16 2017 -0800

    Remove IFF case

commit 2119b25a30ed42eca54f632e7232c9f76ae5755a
Author: guykatzz <katz911@gmail.com>
Date:   Mon Feb 20 12:37:06 2017 -0800

    proof support for bvcomp

commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Fri Feb 17 21:09:04 2017 -0800

    Added missing cases to operator<< for bv rewrite rules.

commit 0ed797c31d0e66cadc35b2397716c841d1aff270
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Fri Feb 17 11:43:51 2017 -0800

    Added rewrite rules for new bitvector kinds.

commit 3b23dffb317de5559f8a95118fef633f711c114a
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Mon Feb 13 14:41:49 2017 -0800

    First draft of bool-to-bv pass.
16 files changed:
proofs/signatures/th_bv_bitblast.plf
src/options/bv_options
src/smt/dump.cpp
src/smt/smt_engine.cpp
src/theory/bv/bitblast_strategies_template.h
src/theory/bv/bitblaster_template.h
src/theory/bv/bv_to_bool.cpp
src/theory/bv/bv_to_bool.h
src/theory/bv/kinds
src/theory/bv/theory_bv_rewrite_rules.h
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
src/theory/bv/theory_bv_rewriter.cpp
src/theory/bv/theory_bv_rewriter.h
src/theory/bv/theory_bv_type_rules.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h