[cvc4] branch master updated (d668c63 -> 80a6dad)
Fabian Wolff
fw-guest at moszumanska.debian.org
Tue Jul 11 23:02:00 UTC 2017
This is an automated email from the git hooks/post-receive script.
fw-guest pushed a change to branch master
in repository cvc4.
from d668c63 Adjust debian/cvc4.manpages
new c9b8284 New upstream version 1.5
new 0a8dbbe Updated version 1.5 from 'upstream/1.5'
new 265015e Remove patches that have been fixed upstream
new 519a9bb Update debian/changelog
new 5b96f54 Use SOURCE_DATE_EPOCH instead of parsing debian/changelog manually
new 42477d4 Update Standards-Version to 4.0.0 in debian/control
new 40ec7e2 Adjust package names to match sonames
new dbc1cdb Add watch file
new cd4918e Rename install files to match new package names
new 80a6dad Add hello-world test in debian/tests/
The 10 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails. The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.
Summary of changes:
AUTHORS | 19 +-
INSTALL | 15 +-
Makefile.am | 4 +-
Makefile.in | 5 +-
NEWS | 17 +-
README | 55 +-
RELEASE-NOTES | 36 +-
THANKS | 44 +-
config/cryptominisat.m4 | 10 +-
configure | 168 +-
configure.ac | 36 +-
contrib/Makefile.in | 1 +
cvc4autoconfig.h.in | 3 +
debian/changelog | 4 +-
debian/control | 17 +-
debian/{libcvc4-3.install => libcvc4-4.install} | 0
...bcvc4parser3.install => libcvc4parser4.install} | 0
debian/patches/01-ref-compare.patch | 17 -
.../{02-timestamps.patch => 01-timestamps.patch} | 0
...-include-paths.patch => 02-include-paths.patch} | 2 +-
debian/patches/04-spelling-errors.patch | 208 -
debian/patches/series | 6 +-
debian/rules | 6 +-
debian/tests/control | 2 +
debian/tests/hello-world | 31 +
debian/watch | 2 +
doc/SmtEngine.3cvc | 95 +-
doc/cvc4.1 | 79 +-
doc/libcvc4.3 | 2 +-
doc/options.3cvc | 132 +-
examples/Makefile.in | 1 +
examples/SimpleVC.java | 4 +-
examples/SimpleVCCompat.java | 4 +-
examples/api/Makefile.in | 1 +
examples/api/bitvectors.cpp | 4 +-
examples/api/bitvectors_and_arrays.cpp | 4 +-
examples/api/combination.cpp | 4 +-
examples/api/datatypes.cpp | 4 +-
examples/api/extract.cpp | 4 +-
examples/api/helloworld.cpp | 4 +-
examples/api/java/BitVectors.java | 4 +-
examples/api/java/BitVectorsAndArrays.java | 4 +-
examples/api/java/CVC4Streams.java | 4 +-
examples/api/java/Combination.java | 4 +-
examples/api/java/Datatypes.java | 4 +-
examples/api/java/HelloWorld.java | 4 +-
examples/api/java/LinearArith.java | 4 +-
examples/api/java/Makefile.in | 1 +
examples/api/java/PipedInput.java | 4 +-
examples/api/java/Strings.java | 4 +-
examples/api/linear_arith.cpp | 4 +-
examples/api/sets.cpp | 4 +-
examples/api/strings.cpp | 4 +-
examples/hashsmt/Makefile.in | 1 +
examples/hashsmt/sha1.hpp | 4 +-
examples/hashsmt/sha1_collision.cpp | 4 +-
examples/hashsmt/sha1_inversion.cpp | 2 +-
examples/hashsmt/word.cpp | 2 +-
examples/hashsmt/word.h | 4 +-
examples/nra-translate/Makefile.in | 1 +
examples/nra-translate/normalize.cpp | 2 +-
examples/nra-translate/smt2info.cpp | 4 +-
examples/nra-translate/smt2todreal.cpp | 2 +-
examples/nra-translate/smt2toisat.cpp | 4 +-
examples/nra-translate/smt2tomathematica.cpp | 2 +-
examples/nra-translate/smt2toqepcad.cpp | 2 +-
examples/nra-translate/smt2toredlog.cpp | 4 +-
examples/sets-translate/Makefile.in | 1 +
examples/sets-translate/sets_translate.cpp | 4 +-
examples/simple_vc_compat_c.c | 4 +-
examples/simple_vc_compat_cxx.cpp | 4 +-
examples/simple_vc_cxx.cpp | 4 +-
examples/translator.cpp | 4 +-
library_versions | 1 +
proofs/lfsc_checker/code.cpp | 19 +
proofs/signatures/Makefile.in | 1 +
proofs/signatures/signatures.cpp | 45 +-
proofs/signatures/smt.plf | 41 +
proofs/signatures/th_bv_bitblast.plf | 4 +-
src/Makefile.am | 636 +-
src/Makefile.in | 1422 +-
src/base/Makefile.in | 1 +
src/base/configuration.cpp | 2 +-
src/base/configuration.h | 2 +-
src/base/configuration_private.h | 7 +-
src/base/cvc4_assert.cpp | 4 +-
src/base/cvc4_assert.h | 4 +-
src/base/exception.cpp | 4 +-
src/base/exception.h | 4 +-
src/base/listener.cpp | 4 +-
src/base/listener.h | 4 +-
src/base/modal_exception.h | 4 +-
src/base/output.cpp | 4 +-
src/base/output.h | 2 +-
src/base/ptr_closer.h | 2 +-
src/base/tls.h.in | 4 +-
src/bindings/Makefile.in | 1 +
src/bindings/compat/Makefile.in | 1 +
src/bindings/compat/c/Makefile.in | 1 +
src/bindings/compat/java/Makefile.in | 1 +
src/bindings/java_iterator_adapter.h | 4 +-
src/bindings/java_stream_adapters.h | 4 +-
src/bindings/swig.h | 4 +-
src/compat/Makefile.in | 1 +
src/compat/cvc3_compat.cpp | 2 +-
src/compat/cvc3_compat.h | 4 +-
src/context/backtrackable.h | 4 +-
src/context/cdchunk_list.h | 4 +-
src/context/cddense_set.h | 4 +-
src/context/cdhashmap.h | 2 +-
src/context/cdhashmap_forward.h | 4 +-
src/context/cdhashset.h | 4 +-
src/context/cdhashset_forward.h | 4 +-
src/context/cdinsert_hashmap.h | 2 +-
src/context/cdinsert_hashmap_forward.h | 4 +-
src/context/cdlist.h | 2 +-
src/context/cdlist_forward.h | 4 +-
src/context/cdmaybe.h | 4 +-
src/context/cdo.h | 2 +-
src/context/cdqueue.h | 4 +-
src/context/cdtrail_hashmap.h | 2 +-
src/context/cdtrail_hashmap_forward.h | 4 +-
src/context/cdtrail_queue.h | 4 +-
src/context/cdvector.h | 4 +-
src/context/context.cpp | 2 +-
src/context/context.h | 4 +-
src/context/context_mm.cpp | 2 +-
src/context/context_mm.h | 2 +-
src/context/stacking_vector.h | 114 -
src/decision/decision_attributes.h | 4 +-
src/decision/decision_engine.cpp | 4 +-
src/decision/decision_engine.h | 4 +-
src/decision/decision_strategy.h | 4 +-
src/decision/justification_heuristic.cpp | 2 +-
src/decision/justification_heuristic.h | 4 +-
src/expr/Makefile.am | 31 +-
src/expr/Makefile.in | 32 +-
src/expr/array.h | 4 +-
src/expr/array_store_all.cpp | 4 +-
src/expr/array_store_all.h | 4 +-
src/expr/ascription_type.h | 4 +-
src/expr/attribute.cpp | 2 +-
src/expr/attribute.h | 2 +-
src/expr/attribute_internals.h | 2 +-
src/expr/attribute_unique_id.h | 4 +-
src/expr/chain.h | 4 +-
src/expr/convenience_node_builders.h | 4 +-
src/expr/datatype.cpp | 38 +-
src/expr/datatype.h | 7 +-
src/expr/emptyset.cpp | 2 +-
src/expr/emptyset.h | 4 +-
src/expr/expr_iomanip.cpp | 4 +-
src/expr/expr_iomanip.h | 4 +-
src/expr/expr_manager_scope.h | 4 +-
src/expr/expr_manager_template.cpp | 10 +-
src/expr/expr_manager_template.h | 12 +-
src/expr/expr_stream.h | 4 +-
src/expr/expr_template.cpp | 17 +-
src/expr/expr_template.h | 2 +-
src/expr/kind_map.h | 4 +-
src/expr/kind_template.h | 4 +-
src/expr/matcher.h | 4 +-
src/expr/metakind_template.h | 9 +-
src/expr/mkexpr | 8 +-
src/expr/mkkind | 11 +-
src/expr/mkmetakind | 11 +-
src/expr/node.cpp | 2 +-
src/expr/node.h | 18 +-
src/expr/node_builder.h | 7 +-
src/expr/node_manager.cpp | 21 +-
src/expr/node_manager.h | 5 +-
src/expr/node_manager_attributes.h | 4 +-
src/expr/node_manager_listeners.cpp | 4 +-
src/expr/node_manager_listeners.h | 4 +-
src/expr/node_self_iterator.h | 4 +-
src/expr/node_value.cpp | 6 +-
src/expr/node_value.h | 4 +-
src/expr/pickle_data.cpp | 4 +-
src/expr/pickle_data.h | 4 +-
src/expr/pickler.cpp | 2 +-
src/expr/pickler.h | 4 +-
src/expr/predicate.cpp | 4 +-
src/expr/predicate.h | 4 +-
src/expr/record.cpp | 4 +-
src/expr/record.h | 4 +-
src/expr/symbol_table.cpp | 4 +-
src/expr/symbol_table.h | 2 +-
src/expr/type.cpp | 27 +-
src/expr/type.h | 2 +-
src/expr/type_checker.h | 4 +-
src/expr/type_checker_template.cpp | 8 +-
src/expr/type_node.cpp | 42 +-
src/expr/type_node.h | 6 +-
src/expr/type_properties_template.h | 4 +-
src/expr/uninterpreted_constant.cpp | 4 +-
src/expr/uninterpreted_constant.h | 4 +-
src/expr/variable_type_map.h | 4 +-
src/git_versioninfo.cpp | 8 +-
src/include/cvc4.h | 4 +-
src/include/cvc4_private.h | 4 +-
src/include/cvc4_private_library.h | 4 +-
src/include/cvc4_public.h | 4 +-
src/include/cvc4parser_private.h | 4 +-
src/include/cvc4parser_public.h | 4 +-
src/lib/Makefile.in | 1 +
src/lib/clock_gettime.c | 4 +-
src/lib/clock_gettime.h | 4 +-
src/lib/ffs.c | 4 +-
src/lib/ffs.h | 4 +-
src/lib/replacements.h | 4 +-
src/lib/strtok_r.c | 4 +-
src/lib/strtok_r.h | 4 +-
src/main/Makefile.in | 1 +
src/main/command_executor.cpp | 2 +-
src/main/command_executor.h | 11 +-
src/main/command_executor_portfolio.cpp | 2 +-
src/main/command_executor_portfolio.h | 4 +-
src/main/driver_unified.cpp | 19 +-
src/main/interactive_shell.cpp | 8 +-
src/main/interactive_shell.h | 4 +-
src/main/main.cpp | 5 +-
src/main/main.h | 6 +-
src/main/portfolio.cpp | 4 +-
src/main/portfolio.h | 4 +-
src/main/portfolio_util.cpp | 2 +-
src/main/portfolio_util.h | 2 +-
src/main/util.cpp | 241 +-
src/options/Makefile.am | 29 +-
src/options/Makefile.in | 30 +-
src/options/argument_extender.h | 4 +-
src/options/argument_extender_implementation.cpp | 4 +-
src/options/argument_extender_implementation.h | 4 +-
src/options/arith_heuristic_pivot_rule.cpp | 4 +-
src/options/arith_heuristic_pivot_rule.h | 4 +-
src/options/arith_options | 26 +-
src/options/arith_options.cpp | 366 +-
src/options/arith_options.h | 768 +-
src/options/arith_propagation_mode.cpp | 4 +-
src/options/arith_propagation_mode.h | 4 +-
src/options/arith_unate_lemma_mode.cpp | 4 +-
src/options/arith_unate_lemma_mode.h | 4 +-
src/options/arrays_options.cpp | 80 +-
src/options/arrays_options.h | 158 +-
src/options/base_handlers.h | 4 +-
src/options/base_options.cpp | 110 +-
src/options/base_options.h | 228 +-
src/options/base_options_template.cpp | 4 +-
src/options/base_options_template.h | 4 +-
src/options/booleans_options.cpp | 8 +-
src/options/booleans_options.h | 14 +-
src/options/builtin_options.cpp | 8 +-
src/options/builtin_options.h | 14 +-
src/options/bv_bitblast_mode.cpp | 2 +-
src/options/bv_bitblast_mode.h | 2 +-
src/options/bv_options.cpp | 186 +-
src/options/bv_options.h | 376 +-
src/options/datatypes_options.cpp | 66 +-
src/options/datatypes_options.h | 130 +-
src/options/decision_mode.cpp | 4 +-
src/options/decision_mode.h | 4 +-
src/options/decision_options.cpp | 48 +-
src/options/decision_options.h | 98 +-
src/options/decision_weight.h | 4 +-
src/options/didyoumean.cpp | 2 +-
src/options/didyoumean.h | 2 +-
src/options/expr_options.cpp | 38 +-
src/options/expr_options.h | 74 +-
src/options/fp_options.cpp | 8 +-
src/options/fp_options.h | 14 +-
src/options/idl_options.cpp | 16 +-
src/options/idl_options.h | 30 +-
src/options/language.cpp | 12 +-
src/options/language.h | 13 +-
src/options/language.i | 2 +
src/options/main_options.cpp | 112 +-
src/options/main_options.h | 226 +-
src/options/open_ostream.cpp | 4 +-
src/options/open_ostream.h | 4 +-
src/options/option_exception.h | 4 +-
src/options/options.h | 4 +-
src/options/options_get_option_template.cpp | 4 +-
src/options/options_handler.cpp | 6 +-
src/options/options_handler.h | 4 +-
src/options/options_holder_template.h | 4 +-
src/options/options_public_functions.cpp | 4 +-
src/options/options_set_option_template.cpp | 4 +-
src/options/options_template.cpp | 4 +-
src/options/parser_options.cpp | 38 +-
src/options/parser_options.h | 74 +-
src/options/printer_modes.cpp | 4 +-
src/options/printer_modes.h | 4 +-
src/options/printer_options.cpp | 24 +-
src/options/printer_options.h | 50 +-
src/options/proof_options.cpp | 34 +-
src/options/proof_options.h | 66 +-
src/options/prop_options.cpp | 70 +-
src/options/prop_options.h | 138 +-
src/options/quantifiers_modes.cpp | 2 +-
src/options/quantifiers_modes.h | 2 +-
src/options/quantifiers_options | 16 +-
src/options/quantifiers_options.cpp | 986 +-
src/options/quantifiers_options.h | 2028 +-
src/options/sep_options.cpp | 44 +-
src/options/sep_options.h | 86 +-
src/options/set_language.cpp | 4 +-
src/options/set_language.h | 4 +-
src/options/sets_options | 3 +
src/options/sets_options.cpp | 32 +-
src/options/sets_options.h | 67 +-
src/options/simplification_mode.cpp | 4 +-
src/options/simplification_mode.h | 4 +-
src/options/smt_options | 51 +-
src/options/smt_options.cpp | 388 +-
src/options/smt_options.h | 784 +-
src/options/strings_options.cpp | 162 +-
src/options/strings_options.h | 322 +-
src/options/theory_options.cpp | 22 +-
src/options/theory_options.h | 44 +-
src/options/theoryof_mode.cpp | 4 +-
src/options/theoryof_mode.h | 4 +-
src/options/uf_options.cpp | 108 +-
src/options/uf_options.h | 216 +-
src/options/ufss_mode.h | 4 +-
src/parser/Makefile.am | 2 +
src/parser/Makefile.in | 6 +-
src/parser/antlr_input.cpp | 48 +-
src/parser/antlr_input.h | 24 +-
src/parser/antlr_input_imports.cpp | 16 +-
src/parser/antlr_line_buffered_input.cpp | 321 +-
src/parser/antlr_line_buffered_input.h | 24 +-
src/parser/antlr_tracing.h | 4 +-
src/parser/antlr_undefines.h | 4 +-
src/parser/bounded_token_buffer.cpp | 4 +-
src/parser/bounded_token_buffer.h | 4 +-
src/parser/bounded_token_factory.cpp | 4 +-
src/parser/bounded_token_factory.h | 4 +-
src/parser/cvc/Cvc.g | 47 +-
src/parser/cvc/Cvc.tokens | 340 +-
src/parser/cvc/CvcLexer.c | 3852 +-
src/parser/cvc/CvcLexer.h | 190 +-
src/parser/cvc/CvcParser.c | 11162 ++--
src/parser/cvc/CvcParser.h | 193 +-
src/parser/cvc/Makefile.in | 1 +
src/parser/cvc/cvc_input.cpp | 2 +-
src/parser/cvc/cvc_input.h | 4 +-
src/parser/input.cpp | 2 +-
src/parser/input.h | 7 +-
src/parser/line_buffer.cpp | 88 +
src/parser/line_buffer.h | 76 +
src/parser/memory_mapped_input_buffer.cpp | 2 +-
src/parser/memory_mapped_input_buffer.h | 4 +-
src/parser/parser.cpp | 4 +-
src/parser/parser.h | 2 +-
src/parser/parser_builder.cpp | 3 +-
src/parser/parser_builder.h | 4 +-
src/parser/parser_exception.h | 4 +-
src/parser/smt1/Makefile.in | 1 +
src/parser/smt1/Smt1.g | 11 +-
src/parser/smt1/Smt1Lexer.c | 866 +-
src/parser/smt1/Smt1Lexer.h | 4 +-
src/parser/smt1/Smt1Parser.c | 419 +-
src/parser/smt1/Smt1Parser.h | 13 +-
src/parser/smt1/smt1.cpp | 2 +-
src/parser/smt1/smt1.h | 4 +-
src/parser/smt1/smt1_input.cpp | 2 +-
src/parser/smt1/smt1_input.h | 4 +-
src/parser/smt2/Makefile.in | 1 +
src/parser/smt2/Smt2.g | 322 +-
src/parser/smt2/Smt2.tokens | 277 +-
src/parser/smt2/Smt2Lexer.c | 60045 ++++++++++---------
src/parser/smt2/Smt2Lexer.h | 337 +-
src/parser/smt2/Smt2Parser.c | 6364 +-
src/parser/smt2/Smt2Parser.h | 290 +-
src/parser/smt2/smt2.cpp | 33 +-
src/parser/smt2/smt2.h | 12 +-
src/parser/smt2/smt2_input.cpp | 5 +-
src/parser/smt2/smt2_input.h | 4 +-
src/parser/smt2/sygus_input.cpp | 4 +-
src/parser/smt2/sygus_input.h | 4 +-
src/parser/tptp/Makefile.in | 1 +
src/parser/tptp/Tptp.g | 17 +-
src/parser/tptp/TptpLexer.c | 720 +-
src/parser/tptp/TptpLexer.h | 4 +-
src/parser/tptp/TptpParser.c | 679 +-
src/parser/tptp/TptpParser.h | 13 +-
src/parser/tptp/tptp.cpp | 4 +-
src/parser/tptp/tptp.h | 4 +-
src/parser/tptp/tptp_input.cpp | 4 +-
src/parser/tptp/tptp_input.h | 4 +-
src/printer/ast/ast_printer.cpp | 4 +-
src/printer/ast/ast_printer.h | 4 +-
src/printer/cvc/cvc_printer.cpp | 28 +-
src/printer/cvc/cvc_printer.h | 4 +-
src/printer/dagification_visitor.cpp | 4 +-
src/printer/dagification_visitor.h | 4 +-
src/printer/printer.cpp | 7 +-
src/printer/printer.h | 4 +-
src/printer/smt1/smt1_printer.cpp | 4 +-
src/printer/smt1/smt1_printer.h | 4 +-
src/printer/smt2/smt2_printer.cpp | 284 +-
src/printer/smt2/smt2_printer.h | 7 +-
src/printer/tptp/tptp_printer.cpp | 4 +-
src/printer/tptp/tptp_printer.h | 4 +-
src/proof/arith_proof.cpp | 4 +-
src/proof/arith_proof.h | 2 +-
src/proof/array_proof.cpp | 31 +-
src/proof/array_proof.h | 2 +-
src/proof/bitvector_proof.cpp | 6 +-
src/proof/bitvector_proof.h | 3 +-
src/proof/clause_id.h | 4 +-
src/proof/cnf_proof.cpp | 2 +-
src/proof/cnf_proof.h | 2 +-
src/proof/lemma_proof.cpp | 19 +-
src/proof/lemma_proof.h | 17 +-
src/proof/proof.h | 4 +-
src/proof/proof_manager.cpp | 80 +-
src/proof/proof_manager.h | 35 +-
src/proof/proof_output_channel.cpp | 18 +-
src/proof/proof_output_channel.h | 7 +
src/proof/proof_utils.cpp | 4 +-
src/proof/proof_utils.h | 4 +-
src/proof/sat_proof.h | 27 +-
src/proof/sat_proof_implementation.h | 91 +-
src/proof/simplify_boolean_node.cpp | 183 +
.../simplify_boolean_node.h} | 22 +-
src/proof/skolemization_manager.cpp | 4 +-
src/proof/skolemization_manager.h | 2 +-
src/proof/theory_proof.cpp | 25 +-
src/proof/theory_proof.h | 5 +-
src/proof/uf_proof.cpp | 89 +-
src/proof/uf_proof.h | 4 +-
src/proof/unsat_core.cpp | 4 +-
src/proof/unsat_core.h | 7 +-
src/prop/bvminisat/Makefile | 77 +-
src/prop/bvminisat/Makefile.in | 1 +
src/prop/bvminisat/bvminisat.cpp | 16 +-
src/prop/bvminisat/bvminisat.h | 16 +-
src/prop/cnf_stream.cpp | 2 +-
src/prop/cnf_stream.h | 4 +-
src/prop/cryptominisat.cpp | 16 +-
src/prop/cryptominisat.h | 16 +-
src/prop/minisat/Makefile | 77 +-
src/prop/minisat/Makefile.in | 1 +
src/prop/minisat/core/Solver.cc | 7 +-
src/prop/minisat/minisat.cpp | 16 +-
src/prop/minisat/minisat.h | 16 +-
src/prop/prop_engine.cpp | 2 +-
src/prop/prop_engine.h | 2 +-
src/prop/registrar.h | 2 +-
src/prop/sat_solver.h | 2 +-
src/prop/sat_solver_factory.cpp | 4 +-
src/prop/sat_solver_factory.h | 4 +-
src/prop/sat_solver_types.h | 4 +-
src/prop/theory_proxy.cpp | 4 +-
src/prop/theory_proxy.h | 2 +-
src/smt/command.cpp | 120 +-
src/smt/command.h | 126 +-
src/smt/command_list.cpp | 4 +-
src/smt/command_list.h | 4 +-
src/smt/dump.cpp | 4 +-
src/smt/dump.h | 4 +-
src/smt/logic_exception.h | 4 +-
src/smt/logic_request.cpp | 4 +-
src/smt/logic_request.h | 4 +-
src/smt/managed_ostreams.cpp | 4 +-
src/smt/managed_ostreams.h | 4 +-
src/smt/model.cpp | 4 +-
src/smt/model.h | 4 +-
src/smt/smt_engine.cpp | 399 +-
src/smt/smt_engine.h | 31 +-
src/smt/smt_engine.i | 1 -
src/smt/smt_engine_check_proof.cpp | 4 +-
src/smt/smt_engine_scope.cpp | 4 +-
src/smt/smt_engine_scope.h | 2 +-
src/smt/smt_statistics_registry.cpp | 4 +-
src/smt/smt_statistics_registry.h | 4 +-
src/smt/term_formula_removal.cpp | 19 +-
src/smt/term_formula_removal.h | 4 +-
src/smt/update_ostream.h | 4 +-
src/smt_util/Makefile.in | 1 +
src/smt_util/boolean_simplification.cpp | 4 +-
src/smt_util/boolean_simplification.h | 4 +-
src/smt_util/lemma_channels.cpp | 4 +-
src/smt_util/lemma_channels.h | 4 +-
src/smt_util/lemma_input_channel.h | 4 +-
src/smt_util/lemma_output_channel.h | 4 +-
src/smt_util/nary_builder.cpp | 4 +-
src/smt_util/nary_builder.h | 4 +-
src/smt_util/node_visitor.h | 2 +-
src/svn_versioninfo.cpp | 8 +-
src/theory/arith/approx_simplex.cpp | 4 +-
src/theory/arith/approx_simplex.h | 4 +-
src/theory/arith/arith_ite_utils.cpp | 4 +-
src/theory/arith/arith_ite_utils.h | 4 +-
src/theory/arith/arith_rewriter.cpp | 10 +-
src/theory/arith/arith_rewriter.h | 2 +-
src/theory/arith/arith_static_learner.cpp | 2 +-
src/theory/arith/arith_static_learner.h | 4 +-
src/theory/arith/arith_utilities.h | 58 +-
src/theory/arith/arithvar.cpp | 4 +-
src/theory/arith/arithvar.h | 4 +-
src/theory/arith/attempt_solution_simplex.cpp | 4 +-
src/theory/arith/attempt_solution_simplex.h | 4 +-
src/theory/arith/bound_counts.h | 4 +-
src/theory/arith/callbacks.cpp | 4 +-
src/theory/arith/callbacks.h | 4 +-
src/theory/arith/congruence_manager.cpp | 7 +-
src/theory/arith/congruence_manager.h | 7 +-
src/theory/arith/constraint.cpp | 4 +-
src/theory/arith/constraint.h | 4 +-
src/theory/arith/constraint_forward.h | 4 +-
src/theory/arith/cut_log.cpp | 4 +-
src/theory/arith/cut_log.h | 2 +-
src/theory/arith/delta_rational.cpp | 4 +-
src/theory/arith/delta_rational.h | 2 +-
src/theory/arith/dio_solver.cpp | 4 +-
src/theory/arith/dio_solver.h | 4 +-
src/theory/arith/dual_simplex.cpp | 4 +-
src/theory/arith/dual_simplex.h | 4 +-
src/theory/arith/error_set.cpp | 4 +-
src/theory/arith/error_set.h | 4 +-
src/theory/arith/fc_simplex.cpp | 4 +-
src/theory/arith/fc_simplex.h | 4 +-
src/theory/arith/infer_bounds.cpp | 4 +-
src/theory/arith/infer_bounds.h | 4 +-
src/theory/arith/kinds | 2 +
src/theory/arith/linear_equality.cpp | 4 +-
src/theory/arith/linear_equality.h | 4 +-
src/theory/arith/matrix.cpp | 4 +-
src/theory/arith/matrix.h | 4 +-
src/theory/arith/nonlinear_extension.cpp | 2271 +
src/theory/arith/nonlinear_extension.h | 208 +
src/theory/arith/normal_form.cpp | 18 +-
src/theory/arith/normal_form.h | 8 +-
src/theory/arith/partial_model.cpp | 4 +-
src/theory/arith/partial_model.h | 4 +-
src/theory/arith/pseudoboolean_proc.cpp | 4 +-
src/theory/arith/pseudoboolean_proc.h | 4 +-
src/theory/arith/simplex.cpp | 4 +-
src/theory/arith/simplex.h | 4 +-
src/theory/arith/simplex_update.cpp | 4 +-
src/theory/arith/simplex_update.h | 4 +-
src/theory/arith/soi_simplex.cpp | 4 +-
src/theory/arith/soi_simplex.h | 4 +-
src/theory/arith/tableau.cpp | 4 +-
src/theory/arith/tableau.h | 4 +-
src/theory/arith/tableau_sizes.cpp | 4 +-
src/theory/arith/tableau_sizes.h | 4 +-
src/theory/arith/theory_arith.cpp | 27 +-
src/theory/arith/theory_arith.h | 8 +-
src/theory/arith/theory_arith_private.cpp | 540 +-
src/theory/arith/theory_arith_private.h | 54 +-
src/theory/arith/theory_arith_private_forward.h | 4 +-
src/theory/arith/theory_arith_type_rules.h | 2 +-
src/theory/arith/type_enumerator.h | 4 +-
src/theory/arrays/array_info.cpp | 2 +-
src/theory/arrays/array_info.h | 2 +-
src/theory/arrays/array_proof_reconstruction.cpp | 2 +-
src/theory/arrays/array_proof_reconstruction.h | 4 +-
src/theory/arrays/static_fact_manager.cpp | 4 +-
src/theory/arrays/static_fact_manager.h | 4 +-
src/theory/arrays/theory_arrays.cpp | 40 +-
src/theory/arrays/theory_arrays.h | 11 +-
src/theory/arrays/theory_arrays_rewriter.cpp | 4 +-
src/theory/arrays/theory_arrays_rewriter.h | 2 +-
src/theory/arrays/theory_arrays_type_rules.h | 9 +-
src/theory/arrays/type_enumerator.h | 8 +-
src/theory/arrays/union_find.cpp | 4 +-
src/theory/arrays/union_find.h | 4 +-
...heory_arith_private_forward.h => assertion.cpp} | 22 +-
src/theory/assertion.h | 52 +
src/theory/atom_requests.cpp | 4 +-
src/theory/atom_requests.h | 4 +-
src/theory/booleans/circuit_propagator.cpp | 4 +-
src/theory/booleans/circuit_propagator.h | 2 +-
src/theory/booleans/theory_bool.cpp | 5 +-
src/theory/booleans/theory_bool.h | 4 +-
src/theory/booleans/theory_bool_rewriter.cpp | 2 +-
src/theory/booleans/theory_bool_rewriter.h | 4 +-
src/theory/booleans/theory_bool_type_rules.h | 2 +-
src/theory/booleans/type_enumerator.h | 6 +-
src/theory/builtin/kinds | 2 +-
src/theory/builtin/theory_builtin.cpp | 4 +-
src/theory/builtin/theory_builtin.h | 4 +-
src/theory/builtin/theory_builtin_rewriter.cpp | 4 +-
src/theory/builtin/theory_builtin_rewriter.h | 4 +-
src/theory/builtin/theory_builtin_type_rules.h | 2 +-
src/theory/builtin/type_enumerator.h | 8 +-
src/theory/bv/abstraction.cpp | 4 +-
src/theory/bv/abstraction.h | 4 +-
src/theory/bv/aig_bitblaster.cpp | 22 +-
src/theory/bv/bitblast_strategies_template.h | 4 +-
src/theory/bv/bitblast_utils.h | 4 +-
src/theory/bv/bitblaster_template.h | 9 +-
src/theory/bv/bv_eager_solver.cpp | 4 +-
src/theory/bv/bv_eager_solver.h | 4 +-
src/theory/bv/bv_inequality_graph.cpp | 4 +-
src/theory/bv/bv_inequality_graph.h | 4 +-
src/theory/bv/bv_quick_check.cpp | 2 +-
src/theory/bv/bv_quick_check.h | 4 +-
src/theory/bv/bv_subtheory.h | 2 +-
src/theory/bv/bv_subtheory_algebraic.cpp | 2 +-
src/theory/bv/bv_subtheory_algebraic.h | 4 +-
src/theory/bv/bv_subtheory_bitblast.cpp | 2 +-
src/theory/bv/bv_subtheory_bitblast.h | 2 +-
src/theory/bv/bv_subtheory_core.cpp | 5 +-
src/theory/bv/bv_subtheory_core.h | 2 +-
src/theory/bv/bv_subtheory_inequality.cpp | 4 +-
src/theory/bv/bv_subtheory_inequality.h | 2 +-
src/theory/bv/bv_to_bool.cpp | 4 +-
src/theory/bv/bv_to_bool.h | 4 +-
src/theory/bv/bvintropow2.cpp | 4 +-
src/theory/bv/bvintropow2.h | 4 +-
src/theory/bv/cd_set_collection.h | 4 +-
src/theory/bv/eager_bitblaster.cpp | 2 +-
src/theory/bv/lazy_bitblaster.cpp | 12 +-
src/theory/bv/slicer.cpp | 4 +-
src/theory/bv/slicer.h | 4 +-
src/theory/bv/theory_bv.cpp | 24 +-
src/theory/bv/theory_bv.h | 4 +-
src/theory/bv/theory_bv_rewrite_rules.h | 29 +-
.../theory_bv_rewrite_rules_constant_evaluation.h | 2 +-
src/theory/bv/theory_bv_rewrite_rules_core.h | 2 +-
.../bv/theory_bv_rewrite_rules_normalization.h | 2 +-
.../theory_bv_rewrite_rules_operator_elimination.h | 2 +-
.../bv/theory_bv_rewrite_rules_simplification.h | 38 +-
src/theory/bv/theory_bv_rewriter.cpp | 12 +-
src/theory/bv/theory_bv_rewriter.h | 2 +-
src/theory/bv/theory_bv_type_rules.h | 4 +-
src/theory/bv/theory_bv_utils.cpp | 4 +-
src/theory/bv/theory_bv_utils.h | 2 +-
src/theory/bv/type_enumerator.h | 8 +-
src/theory/care_graph.h | 62 +
src/theory/datatypes/datatypes_rewriter.h | 64 +-
src/theory/datatypes/datatypes_sygus.cpp | 2 +-
src/theory/datatypes/datatypes_sygus.h | 4 +-
src/theory/datatypes/theory_datatypes.cpp | 143 +-
src/theory/datatypes/theory_datatypes.h | 12 +-
src/theory/datatypes/theory_datatypes_type_rules.h | 24 +-
src/theory/datatypes/type_enumerator.cpp | 2 +-
src/theory/datatypes/type_enumerator.h | 14 +-
src/theory/example/ecdata.cpp | 4 +-
src/theory/example/ecdata.h | 4 +-
src/theory/example/theory_uf_tim.cpp | 4 +-
src/theory/example/theory_uf_tim.h | 4 +-
src/theory/fp/theory_fp.cpp | 4 +-
src/theory/fp/theory_fp.h | 4 +-
src/theory/fp/theory_fp_rewriter.cpp | 4 +-
src/theory/fp/theory_fp_rewriter.h | 4 +-
src/theory/fp/theory_fp_type_rules.h | 4 +-
src/theory/idl/idl_assertion.cpp | 4 +-
src/theory/idl/idl_assertion.h | 4 +-
src/theory/idl/idl_assertion_db.cpp | 4 +-
src/theory/idl/idl_assertion_db.h | 4 +-
src/theory/idl/idl_model.cpp | 4 +-
src/theory/idl/idl_model.h | 4 +-
src/theory/idl/theory_idl.cpp | 2 +-
src/theory/idl/theory_idl.h | 4 +-
src/theory/interrupted.h | 4 +-
src/theory/ite_utilities.cpp | 2 +-
src/theory/ite_utilities.h | 4 +-
src/theory/logic_info.cpp | 8 +-
src/theory/logic_info.h | 4 +-
src/theory/mkrewriter | 8 +-
src/theory/mktheorytraits | 9 +-
src/theory/output_channel.h | 2 +-
src/theory/quantifiers/alpha_equivalence.cpp | 2 +-
src/theory/quantifiers/alpha_equivalence.h | 4 +-
src/theory/quantifiers/ambqi_builder.cpp | 196 +-
src/theory/quantifiers/ambqi_builder.h | 6 +-
src/theory/quantifiers/anti_skolem.cpp | 2 +-
src/theory/quantifiers/anti_skolem.h | 2 +-
src/theory/quantifiers/bounded_integers.cpp | 14 +-
src/theory/quantifiers/bounded_integers.h | 2 +-
src/theory/quantifiers/candidate_generator.cpp | 4 +-
src/theory/quantifiers/candidate_generator.h | 2 +-
src/theory/quantifiers/ce_guided_instantiation.cpp | 1459 +-
src/theory/quantifiers/ce_guided_instantiation.h | 154 +-
src/theory/quantifiers/ce_guided_single_inv.cpp | 9 +-
src/theory/quantifiers/ce_guided_single_inv.h | 4 +-
src/theory/quantifiers/ce_guided_single_inv_ei.cpp | 4 +-
src/theory/quantifiers/ce_guided_single_inv_ei.h | 4 +-
.../quantifiers/ce_guided_single_inv_sol.cpp | 6 +-
src/theory/quantifiers/ce_guided_single_inv_sol.h | 4 +-
src/theory/quantifiers/ceg_instantiator.cpp | 46 +-
src/theory/quantifiers/ceg_instantiator.h | 4 +-
src/theory/quantifiers/ceg_t_instantiator.cpp | 2 +-
src/theory/quantifiers/ceg_t_instantiator.h | 2 +-
src/theory/quantifiers/conjecture_generator.cpp | 5 +-
src/theory/quantifiers/conjecture_generator.h | 4 +-
src/theory/quantifiers/equality_infer.cpp | 2 +-
src/theory/quantifiers/equality_infer.h | 2 +-
src/theory/quantifiers/first_order_model.cpp | 59 +-
src/theory/quantifiers/first_order_model.h | 23 +-
src/theory/quantifiers/full_model_check.cpp | 373 +-
src/theory/quantifiers/full_model_check.h | 8 +-
src/theory/quantifiers/fun_def_engine.cpp | 4 +-
src/theory/quantifiers/fun_def_engine.h | 4 +-
src/theory/quantifiers/fun_def_process.cpp | 205 +-
src/theory/quantifiers/fun_def_process.h | 10 +-
src/theory/quantifiers/inst_match.cpp | 3 +-
src/theory/quantifiers/inst_match.h | 6 +-
src/theory/quantifiers/inst_match_generator.cpp | 296 +-
src/theory/quantifiers/inst_match_generator.h | 69 +-
src/theory/quantifiers/inst_propagator.cpp | 6 +-
src/theory/quantifiers/inst_propagator.h | 2 +-
src/theory/quantifiers/inst_strategy_cbqi.cpp | 55 +-
src/theory/quantifiers/inst_strategy_cbqi.h | 3 +-
.../quantifiers/inst_strategy_e_matching.cpp | 11 +-
src/theory/quantifiers/inst_strategy_e_matching.h | 2 +-
src/theory/quantifiers/instantiation_engine.cpp | 2 +-
src/theory/quantifiers/instantiation_engine.h | 2 +-
src/theory/quantifiers/local_theory_ext.cpp | 6 +-
src/theory/quantifiers/local_theory_ext.h | 2 +-
src/theory/quantifiers/macros.cpp | 22 +-
src/theory/quantifiers/macros.h | 2 +-
src/theory/quantifiers/model_builder.cpp | 298 +-
src/theory/quantifiers/model_builder.h | 25 +-
src/theory/quantifiers/model_engine.cpp | 16 +-
src/theory/quantifiers/model_engine.h | 2 +-
src/theory/quantifiers/quant_conflict_find.cpp | 105 +-
src/theory/quantifiers/quant_conflict_find.h | 4 +-
src/theory/quantifiers/quant_equality_engine.cpp | 4 +-
src/theory/quantifiers/quant_equality_engine.h | 4 +-
src/theory/quantifiers/quant_split.cpp | 2 +-
src/theory/quantifiers/quant_split.h | 2 +-
src/theory/quantifiers/quant_util.cpp | 12 +-
src/theory/quantifiers/quant_util.h | 5 +-
src/theory/quantifiers/quantifiers_attributes.cpp | 4 +-
src/theory/quantifiers/quantifiers_attributes.h | 4 +-
src/theory/quantifiers/quantifiers_rewriter.cpp | 47 +-
src/theory/quantifiers/quantifiers_rewriter.h | 6 +-
src/theory/quantifiers/relevant_domain.cpp | 77 +-
src/theory/quantifiers/relevant_domain.h | 5 +-
src/theory/quantifiers/rewrite_engine.cpp | 2 +-
src/theory/quantifiers/rewrite_engine.h | 2 +-
src/theory/quantifiers/symmetry_breaking.cpp | 4 +-
src/theory/quantifiers/symmetry_breaking.h | 2 +-
src/theory/quantifiers/term_database.cpp | 119 +-
src/theory/quantifiers/term_database.h | 12 +-
src/theory/quantifiers/theory_quantifiers.cpp | 35 +-
src/theory/quantifiers/theory_quantifiers.h | 10 +-
.../quantifiers/theory_quantifiers_type_rules.h | 4 +-
src/theory/quantifiers/trigger.cpp | 163 +-
src/theory/quantifiers/trigger.h | 13 +-
src/theory/quantifiers_engine.cpp | 220 +-
src/theory/quantifiers_engine.h | 26 +-
src/theory/rep_set.cpp | 2 +-
src/theory/rep_set.h | 2 +-
src/theory/rewriter.cpp | 2 +-
src/theory/rewriter.h | 4 +-
src/theory/rewriter_attributes.h | 4 +-
src/theory/rewriter_tables_template.h | 2 +-
src/theory/sep/kinds | 3 +-
src/theory/sep/theory_sep.cpp | 38 +-
src/theory/sep/theory_sep.h | 18 +-
src/theory/sep/theory_sep_rewriter.cpp | 14 +-
src/theory/sep/theory_sep_rewriter.h | 12 +-
src/theory/sep/theory_sep_type_rules.h | 23 +-
src/theory/sets/kinds | 10 +-
src/theory/sets/normal_form.h | 4 +-
src/theory/sets/rels_utils.h | 12 +-
src/theory/sets/theory_sets.cpp | 18 +-
src/theory/sets/theory_sets.h | 10 +-
src/theory/sets/theory_sets_private.cpp | 360 +-
src/theory/sets/theory_sets_private.h | 22 +-
src/theory/sets/theory_sets_rels.cpp | 957 +-
src/theory/sets/theory_sets_rels.h | 111 +-
src/theory/sets/theory_sets_rewriter.cpp | 92 +-
src/theory/sets/theory_sets_rewriter.h | 4 +-
src/theory/sets/theory_sets_type_enumerator.h | 4 +-
src/theory/sets/theory_sets_type_rules.h | 121 +-
src/theory/shared_terms_database.cpp | 2 +-
src/theory/shared_terms_database.h | 2 +-
src/theory/sort_inference.cpp | 4 +-
src/theory/sort_inference.h | 4 +-
src/theory/strings/regexp_operation.cpp | 4 +-
src/theory/strings/regexp_operation.h | 2 +-
src/theory/strings/theory_strings.cpp | 144 +-
src/theory/strings/theory_strings.h | 5 +-
src/theory/strings/theory_strings_preprocess.cpp | 2 +-
src/theory/strings/theory_strings_preprocess.h | 2 +-
src/theory/strings/theory_strings_rewriter.cpp | 77 +-
src/theory/strings/theory_strings_rewriter.h | 2 +-
src/theory/strings/theory_strings_type_rules.h | 6 +-
src/theory/strings/type_enumerator.h | 8 +-
src/theory/substitutions.cpp | 2 +-
src/theory/substitutions.h | 2 +-
src/theory/term_registration_visitor.cpp | 2 +-
src/theory/term_registration_visitor.h | 4 +-
src/theory/theory.cpp | 322 +-
src/theory/theory.h | 338 +-
src/theory/theory_engine.cpp | 158 +-
src/theory/theory_engine.h | 20 +-
src/theory/theory_model.cpp | 235 +-
src/theory/theory_model.h | 23 +-
src/theory/theory_registrar.h | 4 +-
src/theory/theory_test_utils.h | 2 +-
src/theory/theory_traits_template.h | 4 +-
src/theory/type_enumerator.h | 6 +-
src/theory/type_enumerator_template.cpp | 4 +-
src/theory/uf/equality_engine.cpp | 2 +-
src/theory/uf/equality_engine.h | 2 +-
src/theory/uf/equality_engine_types.h | 4 +-
src/theory/uf/symmetry_breaker.cpp | 4 +-
src/theory/uf/symmetry_breaker.h | 4 +-
src/theory/uf/theory_uf.cpp | 37 +-
src/theory/uf/theory_uf.h | 5 +-
src/theory/uf/theory_uf_model.cpp | 2 +-
src/theory/uf/theory_uf_model.h | 4 +-
src/theory/uf/theory_uf_rewriter.h | 4 +-
src/theory/uf/theory_uf_strong_solver.cpp | 2 +-
src/theory/uf/theory_uf_strong_solver.h | 4 +-
src/theory/uf/theory_uf_type_rules.h | 8 +-
src/theory/unconstrained_simplifier.cpp | 4 +-
src/theory/unconstrained_simplifier.h | 4 +-
src/theory/valuation.cpp | 4 +-
src/theory/valuation.h | 2 +-
src/util/Makefile.am | 2 +
src/util/Makefile.in | 23 +-
src/util/abstract_value.cpp | 4 +-
src/util/abstract_value.h | 4 +-
src/util/bin_heap.h | 4 +-
src/util/bitvector.h | 2 +-
src/util/bool.h | 4 +-
src/util/cache.h | 4 +-
src/util/cardinality.cpp | 2 +-
src/util/cardinality.h | 2 +-
src/util/channel.h | 6 +-
src/util/debug.h | 4 +-
src/util/dense_map.h | 4 +-
src/util/divisible.cpp | 4 +-
src/util/divisible.h | 4 +-
src/util/dynamic_array.h | 4 +-
src/util/floatingpoint.cpp | 4 +-
src/util/floatingpoint.h | 4 +-
src/util/gmp_util.h | 4 +-
src/util/hash.h | 4 +-
src/util/index.h | 4 +-
src/util/integer.h.in | 4 +-
src/util/integer_cln_imp.cpp | 4 +-
src/util/integer_cln_imp.h | 2 +-
src/util/integer_gmp_imp.cpp | 4 +-
src/util/integer_gmp_imp.h | 2 +-
src/util/maybe.h | 4 +-
src/util/ntuple.h | 4 +-
src/util/proof.h | 4 +-
src/util/rational.h.in | 4 +-
src/util/rational_cln_imp.cpp | 2 +-
src/util/rational_cln_imp.h | 4 +-
src/util/rational_gmp_imp.cpp | 2 +-
src/util/rational_gmp_imp.h | 4 +-
src/util/regexp.cpp | 4 +-
src/util/regexp.h | 4 +-
src/util/resource_manager.cpp | 4 +-
src/util/resource_manager.h | 2 +-
src/util/result.cpp | 5 +-
src/util/result.h | 2 +-
src/util/safe_print.cpp | 214 +
src/util/safe_print.h | 99 +
src/util/sexpr.cpp | 5 +-
src/util/sexpr.h | 2 +-
src/util/smt2_quote_string.cpp | 4 +-
src/util/smt2_quote_string.h | 4 +-
src/util/statistics.cpp | 19 +-
src/util/statistics.h | 10 +-
src/util/statistics_registry.cpp | 10 +-
src/util/statistics_registry.h | 145 +-
src/util/subrange_bound.cpp | 2 +-
src/util/subrange_bound.h | 2 +-
src/util/tuple.h | 4 +-
src/util/unsafe_interrupt_exception.h | 4 +-
src/util/utility.h | 4 +-
test/Makefile.am | 2 +
test/Makefile.in | 3 +
test/regress/Makefile.in | 1 +
test/regress/regress0/Makefile.am | 8 +-
test/regress/regress0/Makefile.in | 30 +-
test/regress/regress0/arith/Makefile.am | 3 +-
test/regress/regress0/arith/Makefile.in | 11 +-
test/regress/regress0/arith/bug547.2.smt2 | 2 +-
test/regress/regress0/arith/bug716.0.smt2 | 3 +-
test/regress/regress0/arith/bug716.1.cvc | 2 +-
test/regress/regress0/arith/div.02.smt2 | 4 +-
test/regress/regress0/arith/div.03.smt2 | 4 +-
test/regress/regress0/arith/div.05.smt2 | 4 +-
test/regress/regress0/arith/div.06.smt2 | 4 +-
test/regress/regress0/arith/div.09.smt2 | 3 +-
test/regress/regress0/arith/integers/Makefile.in | 1 +
test/regress/regress0/arith/mod-simp.smt2 | 10 +
test/regress/regress0/arith/mod.01.smt2 | 4 +-
test/regress/regress0/arith/mod.02.smt2 | 4 +-
test/regress/regress0/arith/mod.03.smt2 | 4 +-
test/regress/regress0/arith/mult.01.smt2 | 4 +-
test/regress/regress0/arith/mult.02.smt2 | 2 +-
test/regress/regress0/arrays/Makefile.in | 1 +
test/regress/regress0/arrays/bool-array.smt2 | 2 -
test/regress/regress0/aufbv/Makefile.in | 1 +
test/regress/regress0/auflia/Makefile.in | 1 +
test/regress/regress0/bug639.smt2 | 26 +
test/regress/regress0/bug681.smt2 | 54 +
test/regress/regress0/bv/Makefile.am | 5 +-
test/regress/regress0/bv/Makefile.in | 27 +-
test/regress/regress0/bv/bug733.smt2 | 8 +
test/regress/regress0/bv/bug787.smt2 | 91 +
test/regress/regress0/bv/bv-int-collapse2-sat.smt2 | 2 +-
.../regress/regress0/bv/bv2nat-simp-range-sat.smt2 | 5 +
test/regress/regress0/bv/cmu-rdk-3.smt2 | 2 +
test/regress/regress0/bv/core/Makefile.in | 1 +
test/regress/regress0/datatypes/Makefile.am | 9 +-
test/regress/regress0/datatypes/Makefile.in | 55 +-
test/regress/regress0/datatypes/dt-2.6.smt2 | 15 +
test/regress/regress0/datatypes/dt-color-2.6.smt2 | 17 +
.../regress0/datatypes/dt-match-pat-param-2.6.smt2 | 24 +
test/regress/regress0/datatypes/dt-param-2.6.smt2 | 37 +
test/regress/regress0/datatypes/dt-sel-2.6.smt2 | 18 +
test/regress/regress0/datatypes/jsat-2.6.smt2 | 28 +
test/regress/regress0/datatypes/tuple-no-clash.cvc | 11 +
test/regress/regress0/decision/Makefile.in | 1 +
test/regress/regress0/declare-fun-is-match.smt2 | 9 +
test/regress/regress0/expect/Makefile.in | 1 +
test/regress/regress0/expect/scrub.01.smt.expect | 3 +-
test/regress/regress0/expect/scrub.02.smt | 3 +-
test/regress/regress0/expect/scrub.03.smt2.expect | 3 +-
test/regress/regress0/expect/scrub.04.smt2 | 3 +-
test/regress/regress0/expect/scrub.06.cvc | 6 +-
test/regress/regress0/expect/scrub.07.sy.expect | 5 +-
test/regress/regress0/expect/scrub.08.sy | 7 +-
test/regress/regress0/expect/scrub.09.p | 7 +-
test/regress/regress0/fmf/Makefile.am | 8 +-
test/regress/regress0/fmf/Makefile.in | 51 +-
test/regress/regress0/fmf/alg202+1.smt2 | 17 +
.../regress0/fmf/bug-041417-set-options.cvc | 16 +
test/regress/regress0/fmf/constr-ground-to.smt2 | 43 +
.../regress0/fmf/fmf-fun-no-elim-ext-arith.smt2 | 18 +
.../regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 | 25 +
test/regress/regress0/fmf/quant_real_univ.cvc | 14 +
test/regress/regress0/lemmas/Makefile.in | 1 +
test/regress/regress0/nl/Makefile.am | 64 +
test/regress/regress0/{arith => nl}/Makefile.in | 283 +-
test/regress/regress0/nl/all-logic.smt2 | 8 +
test/regress/regress0/nl/bug698.smt2 | 33 +
test/regress/regress0/nl/coeff-sat.smt2 | 16 +
test/regress/regress0/nl/coeff-unsat-base.smt2 | 16 +
test/regress/regress0/nl/coeff-unsat.smt2 | 16 +
test/regress/regress0/nl/combine.smt2 | 13 +
test/regress/regress0/nl/disj-eval.smt2 | 14 +
test/regress/regress0/nl/dist-big.smt2 | 16 +
test/regress/regress0/nl/div-mod-partial.smt2 | 10 +
.../regress0/nl/magnitude-wrong-1020-m.smt2 | 72 +
test/regress/regress0/nl/metitarski-1025.smt2 | 30 +
test/regress/regress0/nl/metitarski-3-4.smt2 | 29 +
test/regress/regress0/nl/metitarski_3_4_2e.smt2 | 30 +
test/regress/regress0/nl/mult-po.smt2 | 20 +
test/regress/regress0/nl/nia-wrong-tl.smt2 | 47 +
test/regress/regress0/nl/nl-help-unsat-quant.smt2 | 419 +
test/regress/regress0/nl/nl-unk-quant.smt2 | 29 +
test/regress/regress0/nl/ones.smt2 | 18 +
test/regress/regress0/nl/poly-1025.smt2 | 29 +
test/regress/regress0/nl/quant-nl.smt2 | 857 +
test/regress/regress0/nl/real-div-ufnra.smt2 | 13 +
test/regress/regress0/nl/red-exp.smt2 | 11 +
test/regress/regress0/nl/rewriting-sums.smt2 | 18 +
test/regress/regress0/nl/simple-mono-unsat.smt2 | 18 +
test/regress/regress0/nl/simple-mono.smt2 | 17 +
test/regress/regress0/nl/subs0-unsat-confirm.smt2 | 18 +
test/regress/regress0/nl/very-easy-sat.smt2 | 30 +
test/regress/regress0/nl/very-simple-unsat.smt2 | 15 +
test/regress/regress0/nl/zero-subset.smt2 | 15 +
test/regress/regress0/parser/Makefile.in | 1 +
test/regress/regress0/precedence/Makefile.in | 1 +
test/regress/regress0/preprocess/Makefile.in | 1 +
test/regress/regress0/push-pop/Makefile.am | 4 +-
test/regress/regress0/push-pop/Makefile.in | 19 +-
test/regress/regress0/push-pop/arith/Makefile.in | 1 +
test/regress/regress0/push-pop/boolean/Makefile.in | 1 +
test/regress/regress0/push-pop/bug821.smt2 | 8 +
.../regress0/push-pop/simple_unsat_cores.smt2 | 10 +
test/regress/regress0/quantifiers/Makefile.am | 7 +-
test/regress/regress0/quantifiers/Makefile.in | 35 +-
test/regress/regress0/quantifiers/RND-small.smt2 | 2 +-
.../regress/regress0/quantifiers/anti-sk-simp.smt2 | 2 +-
test/regress/regress0/quantifiers/ari056.smt2 | 2 +
test/regress/regress0/quantifiers/bug822.smt2 | 1183 +
.../regress0/quantifiers/cbqi-lia-dt-simp.smt2 | 2 +-
.../quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 | 19 +
test/regress/regress0/quantifiers/delta-simp.smt2 | 4 +-
.../regress0/quantifiers/macro-subtype-param.smt2 | 7 +-
.../regress0/quantifiers/macros-real-arg.smt2 | 2 +-
test/regress/regress0/quantifiers/mix-coeff.smt2 | 4 +-
.../regress0/quantifiers/mix-complete-strat.smt2 | 2 +-
test/regress/regress0/quantifiers/mix-simp.smt2 | 4 +-
.../regress/regress0/quantifiers/psyco-001-bv.smt2 | 76 +
test/regress/regress0/quantifiers/psyco-196.smt2 | 2 +
.../regress/regress0/quantifiers/pure_dt_cbqi.smt2 | 2 +
test/regress/regress0/quantifiers/qbv-simp.smt2 | 9 +
.../quantifiers/quaternion_ds1_symm_0428.fof.smt2 | 2 +-
.../regress0/quantifiers/subtype-param-unk.smt2 | 3 +-
.../regress0/quantifiers/subtype-param.smt2 | 2 +-
test/regress/regress0/rels/Makefile.am | 17 +-
test/regress/regress0/rels/Makefile.in | 116 +-
test/regress/regress0/rels/atom_univ2.cvc | 24 +
test/regress/regress0/rels/card_transpose.cvc | 6 +
test/regress/regress0/rels/iden_0.cvc | 28 +
test/regress/regress0/rels/iden_1.cvc | 19 +
test/regress/regress0/rels/iden_1_1.cvc | 22 +
test/regress/regress0/rels/joinImg_0.cvc | 33 +
test/regress/regress0/rels/joinImg_0_1.cvc | 35 +
test/regress/regress0/rels/joinImg_0_2.cvc | 39 +
test/regress/regress0/rels/joinImg_1.cvc | 20 +
test/regress/regress0/rels/joinImg_1_1.cvc | 21 +
test/regress/regress0/rels/joinImg_2.cvc | 33 +
test/regress/regress0/rels/joinImg_2_1.cvc | 24 +
test/regress/regress0/rels/rel_tc_8.cvc | 10 +
test/regress/regress0/rels/rels-sharing-simp.cvc | 14 +
test/regress/regress0/rewriterules/Makefile.in | 1 +
test/regress/regress0/sep/Makefile.am | 3 +-
test/regress/regress0/sep/Makefile.in | 11 +-
test/regress/regress0/sep/nil-no-elim.smt2 | 11 +
test/regress/regress0/sets/Makefile.am | 11 +-
test/regress/regress0/sets/Makefile.in | 75 +-
test/regress/regress0/sets/complement.cvc | 3 +-
test/regress/regress0/sets/complement2.cvc | 3 +-
test/regress/regress0/sets/complement3.cvc | 15 +
.../regress/regress0/sets/int-real-univ-unsat.smt2 | 16 +
test/regress/regress0/sets/int-real-univ.smt2 | 16 +
test/regress/regress0/sets/nonvar-univ.smt2 | 13 +
test/regress/regress0/sets/pre-proc-univ.smt2 | 11 +
test/regress/regress0/sets/sets-poly-int-real.smt2 | 17 +
test/regress/regress0/sets/sets-poly-nonint.smt2 | 11 +
test/regress/regress0/sets/sets-tuple-poly.cvc | 17 +
test/regress/regress0/sets/sharing-simp.smt2 | 15 +
test/regress/regress0/sets/univset-simp.smt2 | 2 +
test/regress/regress0/strings/Makefile.am | 4 +-
test/regress/regress0/strings/Makefile.in | 19 +-
test/regress/regress0/strings/bug799-min.smt2 | 18 +
test/regress/regress0/strings/repl-empty-sem.smt2 | 11 +
test/regress/regress0/sygus/Makefile.in | 1 +
test/regress/regress0/tptp/Makefile.in | 1 +
test/regress/regress0/uf/Makefile.in | 1 +
test/regress/regress0/uflia/Makefile.in | 1 +
test/regress/regress0/uflra/Makefile.am | 3 +-
test/regress/regress0/uflra/Makefile.in | 14 +-
test/regress/regress0/uflra/bug800.smt2 | 168 +
test/regress/regress0/unconstrained/Makefile.in | 1 +
test/regress/regress1/Makefile.am | 2 +-
test/regress/regress1/Makefile.in | 3 +-
test/regress/regress1/aufbv/Makefile.in | 1 +
test/regress/regress1/auflia/Makefile.in | 1 +
test/regress/regress1/bug519.smt2 | 2 +-
test/regress/regress1/bv/Makefile.in | 1 +
test/regress/regress1/datatypes/Makefile.in | 1 +
test/regress/regress1/decision/Makefile.in | 1 +
test/regress/regress1/fmf/Makefile.am | 3 +-
test/regress/regress1/fmf/Makefile.in | 11 +-
.../regress1/fmf/nunchaku2309663.nun.min.smt2 | 79 +
test/regress/regress1/lemmas/Makefile.in | 1 +
.../regress1/{sygus => quantifiers}/Makefile.am | 2 +-
.../regress1/{decision => quantifiers}/Makefile.in | 15 +-
test/regress/regress1/quantifiers/bug802.smt2 | 12 +
test/regress/regress1/rewriterules/Makefile.in | 1 +
test/regress/regress1/sep/Makefile.in | 1 +
test/regress/regress1/sets/Makefile.in | 1 +
test/regress/regress1/strings/Makefile.am | 4 +-
test/regress/regress1/strings/Makefile.in | 19 +-
test/regress/regress1/strings/cmu-prereg-fmf.smt2 | 12 +
.../regress1/strings/cmu-repl-len-nterm.smt2 | 12 +
test/regress/regress1/sygus/Makefile.am | 3 +-
test/regress/regress1/sygus/Makefile.in | 11 +-
test/regress/regress1/sygus/stopwatch-bt.sy | 230 +
test/regress/regress2/Makefile.am | 5 +-
test/regress/regress2/Makefile.in | 11 +-
test/regress/regress2/arith/Makefile.in | 1 +
test/regress/regress2/bug812.smt2 | 117 +
test/regress/regress3/Makefile.in | 1 +
test/regress/regress4/Makefile.in | 1 +
test/regress/run_regression | 2 +-
test/system/CVC4JavaTest.java | 4 +-
test/system/Makefile.in | 1 +
test/system/boilerplate.cpp | 4 +-
test/system/cvc3_george.h | 4 +-
test/system/cvc3_main.cpp | 4 +-
test/system/ouroborous.cpp | 4 +-
test/system/smt2_compliance.cpp | 4 +-
test/system/statistics.cpp | 4 +-
test/system/two_smt_engines.cpp | 4 +-
test/unit/Makefile.am | 1 -
test/unit/Makefile.in | 9 +-
test/unit/expr/expr_manager_public.cpp | 4 +-
test/unit/expr/expr_manager_public.h | 4 +-
test/unit/expr/expr_public.cpp | 4 +-
test/unit/expr/expr_public.h | 2 +-
test/unit/expr/type_cardinality_public.cpp | 4 +-
test/unit/expr/type_cardinality_public.h | 4 +-
test/unit/memory.h | 4 +-
test/unit/util/cardinality_public.cpp | 4 +-
test/unit/util/cardinality_public.h | 4 +-
1097 files changed, 67408 insertions(+), 54220 deletions(-)
rename debian/{libcvc4-3.install => libcvc4-4.install} (100%)
rename debian/{libcvc4parser3.install => libcvc4parser4.install} (100%)
delete mode 100644 debian/patches/01-ref-compare.patch
rename debian/patches/{02-timestamps.patch => 01-timestamps.patch} (100%)
rename debian/patches/{03-include-paths.patch => 02-include-paths.patch} (95%)
delete mode 100644 debian/patches/04-spelling-errors.patch
create mode 100644 debian/tests/control
create mode 100755 debian/tests/hello-world
create mode 100644 debian/watch
delete mode 100644 src/context/stacking_vector.h
create mode 100644 src/parser/line_buffer.cpp
create mode 100644 src/parser/line_buffer.h
create mode 100644 src/proof/simplify_boolean_node.cpp
copy src/{theory/arith/theory_arith_private_forward.h => proof/simplify_boolean_node.h} (54%)
create mode 100644 src/theory/arith/nonlinear_extension.cpp
create mode 100644 src/theory/arith/nonlinear_extension.h
copy src/theory/{arith/theory_arith_private_forward.h => assertion.cpp} (56%)
create mode 100644 src/theory/assertion.h
create mode 100644 src/theory/care_graph.h
create mode 100644 src/util/safe_print.cpp
create mode 100644 src/util/safe_print.h
create mode 100644 test/regress/regress0/arith/mod-simp.smt2
create mode 100644 test/regress/regress0/bug639.smt2
create mode 100644 test/regress/regress0/bug681.smt2
create mode 100644 test/regress/regress0/bv/bug733.smt2
create mode 100644 test/regress/regress0/bv/bug787.smt2
create mode 100644 test/regress/regress0/bv/bv2nat-simp-range-sat.smt2
create mode 100644 test/regress/regress0/datatypes/dt-2.6.smt2
create mode 100644 test/regress/regress0/datatypes/dt-color-2.6.smt2
create mode 100644 test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2
create mode 100644 test/regress/regress0/datatypes/dt-param-2.6.smt2
create mode 100644 test/regress/regress0/datatypes/dt-sel-2.6.smt2
create mode 100644 test/regress/regress0/datatypes/jsat-2.6.smt2
create mode 100644 test/regress/regress0/datatypes/tuple-no-clash.cvc
create mode 100644 test/regress/regress0/declare-fun-is-match.smt2
create mode 100644 test/regress/regress0/fmf/alg202+1.smt2
create mode 100644 test/regress/regress0/fmf/bug-041417-set-options.cvc
create mode 100644 test/regress/regress0/fmf/constr-ground-to.smt2
create mode 100644 test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2
create mode 100644 test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2
create mode 100644 test/regress/regress0/fmf/quant_real_univ.cvc
create mode 100644 test/regress/regress0/nl/Makefile.am
copy test/regress/regress0/{arith => nl}/Makefile.in (91%)
create mode 100644 test/regress/regress0/nl/all-logic.smt2
create mode 100644 test/regress/regress0/nl/bug698.smt2
create mode 100644 test/regress/regress0/nl/coeff-sat.smt2
create mode 100644 test/regress/regress0/nl/coeff-unsat-base.smt2
create mode 100644 test/regress/regress0/nl/coeff-unsat.smt2
create mode 100644 test/regress/regress0/nl/combine.smt2
create mode 100644 test/regress/regress0/nl/disj-eval.smt2
create mode 100644 test/regress/regress0/nl/dist-big.smt2
create mode 100644 test/regress/regress0/nl/div-mod-partial.smt2
create mode 100644 test/regress/regress0/nl/magnitude-wrong-1020-m.smt2
create mode 100644 test/regress/regress0/nl/metitarski-1025.smt2
create mode 100644 test/regress/regress0/nl/metitarski-3-4.smt2
create mode 100644 test/regress/regress0/nl/metitarski_3_4_2e.smt2
create mode 100644 test/regress/regress0/nl/mult-po.smt2
create mode 100644 test/regress/regress0/nl/nia-wrong-tl.smt2
create mode 100644 test/regress/regress0/nl/nl-help-unsat-quant.smt2
create mode 100644 test/regress/regress0/nl/nl-unk-quant.smt2
create mode 100644 test/regress/regress0/nl/ones.smt2
create mode 100644 test/regress/regress0/nl/poly-1025.smt2
create mode 100644 test/regress/regress0/nl/quant-nl.smt2
create mode 100644 test/regress/regress0/nl/real-div-ufnra.smt2
create mode 100644 test/regress/regress0/nl/red-exp.smt2
create mode 100644 test/regress/regress0/nl/rewriting-sums.smt2
create mode 100644 test/regress/regress0/nl/simple-mono-unsat.smt2
create mode 100644 test/regress/regress0/nl/simple-mono.smt2
create mode 100644 test/regress/regress0/nl/subs0-unsat-confirm.smt2
create mode 100644 test/regress/regress0/nl/very-easy-sat.smt2
create mode 100644 test/regress/regress0/nl/very-simple-unsat.smt2
create mode 100644 test/regress/regress0/nl/zero-subset.smt2
create mode 100644 test/regress/regress0/push-pop/bug821.smt2
create mode 100644 test/regress/regress0/push-pop/simple_unsat_cores.smt2
create mode 100644 test/regress/regress0/quantifiers/bug822.smt2
create mode 100644 test/regress/regress0/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
create mode 100644 test/regress/regress0/quantifiers/psyco-001-bv.smt2
create mode 100644 test/regress/regress0/quantifiers/qbv-simp.smt2
create mode 100644 test/regress/regress0/rels/atom_univ2.cvc
create mode 100644 test/regress/regress0/rels/card_transpose.cvc
create mode 100644 test/regress/regress0/rels/iden_0.cvc
create mode 100644 test/regress/regress0/rels/iden_1.cvc
create mode 100644 test/regress/regress0/rels/iden_1_1.cvc
create mode 100644 test/regress/regress0/rels/joinImg_0.cvc
create mode 100644 test/regress/regress0/rels/joinImg_0_1.cvc
create mode 100644 test/regress/regress0/rels/joinImg_0_2.cvc
create mode 100644 test/regress/regress0/rels/joinImg_1.cvc
create mode 100644 test/regress/regress0/rels/joinImg_1_1.cvc
create mode 100644 test/regress/regress0/rels/joinImg_2.cvc
create mode 100644 test/regress/regress0/rels/joinImg_2_1.cvc
create mode 100644 test/regress/regress0/rels/rel_tc_8.cvc
create mode 100644 test/regress/regress0/rels/rels-sharing-simp.cvc
create mode 100644 test/regress/regress0/sep/nil-no-elim.smt2
create mode 100644 test/regress/regress0/sets/complement3.cvc
create mode 100644 test/regress/regress0/sets/int-real-univ-unsat.smt2
create mode 100644 test/regress/regress0/sets/int-real-univ.smt2
create mode 100644 test/regress/regress0/sets/nonvar-univ.smt2
create mode 100644 test/regress/regress0/sets/pre-proc-univ.smt2
create mode 100644 test/regress/regress0/sets/sets-poly-int-real.smt2
create mode 100644 test/regress/regress0/sets/sets-poly-nonint.smt2
create mode 100644 test/regress/regress0/sets/sets-tuple-poly.cvc
create mode 100644 test/regress/regress0/sets/sharing-simp.smt2
create mode 100644 test/regress/regress0/strings/bug799-min.smt2
create mode 100644 test/regress/regress0/strings/repl-empty-sem.smt2
create mode 100644 test/regress/regress0/uflra/bug800.smt2
create mode 100644 test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2
copy test/regress/regress1/{sygus => quantifiers}/Makefile.am (98%)
copy test/regress/regress1/{decision => quantifiers}/Makefile.in (99%)
create mode 100644 test/regress/regress1/quantifiers/bug802.smt2
create mode 100644 test/regress/regress1/strings/cmu-prereg-fmf.smt2
create mode 100644 test/regress/regress1/strings/cmu-repl-len-nterm.smt2
create mode 100644 test/regress/regress1/sygus/stopwatch-bt.sy
create mode 100644 test/regress/regress2/bug812.smt2
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/debian-science/packages/cvc4.git
More information about the debian-science-commits
mailing list