Improved SMT-LIBv2 language support for unsat cores.
[cvc5.git] / src /
2014-08-26 Morgan DetersImproved SMT-LIBv2 language support for unsat cores.
2014-08-26 ajreynolBug fixes for --purify-triggers, --dt-force-assignment.
2014-08-25 Morgan DetersFix Win32 builds.
2014-08-25 ajreynolNew option --purify-triggers. Refactoring of InstMatch...
2014-08-24 Kshitij Bansalremove some debugging code
2014-08-24 Kshitij Bansalimprovements to sets sharing
2014-08-24 Kshitij Bansalfix option alias (minor)
2014-08-23 Morgan DetersUnsat core printing.
2014-08-23 Morgan DetersSome fixes for dump- and get-unsat-core.
2014-08-22 Morgan DetersOne small thing forgotten in core commit.
2014-08-22 Morgan DetersJava-side interface improvements for unsat cores.
2014-08-22 Morgan DetersUnsat core infrastruture and API (SMT-LIB compliance...
2014-08-22 Morgan DetersMerge branch '1.4.x'
2014-08-22 Morgan DetersMerge branch '1.4.x'
2014-08-22 Morgan DetersFix operator-printing issue in SMT2.
2014-08-22 Morgan DetersFix SMT1 parser :extrasorts/:extrapreds.
2014-08-21 ajreynolAvoid doing work in quantifiers engine when no quantifi...
2014-08-20 ajreynolFix --inst-max-level for strategies that use arbitrary...
2014-08-20 ajreynolAdd option for inductive strengthening based on well...
2014-08-19 Morgan DetersMerge branch '1.4.x'
2014-08-19 Morgan DetersProduce error for bad indexed function names in SMT...
2014-08-19 lianahMaking getEqualityStatus more powerful for bit-vector...
2014-08-18 Morgan DetersMerge branch '1.4.x'
2014-08-18 Morgan DetersRevert a8e0ce67 and add test case (resolves bug #578).
2014-08-18 ajreynolAdd support for quantifier-specific instantiation level...
2014-08-15 Kshitij BansalUpdate smt_engine.cpp
2014-08-06 Morgan DetersFirst crack at fixing double-linking issues in build...
2014-08-05 lianahfixed bug575 for bv models
2014-08-05 lianahfixed bug575 for bv models
2014-08-05 ajreynolMinor fix : do not drop instantiation patterns when...
2014-08-04 Morgan DetersSome fixes to symmetry breaker (resolves bug 576).
2014-08-04 Morgan DetersSome fixes to symmetry breaker (resolves bug 576).
2014-08-04 Morgan DetersBetter support for resource-limiting when there aren...
2014-08-01 ajreynolMinor cleanup from previous commit. Better organizatio...
2014-07-31 ajreynolNew module for generating candidate equality conjecture...
2014-07-25 ajreynolMinor bug fix for exhaustive instantiation in model_engine.
2014-07-25 Tianyi Liangbug fix for pierre 0717
2014-07-25 Tianyi Liangfix for regexp union rewriting
2014-07-25 Tianyi Liangpatch for regular expression intersection caching
2014-07-24 Tianyi Liangmerging...
2014-07-24 Tianyi Liangadd delayed length lemmas
2014-07-21 Kshitij Bansalinitialization in model_engine
2014-07-19 ajreynolMinor fix for explanations for co-datatypes. Bug fix...
2014-07-13 Morgan DetersFix a bug in Boolean terms and arrays. Thanks to Jean...
2014-07-11 Morgan DetersSpelling.
2014-07-11 Kshitij Bansalfix for windows build
2014-07-11 Kshitij BansalMerge pull request #48 from kbansal/segfaultfix
2014-07-11 Kshitij BansalMerge pull request #49 from kbansal/cvcparser
2014-07-10 Kshitij Bansalrm warning
2014-07-10 Kshitij Bansalmembership cvc token changed to `IS_IN' to avoid confli...
2014-07-10 Kshitij BansalMerge remote-tracking branch 'origin/master' into segfa...
2014-07-10 Kshitij Bansalfriendlyparser: go back upto 2 words looking for match
2014-07-10 Kshitij Bansalreorganize friendlyparser, behavior unchanged
2014-07-09 Kshitij Bansalsets cvc parser
2014-07-09 Kshitij Bansalsets cvc printer
2014-07-04 Kshitij Bansalinitialize variables
2014-07-03 Kshitij Bansalchange lemma generation behavior
2014-07-01 Kshitij BansalUpdate portfolio_util.cpp
2014-07-01 Morgan DetersUpdate copyrights.
2014-07-01 Morgan DetersMerge pull request #44 from mdeters/prio-queue-updates
2014-07-01 Kshitij Bansalchat about thread creation
2014-07-01 Morgan DetersMerge pull request #45 from mdeters/turn-off-strings-exp
2014-06-30 Kshitij BansalMerge pull request #47 from kbansal/sets
2014-06-30 Kshitij BansalUse FS as the set-logic string for theory of sets
2014-06-29 Kshitij Bansalsets: "insert" operator
2014-06-28 Morgan DetersAutomatically make SMT options from command-line option...
2014-06-28 Morgan DetersFix bug in datatypes options specification
2014-06-27 Morgan DetersAnother fix for 32-bit (amends commit b825605).
2014-06-27 Clark BarrettFix for bug543
2014-06-26 Kshitij BansalMerge pull request #46 from mdeters/bug573
2014-06-26 Morgan DetersFix for 32-bit (esp. win32 failing build).
2014-06-26 Morgan DetersMerge tag 'smtcomp2014-resubmission'
2014-06-26 Morgan DetersPotential fix for bug 573.
2014-06-26 Morgan DetersIgnore error result when an error is squelched via...
2014-06-26 Morgan DetersRemove leftover debugging output.
2014-06-26 Morgan DetersMinor language bindings fixes.
2014-06-26 Morgan DetersAdd missing function definition.
2014-06-25 Andrew ReynoldsMerge pull request #34 from mdeters/datatypes-kinds
2014-06-25 Andrew ReynoldsMerge pull request #37 from mdeters/quants-kinds
2014-06-25 Andrew ReynoldsMerge pull request #38 from mdeters/uf-kinds
2014-06-25 Morgan DetersTurn strings-exp off by default (for the release)
2014-06-25 Kshitij Bansalfix sets eager lemmas
2014-06-25 Kshitij Bansalcosmetic
2014-06-25 Kshitij Bansalmv default care graph function inside the theory implem...
2014-06-25 Kshitij Bansalmake emptyset construction with no arguments private
2014-06-25 Kshitij Bansalrename subseteq to subset in smtlib, all kinds and...
2014-06-25 Kshitij BansalMerge pull request #43 from mdeters/threadstack
2014-06-25 Morgan DetersBinaryHeap unit test and some usability/build fixes...
2014-06-25 Tim KingFixing the previous bugfix.
2014-06-25 Tim KingMerge branch 'master' of github.com:CVC3/CVC4
2014-06-25 Tim KingFixing the previous bugfix.
2014-06-25 Morgan DetersStack-size portfolio fix. If using Boost 1.50, --threa...
2014-06-25 Morgan DetersFix some #line annotations.
2014-06-24 Morgan Detersstack-size portfolio fix. boost 1.50 now required
2014-06-24 Tim KingAlternative lazier heuristic for assertion rewriting.
2014-06-24 Tim KingAlternative lazier heuristic for assertion rewriting.
2014-06-24 Tim KingFixing a soundness bug in arithmetic and a roubustness...
2014-06-24 Tim KingFixing a soundness bug in arithmetic and a roubustness...
2014-06-24 Tianyi LiangMerge pull request #41 from mdeters/tianyi-merge
2014-06-24 Morgan DetersSquashed commit of the following:
next