diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-01-18 07:24:20 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-18 07:24:20 -0600 |
| commit | f2f6bd2a9b6468c07bcf712cd8d000a8c46f0e94 (patch) | |
| tree | 5f8bc9755e10e725afd170b771c31fc754a8ec61 | |
| parent | cd187931548afbe2ae9bf909e03c27aa940b5ed1 (diff) | |
| parent | e9bfbb2f666c8cb4cf783d8ebd398fa9304bb5b7 (diff) | |
Merge branch 'master' into createCheckEntailContainscreateCheckEntailContains
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
| -rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.cpp | 1 | ||||
| -rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.h | 8 | ||||
| -rw-r--r-- | src/theory/bv/bitblast/bitblaster.h | 2 |
4 files changed, 16 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 747fc3ac8..68b7e2251 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1431,6 +1431,12 @@ void SmtEngine::setDefaults() { << endl; setOption("global-negate", false); } + + if (options::bitvectorAig()) + { + throw OptionException( + "bitblast-aig not supported with unsat cores/proofs"); + } } else { diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index b06062cf4..b69704dfb 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -28,6 +28,7 @@ extern "C" { #include "base/abc/abc.h" #include "base/main/main.h" +#include "prop/cnf_stream.h" #include "sat/cnf/cnf.h" extern Aig_Man_t* Abc_NtkToDar(Abc_Ntk_t* pNtk, int fExors, int fRegisters); diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index 62e70d73d..3b48928ca 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -85,6 +85,14 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> Unreachable(); } + prop::SatSolver* getSatSolver() override { return d_satSolver.get(); } + + void setProofLog(proof::BitVectorProof* bvp) override + { + // Proofs are currently not supported with ABC + Unimplemented(); + } + class Statistics { public: diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index b1fc084ed..b28ff3e2a 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -91,7 +91,7 @@ class TBitblaster bool hasBBTerm(TNode node) const; void getBBTerm(TNode node, Bits& bits) const; virtual void storeBBTerm(TNode term, const Bits& bits); - void setProofLog(proof::BitVectorProof* bvp); + virtual void setProofLog(proof::BitVectorProof* bvp); /** * Return a constant representing the value of a in the model. |