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

author	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Fri, 2 Sep 2011 12:39:23 +0000 (12:39 +0000)
committer	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Fri, 2 Sep 2011 12:39:23 +0000 (12:39 +0000)
commit	90267f8729799f44c6fb33ace11b971a16e78dff
tree	94a3bacbc8bba83e8002149232fb9804d2727ec1	tree
parent	1ea434616c48b92189e77b37b3e82dbbee0e0ccc	commit \| diff

* Changing pre-registration to be context dependent -- it is called from the SAT solver on every backtrack
* Updated UF to handle the context dependent pre-registration
* Additionally some small changes in order to satisfy warnings of the eclipse code analysis tool

16 files changed:

RSS Atom

src/main/main.cpp		diff \| blob \| history
src/parser/cvc/cvc_input.h		diff \| blob \| history
src/parser/parser_builder.cpp		diff \| blob \| history
src/parser/smt/smt_input.h		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/sat.cpp		diff \| blob \| history
src/prop/sat.h		diff \| blob \| history
src/theory/arith/theory_arith.h		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/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/equality_engine_impl.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history