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

author	Morgan Deters <mdeters@cs.nyu.edu>
	Fri, 16 Aug 2013 19:15:03 +0000 (15:15 -0400)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Fri, 13 Sep 2013 22:32:39 +0000 (18:32 -0400)
commit	14776d0aeb833a7e728a27af6ef545f20b495f7f
tree	eccc91e0be00cfb9af7d757aae3dd07479c256fb	tree
parent	09fc93244e10b4450592b4ede151873142d54b34	commit \| diff

Documentation fixes, some code typo fixes, file perms, other minor things.

59 files changed:

contrib/get-bug-attachments		diff \| blob \| history
contrib/theoryskel/README.WHATS-NEXT		diff \| blob \| history
doc/SmtEngine.3cvc_template.in		diff \| blob \| history
doc/cvc4.1_template.in		diff \| blob \| history
doc/cvc4.5.in		diff \| blob \| history
doc/libcvc4compat.3.in		diff \| blob \| history
doc/libcvc4parser.3.in		diff \| blob \| history
doc/options.3cvc_template.in		diff \| blob \| history
src/expr/metakind_template.h		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/parser/tptp/tptp.cpp		diff \| blob \| history
src/parser/tptp/tptp.h		diff \| blob \| history
src/parser/tptp/tptp_input.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.h		diff \| blob \| history
src/prop/minisat/mtl/Vec.h		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/options		diff \| blob \| history
src/smt/options		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/arith/approx_simplex.h		diff \| blob \| history
src/theory/arith/bound_counts.h		diff \| blob \| history
src/theory/arith/normal_form.cpp		diff \| blob \| history
src/theory/arith/options		diff \| blob \| history
src/theory/arith/simplex_update.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/idl/idl_assertion.cpp		diff \| blob \| history
src/theory/idl/idl_assertion.h		diff \| blob \| history
src/theory/idl/idl_assertion_db.cpp		diff \| blob \| history
src/theory/idl/idl_assertion_db.h		diff \| blob \| history
src/theory/idl/idl_model.cpp		diff \| blob \| history
src/theory/idl/idl_model.h		diff \| blob \| history
src/theory/idl/theory_idl.cpp		diff \| blob \| history
src/theory/idl/theory_idl.h		diff \| blob \| history
src/theory/ite_simplifier.cpp		diff \| blob \| history
src/theory/ite_simplifier.h		diff \| blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/quantifiers/bounded_integers.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/bounded_integers.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/first_order_reasoning.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/first_order_reasoning.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/full_model_check.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/full_model_check.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/model_engine.h		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/uf/equality_engine.h		diff \| blob \| history
src/util/result.i		diff \| blob \| history
src/util/statistics_registry.h		diff \| blob \| history
test/regress/regress0/fmf/Makefile.am	[changed mode: 0755->0644]	blob \| history
test/regress/regress0/fmf/german169.smt2	[changed mode: 0755->0644]	blob \| history
test/regress/regress0/fmf/german73.smt2	[changed mode: 0755->0644]	blob \| history
test/regress/regress0/fmf/refcount24.cvc.smt2	[changed mode: 0755->0644]	blob \| history

RSS Atom