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

author	Tim King <taking@google.com>
	Tue, 2 Feb 2016 17:47:34 +0000 (09:47 -0800)
committer	Tim King <taking@google.com>
	Tue, 2 Feb 2016 17:47:34 +0000 (09:47 -0800)
commit	e21e99b7dfe45f042260db7eb754e25e7108f288
tree	689bc1fead54d62b46c75196f8be0fb4b35444c9	tree
parent	18973b31c440d998230aaba3e17bd915b168aa6f	commit \| diff

Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. Breaking an edge between the sat solver and command.h.

83 files changed:

examples/hashsmt/sha1_collision.cpp		diff \| blob \| history
examples/hashsmt/sha1_inversion.cpp		diff \| blob \| history
examples/nra-translate/normalize.cpp		diff \| blob \| history
examples/nra-translate/smt2info.cpp		diff \| blob \| history
examples/nra-translate/smt2todreal.cpp		diff \| blob \| history
examples/nra-translate/smt2toisat.cpp		diff \| blob \| history
examples/nra-translate/smt2tomathematica.cpp		diff \| blob \| history
examples/nra-translate/smt2toqepcad.cpp		diff \| blob \| history
examples/nra-translate/smt2toredlog.cpp		diff \| blob \| history
examples/sets-translate/sets_translate.cpp		diff \| blob \| history
examples/translator.cpp		diff \| blob \| history
src/Makefile.am		diff \| blob \| history
src/compat/cvc3_compat.cpp		diff \| blob \| history
src/cvc4.i		diff \| blob \| history
src/decision/decision_engine.h		diff \| blob \| history
src/decision/decision_strategy.h		diff \| blob \| history
src/decision/justification_heuristic.cpp		diff \| blob \| history
src/include/cvc4.h		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/main/command_executor.h		diff \| blob \| history
src/main/command_executor_portfolio.cpp		diff \| blob \| history
src/main/driver_unified.cpp		diff \| blob \| history
src/main/interactive_shell.cpp		diff \| blob \| history
src/main/main.cpp		diff \| blob \| history
src/main/portfolio.h		diff \| blob \| history
src/parser/antlr_input.cpp		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/input.cpp		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/smt1/Smt1.g		diff \| blob \| history
src/parser/smt1/smt1.cpp		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/parser/tptp/tptp.h		diff \| blob \| history
src/printer/ast/ast_printer.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/printer/smt1/smt1_printer.cpp		diff \| blob \| history
src/printer/tptp/tptp_printer.cpp		diff \| blob \| history
src/proof/unsat_core.cpp		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/prop_engine.cpp		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/smt/command.cpp	[new file with mode: 0644]	blob
src/smt/command.h	[new file with mode: 0644]	blob
src/smt/command.i	[new file with mode: 0644]	blob
src/smt/command_list.cpp		diff \| blob \| history
src/smt/dump.cpp	[new file with mode: 0644]	blob
src/smt/dump.h	[new file with mode: 0644]	blob
src/smt/ite_removal.cpp	[new file with mode: 0644]	blob
src/smt/ite_removal.h	[new file with mode: 0644]	blob
src/smt/model.cpp	[new file with mode: 0644]	blob
src/smt/model.h	[new file with mode: 0644]	blob
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/update_ostream.h		diff \| blob \| history
src/smt_util/Makefile.am		diff \| blob \| history
src/smt_util/command.cpp	[deleted file]	blob \| history
src/smt_util/command.h	[deleted file]	blob \| history
src/smt_util/command.i	[deleted file]	blob \| history
src/smt_util/dump.cpp	[deleted file]	blob \| history
src/smt_util/dump.h	[deleted file]	blob \| history
src/smt_util/ite_removal.cpp	[deleted file]	blob \| history
src/smt_util/ite_removal.h	[deleted file]	blob \| history
src/smt_util/model.cpp	[deleted file]	blob \| history
src/smt_util/model.h	[deleted file]	blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/bv/abstraction.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.h		diff \| blob \| history
src/theory/quantifiers/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp		diff \| blob \| history
src/theory/strings/theory_strings.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/theory_model.h		diff \| blob \| history
test/system/ouroborous.cpp		diff \| blob \| history
test/system/smt2_compliance.cpp		diff \| blob \| history
test/unit/parser/parser_black.h		diff \| blob \| history
test/unit/parser/parser_builder_black.h		diff \| blob \| history

RSS Atom