summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quantifiers_rewriter.cpp
AgeCommit message (Collapse)Author
2019-03-26Update copyright headers.Aina Niemetz
2018-09-24Fix quantifiers selector over store rewrite (#2510)Andrew Reynolds
Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in. After the change, we are +61-7 on SMT LIB: https://www.starexec.org/starexec/secure/details/job.jsp?id=30581
2018-09-06Refactor and document quantifiers variable elimination and conditional ↵Andrew Reynolds
splitting (#2424)
2018-09-05 Eliminate select over store in quantifier bodies (#2433)Andrew Reynolds
2018-08-17Remove miscellaneous unused code (#2333)Andrew Reynolds
2018-08-16Move node algorithms to separate file (#2311)Andres Noetzli
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-01Fix quantified bv variable elimination (#2039)Andrew Reynolds
2018-04-09Fix hasSubterm calls for higher-order (#1760)Andrew Reynolds
2018-04-08Add quantifier name attribute. (#1756)Andrew Reynolds
2018-02-27Minor fixes for rec-fun (#1616)Andrew Reynolds
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-01-12Improvements for CBQI BV (#1504)Andrew Reynolds
2018-01-08Improvements to quant+BV/Bool variable elimination (#1495)Andrew Reynolds
2017-11-16(Refactor) Arithmetic monomial sum (#1381)Andrew Reynolds
* Add arithmetic monomial sum utility. * Clang format * Fix * Address review. * Fix missed comment. * Format * Fix
2017-11-09Higher-order prep (#1338)Andrew Reynolds
* Minor preparation for final higher-order merge. * Format
2017-11-01(Refactor) Split term util (#1303)Andrew Reynolds
* Fix some documentation. * Move model basis out of term db. * Moving * Finished moving. * Document Skolemize and term enumeration. * Minor * Model basis to first order model. * Change function name. * Minor * Clang format. * Minor * Format * Minor * Format * Address review.
2017-10-09Split term database (#1206)Andrew Reynolds
* Move equality query to own file, move equality inference to quantifiers engine. * Move quantifiers attributes out of TermDb and into QuantAttribute. * Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header. * Split term database into term util. * Partial fix for #1205 that eliminates need for dependency in node.cpp. * Add more references to github issues.
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
* Refactor conjecture class in ce guided instantiation, move to own file. In preparation for sygus streaming mode. * Infrastructure for streaming guards, more cleanup. * Do explicit exclusion to move to next solution for sygus streaming option, now functional. More cleanup. * More cleanup, add comments. * Update comments * Optimizations for invariant synthesis. Fix corner case for single invocation inference, more encapsulation in single inv utility. Minor fix for variable elimination in quantifiers rewriter. * Fix makefile. * Cleanup. * Remove unused includes. * Minor
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵ajreynol
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
2017-07-07Update copyright headers.Mathias Preiner
2017-06-01Minor optimizations related to cbqi.ajreynol
2017-04-28Do not eliminate non-standard arithmetic operators in recursive function ↵ajreynol
definitions, add regression.
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ajreynol
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2016-12-02Bug fixes and refactoring of parametric datatypes, add some regressions.ajreynol
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-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
Conflicts: src/options/quantifiers_options
2016-09-25Disambiguating a vector insert warning coming from coverity scan.Tim King
2016-09-20More refactoring of cbqi. Add a few regressions. Add option for qcf.ajreynol
2016-09-12Refactor prenex modes.ajreynol
2016-09-03Miniscope top level conjunctions for prenex normal form, allow one level ↵ajreynol
miniscoping in prenex normal form.
2016-09-03Option for prenex normal formajreynol
2016-08-25Minor cleanup preprocessing, add ppNotifyAssertions.ajreynol
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-07-28Fix bug 749.ajreynol
2016-07-19Add infrastructure for tracking instantiation lemmas (for proofs, and ↵ajreynol
minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.
2016-07-05Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ↵ajreynol
not drop patterns from merged prenex (fixes bug 743).
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-06-03Reduce number of passes in quantifiers rewriter.ajreynol
2016-05-24Improvements to symmetry breaking in sygus search. Minor fix for getting ↵ajreynol
instantiations of non-registered quantifiers in sygus.
2016-05-20Improvements to theory combination + strings: do not return trivial care ↵ajreynol
graph, split on length terms for disequal strings. Term indexing for TheoryDatatypes::computeCareGraph. Minor fix in quantifiers rewriter for entailed conditions, strings cardinality.
2016-05-06Minor clean up, fixes related to sygus.ajreynol
2016-05-05Compute term indices lazily in TermDb. Optimization for qcf to recognize ↵ajreynol
irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
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-07Refactor trigger selection, revisions to --relational-trigger. Properly ↵ajreynol
process non-standard user-provided triggers. Avoid entailed instantiations based on equality earlier. Refactor core addInstantiation method, add notification mechanism. Add optional argument to entailment checks. Fix bug for duplicate triggers.
2016-04-04New options for trigger selection, add option --strict-triggers. Do not ↵ajreynol
infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted.
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-30Updates to E-matching to avoid entailed instantiations earlier. Minor ↵ajreynol
updates to datatypes lemmas, other minor changes.
2016-03-18Limit duplicate propagating instances to avoid exponential behavior in ↵ajreynol
QuantConflictFind.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback