作者ric2k1 (Ric)
看板EE_DSnP
標題Re: [請益] 關於sat的error
時間Mon Jan 17 11:23:31 2011
※ 引述《nnthome (nnthome)》之銘言：
: 我按照老師的說明把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也一樣有相同錯誤，這要怎麼解決？
你是用 sat/test 底下的 Makefile 嗎?
請確定一下 sat 目錄底下所有的 .cpp 檔也有被 compile 以及 link.
: 還有在addAigCNF時，是只要丟全部aig gate進去嗎? pi和po要丟進去嗎？
PI ==> newVar()
AIG ==> newVar(), addAigCNF(aigVar, in0Var, in0Inv, in1Var, in1Inv);
PO ==> ignored
: 最後問一下要證明兩個電路不相等是照satTest.cpp的方法先solve（a & !b）再
: solve (b & !a)在將兩個結果or就這樣得到a xor b嗎？
You can use: addXorCNF(Var vf, Var va, bool fa, Var vb, bool fb)
: 不好意思很多問題xd
不會! 請加油!!
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 114.36.62.203
1F：推 nnthome:不好意思教授我的COMPILE還是一直不過，我的資料夾是之前 01/17 12:01
2F：→ nnthome:還沒有SAT的版本，想問教授要做些什麼才能把之後下載的SAT 01/17 12:01
3F：→ nnthome:放進原本的資料夾，而且可以使用，目前我是把SAT複製到SRC 01/17 12:02
4F：→ nnthome:中並在include建立.h的連結，然後在cirFraig.cpp include 01/17 12:03
5F：→ ric2k1:1. copy sat 到 src. 2. 根目錄的 Makefile 加上 sat 01/17 12:03
6F：→ nnthome:sat.h但是一樣在最外層做MAKE仍不會過，用G++直接COMPILE 01/17 12:04
7F：推 nnthome:2.是什麼意思？ 01/17 12:07
8F：推 nnthome:ok了謝謝 01/17 12:09