README_dev.txt

#********************************************************************
# Copyright 2008-2010 Adam Kiezun, Vijay Ganesh
#********************************************************************
# AUTHORS: Adam Kiezun, Vijay Ganesh
#
# BEGIN DATE: October/November 2008
#
# This file belongs to the Hampi string solver project (solver for
# equations over regular expressions)
# 
# LICENSE: Please view LICENSE file in the home dir of this Program
#********************************************************************

This file is intended to help in development of Hampi.
It describes to to build and test Hampi, how the solver works, and how the code is structured.

-------------------------------------------------------- 
How the solver works: Hampi class is the top-level entry point. It calls the
HProgramParser to parse the input and create a HProgram (which
represents the parsed input). The HProgram is then encoded into core
constraints (Constraint) by HConstraintPreparer (this involves
bounding all context-free grammars and changing them to regular
expressions. This is where Hampi often spends the most time). The
Constraint is then passed to STPSolver. The STPSolver checks first if
a simple SAT or UNSAT solution is possible, otherwise STPSolver
encodes the Constraint as list of STPExprs. The encoding writes
regular expression in terms that STP understands (concatenation,
equality, and constants). The encoded STP expressions are put together
in an AndExpr and passed to STP (call to vc.query). Hampi decodes the
solution (i.e., translated bits back to strings).
-------------------------------------------------------- 
How to build
and test: 
./configure 
make 
make verify

--------------------------------------------------------
How to run Hampi (standalone mode):

./hampi.sh a.hmp

(see README.txt for server mode)
--------------------------------------------------------
Top-level package structure.

hampi: Top-level classes, in particular
  Hampi (facade for the solver, both API and file input)
  Solution (solution to the constraint problem)
  HampiException (wrapper exception for Hampi)
  HampiResultException (thrown when a solution is found, to quickly communicate the result)

hampi.constraints: Core constraints. The input language gets translated to those core constraints, and the solving itself works on core constraints. See the paper for another description of the process.
  
hampi.grammars: TODO

hampi.grammars.apps: Utility classes for grammars, eg
   GrammarStringBounder - bounds a context-free grammar, ie, creates a regexp that describes all strings from a grammar that have a specific length
   UnreachableNonterminalRemover - removes unreachable nonterminals from a CFG
   EpsilonProductionRemover - removes productions A -> \epsilon

(These 3 packages are mostly dead code. I think they are referenced only from tests)
hampi.grammars.cykparser: CYK parser
hampi.grammars.lexer: hand-coded lexer
hampi.grammars.parser: hand-coded parser

hampi.parser: Lexer/Parser classes. 
   Lexer and Parser are generated by ANTRL. 
   Files Hampi.g and HampiTree.g are the specification.  
   Lexer and Parser are made by running MakeLexerParser, and then MakeTree. This will regenerate the Lexer and Parser.
   The CFG* classes are for defining context-free grammars. The H* classes are for defining all Hampi constraints. HProgram represents the top-level Hampi input.

NOTE: there's a bit of disoreder about grammars in Hampi. There are 2 packages (hampi.grammars and hampi.parser) - the former represents context-free grammars, the latter represents Hampi's input format. The first should be, in principle, removable. It exists mostly as legacy code.

hampi.stp: Classes the correspond to elements of STP constraints.

hampi.utils: utilities

--------------------------------------------------------