| 2012-08-28 |
Morgan Deters | fix regression tests for automake 1.11 and automake... |
commit | commitdiff | tree |
| 2012-08-28 |
Morgan Deters | Improved compatibility layer, now supports quantifiers... |
commit | commitdiff | tree |
| 2012-08-28 |
Morgan Deters | fixes for Mac and automake 1.12 detection |
commit | commitdiff | tree |
| 2012-08-27 |
Morgan Deters | fix a destruction-order issue that was (1) causing... |
commit | commitdiff | tree |
| 2012-08-27 |
Morgan Deters | * Reversing commit r4258 (which disabled failing regres... |
commit | commitdiff | tree |
| 2012-08-26 |
Kshitij Bansal | minor, lying around in a wd (related to investigating... |
commit | commitdiff | tree |
| 2012-08-26 |
Kshitij Bansal | disabling failing regressions |
commit | commitdiff | tree |
| 2012-08-26 |
Clark Barrett | Array constants finished and working. Unit tests for... |
commit | commitdiff | tree |
| 2012-08-25 |
Morgan Deters | fix unit tests |
commit | commitdiff | tree |
| 2012-08-24 |
Morgan Deters | * disallow internal uses of mkVar() (you have to mkSkol... |
commit | commitdiff | tree |
| 2012-08-24 |
Morgan Deters | disallow assertions to inactive theories. |
commit | commitdiff | tree |
| 2012-08-24 |
Morgan Deters | fix TheoryEngine::collectModelInfo() to only call colle... |
commit | commitdiff | tree |
| 2012-08-24 |
Morgan Deters | fix warning in arrays rewriter |
commit | commitdiff | tree |
| 2012-08-24 |
Morgan Deters | fix get-value output in a couple ways; this fixes bug... |
commit | commitdiff | tree |
| 2012-08-23 |
Morgan Deters | attribute stuff for Clark's array constants |
commit | commitdiff | tree |
| 2012-08-23 |
Clark Barrett | Array constant coding done except for the attributes... |
commit | commitdiff | tree |
| 2012-08-22 |
Morgan Deters | Cap finite cardinalities at 2^64, as discussed in the... |
commit | commitdiff | tree |
| 2012-08-22 |
Morgan Deters | fix some build dependencies in options-building; should... |
commit | commitdiff | tree |
| 2012-08-22 |
Clark Barrett | More progress on array constants. |
commit | commitdiff | tree |
| 2012-08-21 |
Morgan Deters | add some incremental in-tree regressions |
commit | commitdiff | tree |
| 2012-08-21 |
François Bobot | rewriterules: fix a correction bug with --simplificatio... |
commit | commitdiff | tree |
| 2012-08-20 |
Morgan Deters | remove duplicate function TheoryEngine::getTheory(Theor... |
commit | commitdiff | tree |
| 2012-08-20 |
Morgan Deters | removing v1l20009.cvc, a datatypes benchmark where... |
commit | commitdiff | tree |
| 2012-08-20 |
Morgan Deters | minor cleanup |
commit | commitdiff | tree |
| 2012-08-20 |
Morgan Deters | fixes for java bindings |
commit | commitdiff | tree |
| 2012-08-19 |
Clark Barrett | 1. Fix for inst_match.cpp to allow compilation on fedora |
commit | commitdiff | tree |
| 2012-08-16 |
Morgan Deters | The SmtEngine now ensures that setLogicInternal() is... |
commit | commitdiff | tree |
| 2012-08-16 |
Kshitij Bansal | bug 374 (was found through fuzzing 2012-07-18) |
commit | commitdiff | tree |
| 2012-08-16 |
Morgan Deters | Replace propagateAsDecision() with Theory::getNextDecis... |
commit | commitdiff | tree |
| 2012-08-16 |
Morgan Deters | ArrayStoreAll should (for now) only allow constant... |
commit | commitdiff | tree |
| 2012-08-16 |
Morgan Deters | fix exceptions and mkConst() in java binding |
commit | commitdiff | tree |
| 2012-08-16 |
Morgan Deters | some fixes for language bindings |
commit | commitdiff | tree |
| 2012-08-14 |
Morgan Deters | Fixes to integer wrapper classes: |
commit | commitdiff | tree |
| 2012-08-14 |
Tim King | Implements TheoryArith::collectModelInfo(). The curren... |
commit | commitdiff | tree |
| 2012-08-14 |
Tim King | Adds substituteDelta() to DeltaRational which given... |
commit | commitdiff | tree |
| 2012-08-14 |
Tim King | Switched TheoryModel assertEqualityEngine to use const... |
commit | commitdiff | tree |
| 2012-08-14 |
Tim King | Switched a number of EqClassIterator operations to... |
commit | commitdiff | tree |
| 2012-08-13 |
Morgan Deters | fix integer parsing error.. thanks dejan for the report... |
commit | commitdiff | tree |
| 2012-08-13 |
Morgan Deters | Make a few functions in TheoryEngine (like theoryOf... |
commit | commitdiff | tree |
| 2012-08-13 |
Morgan Deters | Minor cleanup. No performance difference expected. |
commit | commitdiff | tree |
| 2012-08-09 |
Morgan Deters | minor isConst()-related fixes to printing; also add... |
commit | commitdiff | tree |
| 2012-08-08 |
Morgan Deters | Fix --no-checking option. |
commit | commitdiff | tree |
| 2012-08-08 |
Morgan Deters | Public interface review items: |
commit | commitdiff | tree |
| 2012-08-07 |
Dejan Jovanović | small fixes |
commit | commitdiff | tree |
| 2012-08-07 |
Morgan Deters | some fixes to command and declaration tab-completion... |
commit | commitdiff | tree |
| 2012-08-07 |
Morgan Deters | Some items from the CVC4 public interface review: |
commit | commitdiff | tree |
| 2012-08-07 |
Morgan Deters | Fix SmtEngine::setInfo() handling for certain keys... |
commit | commitdiff | tree |
| 2012-08-06 |
Morgan Deters | Support setting :regular-output-channel and :diagnostic... |
commit | commitdiff | tree |
| 2012-08-06 |
Dejan Jovanović | removing the sat solver inmterface from being public |
commit | commitdiff | tree |
| 2012-08-06 |
Morgan Deters | Cleanup of some command stuff, fixes broken Java build. |
commit | commitdiff | tree |
| 2012-08-06 |
Dejan Jovanović | fix constant printing for datatypes |
commit | commitdiff | tree |
| 2012-08-05 |
Morgan Deters | Disable failing datatypes regression, pending solution... |
commit | commitdiff | tree |
| 2012-08-04 |
Morgan Deters | isConst() rule for datatypes |
commit | commitdiff | tree |
| 2012-08-03 |
Morgan Deters | the array-store "construle" for isConst |
commit | commitdiff | tree |
| 2012-08-03 |
Morgan Deters | Comparisons for LogicInfos, and associated tests |
commit | commitdiff | tree |
| 2012-08-03 |
Morgan Deters | ArrayStoreAll infrastructure |
commit | commitdiff | tree |
| 2012-08-03 |
Morgan Deters | fix uses of getMetaKind() from outside the expr package... |
commit | commitdiff | tree |
| 2012-08-03 |
Morgan Deters | fix for proofs-enabled builds |
commit | commitdiff | tree |
| 2012-08-03 |
Morgan Deters | better parser makefile fix |
commit | commitdiff | tree |
| 2012-08-02 |
Morgan Deters | fixes to paths in parser makefiles; if you've noticed... |
commit | commitdiff | tree |
| 2012-08-02 |
Morgan Deters | array-store-all class |
commit | commitdiff | tree |
| 2012-08-01 |
Morgan Deters | add isFinished() to type enumerators (so we don't rely... |
commit | commitdiff | tree |
| 2012-08-01 |
Morgan Deters | a couple fixes to SmtEngine::setOption(). thanks Andy... |
commit | commitdiff | tree |
| 2012-08-01 |
Morgan Deters | fixes to some *clean targets |
commit | commitdiff | tree |
| 2012-08-01 |
Morgan Deters | fix for the SmtEngine::beforeSearch() option predicate |
commit | commitdiff | tree |
| 2012-08-01 |
Morgan Deters | some fixes for Mac OS |
commit | commitdiff | tree |
| 2012-07-31 |
Morgan Deters | fixes for portfolio |
commit | commitdiff | tree |
| 2012-07-31 |
Morgan Deters | Moving some instantiation-related stuff from src/theory... |
commit | commitdiff | tree |
| 2012-07-31 |
Morgan Deters | fix some file documentation |
commit | commitdiff | tree |
| 2012-07-31 |
Morgan Deters | Options merge. This commit: |
commit | commitdiff | tree |
| 2012-07-27 |
Morgan Deters | Minor cleanup after today's commits: |
commit | commitdiff | tree |
| 2012-07-27 |
Andrew Reynolds | removing unecessary files |
commit | commitdiff | tree |
| 2012-07-27 |
Andrew Reynolds | merging fmf-devel branch, includes refactored datatype... |
commit | commitdiff | tree |
| 2012-07-27 |
François Bobot | Merge quantifiers2-trunk: |
commit | commitdiff | tree |
| 2012-07-26 |
Morgan Deters | Datatype enumerator work. This version is not a "fair... |
commit | commitdiff | tree |
| 2012-07-18 |
Morgan Deters | more compliance fixes for SMT-LIBv2 |
commit | commitdiff | tree |
| 2012-07-18 |
Morgan Deters | a few fixes for java system test |
commit | commitdiff | tree |
| 2012-07-18 |
Morgan Deters | small change to model-generation function, after discus... |
commit | commitdiff | tree |
| 2012-07-18 |
Morgan Deters | removing an obsolete assertion in model-generation... |
commit | commitdiff | tree |
| 2012-07-18 |
Morgan Deters | removing output operator for SExprTypes, which is never... |
commit | commitdiff | tree |
| 2012-07-17 |
Morgan Deters | SMT-LIBv2 compliance updates: |
commit | commitdiff | tree |
| 2012-07-17 |
Andrew Reynolds | minor fix to prevent getValue from returning null |
commit | commitdiff | tree |
| 2012-07-17 |
Morgan Deters | fix for --produce-models with CVC4 presentation language |
commit | commitdiff | tree |
| 2012-07-17 |
Morgan Deters | fix an obvious oversight: "distinct" wasn't part of... |
commit | commitdiff | tree |
| 2012-07-16 |
Morgan Deters | now passes "make distcheck", which does important check... |
commit | commitdiff | tree |
| 2012-07-16 |
Morgan Deters | fix compiler warning in unit test |
commit | commitdiff | tree |
| 2012-07-16 |
Morgan Deters | stronger two_smt_engines test |
commit | commitdiff | tree |
| 2012-07-16 |
Morgan Deters | fix inadvertent change to system test |
commit | commitdiff | tree |
| 2012-07-16 |
Morgan Deters | Support for having two SmtEngines with the same ExprMan... |
commit | commitdiff | tree |
| 2012-07-16 |
Morgan Deters | found a bug in the initialization order of UF, Equality... |
commit | commitdiff | tree |
| 2012-07-16 |
Morgan Deters | reverse the order of link arguments to -lcln -lgmp... |
commit | commitdiff | tree |
| 2012-07-14 |
Morgan Deters | Type enumerator infrastructure and uninterpreted consta... |
commit | commitdiff | tree |
| 2012-07-14 |
Morgan Deters | Applying Dejan's patch for bug #369, which resolves... |
commit | commitdiff | tree |
| 2012-07-14 |
Morgan Deters | fixing make dist |
commit | commitdiff | tree |
| 2012-07-14 |
Morgan Deters | fix a warning in unit test compilation |
commit | commitdiff | tree |
| 2012-07-14 |
Morgan Deters | svn ignore |
commit | commitdiff | tree |
| 2012-07-14 |
Dejan Jovanović | an example that uses bitvectors to simulate sha1 comput... |
commit | commitdiff | tree |
| 2012-07-12 |
Andrew Reynolds | removing readme from fmf-devel |
commit | commitdiff | tree |
| 2012-07-12 |
Andrew Reynolds | merged fmf-devel branch, includes support for SMT2... |
commit | commitdiff | tree |
| 2012-07-10 |
Morgan Deters | svn ingore |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog