Age | Commit message (Collapse) | Author | |
---|---|---|---|
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. | |||
2016-08-26 | Basic support for EPR+CBQI. Minor cleanup. | ajreynol | |
2016-08-25 | Minor cleanup preprocessing, add ppNotifyAssertions. | ajreynol | |
2016-07-26 | Add option to minimize sygus solutions based on using weakest implicants of ↵ | ajreynol | |
instantiations in unsat cores. | |||
2016-07-19 | Add 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-05-15 | Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. ↵ | ajreynol | |
Enable e-matching when --strings-exp is enabled. | |||
2016-05-06 | Minor clean up, fixes related to sygus. | ajreynol | |
2016-05-05 | Compute 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-04-28 | More work on inst propagate. Optimization for qcf to check instances ↵ | ajreynol | |
eagerly. Improvements to equality query for disequalities. | |||
2016-04-13 | Minor improvements for alpha equivalence and partial quantifier elimination ↵ | ajreynol | |
in incremental mode. Change defaults to addInstantiation method. | |||
2016-04-12 | Optimizations for QCF to check relevant domain of variable argument ↵ | ajreynol | |
positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database. | |||
2016-04-10 | More work on instantiation propagation. Enable external filtering of ↵ | ajreynol | |
instantiations. All quantifiers strategies terminate when a conflict can be established. | |||
2016-04-09 | Minor refactoring of entailment tests and quantifiers util. Initial draft of ↵ | ajreynol | |
instantiation propagator. | |||
2016-04-07 | Refactor 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. |