summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-17Add syguscomp2016 scripts.ajreynol
2016-06-09Dummy commit.Clark Barrett
2016-06-08Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-08LFSC letification is true by defaultGuy
2016-06-08Support 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-06Merge pull request #85 from CVC4/master_for_proof_mergeguykatzz
Merge from proof branch
2016-06-03Remove NodeListMap from datatypes and equality inference. Add option ↵ajreynol
--dt-blast-splits.
2016-06-03Better infrastructure for proving constant disequality.Guy
Added support for the BV case
2016-06-03A better mechanism for handling BV terms with aliases: inject the alias at ↵Guy
the decl_bblast step, instead of having an individual "with alias" rule for each BV operation
2016-06-03Remove NodeListMap from strings, fixes memory leaks. Fix for regexp ↵ajreynol
intersection.
2016-06-03Simple memory fixes, minor cleanup in quantifiers.ajreynol
2016-06-03Reduce number of passes in quantifiers rewriter.ajreynol
2016-06-02Fixed a magical bug that only appears when compiling with clang:Guy
The assignment d_exprToVariableName[*it] = assignAlias(*it) Creates an empty value for *it in d_exprToVariableName, causing the assertion in assignAlias to fail
2016-06-02FixGuy
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-30Added Guy to authors list.Clark Barrett
2016-05-28Fix buildClark Barrett
2016-05-28Updated incremental run scriptClark Barrett
2016-05-28Disabling failing unit test for nowClark Barrett
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-26Updated incremental scriptClark Barrett
2016-05-26Fixed bug in run scriptClark Barrett
2016-05-26Added cryptominisat flag to QF_NIAKshitij Bansal
2016-05-26Merge branch 'master' of https://github.com/CVC4/CVC4Clark Barrett
2016-05-26Small change in run scriptClark Barrett
2016-05-26Changed aig_bitblaster to work with cryptominisatlianah
2016-05-26Disabled m4ri in cryptominisat cmake commandlianah
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-25Fixed unit testLiana Hadarean
2016-05-24Fixed build issue due to dummy Cryptominisat constructor.Liana Hadarean
2016-05-24Forgot to add second patch file.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-20Updated AUTHORS fileClark Barrett
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback