cvc5.git
2016-08-03 GuyFixed an issue where arrays proofs would sometimes...
2016-08-03 barrettcwMerge pull request #87 from 4tXJ7f/fix_oob_access
2016-07-30 ajreynolPrioritize inferences when processing normal forms...
2016-07-28 GuyThe "aggressive" optimizer for lemma L now returns...
2016-07-28 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-07-28 GuyBug fix involving negated lemmas
2016-07-28 ajreynolFix bug 749.
2016-07-28 GuyAdd the negative conjunction case
2016-07-28 Andres NotzliFix out-of-bounds access in ExprManager
2016-07-28 GuyProper instrumentation of the preprocessing phase
2016-07-28 Guyproper handling of ITEs
2016-07-27 GuyProper handling of IFF lemmas in the unsat core.
2016-07-27 GuyAdded an option for a more aggressive weakest implicant...
2016-07-27 GuyIf we can't find a weaker implicant, fail gracefully...
2016-07-27 guykatzzMerge pull request #86 from 4tXJ7f/fix_warnings
2016-07-27 Andres NotzliFix warnings in src/proof
2016-07-26 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-07-26 GuyBug fix:
2016-07-26 ajreynolAdd option to minimize sygus solutions based on using...
2016-07-26 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-07-26 GuyLetification of BV constants
2016-07-26 ajreynolMinor improvements to strings related to constant split...
2016-07-26 GuyAdded functionality to retrieve a lemma's "weakest...
2016-07-26 GuyBug fix
2016-07-26 GuyPropagate the usage of proof let maps into constant...
2016-07-25 GuyBug fix
2016-07-25 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-07-25 Guycleanup
2016-07-25 GuyUse letification for the aliasing declarations as well...
2016-07-25 GuyProper handling for lemmas that are conjuncts:
2016-07-22 ajreynolMinor, error handling for polymorphism + sep logic.
2016-07-21 ajreynolFixes for strings, explanations for constant split...
2016-07-20 ajreynolInfrastructure for storing and printing heap models...
2016-07-20 ajreynolPrint only instantiations that are in the unsat core...
2016-07-20 ajreynolInfer conflicts in strings based on abstracting equalit...
2016-07-20 GuyBug fix
2016-07-20 GuyAllow a caller to query whether an unsat core is availa...
2016-07-19 ajreynolAdd infrastructure for tracking instantiation lemmas...
2016-07-16 ajreynolRefactor strings extf evaluation info. Ensure strings...
2016-07-15 GuyMoved the assertion to a better spot
2016-07-15 GuyThe ProofManager now allows theory solvers to get their...
2016-07-15 ajreynolMinor simplification to normal form explanations.
2016-07-08 ajreynolMinor fix to last commit.
2016-07-08 ajreynolSimplifications for strings normal forms, fix case...
2016-07-07 ajreynolEnsure heap disjointness in sep refinements.
2016-07-07 ajreynolRefactoring of strings preprocess module. When enabled...
2016-07-06 GuyA few proof bugs fixed
2016-07-06 ajreynolMinor cleanup in strings, mostly related to negated...
2016-07-06 ajreynolAdd comment field for model, resolves hack for printing...
2016-07-05 ajreynolRefactor last call for theories, only create one model...
2016-07-05 ajreynolAdd option --trigger-active-sel. Recognize simple trigg...
2016-07-01 GuyWhen proving a lemma, ignore literals that don't belong...
2016-07-01 GuyHandle bitvector lemmas where a literal gets rewritten...
2016-06-30 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-06-30 GuySupport for the letification of chained AND and OR...
2016-06-23 Clark BarrettAdd theory/sep/kinds to EXTRA_DIST to fix distcheck...
2016-06-23 Clark BarrettFixed some warnings, fixed bug in cdhashmap that was...
2016-06-20 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-06-20 GuyAddressed a bug that occurs when proof production is...
2016-06-20 ajreynolMinor change to sep/kinds
2016-06-20 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-06-20 GuyFixed a bug where the proofManager's init() call was...
2016-06-18 ajreynolFix unit test.
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-17 ajreynolAdd syguscomp2016 scripts.
2016-06-09 Clark BarrettDummy commit.
2016-06-08 GuyMerge branch 'master' of https://github.com/CVC4/CVC4
2016-06-08 GuyLFSC letification is true by default
2016-06-08 GuySupport for printing a global let map in LFSC proofs.
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 GuyBetter infrastructure for proving constant disequality.
2016-06-03 GuyA better mechanism for handling BV terms with aliases...
2016-06-03 ajreynolRemove NodeListMap from strings, fixes memory leaks...
2016-06-03 ajreynolSimple memory fixes, minor cleanup in quantifiers.
2016-06-03 ajreynolReduce number of passes in quantifiers rewriter.
2016-06-02 GuyFixed a magical bug that only appears when compiling...
2016-06-02 GuyFix
2016-06-02 GuyMerge from proof branch
2016-06-02 GuyRevert "Merging proof branch"
2016-06-02 GuyMerging proof branch
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-31 Clark BarrettAdded Guy to authors list.
2016-05-28 Clark BarrettFix build
2016-05-28 Clark BarrettUpdated incremental run script
2016-05-28 Clark BarrettDisabling failing unit test for now
2016-05-28 Clark BarrettRemoving check that is no longer valid.
2016-05-27 Clark BarrettMerged QF_UFBV support from experimental branch
2016-05-27 Clark BarrettEnabled bit-blasting option for QF_UFBV
2016-05-27 Clark BarrettUpdated incremental script
2016-05-27 Clark BarrettFixed bug in run script
2016-05-26 Kshitij BansalAdded cryptominisat flag to QF_NIA
2016-05-26 Clark BarrettMerge branch 'master' of https://github.com/CVC4/CVC4
2016-05-26 Clark BarrettSmall change in run script
2016-05-26 lianahChanged aig_bitblaster to work with cryptominisat
2016-05-26 lianahDisabled m4ri in cryptominisat cmake command
2016-05-26 Kshitij BansalFix for aig_bitblaster.cpp
2016-05-26 ajreynolUse term indexing in TheoryUF::computeCareGraph. Do...
next