summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2016-06-20Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-20Fixed a bug where the proofManager's init() call was not getting called, resu...Guy
2016-06-18Fix unit test.ajreynol
2016-06-17Cleanup from last commit, treat sep.nil as variable kind.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-06Merge pull request #85 from CVC4/master_for_proof_mergeguykatzz
2016-06-03Remove NodeListMap from datatypes and equality inference. Add option --dt-bla...ajreynol
2016-06-03Remove NodeListMap from strings, fixes memory leaks. Fix for regexp intersect...ajreynol
2016-06-03Simple memory fixes, minor cleanup in quantifiers.ajreynol
2016-06-03Reduce number of passes in quantifiers rewriter.ajreynol
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
2016-06-01Merging proof branchGuy
2016-06-01Fix to ignore a case of triggers with no free variables.ajreynol
2016-06-01Initial infrastructure for bounded set quantification (disabled). Refactoring...ajreynol
2016-05-27Merged QF_UFBV support from experimental branchClark Barrett
2016-05-26Changed aig_bitblaster to work with cryptominisatlianah
2016-05-26Fix for aig_bitblaster.cppKshitij Bansal
2016-05-26Use term indexing in TheoryUF::computeCareGraph. Do not reject model value in...ajreynol
2016-05-24Merged cryptominisat from experimental branch.Liana Hadarean
2016-05-24Improvements to symmetry breaking in sygus search. Minor fix for getting inst...ajreynol
2016-05-23Fix related to parametric sorts whose interpretation is finite due to uninter...ajreynol
2016-05-21Minor fix for strings.ajreynol
2016-05-20Minor fix to strings, cleanup in datatypes.ajreynol
2016-05-20Improvements to theory combination + strings: do not return trivial care grap...ajreynol
2016-05-18Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. Mino...ajreynol
2016-05-17Minor fix cbqi for constant monomials.ajreynol
2016-05-16Enable --sygus-direct-eval by default, limit to terms that do not induce Bool...ajreynol
2016-05-15Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. En...ajreynol
2016-05-12Add casc scripts. Improvements to qcf related to nested quantifiers and varia...ajreynol
2016-05-10Fix for --inst-max-levelajreynol
2016-05-10Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor optimizatio...ajreynol
2016-05-09Re-enabling ite simplification in incremental mode - no reason whyClark Barrett
2016-05-06Minor clean up, fixes related to sygus.ajreynol
2016-05-05Compute term indices lazily in TermDb. Optimization for qcf to recognize irre...ajreynol
2016-05-02Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ...ajreynol
2016-04-28Workaround for a problem in clangClark Barrett
2016-04-28More work on inst propagate. Optimization for qcf to check instances eagerly...ajreynol
2016-04-15Rolling back the rewrite codeGuy
2016-04-14Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-04-14Remove some no-longer-required rewrites of array lemmasGuy
2016-04-14Add option --snorm-infer-eq to infer equalities based on normalization in Ari...ajreynol
2016-04-14Add missing function for regexp to expr manager.ajreynol
2016-04-13Minor improvements for alpha equivalence and partial quantifier elimination i...ajreynol
2016-04-13Handle parametric datatypes with --quant-ind. Minor updates.ajreynol
2016-04-12Bug fixes related to parametric datatypes + theory combination + quantifiers....ajreynol
2016-04-12Optimizations for QCF to check relevant domain of variable argument positions...ajreynol
2016-04-11Minor fixes for inst match generators. Updates to qip.googleajreynol
2016-04-10More work on instantiation propagation. Enable external filtering of instanti...ajreynol
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback