作者nnthome (nnthome)
看板EE_DSnP
标题[请益] 关於sat的error
时间Mon Jan 17 09:56:35 2011
我按照老师的说明把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