我按照老師的說明把sat目錄下有.h的檔案都建立link到include資料夾之下，
然後測一下,建立一個sat object沒問題,compile會過,
但接下來使用initialize()時，再去make就會出現sat的destructor錯誤：
satTest.cpp:(.text._ZN6SolverD1Ev[Solver::~Solver()]+0x3b): undefined
reference to `Solver::remove(Clause*, bool)'
satTest.cpp:(.text._ZN6SolverD1Ev[Solver::~Solver()]+0xae): undefined
reference to `Solver::remove(Clause*, bool)'
satTest.cpp:(.text._ZN6SolverD1Ev[Solver::~Solver()]+0xea): undefined
reference to `Solver::remove(Clause*, bool)'
satTest.cpp:(.text._ZN6SolverD1Ev[Solver::~Solver()]+0x10a): undefined
reference to `Solver::remove(Clause*, bool)'
/tmp/ccex6K2G.o: In function `Solver::addClause(vec<Lit> const&, bool)':
satTest.cpp:(.text._ZN6Solver9addClauseERK3vecI3LitEb[Solver::addClause(vec<Lit>
const&, bool)]+0x32): undefined reference to `Solver::newClause(vec<Lit>
const&, bool, int, bool)'
/tmp/ccex6K2G.o: In function `SatSolver::initialize()':
satTest.cpp:(.text._ZN9SatSolver10initializeEv[SatSolver::initialize()]+0x24):
undefined reference to `Solver::newVar()'
/tmp/ccex6K2G.o: In function `SatSolver::newVar()':
等等等等
錯誤訊息，然後我去compile sat/test/satTest.cpp也一樣有相同錯誤，這要怎麼解決？
還有在addAigCNF時，是只要丟全部aig gate進去嗎? pi和po要丟進去嗎？
最後問一下要證明兩個電路不相等是照satTest.cpp的方法先solve（a & !b）再
solve (b & !a)在將兩個結果or就這樣得到a xor b嗎？
不好意思很多問題xd
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 114.25.7.79