Add priorities to getNextDecision. Properly handle case for finite types + unbounded...
[cvc5.git] / src / theory / quantifiers /
2016-11-03 ajreynolAdd priorities to getNextDecision. Properly handle...
2016-11-02 ajreynolFix bug in separation logic for finite pto-data types...
2016-11-02 ajreynolFix a few obvious memory leaks in sygus and quantifiers...
2016-10-13 Tim KingRevert "Merge branch 'origin' of https://github.com...
2016-10-11 Paul MengMerge branch 'origin' of https://github.com/CVC4/CVC4.git
2016-10-01 Tim KingMerge pull request #93 from timothy-king/clang-format
2016-09-29 ajreynolAddress some coverity warnings, add another stat.
2016-09-29 ajreynolMinor cleanup and additions to quantifiers statistics.
2016-09-26 Tim KingAdding a destructor to QuantAntiSkolem.
2016-09-26 Tim KingAdding a destructor to TermDb.
2016-09-26 Tim KingAdding a destructor to CegqiOutputSingleInv.
2016-09-26 Tim KingDisambiguating a vector insert warning coming from...
2016-09-25 Tim KingRemoving an unused iterator.
2016-09-21 ajreynolRemove duplicate code from my last commit
2016-09-20 ajreynolRefactor, separate theory-specific counterexample-guide...
2016-09-20 ajreynolMore refactoring of cbqi. Add a few regressions. Add...
2016-09-17 guykatzzMerge branch 'master' of https://github.com/CVC4/CVC4
2016-09-17 ajreynolUse matching heuristics for EPR instantiation.
2016-09-16 ajreynolMore refactoring of cbqi, start developing new interface.
2016-09-15 ajreynolFurther refactor cbqi.
2016-09-15 ajreynolBegin refactoring of cbqi, remove a few dead options...
2016-09-15 ajreynolMake sep pto a trigger kind, track in equality engines...
2016-09-15 ajreynolRefactor setIncomplete in quantifiers.
2016-09-14 ajreynolLemma cache in theory sep. Minor optimization for sets...
2016-09-13 ajreynolMinor changes to sep logic, epr, quantifier splitting.
2016-09-12 ajreynolRefactor prenex modes.
2016-09-12 ajreynolRemove old implementation of cbqi
2016-09-03 ajreynolMiniscope top level conjunctions for prenex normal...
2016-09-03 ajreynolOption for prenex normal form
2016-09-02 Tim KingMerge pull request #91 from timothy-king/no-throw
2016-09-01 ajreynolFix boolean term issue in invariants from sygus. Minor...
2016-09-01 ajreynolCleanup quantifier elimination in smt engine.
2016-09-01 ajreynolUpdates to cbqi. New strategy --cbqi-nested-qe to...
2016-09-01 Tim KingRemoving the forward declaration of QuantInfo from...
2016-08-26 ajreynolBasic support for EPR+CBQI. Minor cleanup.
2016-08-25 ajreynolMinor cleanup preprocessing, add ppNotifyAssertions.
2016-08-25 ajreynolOptions for counterexample guided instantiation.
2016-08-24 PaulMengMerge remote-tracking branch 'origin/master'
2016-08-15 ajreynolEnable bounded set membership with --fmf-bound. Map...
2016-08-12 ajreynolMinor fixes to model construction to take singleton...
2016-08-03 barrettcwMerge pull request #87 from 4tXJ7f/fix_oob_access
2016-07-28 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-07-28 ajreynolFix bug 749.
2016-07-26 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-07-26 ajreynolAdd option to minimize sygus solutions based on using...
2016-07-20 ajreynolInfrastructure for storing and printing heap models...
2016-07-20 ajreynolPrint only instantiations that are in the unsat core...
2016-07-19 ajreynolAdd infrastructure for tracking instantiation lemmas...
2016-07-05 ajreynolAdd option --trigger-active-sel. Recognize simple trigg...
2016-07-05 PaulMengMerge branch 'master' of https://github.com/CVC4/CVC4.git
2016-06-20 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-06-17 ajreynolCleanup from last commit, treat sep.nil as variable...
2016-06-17 ajreynolSupport for separation logic. Enable cbqi by default...
2016-06-08 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-06-06 guykatzzMerge pull request #85 from CVC4/master_for_proof_merge
2016-06-04 ajreynolRemove NodeListMap from datatypes and equality inferenc...
2016-06-03 ajreynolSimple memory fixes, minor cleanup in quantifiers.
2016-06-03 ajreynolReduce number of passes in quantifiers rewriter.
2016-06-01 ajreynolFix to ignore a case of triggers with no free variables.
2016-06-01 ajreynolInitial infrastructure for bounded set quantification...
2016-05-26 Clark BarrettMerge branch 'master' of https://github.com/CVC4/CVC4
2016-05-26 ajreynolUse term indexing in TheoryUF::computeCareGraph. Do...
2016-05-24 ajreynolImprovements to symmetry breaking in sygus search....
2016-05-23 ajreynolFix related to parametric sorts whose interpretation...
2016-05-20 ajreynolImprovements to theory combination + strings: do not...
2016-05-18 ajreynolRefactor modes for sygus+single invocation. Add option...
2016-05-17 ajreynolMinor fix cbqi for constant monomials.
2016-05-16 ajreynolEnable --sygus-direct-eval by default, limit to terms...
2016-05-15 ajreynolWork on --sygus-direct-eval. Minor optimizations, updat...
2016-05-12 ajreynolAdd casc scripts. Improvements to qcf related to nested...
2016-05-10 ajreynolAdd smt comp 2016 scripts. Fix for --relevant-triggers...
2016-05-06 ajreynolMinor clean up, fixes related to sygus.
2016-05-05 ajreynolCompute term indices lazily in TermDb. Optimization...
2016-05-02 ajreynolClean up issues related to compiled scc in LFSC. Refact...
2016-04-28 ajreynolMore work on inst propagate. Optimization for qcf...
2016-04-20 PaulMengupdate from the master
2016-04-13 ajreynolMinor improvements for alpha equivalence and partial...
2016-04-13 ajreynolHandle parametric datatypes with --quant-ind. Minor...
2016-04-12 ajreynolBug fixes related to parametric datatypes + theory...
2016-04-12 ajreynolOptimizations for QCF to check relevant domain of varia...
2016-04-11 ajreynolMinor fixes for inst match generators. Updates to qip.
2016-04-10 ajreynolMore work on instantiation propagation. Enable external...
2016-04-09 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-04-09 ajreynolMinor refactoring of entailment tests and quantifiers...
2016-04-07 ajreynolRefactor trigger selection, revisions to --relational...
2016-04-04 ajreynolNew options for trigger selection, add option --strict...
2016-04-04 Tim KingUpdating the copyright headers and scripts.
2016-04-01 ajreynolImprovements to equality inference module: add missing...
2016-03-31 ajreynolImprovements to trigger selection, min triggers by...
2016-03-30 ajreynolUpdates to E-matching to avoid entailed instantiations...
2016-03-28 ajreynolMinor cleanup from last commit (quant util, equality...
2016-03-28 ajreynolImplement equality inference module for arithmetic...
2016-03-24 Tim KingFreeing CegConjecture::d_ceg_si. Also making d_ceg_si...
2016-03-24 Tim KingFixing a memory leak in CDInstMatchTrie::d_data.
2016-03-24 Tim KingFix for a memory leak in InstStrategyCegqi.
2016-03-24 Tim KingFixing a memory leak in QuantInfo::d_var_mg.
2016-03-23 Tim KingFixing memory leaks in Trigger and TriggerTrie.
2016-03-22 ajreynolBug fix for define functions + incremental. Minor work...
2016-03-18 ajreynolLimit duplicate propagating instances to avoid exponent...
2016-03-16 ajreynolChange internal representative selection for finite...
next