Age | Commit message (Collapse) | Author | |
---|---|---|---|
2011-10-29 | fix some doxygen warnings | Morgan Deters | |
2011-10-29 | support for proof regressions in other parts of the test tree | Morgan Deters | |
2011-10-29 | fix unit tests | Morgan Deters | |
2011-10-29 | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, ↵ | Morgan Deters | |
SmtEngine::getProof(), a few other things.. | |||
2011-10-28 | proof regressions | Morgan 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-28 | merged 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-28 | Adding a check in Polynomial::parsePolynomial to better enforce the ↵ | Tim King | |
arithmetic normal form when assertions are enabled. | |||
2011-10-25 | Initialize resource limit and millisecond limit options | Kshitij Bansal | |
2011-10-23 | Implement 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-21 | some printing and parser fixes for problems recently uncovered | Morgan Deters | |
2011-10-21 | add 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-20 | add support for QF_AUFLIA and QF_AUFLIRA logic strings in SMT inputs, for ↵ | Morgan Deters | |
testing | |||
2011-10-19 | fix configure step on Ubuntu oneiric (11.10)-- related to bug #284 | Morgan Deters | |
2011-10-19 | fix bug #264: competition / other static library builds when readline isn't ↵ | Morgan Deters | |
available | |||
2011-10-19 | Adding support for QF_UFLIA to the smt2 parser. | Tim King | |
2011-10-19 | Merging 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-17 | Sharing work | Dejan Jovanović | |
2011-10-13 | fix make dist | Morgan Deters | |
2011-10-13 | Interruption, 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-07 | Some new Datatype public functionality, as per Chris Conway's suggestions on ↵ | Morgan Deters | |
the dev mailing list. | |||
2011-10-06 | don't build language bindings unless expressly requested with ↵ | Morgan Deters | |
--enable-language-bindings | |||
2011-10-05 | Reverting a fix from earlier today that fixed a Mac OS warning but ↵ | Morgan Deters | |
completely broke Linux. :-( | |||
2011-10-05 | ensureLiteral() in CNF stream to support Andy's quantifiers work; an update ↵ | Morgan Deters | |
to model gen on booleans; and a little cleanup | |||
2011-10-05 | minor visibility fixes | Morgan Deters | |
2011-10-05 | remove some debugging code that slowed down last night's regressions | Morgan Deters | |
2011-10-04 | Disabling the variable removal hueristic by default. | Tim King | |
2011-10-04 | also add test case | Morgan Deters | |
2011-10-04 | fixes to context-dependent caching substitutions | Morgan Deters | |
2011-10-04 | add a guard for history saving, to enable building without GNU history library | Morgan Deters | |
2011-10-04 | compatibility, bindings | Morgan Deters | |
2011-10-04 | cvc3 compatibility layer; and another libantlr3c v3.4 incompatibility fix | Morgan Deters | |
2011-10-04 | compat layer cleanup | Morgan Deters | |
2011-10-04 | oops, one more fix, hopefully the last | Morgan Deters | |
2011-10-04 | Yet Another Antlr3 Mod---this time, all my fault: for configuration ↵ | Morgan Deters | |
auto-detection of libantlr3c, I chose an innocent-looking function that was present in both versions. But it's signature had changed, breaking source compatibility in both directions. Just like the other function that started the whole mess. Silly me. | |||
2011-10-04 | Oh, here's another cute compatibility fix for libantlr3c 3.4-beta4. They ↵ | Morgan Deters | |
#define true and false to their own ANTLR3_TRUE and ANTLR3_FALSE, wreaking havoc on our parsers. I'm really fed up with this package. | |||
2011-10-04 | mimicking Chris's recent contribution to QueryResult in CVC3 in the ↵ | Morgan Deters | |
compatibility layer | |||
2011-10-04 | more fixes for libantlr3c v3.4 | Morgan Deters | |
2011-10-04 | support for configure-discovery of antlr3-3.4-beta4 | Morgan Deters | |
2011-10-03 | user push/pop support in minisat and simplification; also bindings work | Morgan Deters | |
2011-10-03 | Importing Chris's recent changes to CVC3's ValidityChecker into the ↵ | Morgan Deters | |
compatibility layer | |||
2011-09-30 | fix to CNF undoTranslate(), to support incrementality | Morgan Deters | |
2011-09-30 | forgot to put some things in the distro | Morgan Deters | |
2011-09-30 | interfaces fixes and cleanups...and examples of each interface! | Morgan Deters | |
2011-09-30 | more push/pop infrastructure, some SAT stuff | Morgan Deters | |
2011-09-30 | fixes to incremental simplification, cnf routines, other stuff in ↵ | Morgan Deters | |
preparation of user push/pop in SAT solver | |||
2011-09-29 | compatibility work, documentation | Morgan Deters | |
2011-09-29 | build system fixes | Morgan Deters | |
2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵ | Morgan Deters | |
and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863 | |||
2011-09-29 | some test fixes | Morgan Deters | |