Skip to content
No description, website, or topics provided.
C++ C SMT M4 Python Java Other
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.idea Merged everything from LibStrangerNoRestructure Sep 8, 2016
build The install-build-deps.py script incorrectly thinks glog is not an au… Mar 20, 2018
docs
external
lib fix Q: java interface not up to date with Solver.h May 17, 2019
m4 Update configure for debug control Sep 9, 2016
src
test save status Jul 5, 2018
.gitignore string solver up and working, but needs more testing Oct 4, 2016
.gitmodules Add testing lib and bug fixes Oct 15, 2015
AUTHORS Update AUTHORS Sep 10, 2018
COPYING Update COPYING license Oct 13, 2015
ChangeLog Add initial files Apr 14, 2015
INSTALL Add initial files Apr 14, 2015
Makefile.am
NEWS Add initial files Apr 14, 2015
README Fix bugs Oct 9, 2015
README.md Update README.md Mar 7, 2019
TODO StringAutomaton and RelationalStringAutomaton have been merged into S… Aug 21, 2017
TODO_AutomataOperations preliminary identification of StringAutomaton operations Aug 14, 2017
autogen.sh Add testing lib and bug fixes Oct 15, 2015
configure.ac
spf-with-abc-readme.md Create spf-with-abc-readme.md Mar 7, 2019

README.md

ABC

The Automata Based Counter (ABC) is a string and numeric constriant solver and model counter. ABC provides solutions to systems of string and numeric constraints in the form of a deterministic finite automaton. In addition ABC produces symbolic representation of the number of strings and integers within a length bound, k, that satisfy a set of constraints. ABC can also output the number of satisfying solutions given a bound.

Publications

###ABC algorithmic details:

  • A new publication is coming with improvements over CAV'15 version of ABC.

###ABC use cases:

Setup

ABC is a C++ executable and a C++ shared library with JNI interfaces. You can use it as a static or dynamic lib or you can run it from command line.

###Download

$ cd <your home directory or a preferred directory>
$ git clone --recursive git@github.com:vlab-cs-ucsb/ABC.git ABC # or use https://github.com/vlab-cs-ucsb/ABC.git

ABC testing depends on googletest and googlemock as subprojects. It is important to clone with --recursive option.

###Easy(Automated) Setup

  • ABC. Clone ABC source and run build script. It automatically tries to install required system packages and dependent projects; Glog and Mona. After installing dependencies, it installs ABC. If script does not work please try step-by-step guide or contact us. (That script is tested with Linux machines. You can still use build script in other posix systems if you resolve system dependencies manually.)
$ cd ABC/build
$ ./install-build-deps.py

###Step-by-Step(Semi-automated) Setup ####System Dependencies

  • C++ compiler with C++14 support. Latest ABC compilation is tested with g++ 5.4.0 on Ubuntu 16.04.
  • Git
  $ sudo apt install git
  • ABC is an autotools project, you need to setup autotools in your system. Please make sure you have installed all the tools below.
  $ sudo apt install build-essential autoconf automake libtool intltool
  $ sudo apt install flex bison
  • Python (optional). A short installation script is written in pyhton.
  $ sudo apt install python

####Project Dependencies

  • Glog logging library for C++. It is an autotools project. Please follow the instructions in their website if the below shortcut doesn't work for you. Don't forget to apply patch as below:
$ cd <your home directory or a preferred directory>
$ git clone https://github.com/google/glog.git
$ cd glog
$ git apply <ABC_ROOT_DIR>/external/glog/glog_abc_autotools.patch
$ libtoolize && aclocal && automake --gnu --add-missing && autoreconf -ivf
$ ./configure
$ make all
$ sudo make install
$ sudo ldconfig

You should have glog libraries installed at /usr/local/lib and headers installed at /usr/local/include/glog/ after running above commands.

  • Mona is used for symbolic representation of automata. Don't forget to apply patch as below:
  $ cd <your home directory or a preferred directory>
  $ git clone https://github.com/cs-au-dk/MONA.git
  $ cd MONA
  $ git apply <ABC_ROOT_DIR>/external/mona/mona_abc.patch
  $ libtoolize && aclocal && automake --gnu --add-missing && autoreconf -ivf
  $ ./configure
  $ make all
  $ sudo make install
  $ sudo ldconfig

You should have mona libraries installed at /usr/local/lib and headers installed at /usr/local/include/mona/ after running above commands.

####ABC Installation

  $ cd <your home directory or a preferred directory>
  $ git clone --recursive git@github.com:vlab-cs-ucsb/ABC.git ABC // or use https://github.com/vlab-cs-ucsb/ABC.git
  $ cd ABC
  $ ./autogen.sh
  $ ./configure
  $ make all
  $ sudo make install
  $ sudo ldconfig

If you want to use ABC with JAVA programs, make sure JAVA_HOME environment variable is set and has a valid Java installation path before running ./configure command.

At this point you should have all necessary libraries installed at /usr/local/lib directory. You should also have all necessary header files at
/usr/local/include/glog,
/usr/local/include/mona,
/usr/local/include/abc
directories.

Usage

C++

You can link to dynamic library generated in your program. An example executable for mtabc is generated for you and install in your system. You can run mtabc executable at your home directory as:

$ abc -i <input_file_path> $ abc --help #lists available command line options

E.g.,

$ abc -i /test/fixtures/solver/ConstraintSolver/test_visitBegins_01.smt2

For an example of model counting a string with bound <= 5:

$ abc -i /test/fixtures/solver/ConstraintSolver/test_visitBegins_01.smt2 -v 0 -bs 5

where -v 0 disables debugging output, and -bs 5 means count solutions with bound <= 5

If there are more than one string variables, you can specify which one you want to model count with the argument: --count-variable <VARIABLE_NAME>

You can take a look at <abc source folder>/src/main.cpp to see how abc is used in a C++ program as a shared library.

(More documentation on ABC input language and format will be provided, please see <abc-source-folder>/test/fixtures folder for examples)

JAVA

You have to compile ABC with your JAVA_HOME path is set to a valid java path. Once you set your JAVA_HOME path, you need to install/re-install ABC on your system.

You need to set Java VM argument java.library.path to path where your shared libraries are install, or alternatively you can set LD_LIBRARY_PATH environment variable to that path.

You can use <abc-source-folder>/lib/ABCJava as an example Java program that calls abc.

In your Java project all you have to do is to include the contents of <abc-source-folder>/lib/ABCJava/src/. vlab.cs.ucsb.edu.DriverProxy.java class is the class that makes abc calls.

SPF (Symbolic Execution)

https://github.com/vlab-cs-ucsb/ABC/blob/master/spf-with-abc-readme.md

ABC Language Specification

to be prepared...

Contributing to ABC Source

####Workflow

1- Always start working on your own branch, do not directly work on master branch

2- Follow rebase work flow whenever possible

3- If you are not sure how to merge/rebase with/onto master, create a fresh branch out of master and first try to merge/rebase using that branch.

####Coding Style

Please follow Google C++ Style Guide.

You can’t perform that action at this time.