cvc5.git
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.
2012-06-27 Tim KingAdding reduce() to the ArithPriorityQueue. This reduces...
2012-06-25 Tim KingAdded a warning to arithmetic for a known dio solver...
2012-06-22 François BobotTPTP: add parser for cnf and fof
2012-06-22 François Bobotparser: add some acces function and recover the origina...
2012-06-22 François Bobotfix : function AntlrInput::tokenTextSubstr
2012-06-22 François BobotParser: add the possibility to bind at level 0.
2012-06-18 Morgan Detersqf_lra strategy
2012-06-18 Clark BarrettReverting buggy rewriter code
2012-06-18 Morgan Detersanother qf_lra strategy update
2012-06-18 Clark BarrettFixed bug in rewriter
2012-06-18 Morgan Detersunnecessary ^ in regular expression; warning produced...
2012-06-18 Morgan DetersQF_LRA strategy in run script, now final (?) for smt...
2012-06-18 Morgan Detersfinal sources (?) for competition
2012-06-18 Clark BarrettFix for slow array rewrite and minor bug fix in arrays...
2012-06-18 Clark Barrettsmall bug fix and performance fix in ite simplifier
2012-06-18 Andrew Reynoldsfixed smt version 1 parser for quantifiers
2012-06-18 Kshitij Bansaltracing code to make sure decision options are being...
2012-06-18 Kshitij Bansalbugfix, enable only QF_LRA, not other arith
2012-06-18 Kshitij BansalQF_LRA, Quantifiers: enable use decision for (only...
2012-06-18 Morgan DetersFixing bug 360. The driver wasn't exiting when there...
2012-06-17 Kshitij BansalQF_AUFLIA: enable use decision for (only for) stopping...
2012-06-17 Dejan Jovanovićfixing a problem due to lemmas produced while backtracking
2012-06-17 Kshitij Bansal--decision=justification-stoponly : use decision engine...
2012-06-17 Dejan Jovanovićenabling theoryof=term for quantifiers with sharing
2012-06-17 Dejan Jovanovićfixing wrong assertion
2012-06-17 Clark BarrettRemoved assertion that can fail
2012-06-17 Dejan Jovanovićfixing makefile error that brakes build
next