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

author	Liana Hadarean <lianah@cs.nyu.edu>
	Mon, 17 Nov 2014 20:26:42 +0000 (15:26 -0500)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Mon, 17 Nov 2014 20:26:42 +0000 (15:26 -0500)
commit	3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5
tree	845ae47600ffff9c68fa654c0f78d3474e406beb	tree
parent	d8da3b13bc9df7750723cf3da38edc8cb6f67d3d	commit \| diff

Resource-limiting work.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

60 files changed:

.mailmap		diff \| blob \| history
src/cvc4.i		diff \| blob \| history
src/decision/decision_engine.h		diff \| blob \| history
src/expr/command.cpp		diff \| blob \| history
src/expr/command.h		diff \| blob \| history
src/expr/expr_manager_template.cpp		diff \| blob \| history
src/expr/expr_manager_template.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/main/driver_unified.cpp		diff \| blob \| history
src/main/interactive_shell.cpp		diff \| blob \| history
src/main/interactive_shell.h		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/printer/ast/ast_printer.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/prop/bvminisat/bvminisat.cpp		diff \| blob \| history
src/prop/bvminisat/bvminisat.h		diff \| blob \| history
src/prop/bvminisat/core/Solver.h		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/prop/minisat/minisat.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/smt/options		diff \| blob \| history
src/smt/options_handlers.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/smt/smt_engine_scope.h		diff \| blob \| history
src/theory/bv/bitblaster_template.h		diff \| blob \| history
src/theory/bv/bv_eager_solver.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.cpp		diff \| blob \| history
src/theory/bv/eager_bitblaster.cpp		diff \| blob \| history
src/theory/bv/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/rewriter_tables_template.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_test_utils.h		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/resource_manager.cpp	[new file with mode: 0644]	blob
src/util/resource_manager.h	[new file with mode: 0644]	blob
src/util/resource_manager.i	[new file with mode: 0644]	blob
src/util/unsafe_interrupt_exception.h	[new file with mode: 0644]	blob
src/util/unsafe_interrupt_exception.i	[new file with mode: 0644]	blob
test/unit/theory/theory_bv_white.h		diff \| blob \| history

RSS Atom