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).

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 747fc3ac8d96f9a152f26f8f152a22e4c619c7e3..68b7e225112693d2d4028c5ae4b9c02dca215e05 100644 (file)
--- 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 b06062cf414b2f36de7a65359f9ac6f19cee68d1..b69704dfb1129bc1e723b3714890b8f51e6d678a 100644 (file)
--- 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 62e70d73dc4f1b4c79d0c974da5eba4311b59e8b..3b48928ca3ca9f84010e3989c8d44065e336ab2c 100644 (file)
--- 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 b1fc084ed470eb6add4dceb274772eb0e48ef413..b28ff3e2a2d1f80fe04c5660cf9ee87f87f3ed7b 100644 (file)
--- 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.