projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4279450) | patch
Merge from quantifiers2-trunkmerge branch.
authorMorgan Deters <mdeters@gmail.com>
Mon, 11 Jun 2012 16:28:23 +0000 (16:28 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 11 Jun 2012 16:28:23 +0000 (16:28 +0000)
commit3378e253fcdb34c753407bb16d08929da06b3aaa
treedb7c7118dd0d1594175b56866f845b42426ae0a7tree
parent42794501e81c44dce5c2f7687af288af030ef63ecommit | diff
Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.
207 files changed:
.gitignore diff | blob | history
src/bindings/compat/java/src/cvc3/Embedded.java diff | blob | history
src/bindings/compat/java/src/cvc3/Expr_impl.cpp diff | blob | history
src/context/cdhashmap.h diff | blob | history
src/expr/kind_template.h diff | blob | history
src/expr/mkexpr diff | blob | history
src/expr/mkkind diff | blob | history
src/expr/mkmetakind diff | blob | history
src/expr/node.h diff | blob | history
src/expr/node_manager.h diff | blob | history
src/parser/cvc/Cvc.g diff | blob | history
src/parser/smt/Smt.g diff | blob | history
src/parser/smt/smt.cpp diff | blob | history
src/parser/smt/smt.h diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp 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.cpp diff | blob | history
src/prop/minisat/minisat.h diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/prop/prop_engine.h diff | blob | history
src/prop/sat_solver.h diff | blob | history
src/theory/Makefile.am diff | blob | history
src/theory/arith/Makefile.am diff | blob | history
src/theory/arith/congruence_manager.h diff | blob | history
src/theory/arith/kinds diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
src/theory/arith/theory_arith_instantiator.cpp [new file with mode: 0644] blob
src/theory/arith/theory_arith_instantiator.h [new file with mode: 0644] blob
src/theory/arrays/Makefile.am diff | blob | history
src/theory/arrays/kinds 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_instantiator.cpp [new file with mode: 0644] blob
src/theory/arrays/theory_arrays_instantiator.h [new file with mode: 0644] blob
src/theory/booleans/theory_bool.h diff | blob | history
src/theory/builtin/theory_builtin.h diff | blob | history
src/theory/bv/bv_subtheory_eq.h diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history
src/theory/bv/theory_bv.h diff | blob | history
src/theory/datatypes/Makefile.am diff | blob | history
src/theory/datatypes/kinds diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/datatypes/theory_datatypes_instantiator.cpp [new file with mode: 0644] blob
src/theory/datatypes/theory_datatypes_instantiator.h [new file with mode: 0644] blob
src/theory/example/theory_uf_tim.cpp diff | blob | history
src/theory/example/theory_uf_tim.h diff | blob | history
src/theory/inst_match.cpp [new file with mode: 0644] blob
src/theory/inst_match.h [new file with mode: 0644] blob
src/theory/inst_match_impl.h [new file with mode: 0644] blob
src/theory/instantiator_default.cpp [new file with mode: 0644] blob
src/theory/instantiator_default.h [new file with mode: 0644] blob
src/theory/instantiator_tables_template.cpp [new file with mode: 0644] blob
src/theory/mkinstantiator [new file with mode: 0755] blob
src/theory/mkrewriter diff | blob | history
src/theory/mktheorytraits diff | blob | history
src/theory/output_channel.h diff | blob | history
src/theory/quantifiers/Makefile [new file with mode: 0644] blob
src/theory/quantifiers/Makefile.am [new file with mode: 0644] blob
src/theory/quantifiers/instantiation_engine.cpp [new file with mode: 0644] blob
src/theory/quantifiers/instantiation_engine.h [new file with mode: 0644] blob
src/theory/quantifiers/kinds [new file with mode: 0644] blob
src/theory/quantifiers/model_engine.cpp [new file with mode: 0644] blob
src/theory/quantifiers/model_engine.h [new file with mode: 0644] blob
src/theory/quantifiers/quantifiers_rewriter.cpp [new file with mode: 0644] blob
src/theory/quantifiers/quantifiers_rewriter.h [new file with mode: 0644] blob
src/theory/quantifiers/theory_quantifiers.cpp [new file with mode: 0644] blob
src/theory/quantifiers/theory_quantifiers.h [new file with mode: 0644] blob
src/theory/quantifiers/theory_quantifiers_instantiator.cpp [new file with mode: 0644] blob
src/theory/quantifiers/theory_quantifiers_instantiator.h [new file with mode: 0644] blob
src/theory/quantifiers/theory_quantifiers_type_rules.h [new file with mode: 0644] blob
src/theory/quantifiers_engine.cpp [new file with mode: 0644] blob
src/theory/quantifiers_engine.h [new file with mode: 0644] blob
src/theory/rewriterules/Makefile [new file with mode: 0644] blob
src/theory/rewriterules/Makefile.am [new file with mode: 0644] blob
src/theory/rewriterules/README.WHATS-NEXT [new file with mode: 0644] blob
src/theory/rewriterules/kinds [new file with mode: 0644] blob
src/theory/rewriterules/theory_rewriterules.cpp [new file with mode: 0644] blob
src/theory/rewriterules/theory_rewriterules.h [new file with mode: 0644] blob
src/theory/rewriterules/theory_rewriterules_params.h [new file with mode: 0644] blob
src/theory/rewriterules/theory_rewriterules_preprocess.h [new file with mode: 0644] blob
src/theory/rewriterules/theory_rewriterules_rewriter.h [new file with mode: 0644] blob
src/theory/rewriterules/theory_rewriterules_rules.cpp [new file with mode: 0644] blob
src/theory/rewriterules/theory_rewriterules_rules.h [new file with mode: 0644] blob
src/theory/rewriterules/theory_rewriterules_type_rules.h [new file with mode: 0644] blob
src/theory/shared_terms_database.cpp diff | blob | history
src/theory/shared_terms_database.h diff | blob | history
src/theory/term_registration_visitor.cpp 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/theory_test_utils.h diff | blob | history
src/theory/trigger.cpp [new file with mode: 0644] blob
src/theory/trigger.h [new file with mode: 0644] blob
src/theory/uf/Makefile.am diff | blob | history
src/theory/uf/equality_engine.cpp diff | blob | history
src/theory/uf/equality_engine.h diff | blob | history
src/theory/uf/inst_strategy.cpp [new file with mode: 0644] blob
src/theory/uf/inst_strategy.h [new file with mode: 0644] blob
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_candidate_generator.cpp [new file with mode: 0644] blob
src/theory/uf/theory_uf_candidate_generator.h [new file with mode: 0644] blob
src/theory/uf/theory_uf_instantiator.cpp [new file with mode: 0644] blob
src/theory/uf/theory_uf_instantiator.h [new file with mode: 0644] blob
src/theory/uf/theory_uf_strong_solver.cpp [new file with mode: 0644] blob
src/theory/uf/theory_uf_strong_solver.h [new file with mode: 0644] blob
src/theory/uf/theory_uf_type_rules.h diff | blob | history
src/theory/valuation.cpp diff | blob | history
src/theory/valuation.h diff | blob | history
src/util/datatype.cpp diff | blob | history
src/util/datatype.h diff | blob | history
src/util/ite_removal.cpp diff | blob | history
src/util/options.cpp diff | blob | history
src/util/options.h diff | blob | history
test/Makefile.am diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/AdditiveMethods_OwnedResults.Mz.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/Arrays_Q1-noinfer.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/Makefile [new file with mode: 0644] blob
test/regress/regress0/quantifiers/Makefile.am [new file with mode: 0644] blob
test/regress/regress0/quantifiers/array-unsat-simp3.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect [new file with mode: 0644] blob
test/regress/regress0/quantifiers/bignum_quant.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/bug269.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/bug290.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/bug291.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/bug291.smt2.expect [new file with mode: 0644] blob
test/regress/regress0/quantifiers/burns13.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/burns4.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/ex1.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/ex1.smt2.expect [new file with mode: 0644] blob
test/regress/regress0/quantifiers/ex3.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/ex6.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/ex7.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/ex7.smt2.expect [new file with mode: 0644] blob
test/regress/regress0/quantifiers/gauss_init_0030.fof.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/javafe.ast.ArrayInit.35.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/javafe.ast.StmtVec.009.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/javafe.ast.WhileStmt.447.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/opisavailable-12.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/piVC_5581bd.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/ricart-agrawala6.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/set3.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/set8.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/smtlib384a03.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/smtlib46f14a.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/smtlibf957ea.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/symmetric_unsat_7.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/Makefile [new file with mode: 0644] blob
test/regress/regress0/rewriterules/Makefile.am [new file with mode: 0644] blob
test/regress/regress0/rewriterules/datatypes.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/datatypes2.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/datatypes3.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/datatypes_clark.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/datatypes_sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_010.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_010_lemma.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_020.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_020_sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_040.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_040_lemma.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_040_lemma_trigger.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_080.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_1280.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_1280_lemma_trigger.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_160.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_160_lemma.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_160_lemma_trigger.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_160_sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_2560.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_2560_sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_640.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_640_lemma.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_640_sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_inv_1280.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_inv_160.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_n.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_trick.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_trick2.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_trick3.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/length_trick3_int.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/test_guards.smt2 [new file with mode: 0644] blob
test/regress/regress0/uflia/xs-09-16-3-4-1-5.smt diff | blob | history
test/regress/regress1/xs-11-20-5-2-5-3.smt diff | blob | history
test/unit/prop/cnf_stream_black.h diff | blob | history
test/unit/theory/theory_arith_white.h diff | blob | history
test/unit/theory/theory_black.h diff | blob | history
test/unit/theory/theory_engine_white.h diff | blob | history