summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/candidate_generator.h
AgeCommit message (Collapse)Author
2018-03-23Minor reorganization for ematching (#1701)Andrew Reynolds
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
Removing more miscellaneous throw specifiers.
2017-07-07Update copyright headers.Mathias Preiner
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing changes made to 5f415d4585134612bc24e9a823289fee35541a01.
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
Conflicts: proofs/signatures/Makefile.am src/Makefile.am src/expr/datatype.cpp src/options/datatypes_options src/options/options_template.cpp src/options/quantifiers_options src/proof/arith_proof.cpp src/proof/arith_proof.h src/proof/array_proof.cpp src/proof/array_proof.h src/proof/bitvector_proof.cpp src/proof/bitvector_proof.h src/proof/cnf_proof.cpp src/proof/cnf_proof.h src/proof/proof_manager.cpp src/proof/proof_manager.h src/proof/sat_proof.h src/proof/sat_proof_implementation.h src/proof/skolemization_manager.h src/proof/theory_proof.cpp src/proof/theory_proof.h src/proof/uf_proof.cpp src/proof/uf_proof.h src/prop/cnf_stream.cpp src/prop/cnf_stream.h src/prop/minisat/core/Solver.cc src/prop/prop_engine.cpp src/prop/prop_engine.h src/prop/theory_proxy.cpp src/smt/smt_engine.cpp src/smt/smt_engine_check_proof.cpp src/theory/arrays/array_proof_reconstruction.cpp src/theory/arrays/theory_arrays.cpp src/theory/bv/eager_bitblaster.cpp src/theory/bv/lazy_bitblaster.cpp src/theory/datatypes/theory_datatypes.cpp src/theory/quantifiers/alpha_equivalence.cpp src/theory/quantifiers/candidate_generator.cpp src/theory/quantifiers/candidate_generator.h src/theory/quantifiers/ce_guided_single_inv.cpp src/theory/quantifiers/ceg_instantiator.cpp src/theory/quantifiers/conjecture_generator.cpp src/theory/quantifiers/equality_infer.cpp src/theory/quantifiers/equality_infer.h src/theory/quantifiers/inst_match_generator.cpp src/theory/quantifiers/inst_propagator.cpp src/theory/quantifiers/inst_propagator.h src/theory/quantifiers/inst_strategy_e_matching.cpp src/theory/quantifiers/inst_strategy_e_matching.h src/theory/quantifiers/instantiation_engine.cpp src/theory/quantifiers/model_builder.cpp src/theory/quantifiers/model_engine.cpp src/theory/quantifiers/quant_conflict_find.cpp src/theory/quantifiers/quant_conflict_find.h src/theory/quantifiers/quant_split.cpp src/theory/quantifiers/quant_util.cpp src/theory/quantifiers/quantifiers_rewriter.cpp src/theory/quantifiers/quantifiers_rewriter.h src/theory/quantifiers/term_database.cpp src/theory/quantifiers/term_database.h src/theory/quantifiers/trigger.cpp src/theory/quantifiers/trigger.h src/theory/quantifiers_engine.cpp src/theory/quantifiers_engine.h src/theory/sets/kinds src/theory/sets/theory_sets_private.cpp src/theory/sets/theory_sets_private.h src/theory/sets/theory_sets_rewriter.cpp src/theory/sets/theory_sets_type_rules.h src/theory/strings/theory_strings.cpp src/theory/strings/theory_strings.h src/theory/theory_engine.cpp src/theory/theory_engine.h src/theory/uf/equality_engine.cpp test/regress/regress0/fmf/Makefile.am test/regress/regress0/quantifiers/Makefile.am test/regress/regress0/strings/Makefile.am test/regress/regress0/sygus/Makefile.am test/regress/regress0/sygus/max2-univ.sy
2016-05-02Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ↵ajreynol
do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
2016-04-20update from the masterPaulMeng
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-31Improvements to trigger selection, min triggers by default. Optimizations ↵ajreynol
for E-matching. Minor work to equality infer.
2016-03-30Updates to E-matching to avoid entailed instantiations earlier. Minor ↵ajreynol
updates to datatypes lemmas, other minor changes.
2016-03-22Bug fix for define functions + incremental. Minor work on relational triggers.ajreynol
2015-11-10Fix infinite loop in datatype enumerator. Minor fixes and improvements to ↵ajreynol
cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2014-11-18Add local theory extensions instantiation strategy (incomplete). Refactor ↵ajreynol
how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.
2014-09-16Bug fix variable triggers with --inst-max-level : use term in EQC with ↵ajreynol
minimal instantiation level.
2014-07-01Update copyrights.Morgan Deters
2014-01-18Performance optimization for E-matching, working on using QCF module for ↵Andrew Reynolds
propagations.
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-06-24Add options for symmetry breaking in uf+ss totality axiom approach, option ↵Andrew Reynolds
for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2012-10-16first draft of new inst gen method (still with bugs), some cleanup of ↵Andrew Reynolds
quantifiers code
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-07-31Moving some instantiation-related stuff from src/theory to ↵Morgan Deters
src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat. The namespaces weren't changed, only the file locations.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback