Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-09-17 | Encapsulate relevant domain (#3293) | Andrew Reynolds | |
2019-09-16 | Remove equality inference option for quantifiers (#3282) | Andrew Reynolds | |
2019-09-12 | Encapsulate synth engine (#3271) | Andrew Reynolds | |
2019-09-11 | Refactoring finite bounds in Quantifiers Engine (#3261) | Andrew Reynolds | |
2019-09-11 | Infrastructure for instantiation rewriter (#3262) | Andrew Reynolds | |
2019-09-04 | Refactoring CEGQI interface (#3239) | Andrew Reynolds | |
2019-08-17 | Move quantifiers relevance module inside E-matching module (#3186) | Andrew Reynolds | |
2019-08-12 | Give rewrite engine pointer to conflict-based instantiation module (#3174) | Andrew Reynolds | |
2019-08-08 | Reorganize includes for quantifiers engine (#3169) | Andrew Reynolds | |
2019-08-05 | Remove forward declarations in quantifiers engine (#3156) | Andrew Reynolds | |
2019-08-01 | Move some generic utilities out of quantifiers (#3139) | Andrew Reynolds | |
2019-04-24 | Do not use __ prefix for header guards. (#2974) | Mathias Preiner | |
Fixes 2887. | |||
2019-03-26 | Update copyright headers. | Aina Niemetz | |
2018-09-18 | Move and rename sygus solver classes (#2488) | Andrew Reynolds | |
2018-09-17 | Clean remaining references to getNextDecisionRequest in quantifiers. (#2484) | Andrew Reynolds | |
2018-09-10 | Squash implementation of counterexample-guided instantiation (#2423) | Andrew Reynolds | |
2018-08-28 | Split term canonize utility to own file and document (#2398) | Andrew Reynolds | |
2018-08-24 | Clean up quantifiers engine initialization. (#2371) | Andrew Reynolds | |
2018-07-02 | Remove miscellaneous dead and unused code from quantifiers (#2121) | Andrew Reynolds | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-05-30 | Fixes for quantifiers + incremental (#2009) | Andrew Reynolds | |
2018-05-27 | Fix cegqi assertions for quantified non-linear cases. (#1999) | Andrew Reynolds | |
2018-03-23 | Remove unused code (#1700) | Andrew Reynolds | |
2018-03-06 | Simplify initialization of quantifiers engine (#1641) | Andrew Reynolds | |
2018-02-02 | Option to check solutions produced by SyGuS solver (#1553) | Haniel Barbosa | |
2017-12-06 | Remove CDChunkList (#1414) | Andres Noetzli | |
2017-11-24 | (Refactor) Instantiate utility (#1387) | Andrew Reynolds | |
2017-11-14 | Make QEffort an enum (#1366) | Andrew Reynolds | |
* Make QEffort an enum. * Format * Minor * Fix | |||
2017-11-01 | (Move-only) Split quant util (#1306) | Andrew Reynolds | |
* Initial draft of splitting quant util. * Minor * Document recursive term builder. * Rename file, minor. * Clang 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-28 | (Move only) Move enumerative instantiation strategy to its own file and ↵ | Andrew Reynolds | |
document (#1290) * Move, document, and rename enumerative instantiation. * Clang format. | |||
2017-10-28 | Document term db (#1220) | Andrew Reynolds | |
* Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206. * Minor * Minor * Change namespace style. * Address review * Fix incorrectly merged portion that led to regression failures. * New clang format, fully document relevant domain. * Clang format again. * Minor | |||
2017-10-10 | Fix memory leak in quantifiers engine (#1219) | Andres Noetzli | |
Commit 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 introduced a memory leak where d_quant_attr was not deleted when the QuantifiersEngine was destroyed. This commit fixes the issue by turning d_quant_attr into an std::unique_ptr. | |||
2017-10-09 | Split 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-29 | Simplify representation of inversion Skolems for bv cegqi (#1164) | Andrew Reynolds | |
* Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression. * Enable other regression | |||
2017-07-20 | Moving from the gnu extensions for hash maps to the c++11 hash maps | Tim King | |
* Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes. | |||
2017-07-07 | Update copyright headers. | Mathias Preiner | |
2017-06-01 | Minor optimizations related to cbqi. | ajreynol | |
2017-05-15 | Make conflict-based instantiation abort if a ground conflict is found in the ↵ | ajreynol | |
master equality engine during term indexing, fixes bug 801. | |||
2017-03-29 | Add quantifiers options related to model and master equality engine. | ajreynol | |
2017-03-27 | Making ppNotifyAssertions take a const vector. | Tim King | |
2016-12-29 | Adding a destructor to InstantiationNotify. | Tim King | |
2016-12-07 | Refactoring, generalization of bounded inference module. Simplification of ↵ | ajreynol | |
rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions. | |||
2016-11-21 | Refactoring related to track instantiation option. | ajreynol | |
2016-11-03 | Add priorities to getNextDecision. Properly handle case for finite types + ↵ | ajreynol | |
unbounded heaps in sep logic. Fix another simple memory leak in sygus. | |||
2016-10-28 | Add get instantiations utilities to API. | ajreynol | |
2016-09-29 | Address some coverity warnings, add another stat. | ajreynol | |
2016-09-29 | Minor cleanup and additions to quantifiers statistics. | ajreynol | |
2016-09-14 | Lemma cache in theory sep. Minor optimization for sets. Minor improvements ↵ | ajreynol | |
to EPR | |||
2016-09-01 | Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested ↵ | ajreynol | |
quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly. |