]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(initial) | patch
Round $n$ as I try to incorporate my work from the summer. Major updates
authorkatelman <katelman@e59a4935-1847-0410-ae03-e826735625c1>
Wed, 22 Oct 2008 19:18:17 +0000 (19:18 +0000)
committerkatelman <katelman@e59a4935-1847-0410-ae03-e826735625c1>
Wed, 22 Oct 2008 19:18:17 +0000 (19:18 +0000)
commitb4a0122adb658edf83309a6a4bd6b86cfe23b0f8
tree85a369efbb4024265521b6787a86474457c9c832tree | snapshot
Round $n$ as I try to incorporate my work from the summer. Major updates
include (a) the newest version of MiniSat, (b) improved CNF conversion, and (c)
various other improvements.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@32 e59a4935-1847-0410-ae03-e826735625c1
165 files changed:
AST/AST.cpp [new file with mode: 0644] blob
AST/AST.h [new file with mode: 0644] blob
AST/ASTKind.kinds [new file with mode: 0644] blob
AST/ASTUtil.cpp [new file with mode: 0644] blob
AST/ASTUtil.h [new file with mode: 0644] blob
AST/BitBlast.cpp [new file with mode: 0644] blob
AST/Makefile [new file with mode: 0644] blob
AST/STLport_config.h [new file with mode: 0644] blob
AST/SimpBool.cpp [new file with mode: 0644] blob
AST/ToCNF.cpp [new file with mode: 0644] blob
AST/ToSAT.cpp [new file with mode: 0644] blob
AST/Transform.cpp [new file with mode: 0644] blob
AST/asttest.cpp [new file with mode: 0644] blob
AST/bbtest.cpp [new file with mode: 0644] blob
AST/cnftest.cpp [new file with mode: 0644] blob
AST/genkinds.pl [new file with mode: 0755] blob
INSTALL [new file with mode: 0644] blob
LICENSE [new file with mode: 0644] blob
Makefile [new file with mode: 0644] blob
Makefile.common [new file with mode: 0644] blob
Makefile.cvc [new file with mode: 0644] blob
Makefile.in [new file with mode: 0644] blob
Makefile.smt [new file with mode: 0644] blob
PAPERS/EXE-STP-TISSEC-Journal-2007.pdf [new file with mode: 0644] blob
PAPERS/EXE-STP.pdf [new file with mode: 0644] blob
PAPERS/vijayganesh-stp-paper.pdf [new file with mode: 0644] blob
README [new file with mode: 0644] blob
TALKS/MIT-vijayganesh-stp-talk.pdf [new file with mode: 0644] blob
TALKS/MIT-vijayganesh-stp-talk.ppt [new file with mode: 0644] blob
big-test/dsa_chop_allopt.stp [new file with mode: 0644] blob
big-test/dsa_chop_allopt.stp.cvc [new file with mode: 0644] blob
big-test/dsa_chop_dc.stp [new file with mode: 0644] blob
big-test/dsa_chop_dc.stp.cvc [new file with mode: 0644] blob
big-test/dsa_chop_noopt-nossa.stp [new file with mode: 0644] blob
big-test/dsa_chop_noopt-nossa.stp.cvc [new file with mode: 0644] blob
big-test/dsa_chop_noopt-ssa.stp [new file with mode: 0644] blob
big-test/dsa_chop_noopt-ssa.stp.cvc [new file with mode: 0644] blob
big-test/dsa_chop_noopt.stp [new file with mode: 0644] blob
big-test/dsa_chop_noopt.stp.cvc [new file with mode: 0644] blob
big-test/histar-big-tests/chained-call-slowdown/README [new file with mode: 0644] blob
big-test/histar-big-tests/chained-call-slowdown/test [new file with mode: 0755] blob
big-test/histar-big-tests/chained-call-slowdown/test.c [new file with mode: 0644] blob
big-test/histar-big-tests/histar-long-query14143.cvc [new file with mode: 0644] blob
big-test/histar-big-tests/histar-long-query14262.cvc [new file with mode: 0644] blob
big-test/histar-big-tests/histar-long-query14281.cvc [new file with mode: 0644] blob
big-test/histar-big-tests/histar-long-query14286.cvc [new file with mode: 0644] blob
big-test/histar-big-tests/histar-long-query14295.cvc [new file with mode: 0644] blob
big-test/histar-big-tests/histar-long-query14398.cvc [new file with mode: 0644] blob
big-test/histar-big-tests/histar-long-query14426.cvc [new file with mode: 0644] blob
big-test/histar-big-tests/histar-long-query14466.cvc [new file with mode: 0644] blob
big-test/histar-big-tests/histar-long-query14510.cvc [new file with mode: 0644] blob
big-test/histar-big-tests/slow-with-cvs/README [new file with mode: 0644] blob
big-test/histar-big-tests/slow-with-cvs/test.c [new file with mode: 0644] blob
bin/run_tests [new file with mode: 0755] blob
bin/run_tests.smt [new file with mode: 0755] blob
bitvec/Makefile [new file with mode: 0644] blob
bitvec/consteval.cpp [new file with mode: 0644] blob
c-api-tests/array-cvcl-02.c [new file with mode: 0644] blob
c-api-tests/b4-c.c [new file with mode: 0644] blob
c-api-tests/b4-c2.c [new file with mode: 0644] blob
c-api-tests/getbvunsignedlonglong-check.c [new file with mode: 0644] blob
c-api-tests/multiple-queries.c [new file with mode: 0644] blob
c-api-tests/print.c [new file with mode: 0644] blob
c-api-tests/push-pop-1.c [new file with mode: 0644] blob
c-api-tests/push-pop.c [new file with mode: 0644] blob
c-api-tests/sbvmod.c [new file with mode: 0644] blob
c-api-tests/simplify.c [new file with mode: 0644] blob
c-api-tests/simplify1.c [new file with mode: 0644] blob
c-api-tests/stp-counterex.c [new file with mode: 0644] blob
c-api-tests/stp-div-001.c [new file with mode: 0644] blob
c-api-tests/stpcheck.c [new file with mode: 0644] blob
c-api-tests/x.c [new file with mode: 0644] blob
c-api-tests/y.c [new file with mode: 0644] blob
c_interface/Makefile [new file with mode: 0644] blob
c_interface/c_interface.cpp [new file with mode: 0644] blob
c_interface/c_interface.h [new file with mode: 0644] blob
c_interface/fdstream.h [new file with mode: 0644] blob
clean-install [new file with mode: 0755] blob
config.info [new file with mode: 0644] blob
configure [new file with mode: 0755] blob
constantbv/Makefile [new file with mode: 0644] blob
constantbv/constantbv.cpp [new file with mode: 0644] blob
constantbv/constantbv.h [new file with mode: 0644] blob
eric-test/acl2-stp1.cvc [new file with mode: 0644] blob
eric-test/acl2-stp2.cvc [new file with mode: 0644] blob
eric-test/acl2-stp26.cvc [new file with mode: 0644] blob
eric-test/acl2-stp3.cvc [new file with mode: 0644] blob
eric-test/acl2-stp4.cvc [new file with mode: 0644] blob
eric-test/tmpstpfile18340.cvc [new file with mode: 0644] blob
eric-test/tmpstpfile23060b.cvc [new file with mode: 0644] blob
generated_tests/extract.pl [new file with mode: 0755] blob
generated_tests/form_128.var_32.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_16.var_32.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_256.var_32.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_32.var_128.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_32.var_16.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_32.var_256.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_32.var_32.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_32.var_4.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_32.var_64.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_32.var_8.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_4.var_32.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_64.var_32.bits_32.cvc [new file with mode: 0644] blob
generated_tests/form_8.var_32.bits_32.cvc [new file with mode: 0644] blob
generated_tests/g.cvc [new file with mode: 0644] blob
generated_tests/gen2.cvc [new file with mode: 0644] blob
generated_tests/run-experiments.pl [new file with mode: 0755] blob
generated_tests/testgen.pl [new file with mode: 0755] blob
liblinks.sh [new file with mode: 0755] blob
ocaml-wrapper/COPYRIGHT-NOTICE [new file with mode: 0644] blob
ocaml-wrapper/Makefile [new file with mode: 0644] blob
ocaml-wrapper/OCamlMakefile [new file with mode: 0644] blob
ocaml-wrapper/libstp.idl [new file with mode: 0644] blob
ocaml-wrapper/libstp_regerrorhandler.c [new file with mode: 0644] blob
ocaml-wrapper/stpvc.ml [new file with mode: 0644] blob
ocaml-wrapper/stpvc.mli [new file with mode: 0644] blob
parser/.PL.y.swp [new file with mode: 0644] blob
parser/.parsePL.cpp.swp [new file with mode: 0644] blob
parser/Makefile [new file with mode: 0644] blob
parser/Makefile.smt [new file with mode: 0644] blob
parser/PL.lex [new file with mode: 0644] blob
parser/PL.y [new file with mode: 0644] blob
parser/let-funcs.cpp [new file with mode: 0644] blob
parser/main.cpp [new file with mode: 0644] blob
parser/smtlib.lex [new file with mode: 0644] blob
parser/smtlib.y [new file with mode: 0644] blob
regressions/2007-07-21-regress.log_bigarray-test [new file with mode: 0644] blob
regressions/2007-07-22-regress.log [new file with mode: 0644] blob
regressions/2008-01-14-regress.log [new file with mode: 0644] blob
regressions/2008-01-14-regress.log-big-test [new file with mode: 0644] blob
regressions/2008-01-14-regress.log-bigarray-test [new file with mode: 0644] blob
regressions/2008-01-15-regress.log [new file with mode: 0644] blob
regressions/2008-01-15-regress.log-bigarray-test [new file with mode: 0644] blob
regressions/README [new file with mode: 0644] blob
sat/LICENSE [new file with mode: 0644] blob
sat/README [new file with mode: 0644] blob
sat/core/Main.C [new file with mode: 0644] blob
sat/core/Makefile [new file with mode: 0644] blob
sat/core/Solver.C [new file with mode: 0644] blob
sat/core/Solver.h [new file with mode: 0644] blob
sat/core/SolverTypes.h [new file with mode: 0644] blob
sat/core/depend.mk [new file with mode: 0644] blob
sat/mtl/Alg.h [new file with mode: 0644] blob
sat/mtl/BasicHeap.h [new file with mode: 0644] blob
sat/mtl/BoxedVec.h [new file with mode: 0644] blob
sat/mtl/Heap.h [new file with mode: 0644] blob
sat/mtl/Map.h [new file with mode: 0644] blob
sat/mtl/Queue.h [new file with mode: 0644] blob
sat/mtl/Sort.h [new file with mode: 0644] blob
sat/mtl/Vec.h [new file with mode: 0644] blob
sat/mtl/template.mk [new file with mode: 0644] blob
sat/simp/Main.C [new file with mode: 0644] blob
sat/simp/Makefile [new file with mode: 0644] blob
sat/simp/SimpSolver.C [new file with mode: 0644] blob
sat/simp/SimpSolver.h [new file with mode: 0644] blob
sat/simp/depend.mk [new file with mode: 0644] blob
simplifier/Makefile [new file with mode: 0644] blob
simplifier/bvsolver.cpp [new file with mode: 0644] blob
simplifier/bvsolver.h [new file with mode: 0644] blob
simplifier/simplifier.cpp [new file with mode: 0644] blob
web/stp-docs.html [new file with mode: 0644] blob
web/stp-papers.html [new file with mode: 0644] blob
web/stp-tools.html [new file with mode: 0644] blob
web/stp.html [new file with mode: 0644] blob
web/template.html [new file with mode: 0644] blob
STP Constraint Solver.