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

author	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Thu, 3 May 2012 20:18:18 +0000 (20:18 +0000)
committer	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Thu, 3 May 2012 20:18:18 +0000 (20:18 +0000)
commit	1433806056059339dd16ae8e431feaae23553150
tree	cf678baa687b1a19e479c28a1c01470bb2f120c7	tree
parent	8ef2015de66fc409a2a2958b9452c0c9b1456ee3	commit \| diff

Some cleanup starting off from trying to understand the sharing code. Changes include
* fixed term visitor from the bvprop branch
* removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles
* moved the LogicInfo into the theory constructor

30 files changed:

src/decision/justification_heuristic.cpp		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/prop/bvminisat/core/Solver.cc		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/booleans/theory_bool.h		diff \| blob \| history
src/theory/builtin/theory_builtin.h		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_normalization.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/mktheorytraits		diff \| blob \| history
src/theory/term_registration_visitor.cpp		diff \| blob \| history
src/theory/term_registration_visitor.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/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
test/unit/theory/theory_arith_white.h		diff \| blob \| history
test/unit/theory/theory_black.h		diff \| blob \| history
test/unit/theory/theory_bv_white.h		diff \| blob \| history
test/unit/theory/theory_engine_white.h		diff \| blob \| history

RSS Atom