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

author	ajreynol <andrew.j.reynolds@gmail.com>
	Thu, 2 Mar 2017 20:45:21 +0000 (14:45 -0600)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Thu, 2 Mar 2017 20:45:21 +0000 (14:45 -0600)
commit	1f4b954a2cc7667a56a3007fa75c125fba93ed23
tree	ea8734e89aa5fba170781c7148d3fd886c597d4e	tree
parent	21b0cedd7dadd96e5d256885e3b65a926a7e4a81	commit \| diff

Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.

130 files changed:

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
src/compat/cvc3_compat.cpp		diff \| blob \| history
src/decision/justification_heuristic.cpp		diff \| blob \| history
src/expr/expr_template.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/options/boolean_term_conversion_mode.cpp		diff \| blob \| history
src/options/boolean_term_conversion_mode.h		diff \| blob \| history
src/options/booleans_options		diff \| blob \| history
src/options/expr_options		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/options/options_handler.h		diff \| blob \| history
src/parser/cvc/Cvc.g		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.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/proof/arith_proof.cpp		diff \| blob \| history
src/proof/array_proof.cpp		diff \| blob \| history
src/proof/bitvector_proof.cpp		diff \| blob \| history
src/proof/cnf_proof.cpp		diff \| blob \| history
src/proof/proof_utils.cpp		diff \| blob \| history
src/proof/proof_utils.h		diff \| blob \| history
src/proof/theory_proof.cpp		diff \| blob \| history
src/proof/uf_proof.cpp		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/smt/boolean_terms.cpp		diff \| blob \| history
src/smt/boolean_terms.h		diff \| blob \| history
src/smt/ite_removal.cpp		diff \| blob \| history
src/smt/ite_removal.h		diff \| blob \| history
src/smt/model_postprocessor.cpp		diff \| blob \| history
src/smt/model_postprocessor.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/arrays/theory_arrays_rewriter.h		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/kinds		diff \| blob \| history
src/theory/booleans/theory_bool.cpp		diff \| blob \| history
src/theory/booleans/theory_bool.h		diff \| blob \| history
src/theory/booleans/theory_bool_rewriter.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.h		diff \| blob \| history
src/theory/bv/aig_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast_utils.h		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/bv_to_bool.cpp		diff \| blob \| history
src/theory/bv/eager_bitblaster.cpp		diff \| blob \| history
src/theory/bv/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.h		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.h		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/ite_utilities.cpp		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.cpp		diff \| blob \| history
src/theory/quantifiers/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_instantiation.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_process.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_propagator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/macros.cpp		diff \| blob \| history
src/theory/quantifiers/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_equality_engine.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers/trigger.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep_rewriter.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rels.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
src/theory/sort_inference.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/kinds		diff \| blob \| history
src/theory/uf/symmetry_breaker.cpp		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
src/theory/uf/theory_uf_rewriter.h		diff \| blob \| history
src/theory/uf/theory_uf_strong_solver.cpp		diff \| blob \| history
src/theory/unconstrained_simplifier.cpp		diff \| blob \| history
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/arrays/Makefile.am		diff \| blob \| history
test/regress/regress0/arrays/bool-array.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bt-test-00.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bt-test-01.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug217.smt2		diff \| blob \| history
test/regress/regress0/datatypes/Makefile.am		diff \| blob \| history
test/regress/regress0/datatypes/bug597-rbt.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/bug604.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/example-dailler-min.smt2	[new file with mode: 0644]	blob
test/regress/regress0/fmf/Makefile.am		diff \| blob \| history
test/regress/regress0/fmf/bug651.smt2	[new file with mode: 0644]	blob
test/regress/regress0/fmf/bug652.smt2	[new file with mode: 0644]	blob
test/regress/regress0/push-pop/Makefile.am		diff \| blob \| history
test/regress/regress0/push-pop/bug691.smt2	[new file with mode: 0644]	blob
test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2		diff \| blob \| history
test/regress/regress0/uf/Makefile.am		diff \| blob \| history
test/regress/regress0/uf/bool-pred-nested.smt2	[new file with mode: 0644]	blob
test/unit/expr/node_black.h		diff \| blob \| history
test/unit/prop/cnf_stream_white.h		diff \| blob \| history
test/unit/util/boolean_simplification_black.h		diff \| blob \| history

RSS Atom