summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
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). ↵ajreynol
Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.
2016-05-27Removing check that is no longer valid.Clark Barrett
2016-05-27Merged QF_UFBV support from experimental branchClark Barrett
2016-05-27Enabled bit-blasting option for QF_UFBVClark Barrett
2016-05-26Merge branch 'master' of https://github.com/CVC4/CVC4Clark 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 ↵ajreynol
instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.
2016-05-26Updated script, fixed bug in QF_NIA conversion.Clark Barrett
2016-05-24Fixed build issue due to dummy Cryptominisat constructor.Liana Hadarean
2016-05-24Merged cryptominisat from experimental branch.Liana Hadarean
2016-05-24Improvements to symmetry breaking in sygus search. Minor fix for getting ↵ajreynol
instantiations of non-registered quantifiers in sygus.
2016-05-23Fix related to parametric sorts whose interpretation is finite due to ↵ajreynol
uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor.
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 ↵ajreynol
graph, split on length terms for disequal strings. Term indexing for TheoryDatatypes::computeCareGraph. Minor fix in quantifiers rewriter for entailed conditions, strings cardinality.
2016-05-18Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. ↵ajreynol
Minor fixes for inst max level.
2016-05-17Minor fix cbqi for constant monomials.ajreynol
2016-05-16Fix memory leak in interactive_shell.cppClark Barrett
2016-05-16Enable --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-15Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. ↵ajreynol
Enable e-matching when --strings-exp is enabled.
2016-05-12Add casc scripts. Improvements to qcf related to nested quantifiers and ↵ajreynol
variable ordering.
2016-05-10Fix for --inst-max-levelajreynol
2016-05-10Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor ↵ajreynol
optimizations to sygus and qcf.
2016-05-09Re-enabling ite simplification in incremental mode - no reason whyClark Barrett
it should be a problem.
2016-05-06Minor clean up, fixes related to sygus.ajreynol
2016-05-05Compute 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-05-05Removing a null pointer reference that was found by -fsanitize=null.Tim King
2016-05-02Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ↵ajreynol
do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
2016-04-30Reviewed Tim's Asan changes and improved SatProof comments.Liana Hadarean
2016-04-28Workaround for a problem in clangClark Barrett
2016-04-28More work on inst propagate. Optimization for qcf to check instances ↵ajreynol
eagerly. Improvements to equality query for disequalities.
2016-04-26Fixing memory leaks for garbage collection of ResChains in the sat proof ↵Tim King
implementation. As a part of tracking this down, I've modified a number of accessor functions in TSatProof to be const. An expert in this code will need to do a pass over this.
2016-04-26Fixing a memory leak of the ProofManager.Tim King
2016-04-19Fixed typoClark Barrett
2016-04-18More fixes for python interfaceClark Barrett
2016-04-15Rolling back the rewrite codeGuy
2016-04-15Fix for bug 717Clark Barrett
2016-04-15Fixes for python bindingsClark Barrett
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 ↵ajreynol
ArithCongruenceManager at standard effort (disabled by default).
2016-04-14Add missing function for regexp to expr manager.ajreynol
2016-04-13Update native language support for strings.ajreynol
2016-04-13Minor improvements for alpha equivalence and partial quantifier elimination ↵ajreynol
in incremental mode. Change defaults to addInstantiation method.
2016-04-13Handle parametric datatypes with --quant-ind. Minor updates.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback