GitHub - ryosu-sato/fpat

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 14 Commits
lib		lib
.depend		.depend
.gitignore		.gitignore
AEHCCSSolver.ml		AEHCCSSolver.ml
CHGenInterpProver.ml		CHGenInterpProver.ml
CNF.ml		CNF.ml
CNF.mli		CNF.mli
CSIsatInterface.ml		CSIsatInterface.ml
CSIsatInterface.mli		CSIsatInterface.mli
DNF.ml		DNF.ml
DNF.mli		DNF.mli
EAHCCSSolver.ml		EAHCCSSolver.ml
FPATConfig.ml		FPATConfig.ml
HCCS.ml		HCCS.ml
HCCS.mli		HCCS.mli
HCCSSolver.ml		HCCSSolver.ml
HCCSSolver.mli		HCCSSolver.mli
META		META
Makefile.in		Makefile.in
NNF.ml		NNF.ml
NNF.mli		NNF.mli
README		README
SMTProver.ml		SMTProver.ml
Z3Interface.ml		Z3Interface.ml
absTerm.ml		absTerm.ml
absTerm.mli		absTerm.mli
absTypInfer.ml		absTypInfer.ml
absType.ml		absType.ml
apronInterface.ml		apronInterface.ml
atom.ml		atom.ml
atom.mli		atom.mli
atpInterface.ml		atpInterface.ml
atpInterface.mli		atpInterface.mli
bag.ml		bag.ml
bag.mli		bag.mli
binder.ml		binder.ml
bitVector.ml		bitVector.ml
bool.ml		bool.ml
boolAtom.ml		boolAtom.ml
boolClause.ml		boolClause.ml
boolCube.ml		boolCube.ml
boolFormula.ml		boolFormula.ml
boolHCCSSolver.ml		boolHCCSSolver.ml
boolTerm.ml		boolTerm.ml
bwIPHCCSSolver.ml		bwIPHCCSSolver.ml
bwIPHCCSSolver.mli		bwIPHCCSSolver.mli
callId.ml		callId.ml
callTree.ml		callTree.ml
checkHCCSSolver.ml		checkHCCSSolver.ml
checkInterpProver.ml		checkInterpProver.ml
clause.ml		clause.ml
clause.mli		clause.mli
coeff.ml		coeff.ml
combination.ml		combination.ml
combinator.ml		combinator.ml
compTree.ml		compTree.ml
compTreeExpander.ml		compTreeExpander.ml
complementHCCSSolver.ml		complementHCCSSolver.ml
configure.in		configure.in
conjunction.ml		conjunction.ml
conjunction.mli		conjunction.mli
const.ml		const.ml
const.mli		const.mli
cube.ml		cube.ml
cube.mli		cube.mli
cunAtom.ml		cunAtom.ml
cunFormula.ml		cunFormula.ml
cunLiteral.ml		cunLiteral.ml
cunTerm.ml		cunTerm.ml
cvc3Interface.ml		cvc3Interface.ml
disjunction.ml		disjunction.ml
disjunction.mli		disjunction.mli
dummy.c		dummy.c
dummy.ml		dummy.ml
dune-project		dune-project
encBoolHCCSSolver.ml		encBoolHCCSSolver.ml
envFun.ml		envFun.ml
expandDagHCCSSolver.ml		expandDagHCCSSolver.ml
extConjunction.ml		extConjunction.ml
extDisjunction.ml		extDisjunction.ml
farkas.ml		farkas.ml
fdef.ml		fdef.ml
float.ml		float.ml
formula.ml		formula.ml
formula.mli		formula.mli
formulaSimplifier.ml		formulaSimplifier.ml
fpat.opam		fpat.opam
fwHCCSSolver.ml		fwHCCSSolver.ml
genHCCSSolver.ml		genHCCSSolver.ml
genInterpProver.ml		genInterpProver.ml
genInterpProver.mli		genInterpProver.mli
generalizingInterpProver.ml		generalizingInterpProver.ml
global.ml		global.ml
graph_.ml		graph_.ml
hornClause.ml		hornClause.ml
hornClause.mli		hornClause.mli
idnt.ml		idnt.ml
idnt.mli		idnt.mli
inlineHCCSSolver.ml		inlineHCCSSolver.ml
intAtom.ml		intAtom.ml

Repository files navigation

FPAT
====

FPAT is a Framework for Program Analysis and Transformation.
This is a forked version for [MoCHi](https://github.com/hopv/MoCHi).

Authors
-------

FPAT was developed and is maintained by Hiroshi Unno <uhiro@cs.tsukuba.ac.jp> 

Contributors
------------

Daisuke Okamoto <okamoto@logic.cs.tsukuba.ac.jp>
Kodai Hashimoto <kodai@logic.cs.tsukuba.ac.jp>
Sho Torii <sho@logic.cs.tsukuba.ac.jp>
Hiroki Sakamoto <sakamoto@logic.cs.tsukuba.ac.jp>