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

author	Liana Hadarean <lianahady@gmail.com>
	Wed, 27 Jan 2016 00:04:26 +0000 (16:04 -0800)
committer	Liana Hadarean <lianahady@gmail.com>
	Wed, 27 Jan 2016 00:04:26 +0000 (16:04 -0800)
commit	42b665f2a00643c81b42932fab1441987628c5a5
tree	aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f	tree
parent	7006d5ba2f68c01638a2ab2c98a86b41dcf4467c	commit \| diff

Merged bit-vector and uf proof branch.

92 files changed:

proofs/signatures/Makefile.am		diff \| blob \| history
proofs/signatures/core_rewrites.plf	[new file with mode: 0644]	blob
proofs/signatures/ex-mem.plf		diff \| blob \| history
proofs/signatures/ex_bv.plf	[changed mode: 0755->0644]	diff \| blob \| history
proofs/signatures/ex_bv_rewrite.plf	[new file with mode: 0644]	blob
proofs/signatures/sat.plf		diff \| blob \| history
proofs/signatures/smt.plf		diff \| blob \| history
proofs/signatures/th_arrays.plf		diff \| blob \| history
proofs/signatures/th_bv.plf	[changed mode: 0755->0644]	diff \| blob \| history
proofs/signatures/th_bv_bitblast.plf	[new file with mode: 0644]	blob
src/Makefile.am		diff \| blob \| history
src/options/bv_options		diff \| blob \| history
src/proof/array_proof.h	[new file with mode: 0644]	blob
src/proof/bitvector_proof.cpp	[new file with mode: 0644]	blob
src/proof/bitvector_proof.h	[new file with mode: 0644]	blob
src/proof/cnf_proof.cpp		diff \| blob \| history
src/proof/cnf_proof.h		diff \| blob \| history
src/proof/proof.h		diff \| blob \| history
src/proof/proof_manager.cpp		diff \| blob \| history
src/proof/proof_manager.h		diff \| blob \| history
src/proof/proof_utils.cpp	[new file with mode: 0644]	blob
src/proof/proof_utils.h	[new file with mode: 0644]	blob
src/proof/sat_proof.h		diff \| blob \| history
src/proof/sat_proof_implementation.h	[new file with mode: 0644]	blob
src/proof/theory_proof.cpp		diff \| blob \| history
src/proof/theory_proof.h		diff \| blob \| history
src/proof/uf_proof.cpp	[new file with mode: 0644]	blob
src/proof/uf_proof.h	[new file with mode: 0644]	blob
src/prop/bvminisat/bvminisat.cpp		diff \| blob \| history
src/prop/bvminisat/bvminisat.h		diff \| blob \| history
src/prop/bvminisat/core/Solver.cc		diff \| blob \| history
src/prop/bvminisat/core/Solver.h		diff \| blob \| history
src/prop/bvminisat/core/SolverTypes.h		diff \| blob \| history
src/prop/bvminisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/bvminisat/simp/SimpSolver.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/core/SolverTypes.h		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/prop/minisat/minisat.h		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/prop/sat_solver_factory.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine_check_proof.cpp		diff \| blob \| history
src/smt/smt_engine_scope.h		diff \| blob \| history
src/smt_util/command.cpp		diff \| blob \| history
src/smt_util/command.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/bv/bitblast_strategies_template.h		diff \| blob \| history
src/theory/bv/bitblast_utils.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_eager_solver.h		diff \| blob \| history
src/theory/bv/bv_subtheory.h		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.h		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/bv/theory_bv_rewrite_rules_core.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.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/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/kinds		diff \| blob \| history
src/theory/uf/symmetry_breaker.cpp		diff \| blob \| history
src/theory/uf/symmetry_breaker.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
src/theory/uf/theory_uf_type_rules.h		diff \| blob \| history
test/regress/regress0/bv/Makefile.am		diff \| blob \| history
test/regress/regress0/bv/bv-proof00.smt	[new file with mode: 0644]	blob
test/regress/run_regression		diff \| blob \| history
test/unit/prop/cnf_stream_white.h		diff \| blob \| history
test/unit/theory/theory_engine_white.h		diff \| blob \| history
test/unit/theory/theory_white.h		diff \| blob \| history

RSS Atom