cvc5.git
2012-08-20 Morgan Detersfixes for java bindings
2012-08-19 Clark Barrett1. Fix for inst_match.cpp to allow compilation on fedora
2012-08-16 Morgan DetersThe SmtEngine now ensures that setLogicInternal() is...
2012-08-16 Kshitij Bansalbug 374 (was found through fuzzing 2012-07-18)
2012-08-16 Morgan DetersReplace propagateAsDecision() with Theory::getNextDecis...
2012-08-16 Morgan DetersArrayStoreAll should (for now) only allow constant...
2012-08-16 Morgan Detersfix exceptions and mkConst() in java binding
2012-08-16 Morgan Deterssome fixes for language bindings
2012-08-14 Morgan DetersFixes to integer wrapper classes:
2012-08-14 Tim KingImplements TheoryArith::collectModelInfo(). The curren...
2012-08-14 Tim KingAdds substituteDelta() to DeltaRational which given...
2012-08-14 Tim KingSwitched TheoryModel assertEqualityEngine to use const...
2012-08-14 Tim KingSwitched a number of EqClassIterator operations to...
2012-08-13 Morgan Detersfix integer parsing error.. thanks dejan for the report...
2012-08-13 Morgan DetersMake a few functions in TheoryEngine (like theoryOf...
2012-08-13 Morgan DetersMinor cleanup. No performance difference expected.
2012-08-09 Morgan Detersminor isConst()-related fixes to printing; also add...
2012-08-08 Morgan DetersFix --no-checking option.
2012-08-08 Morgan DetersPublic interface review items:
2012-08-07 Dejan Jovanovićsmall fixes
2012-08-07 Morgan Deterssome fixes to command and declaration tab-completion...
2012-08-07 Morgan DetersSome items from the CVC4 public interface review:
2012-08-07 Morgan DetersFix SmtEngine::setInfo() handling for certain keys...
2012-08-06 Morgan DetersSupport setting :regular-output-channel and :diagnostic...
2012-08-06 Dejan Jovanovićremoving the sat solver inmterface from being public
2012-08-06 Morgan DetersCleanup of some command stuff, fixes broken Java build.
2012-08-06 Dejan Jovanovićfix constant printing for datatypes
2012-08-05 Morgan DetersDisable failing datatypes regression, pending solution...
2012-08-04 Morgan DetersisConst() rule for datatypes
2012-08-03 Morgan Detersthe array-store "construle" for isConst
2012-08-03 Morgan DetersComparisons for LogicInfos, and associated tests
2012-08-03 Morgan DetersArrayStoreAll infrastructure
2012-08-03 Morgan Detersfix uses of getMetaKind() from outside the expr package...
2012-08-03 Morgan Detersfix for proofs-enabled builds
2012-08-03 Morgan Detersbetter parser makefile fix
2012-08-02 Morgan Detersfixes to paths in parser makefiles; if you've noticed...
2012-08-02 Morgan Detersarray-store-all class
2012-08-01 Morgan Detersadd isFinished() to type enumerators (so we don't rely...
2012-08-01 Morgan Detersa couple fixes to SmtEngine::setOption(). thanks Andy...
2012-08-01 Morgan Detersfixes to some *clean targets
2012-08-01 Morgan Detersfix for the SmtEngine::beforeSearch() option predicate
2012-08-01 Morgan Deterssome fixes for Mac OS
2012-07-31 Morgan Detersfixes for portfolio
2012-07-31 Morgan DetersMoving some instantiation-related stuff from src/theory...
2012-07-31 Morgan Detersfix some file documentation
2012-07-31 Morgan DetersOptions merge. This commit:
2012-07-27 Morgan DetersMinor cleanup after today's commits:
2012-07-27 Andrew Reynoldsremoving unecessary files
2012-07-27 Andrew Reynoldsmerging fmf-devel branch, includes refactored datatype...
2012-07-27 François BobotMerge quantifiers2-trunk:
2012-07-26 Morgan DetersDatatype enumerator work. This version is not a "fair...
2012-07-18 Morgan Detersmore compliance fixes for SMT-LIBv2
2012-07-18 Morgan Detersa few fixes for java system test
2012-07-18 Morgan Deterssmall change to model-generation function, after discus...
2012-07-18 Morgan Detersremoving an obsolete assertion in model-generation...
2012-07-18 Morgan Detersremoving output operator for SExprTypes, which is never...
2012-07-17 Morgan DetersSMT-LIBv2 compliance updates:
2012-07-17 Andrew Reynoldsminor fix to prevent getValue from returning null
2012-07-17 Morgan Detersfix for --produce-models with CVC4 presentation language
2012-07-17 Morgan Detersfix an obvious oversight: "distinct" wasn't part of...
2012-07-16 Morgan Detersnow passes "make distcheck", which does important check...
2012-07-16 Morgan Detersfix compiler warning in unit test
2012-07-16 Morgan Detersstronger two_smt_engines test
2012-07-16 Morgan Detersfix inadvertent change to system test
2012-07-16 Morgan DetersSupport for having two SmtEngines with the same ExprMan...
2012-07-16 Morgan Detersfound a bug in the initialization order of UF, Equality...
2012-07-16 Morgan Detersreverse the order of link arguments to -lcln -lgmp...
2012-07-14 Morgan DetersType enumerator infrastructure and uninterpreted consta...
2012-07-14 Morgan DetersApplying Dejan's patch for bug #369, which resolves...
2012-07-14 Morgan Detersfixing make dist
2012-07-14 Morgan Detersfix a warning in unit test compilation
2012-07-14 Morgan Deterssvn ignore
2012-07-14 Dejan Jovanovićan example that uses bitvectors to simulate sha1 comput...
2012-07-12 Andrew Reynoldsremoving readme from fmf-devel
2012-07-12 Andrew Reynoldsmerged fmf-devel branch, includes support for SMT2...
2012-07-10 Morgan Deterssvn ingore
2012-07-10 Dejan Jovanović* fixing the simple_vc_cxx.cpp compile issue (no more...
2012-07-10 Dejan Jovanovićgoing back to 1. being a non decimal
2012-07-10 Dejan Jovanovićsmall changes:
2012-07-09 Morgan Detersminor fix-ups
2012-07-09 Morgan Detersfix portfolio build
2012-07-09 Morgan Detersfix eXecutable bit on a script
2012-07-08 Morgan Detersminor SMT-LIBv2 compliance issues
2012-07-08 Morgan Detersremove a debugging line from configure script that...
2012-07-08 Morgan Detersanother signed-ness warning fix for newer GCC
2012-07-08 Morgan DetersMinor changes to avoid some warnings on GCC 4.7.1 ...
2012-07-08 Morgan DetersBugs resolved by this commit: #314, #322, #359, #364...
2012-07-07 Morgan DetersVarious fixes to documentation---typos, some incomplete...
2012-07-06 Tim KingAdding std namespace to a couple of make_pair instances.
2012-07-06 Tim KingAdded include unistd to main/util.cpp
2012-07-06 Tim KingAdded virtual destructor to PpRewrite.
2012-07-01 Morgan DetersSome changes to configure.ac:
2012-06-28 Morgan Deterssvn:ignore
2012-06-28 Clark BarrettFixed bug in bv rewriter that caused wrong answer in...
2012-06-28 Morgan Detersfix a link error on church, due to Antlr #defining...
2012-06-27 Tim KingFixing a bug in proof production for the DioSolver.
2012-06-27 Tim KingThis adds TheoryArith::safeToReset(). This fixes bug...
2012-06-27 Tim KingAdding access to simplex's ArithPriorityQueue to Theory...
2012-06-27 Tim KingImproved debugging output.
2012-06-27 Tim KingImproved debugging output.
next