summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-11-15additional minor changes to get python binding on better footingMorgan Deters
2011-11-15fixes for python language binding, added python exampleMorgan Deters
2011-11-14public tests need to be linked against gmp/cln explicitly---looks like a ↵Morgan Deters
subtle linker change in Ubuntu 11.10 oneiric :-(
2011-11-06datatype stuff in compatibility interface implementedMorgan Deters
2011-11-05Context::ScopedPush implemented (in support of theory speculation, like ↵Morgan Deters
upcoming internal branch-&-bound for integers)
2011-11-04STRING_TYPE and CONST_STRING and associate type infrastructure implemented.Morgan Deters
2011-11-02Only print a shortlist of most-commonly-used options on option processing ↵Morgan Deters
errors; reduces clutter, increases usability
2011-11-02give an option error if the user specifies --proof in a non-proof-enabled buildMorgan Deters
2011-11-02fully implement the always-check-again-after-the-output-channel-is-used fix ↵Morgan Deters
for bug #275. will finally close #275.
2011-11-02Sometimes antlr decides to generate lexers and parsers in a different ↵Morgan Deters
directory than specified by "-o dir" ?! Fix that by specifying "-fo dir".
2011-11-02better Integer asserts when there's overflow on conversion to unsigned long ↵Morgan Deters
/ long
2011-11-01Improvements to header installation on user machines. Internally, we canMorgan Deters
still write, for example: #include "expr/node.h" but public CVC4 headers, upon installation to /usr/include/cvc4 (or wherever), have such #includes rewritten automatically to: #include <cvc4/expr/node.h>
2011-10-31fixes to assertions in GMP to match CLN behaviorMorgan Deters
2011-10-31Added assertions to the CLN implementation of Integer for getLong() and ↵Tim King
getUnsignedLong().
2011-10-31another make distclean fixMorgan Deters
2011-10-31fixes to "make distclean" and "make maintainerclean"Morgan Deters
2011-10-31fix to "make install"Morgan Deters
2011-10-29fix some doxygen warningsMorgan Deters
2011-10-29support for proof regressions in other parts of the test treeMorgan Deters
2011-10-29fix unit testsMorgan Deters
2011-10-29Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, ↵Morgan Deters
SmtEngine::getProof(), a few other things..
2011-10-28proof regressionsMorgan Deters
2011-10-28* ability to output NodeBuilders without first converting them to ↵Morgan Deters
Nodes---useful for debugging. * language-dependent Node::toString() * some minor proof-related cleanup
2011-10-28merged the proofgen3 branch into trunk:Liana Hadarean
- can now output LFSC checkable resolution proofs - added configuration option --enable-proof - added command line argument --proof To turn proofs on build with proofs enabled and run with --proof.
2011-10-28Adding a check in Polynomial::parsePolynomial to better enforce the ↵Tim King
arithmetic normal form when assertions are enabled.
2011-10-25Initialize resource limit and millisecond limit optionsKshitij Bansal
2011-10-23Implement changes from yesterday morning's meeting (10/21/2011):Morgan Deters
* OutputChannel::lemma() now returns an unsigned int. This facility isn't functional yet, but the signature is there. For now, it always returns the current user level (which is "correct" from the interface point of view, but not what we want). * Pseudobooleans disabled. This should fix some quantifier benchmarks Andy's been working with on the quantifiers2 branch. * --limit / --time-limit options renamed --rlimit and --tlimit. There may be slowdown from disabling pseudobooleans.
2011-10-21some printing and parser fixes for problems recently uncoveredMorgan Deters
2011-10-21add gcc version information to Configuration, and warn when building with ↵Morgan Deters
v4.5.1 which has a buggy optimizer (resolves bug #266)
2011-10-20add support for QF_AUFLIA and QF_AUFLIRA logic strings in SMT inputs, for ↵Morgan Deters
testing
2011-10-19fix configure step on Ubuntu oneiric (11.10)-- related to bug #284Morgan Deters
2011-10-19fix bug #264: competition / other static library builds when readline isn't ↵Morgan Deters
available
2011-10-19Adding support for QF_UFLIA to the smt2 parser.Tim King
2011-10-19Merging the branch branches/arithmetic/push-pop-support from r2247 to r2256 ↵Tim King
into trunk. Arithmetic should now be closer to being able to support push and pop.
2011-10-17Sharing workDejan Jovanović
2011-10-13fix make distMorgan Deters
2011-10-13Interruption, time-out, and deterministic time-out ("resource-out") features.Morgan Deters
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API This will need more work, but it's a start. Also implemented TheoryEngine::properPropagation(). Other minor things.
2011-10-07Some new Datatype public functionality, as per Chris Conway's suggestions on ↵Morgan Deters
the dev mailing list.
2011-10-06don't build language bindings unless expressly requested with ↵Morgan Deters
--enable-language-bindings
2011-10-05Reverting a fix from earlier today that fixed a Mac OS warning but ↵Morgan Deters
completely broke Linux. :-(
2011-10-05ensureLiteral() in CNF stream to support Andy's quantifiers work; an update ↵Morgan Deters
to model gen on booleans; and a little cleanup
2011-10-05minor visibility fixesMorgan Deters
2011-10-05remove some debugging code that slowed down last night's regressionsMorgan Deters
2011-10-04Disabling the variable removal hueristic by default.Tim King
2011-10-04also add test caseMorgan Deters
2011-10-04fixes to context-dependent caching substitutionsMorgan Deters
2011-10-04add a guard for history saving, to enable building without GNU history libraryMorgan Deters
2011-10-04compatibility, bindingsMorgan Deters
2011-10-04cvc3 compatibility layer; and another libantlr3c v3.4 incompatibility fixMorgan Deters
2011-10-04compat layer cleanupMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback