GitHub - dbueno/bitfunc: Library for building bit-vector and array constraints directly on top of a SAT solver

dbueno / bitfunc Public

Notifications You must be signed in to change notification settings
Fork 0
Star 0

Library for building bit-vector and array constraints directly on top of a SAT solver

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 5 Commits
funcsat		funcsat
llvm-frontend		llvm-frontend
m4		m4
src		src
test		test
.gitignore		.gitignore
.pylintrc		.pylintrc
Bitfunc.hsc		Bitfunc.hsc
BitfuncTest.hs		BitfuncTest.hs
Bitfunc_hs.chs		Bitfunc_hs.chs
COPYRIGHT		COPYRIGHT
Doxyfile		Doxyfile
Makefile.am		Makefile.am
Makefile.in		Makefile.in
README		README
_bitfunc_cy.pxd		_bitfunc_cy.pxd
aclocal.m4		aclocal.m4
ar-lib		ar-lib
bap_parse_il.c		bap_parse_il.c
bitfunc.h		bitfunc.h
bitfunc_cy.c		bitfunc_cy.c
bitfunc_cy.pyx		bitfunc_cy.pyx
common.am		common.am
compile		compile
config.guess		config.guess
config.sub		config.sub
configure		configure
configure.ac		configure.ac
create-bundle.sh		create-bundle.sh
depcomp		depcomp
flake.lock		flake.lock
flake.nix		flake.nix
install-sh		install-sh
ltmain.sh		ltmain.sh
makeitcrash.c		makeitcrash.c
missing		missing
py-compile		py-compile
runonvm		runonvm
test_bitfunc.py		test_bitfunc.py
todo.org		todo.org

Repository files navigation

-*- mode: outline -*-

This is bitfunc. It is written and developed by Denis Bueno <denis.bueno@sandia.gov>.

Copyright 2012 Sandia Corporation. Under the terms of Contract
DE-AC04-94AL85000, there is a non-exclusive license for use of this work by or
on behalf of the U.S. Government. Export of this program may require a license
from the United States Government.

* Dependencies

  - autoconf
  - automake
  - autoconf-archive (on some systems)
  - pkg-config
  - libtool
  - Cython >= 0.15
  - gcc (we use a bunch of its optimizations)
  - picosat-936 (optional, but strongly recommended): http://fmv.jku.at/picosat/picosat-936.tar.gz

If you want to _hack_ on bitfunc, then you need a few more things:

  - Don Knuth's CWEB. funcsat, a SAT solver bundled with bitfunc, uses CWEB.

* Installation

First, untar picosat and compile it with ./configure && make.

curl -O http://fmv.jku.at/picosat/picosat-936.tar.gz
tar xzf picosat-936.tar.gz
cd picosat-936 && ./configure && make

Next, compile bitfunc:

./configure --prefix=/path/to/somewhere --with-picosat=/path/to/picosat-936
make 
make install

* Python API

Assuming you have Python 2.7-ish with the dev stuff installed, after
installation to $DIR, add $DIR/lib/python2.7/site-packages to $PYTHONPATH. To
test, you should be able to do:

    python -c 'import bitfunc'

without problems.