Fix ABC build (#2808)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 18 Jan 2019 08:43:53 +0000 (00:43 -0800)
committerGitHub <noreply@github.com>
Fri, 18 Jan 2019 08:43:53 +0000 (00:43 -0800)
commite9bfbb2f666c8cb4cf783d8ebd398fa9304bb5b7
tree7280fa55e2a4c6331b71c3c0c5454b1b0b40aad6
parent78d7485639cdf0769c13606b8ad3f5e9455153f1
 Fix ABC build (#2808)

PR #2786 introduced a pure virtual method `TBitblaster::getSatSolver()`.
`AigBitblaster` was missing the implementation of that method. This
commit adds an implementation that simply returns the underlying SAT
solver. Note: The method is currently only used for proofs and CVC4 does
not support proofs in combination with ABC. To make this explicit, the
commit also adds a check in `SmtEngine::setDefaults()` that makes sure
that we are not trying to produce proofs with `--bitblast-aig` (before
the commit, we just crashed with an assertion failure/null pointer
dereference).
src/smt/smt_engine.cpp
src/theory/bv/bitblast/aig_bitblaster.cpp
src/theory/bv/bitblast/aig_bitblaster.h
src/theory/bv/bitblast/bitblaster.h