chengyinwu / v3 Goto Github PK

An Extensible Framework for Hardware Verification and Debugging

License: Other

Makefile 2.55% Verilog 1.25% Shell 0.11% C 0.67% C++ 95.43%

v3's Introduction

Copyright(c) 2012-2014 DVLab, GIEE, NTU, Taiwan
NOTE THAT V3 IS CURRENTLY FOR NON-COMMERCIAL USE ONLY !!!
EXPLOIT V3 WITHOUT EXPLICIT PERMISSIONS IS PROHIBITED !!!

LATEST NOTE

Our webpage server has been terribly crashed for a long time and it's still under repair. Please contact us if you need more materials.

AUTHOR (Contact)

Cheng-Yin Wu: Software Developer at Athena Capital Research LLC
Chung-Yang (Ric) Huang: Professor at National Taiwan University

INTRODUCTION

V3 is a new and extensible framework for hardware verification and debugging researches on both Boolean-level and word-level designs. It is a powerful tool for users and an elaborate framework for developers as well.

The architecture of V3 consists of four logical layers:

Language layer parses in and writes out Boolean-level (e.g. AIGER) as well as word-level (e.g. BTOR, Verilog) designs.
Network layer properly models design behaviours into networks while preserving abstraction levels of designs.
Application layer is equipped with verification applications, including design simulation. In particular, state-of-the-art SAT-based model checking algorithms (e.g. bounded model checking and induction) are implemented for tackling both safety and liveness properties. Furthermore, V3 confirms verification results and provides counterexample visualization for improving design debugging.
Solver layer adopts certain representative SAT solvers (e.g. MiniSAT) as well as SMT solvers (e.g. Boolector) as core engines for formal applications. The communication between layers are defined by extensible APIs: Network layer provides network API for network creation and information retrieval while solver layer defines generic solver API for applications to communicate with different solvers.

Due to publication issues, we keep the implementation of several algorithms private.

DOWNLOAD

Get the latest V3 source code: git clone https://github.com/chengyinwu/V3

INSTALL V3:

Please perform the following instructions under directory "engine":

$ cd <root-directory-of-V3>/engine;

This release of V3 requires at least the following engines:

Minisat : a satisfiability solver (SAT solver)
Boolector : a word-level solver (SMT solver)
QuteRTL : a RTL (Verilog) front-end

Please install these engines by executing corresponding scripts under the directory. Or please follow our documentation "Linking Engines with V3" for manual installation.

Minisat : ./minisat.script
Boolector : ./boolector.script
QuteRTL : ./quteRTL.script

Now you are ready to install V3 with the procedures as described in COMPILATION.

COMPILATION

$ cd <root-directory-of-V3>
$ make clean; make

EXECUTION

cd <root-directory-of-V3>
$ bin/v3

Please also find the tutorial and documentation for V3 programmers.

COMMANDS

# Common Commands
DOfile                  # Execute the commands in the dofile
HELp                    # Print this help message
HIStory                 # Print command history
Quit                    # Quit the execution
SET LOgfile             # Redirect messages to files
USAGE                   # Report resource usage

# I/O Commands
REAd Aig                # Read AIGER Designs
REAd Btor               # Read BTOR Designs
REAd Rtl                # Read RTL (Verilog) Designs
WRIte Aig               # Write AIGER Designs
WRIte Btor              # Write BTOR Network
WRIte Rtl               # Write RTL (Verilog) Designs

# Print Commands
PLOt NTk                # Plot Network Topology
PRInt NEt               # Print Net Information
PRInt NTk               # Print Network Information

# Synthesis Commands
BLAst NTk               # Bit-blast Word-level Networks into Boolean-level Networks
DUPlicate NTk           # Duplicate Current Ntk from Verbosity Settings
EXPand NTk              # Perform Time-frame Expansion for Networks
FLAtten NTk             # Flatten Hierarchical Networks
MITer NTk               # Miter Two Networks
PRInt NTKVerbosity      # Print Verbosities for Network Duplication
REDuce NTk              # Perform COI Reduction on Current Network
REWrite NTk             # Perform Rule-based Rewriting on Current Network
SET NTKVerbosity        # Set Verbosities for Network Duplication
STRash NTk              # Perform Structural Hashing on Current Network

# Manipulation Commands
@CD                     # Change Design for Current Network
@LN                     # Link a Network with an instance of Current Network
@LS                     # List Network Instances of Current Network
@PWD                    # Print the Path of Current Network

# Extraction Commands
ELAborate FSM           # Elaborate Network and Construct FSM from Input Specification
EXTract FSM             # Extract Finite State Machines from Current Network
PLOT FSM                # Plot Finite State Machines into *.png files
WRIte FSM               # Output Finite State Machines Specifications

