Age | Commit message (Collapse) | Author | |
---|---|---|---|
2016-10-05 | Added an option that allow empty dependencies when attempting to minimize ↵ | guykatzz | |
preprocessing holes | |||
2016-09-20 | More refactoring of cbqi. Add a few regressions. Add option for qcf. | ajreynol | |
2016-09-16 | Use matching heuristics for EPR instantiation. | ajreynol | |
2016-09-15 | Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by ↵ | ajreynol | |
default in EPR mode. | |||
2016-09-12 | Refactor prenex modes. | ajreynol | |
2016-09-12 | Remove old implementation of cbqi | ajreynol | |
2016-09-09 | Support for separation logic + EPR. Refactor preprocessing of sep.nil, only ↵ | ajreynol | |
allow sep disequal card constants when type is monotonic. Update logics on sep regressions. | |||
2016-09-03 | Option for prenex normal form | ajreynol | |
2016-09-01 | Fix boolean term issue in invariants from sygus. Minor default options ↵ | ajreynol | |
changes for cbqi. | |||
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-31 | Removing typeof from didyoumean.cpp. | Tim King | |
2016-08-26 | Basic support for EPR+CBQI. Minor cleanup. | ajreynol | |
2016-08-25 | Options for counterexample guided instantiation. | ajreynol | |
2016-08-15 | Enable bounded set membership with --fmf-bound. Map to term models for ↵ | ajreynol | |
bounded set membership. | |||
2016-08-11 | Add support for fewer preprocessing holes | Andres Notzli | |
This commit adds support for the --fewer-preprocessing-holes flag. This flag changes the preprocessing part in proofs in two ways: it (1) removes assertions that are just restating inputs and uses the inputs directly instead and it (2) changes the form of the preprocessed assertions to contain the input that they originate from. The code in this commit is mostly taken from the proofs branch in Guy's fork. | |||
2016-07-27 | Added an option for a more aggressive weakest implicant optimization | Guy | |
2016-07-26 | Add option to minimize sygus solutions based on using weakest implicants of ↵ | ajreynol | |
instantiations in unsat cores. | |||
2016-07-26 | Minor improvements to strings related to constant splitting, including a few ↵ | ajreynol | |
options (disabled by default). | |||
2016-07-20 | Print only instantiations that are in the unsat core when --proof is ↵ | ajreynol | |
enabled. Add option to minimize sygus solutions based on unsat core (disabled by default). | |||
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-07-16 | Refactor strings extf evaluation info. Ensure strings eager preprocess ↵ | ajreynol | |
eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations. | |||
2016-07-06 | Add comment field for model, resolves hack for printing sep logic models. | ajreynol | |
2016-07-05 | Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ↵ | ajreynol | |
not drop patterns from merged prenex (fixes bug 743). | |||
2016-06-23 | Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black, | Clark Barrett | |
re-enabled cdmap_black. | |||
2016-06-17 | Support for separation logic. Enable cbqi by default for pure BV. | ajreynol | |
2016-06-08 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy | |
2016-06-08 | LFSC letification is true by default | Guy | |
2016-06-08 | Support for printing a global let map in LFSC proofs. | Guy | |
Added a flag to enable/disbale this feature (enabled by default). Also, added some infrastructure for proving rewrite rules. | |||
2016-06-06 | Merge pull request #85 from CVC4/master_for_proof_merge | guykatzz | |
Merge from proof branch | |||
2016-06-03 | Remove NodeListMap from datatypes and equality inference. Add option ↵ | ajreynol | |
--dt-blast-splits. | |||
2016-06-01 | Merge from proof branch | Guy | |
2016-06-01 | Revert "Merging proof branch" | Guy | |
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8. | |||
2016-06-01 | Merging proof branch | Guy | |
2016-05-24 | Merged cryptominisat from experimental branch. | Liana Hadarean | |
2016-05-24 | Improvements to symmetry breaking in sygus search. Minor fix for getting ↵ | ajreynol | |
instantiations of non-registered quantifiers in sygus. | |||
2016-05-18 | Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. ↵ | ajreynol | |
Minor fixes for inst max level. | |||
2016-05-16 | Enable --sygus-direct-eval by default, limit to terms that do not induce ↵ | ajreynol | |
Boolean structure. Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi. | |||
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-12 | Add casc scripts. Improvements to qcf related to nested quantifiers and ↵ | ajreynol | |
variable ordering. | |||
2016-05-10 | Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor ↵ | ajreynol | |
optimizations to sygus and qcf. | |||
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-14 | Add option --snorm-infer-eq to infer equalities based on normalization in ↵ | ajreynol | |
ArithCongruenceManager at standard effort (disabled by default). | |||
2016-04-13 | Handle parametric datatypes with --quant-ind. Minor updates. | ajreynol | |
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-09 | cardinality operation for finite sets (based on my thesis / ijcar16 paper) | Kshitij Bansal | |
Some further cleanup/fixes pending This is squash of 39 commits (kbansal/card branch + cleanup): * add card operator * local reasoning * towards graph building * first implementation * close cardinality terms * model building * more * more * more * Add aggressive sets rewriting. * Recursively aggressive rewrite sets. * Fix * incomplete card2 implementation * ... * Avoid using auto in sets. * fix merge * more * ... * more * ... * Fixed for loops * Slight modification to computeRelevantTerms * more * .. * more * ... * mv empty set lemma generation to later point * more options/reordering * debug related * more trace * ... * fix merge_nodes, models * rm warnigns * fix compile errors * warning * bug fixes/cleanup * mroe fixes * cleanup * ... | |||
2016-04-09 | Minor refactoring of entailment tests and quantifiers util. Initial draft of ↵ | ajreynol | |
instantiation propagator. | |||
2016-04-04 | New 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-03 | Updating the copyright headers and scripts. | Tim King | |
2016-04-01 | Improvements to equality inference module: add missing cases for solvable ↵ | ajreynol | |
variables, do not infer equalities that are derivable by transitivity of other inferred equalities, refactor solved vars/eqc into one, option to track explanations. Handle case when equality inference in quantifiers can derive purely arithmetic ground conflicts at full effort. |