git.libre-soc.org Git - cvc5.git/commit

author	Morgan Deters <mdeters@gmail.com>
	Tue, 8 Dec 2009 10:10:20 +0000 (10:10 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Tue, 8 Dec 2009 10:10:20 +0000 (10:10 +0000)
commit	2163539a8b839acf98bda0e1a65f1fcca5232fb2
tree	207a09896626f678172ec774459defa6690b0200	tree
parent	abe5fb451ae66a4bedc88d870e99f76de4eb323c	commit \| diff

work on propositional layer, expression builder support for large expressions, output classes, and minisat

46 files changed:

Makefile.builds.in		diff \| blob \| history
configure.ac		diff \| blob \| history
contrib/dimacs_to_smt.pl	[new file with mode: 0755]	blob
src/expr/expr.h		diff \| blob \| history
src/expr/expr_builder.cpp		diff \| blob \| history
src/expr/expr_builder.h		diff \| blob \| history
src/expr/expr_manager.cpp		diff \| blob \| history
src/expr/expr_manager.h		diff \| blob \| history
src/expr/expr_value.cpp		diff \| blob \| history
src/expr/expr_value.h		diff \| blob \| history
src/expr/kind.h		diff \| blob \| history
src/main/getopt.cpp		diff \| blob \| history
src/main/main.cpp		diff \| blob \| history
src/parser/antlr_parser.cpp		diff \| blob \| history
src/parser/antlr_parser.h		diff \| blob \| history
src/parser/cvc/Makefile.am		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/smt/Makefile.am		diff \| blob \| history
src/parser/symbol_table.h		diff \| blob \| history
src/prop/minisat/core/Solver.C		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/minisat/core/SolverTypes.h		diff \| blob \| history
src/prop/minisat/mtl/Alg.h		diff \| blob \| history
src/prop/minisat/mtl/BasicHeap.h		diff \| blob \| history
src/prop/minisat/mtl/BoxedVec.h		diff \| blob \| history
src/prop/minisat/mtl/Heap.h		diff \| blob \| history
src/prop/minisat/mtl/Map.h		diff \| blob \| history
src/prop/minisat/mtl/Queue.h		diff \| blob \| history
src/prop/minisat/mtl/Sort.h		diff \| blob \| history
src/prop/minisat/mtl/Vec.h		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.C		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/util/Assert.h	[new file with mode: 0644]	blob
src/util/Makefile.am		diff \| blob \| history
src/util/assert.h	[deleted file]	blob \| history
src/util/command.cpp		diff \| blob \| history
src/util/decision_engine.cpp	[new file with mode: 0644]	blob
src/util/decision_engine.h		diff \| blob \| history
src/util/literal.h		diff \| blob \| history
src/util/output.cpp	[new file with mode: 0644]	blob
src/util/output.h		diff \| blob \| history

RSS Atom