# Simulation Commands
PLOt TRace              # Plot simulation or counterexample traces
SIM NTk                 # Simulate on Current Network

# Verification Commands
CHEck REsult            # Verify Verification Result
ELAborate PRoperty      # Elaborate Properties on a Duplicated Network
PLOt REsult             # Plot Verification Results
PRInt REport            # Print Verbosities for Verification Report
PRInt SOlver            # Print Active Solver for Verification
SET PRoperty            # Set Properties on Current Network
SET REport              # Set Verbosities for Verification Report
SET SOlver              # Set Active Solver for Verification
VERify BMC              # Perform Bounded Model Checking
VERify ITP              # Perform Interpolation-based Model Checking
VERify KLIVE            # Perform K-Liveness for Liveness Checking
VERify PDR              # Perform Property Directed Reachability
VERify SEC              # Perform Sequential Equivalence Checking
VERify SIM              # Perform (Constrained) Random Simulation
VERify UMC              # Perform Unbounded Model Checking
WRIte REsult            # Write Verification Results

# Model Checking Commands
READ PROperty           # Read property specification from external file
RUN                     # Run V3 Model Checker
WRITE PROperty          # Write property specification into file

# Debugging Commands
OPTimize TRace          # Optimize a Counterexample Trace
SIMplify TRace          # Simplify Counterexample Traces

LICENSE

Please refer to the COPYING file.

v3's People

Contributors

Stargazers

Watchers

Forkers

sillyduck kslaughter wqhic silky ruochendai78 hhhuuugggooo

v3's Issues

Does currently not build due to a HTTP/403 error for a dependency

The README page refers to http://dvlab.ee.ntu.edu.tw/~publication/V3/download.html - unfortunately, visiting this page yields a "403 Forbidden" message.

For the same reason, the scripts to build V3 currently fail.

Failed to make V3 in current vision

Issues

It seems that some files are missing in V3/engine to compile the shell scripts.
Makefile in the root directory has some bugs.

Below is one solution by TAs in Prof. Chung Yang (Ric) Huang's NTU SoCV course:

Change the INSTALL script in the root directory as follows (remove the original V3/engine and paste the correct one ; patch makefile.diff to the original Makefile to fix the bug)
new INSTALL.sh must be like

git clone https://github.com/chengyinwu/V3
rm -rf V3/engine
cp -rf v3_needed/SoCV_v3_engine V3/engine
cp v3_needed/Makefile.in.diff V3/src
cd V3/engine/; ./boolector.script; ./minisat.script; ./quteRTL.script; cd ../
cd src; patch Makefile.in < Makefile.in.diff; cd ..; make;

v3_needed.zip

compiling error for libreadline

I have encountered an issue to build v3. Thanks. I am using ubuntu 18.04 and g++-5.

building v3...
/usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/libreadline.a(complete.o): In function rl_username_completion_function': (.text+0x4419): warning: Using 'getpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/libreadline.a(tilde.o): In function tilde_expand_word':
(.text+0x134): warning: Using 'getpwnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
/usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/libreadline.a(shell.o): In function sh_get_home_dir': (.text+0x109): warning: Using 'getpwuid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/libreadline.a(complete.o): In function rl_username_completion_function':
(.text+0x440f): warning: Using 'setpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
(.text+0x44a9): warning: Using 'endpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::solve()': v3SvrMiniSat.cpp:(.text+0x1d3): undefined reference to Solver::solve_()'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::setImplyInit()': v3SvrMiniSat.cpp:(.text+0x465): undefined reference to Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x5e8): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::newVar(unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x814): undefined reference to Solver::newVar(lbool, bool)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::assertProperty(unsigned long const&, bool const&)':
v3SvrMiniSat.cpp:(.text+0x1123): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::assertProperty(V3NetId const&, bool const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x11db): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::assump_solve()':
v3SvrMiniSat.cpp:(.text+0x1292): undefined reference to Solver::solve_()' ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::setTargetValue(V3NetId const&, V3BitVecX const&, unsigned int const&, unsigned long const&)':
v3SvrMiniSat.cpp:(.text+0x1445): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x14d5): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x1529): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x1593): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x15ed): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x1645): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x1699): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::setImplyIntersection(std::vector<unsigned long, std::allocator > const&)':
v3SvrMiniSat.cpp:(.text+0x1851): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x1955): undefined reference to Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::assertInit()': v3SvrMiniSat.cpp:(.text+0x1c54): undefined reference to Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::assertImplyUnion(std::vector<unsigned long, std::allocator<unsigned long> > const&)': v3SvrMiniSat.cpp:(.text+0x1d9e): undefined reference to Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::setImplyUnion(std::vector<unsigned long, std::allocator<unsigned long> > const&)': v3SvrMiniSat.cpp:(.text+0x1ee5): undefined reference to Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x1fb6): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_FALSE_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x2066): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x20d6): undefined reference to Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_PI_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x2154): undefined reference to Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_AND_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x2225): undefined reference to Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_XOR_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x2425): undefined reference to Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_MUX_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x2626): undefined reference to Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_RED_AND_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x28de): undefined reference to Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x29fe): more undefined references to Solver::newVar(lbool, bool)' follow ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_CONST_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x3bed): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_SLICE_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x3e45): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x3f55): undefined reference to Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_MERGE_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x4065): undefined reference to Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_EQUALITY_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x42b5): undefined reference to Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_GEQ_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x44dc): undefined reference to Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x4646): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x468e): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x46f9): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x480d): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x4863): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x48bb): more undefined references to Solver::addClause_(vec<Lit, int>&)' follow
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_SHL_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x530a): undefined reference to Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x5523): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x55bd): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x565b): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x58de): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x59ce): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x5abe): undefined reference to Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x5ba6): more undefined references to Solver::addClause_(vec<Lit, int>&)' follow ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_SHL_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x6399): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x654f): undefined reference to Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_SHR_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x6714): undefined reference to Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x692f): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x69cc): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x6a6d): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x6c8e): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x6d7e): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x6e6d): undefined reference to Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x6f56): more undefined references to Solver::addClause_(vec<Lit, int>&)' follow ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_SHR_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x7799): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x7958): undefined reference to Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_DIV_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x7a05): undefined reference to Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x7c5f): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x7cb6): undefined reference to Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x7e64): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x7fa5): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x8096): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x81e5): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x82d6): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x8425): undefined reference to Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x8516): more undefined references to Solver::addClause_(vec<Lit, int>&)' follow ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_MODULO_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x8fe7): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x9240): undefined reference to Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x928f): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x944b): undefined reference to Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x9585): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x9676): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x97b5): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x98a6): undefined reference to Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x99e5): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x9ad6): more undefined references to Solver::addClause_(vec<Lit, int>&)' follow
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_FF_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0xa5b4): undefined reference to Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0xa645): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0xa755): undefined reference to Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0xa8a4): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0xaa5a): undefined reference to Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::reset()': v3SvrMiniSat.cpp:(.text+0xab61): undefined reference to Solver::Solver()'
v3SvrMiniSat.cpp:(.text+0xabbf): undefined reference to Solver::newVar(lbool, bool)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::V3SvrMiniSat(V3Ntk const*, bool const&)':
v3SvrMiniSat.cpp:(.text+0xaeca): undefined reference to Solver::Solver()' v3SvrMiniSat.cpp:(.text+0xaefc): undefined reference to Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::V3SvrMiniSat(V3SvrMiniSat const&)': v3SvrMiniSat.cpp:(.text+0xb1af): undefined reference to Solver::Solver()'
v3SvrMiniSat.cpp:(.text+0xb1e1): undefined reference to Solver::newVar(lbool, bool)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::simplify()':
v3SvrMiniSat.cpp:(.text+0x175): undefined reference to Solver::simplify()' ../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::reserveFormula()':
v3SvrMiniSat.cpp:(.text.ZN12V3SvrMiniSat14reserveFormulaEv[ZN12V3SvrMiniSat14reserveFormulaEv]+0x1d): undefined reference to Solver::newVar(lbool, bool)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function void buf(Solver*, Lit const&, Lit const&)':
v3SvrMiniSat.cpp:(.text.Z3bufI6SolverEvPT_RK3LitS5[Z3bufI6SolverEvPT_RK3LitS5]+0x83): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text._Z3bufI6SolverEvPT_RK3LitS5_[_Z3bufI6SolverEvPT_RK3LitS5_]+0xc9): undefined reference to Solver::addClause(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function void xor_2<Solver>(Solver*, Lit const&, Lit const&, Lit const&)': v3SvrMiniSat.cpp:(.text._Z5xor_2I6SolverEvPT_RK3LitS5_S5_[_Z5xor_2I6SolverEvPT_RK3LitS5_S5_]+0x9e): undefined reference to Solver::addClause(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text.Z5xor_2I6SolverEvPT_RK3LitS5_S5[Z5xor_2I6SolverEvPT_RK3LitS5_S5]+0x106): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text._Z5xor_2I6SolverEvPT_RK3LitS5_S5_[_Z5xor_2I6SolverEvPT_RK3LitS5_S5_]+0x159): undefined reference to Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text.Z5xor_2I6SolverEvPT_RK3LitS5_S5[Z5xor_2I6SolverEvPT_RK3LitS5_S5]+0x1ac): more undefined references to `Solver::addClause_(vec<Lit, int>&)' follow
collect2: error: ld returned 1 exit status
Makefile:11: recipe for target '../../v3' failed
make[1]: *** [../../v3] Error 1

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.