Commit 37c14672 authored by Farid Alijani's avatar Farid Alijani
Browse files

sat solver princton

parent 3550d6f7

Microsoft Visual Studio Solution File, Format Version 12.00
# Visual Studio 2013
VisualStudioVersion = 12.0.31101.0
MinimumVisualStudioVersion = 10.0.40219.1
Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "SAT_Princeton", "SAT_Princeton\SAT_Princeton.vcxproj", "{B485F0F0-E379-4206-A8A7-DD6D5CE4049B}"
EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|Win32 = Debug|Win32
Release|Win32 = Release|Win32
EndGlobalSection
GlobalSection(ProjectConfigurationPlatforms) = postSolution
{B485F0F0-E379-4206-A8A7-DD6D5CE4049B}.Debug|Win32.ActiveCfg = Debug|Win32
{B485F0F0-E379-4206-A8A7-DD6D5CE4049B}.Debug|Win32.Build.0 = Debug|Win32
{B485F0F0-E379-4206-A8A7-DD6D5CE4049B}.Release|Win32.ActiveCfg = Release|Win32
{B485F0F0-E379-4206-A8A7-DD6D5CE4049B}.Release|Win32.Build.0 = Release|Win32
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
EndGlobalSection
EndGlobal
Build started 12/10/2016 10:08:34 PM.
1>Project "E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\SAT_Princeton\SAT_Princeton\SAT_Princeton.vcxproj" on node 2 (Build target(s)).
1>ClCompile:
C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\bin\CL.exe /c /ZI /nologo /W3 /WX- /sdl /Od /Oy- /D WIN32 /D _CRT_SECURE_NO_WARNINGS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Fo"Debug\\" /Fd"Debug\vc120.pdb" /Gd /TP /analyze- /errorReport:prompt solver.cpp
solver.cpp
Link:
C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\bin\link.exe /ERRORREPORT:PROMPT /OUT:"E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\SAT_Princeton\Debug\SAT_Princeton.exe" /INCREMENTAL /NOLOGO kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /MANIFEST /MANIFESTUAC:"level='asInvoker' uiAccess='false'" /manifest:embed /DEBUG /PDB:"E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\SAT_Princeton\Debug\SAT_Princeton.pdb" /SUBSYSTEM:CONSOLE /TLBID:1 /DYNAMICBASE /NXCOMPAT /IMPLIB:"E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\SAT_Princeton\Debug\SAT_Princeton.lib" /MACHINE:X86 Debug\solver.obj
1>solver.obj : error LNK2019: unresolved external symbol "void * __cdecl SAT_InitManager(void)" (?SAT_InitManager@@YAPAXXZ) referenced in function _main
1>solver.obj : error LNK2019: unresolved external symbol "char * __cdecl SAT_Version(void *)" (?SAT_Version@@YAPADPAX@Z) referenced in function _main
1>solver.obj : error LNK2019: unresolved external symbol "void __cdecl SAT_SetNumVariables(void *,int)" (?SAT_SetNumVariables@@YAXPAXH@Z) referenced in function "void __cdecl read_cnf(void *,char *)" (?read_cnf@@YAXPAXPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "void __cdecl SAT_AddClause(void *,int *,int,int)" (?SAT_AddClause@@YAXPAXPAHHH@Z) referenced in function "void __cdecl read_cnf(void *,char *)" (?read_cnf@@YAXPAXPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_Solve(void *)" (?SAT_Solve@@YAHPAX@Z) referenced in function _main
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_GetVarAsgnment(void *,int)" (?SAT_GetVarAsgnment@@YAHPAXH@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "float __cdecl SAT_GetElapsedCPUTime(void *)" (?SAT_GetElapsedCPUTime@@YAMPAX@Z) referenced in function "void __cdecl output_status(void *)" (?output_status@@YAXPAX@Z)
1>solver.obj : error LNK2019: unresolved external symbol "float __cdecl SAT_GetCPUTime(void *)" (?SAT_GetCPUTime@@YAMPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_NumVariables(void *)" (?SAT_NumVariables@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_InitNumLiterals(void *)" (?SAT_InitNumLiterals@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_InitNumClauses(void *)" (?SAT_InitNumClauses@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "long __cdecl SAT_NumAddedLiterals(void *)" (?SAT_NumAddedLiterals@@YAJPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_NumAddedClauses(void *)" (?SAT_NumAddedClauses@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_NumShrinkings(void *)" (?SAT_NumShrinkings@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_NumDeletedClauses(void *)" (?SAT_NumDeletedClauses@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_NumDelOrigCls(void *)" (?SAT_NumDelOrigCls@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "long __cdecl SAT_NumDeletedLiterals(void *)" (?SAT_NumDeletedLiterals@@YAJPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_NumDecisions(void *)" (?SAT_NumDecisions@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_NumDecisionsStackConf(void *)" (?SAT_NumDecisionsStackConf@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_NumDecisionsVsids(void *)" (?SAT_NumDecisionsVsids@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_NumDecisionsShrinking(void *)" (?SAT_NumDecisionsShrinking@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_Random_Seed(void *)" (?SAT_Random_Seed@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "long __cdecl SAT_NumImplications(void *)" (?SAT_NumImplications@@YAJPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_MaxDLevel(void *)" (?SAT_MaxDLevel@@YAHPAX@Z) referenced in function "void __cdecl handle_result(void *,int,char *)" (?handle_result@@YAXPAXHPAD@Z)
1>solver.obj : error LNK2019: unresolved external symbol "float __cdecl SAT_AverageBubbleMove(void *)" (?SAT_AverageBubbleMove@@YAMPAX@Z) referenced in function "void __cdecl output_status(void *)" (?output_status@@YAXPAX@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_GetFirstClause(void *)" (?SAT_GetFirstClause@@YAHPAX@Z) referenced in function "void __cdecl verify_solution(void *)" (?verify_solution@@YAXPAX@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_GetNextClause(void *,int)" (?SAT_GetNextClause@@YAHPAXH@Z) referenced in function "void __cdecl verify_solution(void *)" (?verify_solution@@YAXPAX@Z)
1>solver.obj : error LNK2019: unresolved external symbol "int __cdecl SAT_GetClauseNumLits(void *,int)" (?SAT_GetClauseNumLits@@YAHPAXH@Z) referenced in function "void __cdecl verify_solution(void *)" (?verify_solution@@YAXPAX@Z)
1>solver.obj : error LNK2019: unresolved external symbol "void __cdecl SAT_GetClauseLits(void *,int,int *)" (?SAT_GetClauseLits@@YAXPAXHPAH@Z) referenced in function "void __cdecl verify_solution(void *)" (?verify_solution@@YAXPAX@Z)
1>E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\SAT_Princeton\Debug\SAT_Princeton.exe : fatal error LNK1120: 29 unresolved externals
1>Done Building Project "E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\SAT_Princeton\SAT_Princeton\SAT_Princeton.vcxproj" (Build target(s)) -- FAILED.
Build FAILED.
Time Elapsed 00:00:01.98
B^E:\LTH\GIT_REPOSITORY\THESIS\MOBILEROBOT\MACHINE_LEARNING\SAT_PRINCETON\SAT_PRINCETON\SOLVER.CPP
B^E:\LTH\GIT_REPOSITORY\THESIS\MOBILEROBOT\MACHINE_LEARNING\SAT_PRINCETON\SAT_PRINCETON\SOLVER.CPP
#TargetFrameworkVersion=v4.0:PlatformToolSet=v120:EnableManagedIncrementalBuild=false:VCToolArchitecture=Native32Bit
Debug|Win32|E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\SAT_Princeton\|
B^E:\LTH\GIT_REPOSITORY\THESIS\MOBILEROBOT\MACHINE_LEARNING\SAT_PRINCETON\SAT_PRINCETON\SOLVER.CPP
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment