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

author	Morgan Deters <mdeters@cs.nyu.edu>
	Fri, 22 Aug 2014 20:59:28 +0000 (16:59 -0400)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Fri, 22 Aug 2014 21:58:14 +0000 (17:58 -0400)
commit	2dbe1f150d30f0fb0c8522f891104270ce09db4c
tree	1305f3de890f4353c3b5695a93ab7e2419760617	tree
parent	4ec2c8eb8b8a50dc743119100767e101f19305f6	commit \| diff

Unsat core infrastruture and API (SMT-LIB compliance to come).

46 files changed:

NEWS		diff \| blob \| history
src/expr/command.cpp		diff \| blob \| history
src/expr/command.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
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/sat_proof.cpp		diff \| blob \| history
src/proof/sat_proof.h		diff \| blob \| history
src/prop/bvminisat/bvminisat.cpp		diff \| blob \| history
src/prop/bvminisat/bvminisat.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/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/prop_engine.h		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/options		diff \| blob \| history
src/smt/options_handlers.h		diff \| blob \| history
src/smt/simplification_mode.cpp		diff \| blob \| history
src/smt/simplification_mode.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/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/bv/eager_bitblaster.cpp		diff \| blob \| history
src/theory/bv/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/ite_removal.cpp		diff \| blob \| history
src/util/ite_removal.h		diff \| blob \| history
src/util/unsat_core.cpp	[new file with mode: 0644]	blob
src/util/unsat_core.h	[new file with mode: 0644]	blob
src/util/unsat_core.i	[new file with mode: 0644]	blob
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/simplification_bug3.cvc	[deleted file]	blob \| history

RSS Atom