From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 18 Jan 2019 08:43:53 +0000 (-0800)
Subject:  Fix ABC build (#2808)
X-Git-Tag: cvc5-1.0.0~4279
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e9bfbb2f666c8cb4cf783d8ebd398fa9304bb5b7;p=cvc5.git

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