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

author	Clark Barrett <clarkbarrett@google.com>
	Tue, 21 Apr 2015 23:34:15 +0000 (16:34 -0700)
committer	Clark Barrett <clarkbarrett@google.com>
	Tue, 21 Apr 2015 23:34:15 +0000 (16:34 -0700)
commit	d95fe7675e20eaee86b8e804469e6db83265a005
tree	34616ecdc217d608b97d9432a368b20c75039542	tree
parent	22601bce9648a8e784527e4e5d176f634d234797	commit \| diff

Changes needed to compile at Google, plus some bug fixes from Google.

45 files changed:

proofs/lfsc_checker/check.h		diff \| blob \| history
src/context/context.h		diff \| blob \| history
src/decision/justification_heuristic.cpp		diff \| blob \| history
src/decision/justification_heuristic.h		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_value.cpp		diff \| blob \| history
src/expr/node_value.h		diff \| blob \| history
src/expr/pickler.h		diff \| blob \| history
src/expr/type_node.cpp		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/prop/bvminisat/mtl/Map.h		diff \| blob \| history
src/prop/minisat/core/SolverTypes.h		diff \| blob \| history
src/prop/minisat/mtl/Map.h		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/bound_counts.h		diff \| blob \| history
src/theory/arith/callbacks.h		diff \| blob \| history
src/theory/arith/linear_equality.h		diff \| blob \| history
src/theory/arith/matrix.h		diff \| blob \| history
src/theory/arith/simplex.h		diff \| blob \| history
src/theory/bv/bitblaster_template.h		diff \| blob \| history
src/theory/bv/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/fp/theory_fp_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/ambqi_builder.h		diff \| blob \| history
src/theory/quantifiers/bounded_integers.h		diff \| blob \| history
src/theory/quantifiers/candidate_generator.h		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv.h		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.h		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.h		diff \| blob \| history
src/theory/quantifiers/full_model_check.h		diff \| blob \| history
src/theory/quantifiers/inst_match_generator.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.h		diff \| blob \| history
src/theory/quantifiers/model_builder.h		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.h		diff \| blob \| history
src/theory/strings/options		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
src/theory/theory_model.h		diff \| blob \| history
src/util/didyoumean.cpp		diff \| blob \| history

RSS Atom