作者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