Morgan Deters [Fri, 4 Nov 2011 16:52:06 +0000 (16:52 +0000)]
STRING_TYPE and CONST_STRING and associate type infrastructure implemented.
Morgan Deters [Wed, 2 Nov 2011 13:55:48 +0000 (13:55 +0000)]
Only print a shortlist of most-commonly-used options on option processing errors; reduces clutter, increases usability
Morgan Deters [Wed, 2 Nov 2011 13:05:11 +0000 (13:05 +0000)]
give an option error if the user specifies --proof in a non-proof-enabled build
Morgan Deters [Wed, 2 Nov 2011 01:48:41 +0000 (01:48 +0000)]
fully implement the always-check-again-after-the-output-channel-is-used fix for bug #275. will finally close #275.
Morgan Deters [Wed, 2 Nov 2011 00:40:40 +0000 (00:40 +0000)]
Sometimes antlr decides to generate lexers and parsers in a different directory than specified by "-o dir" ?! Fix that by specifying "-fo dir".
Morgan Deters [Wed, 2 Nov 2011 00:01:48 +0000 (00:01 +0000)]
better Integer asserts when there's overflow on conversion to unsigned long / long
Morgan Deters [Tue, 1 Nov 2011 17:08:55 +0000 (17:08 +0000)]
Improvements to header installation on user machines. Internally, we can
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>
Morgan Deters [Mon, 31 Oct 2011 23:56:07 +0000 (23:56 +0000)]
fixes to assertions in GMP to match CLN behavior
Tim King [Mon, 31 Oct 2011 21:43:11 +0000 (21:43 +0000)]
Added assertions to the CLN implementation of Integer for getLong() and getUnsignedLong().
Morgan Deters [Mon, 31 Oct 2011 21:25:07 +0000 (21:25 +0000)]
another make distclean fix
Morgan Deters [Mon, 31 Oct 2011 21:01:13 +0000 (21:01 +0000)]
fixes to "make distclean" and "make maintainerclean"
Morgan Deters [Mon, 31 Oct 2011 19:32:55 +0000 (19:32 +0000)]
fix to "make install"
Morgan Deters [Sat, 29 Oct 2011 19:09:06 +0000 (19:09 +0000)]
fix some doxygen warnings
Morgan Deters [Sat, 29 Oct 2011 18:22:38 +0000 (18:22 +0000)]
support for proof regressions in other parts of the test tree
Morgan Deters [Sat, 29 Oct 2011 08:11:12 +0000 (08:11 +0000)]
fix unit tests
Morgan Deters [Sat, 29 Oct 2011 05:21:49 +0000 (05:21 +0000)]
Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::getProof(), a few other things..
Morgan Deters [Fri, 28 Oct 2011 22:08:55 +0000 (22:08 +0000)]
proof regressions
Morgan Deters [Fri, 28 Oct 2011 20:30:24 +0000 (20:30 +0000)]
* ability to output NodeBuilders without first converting them to Nodes---useful for debugging.
* language-dependent Node::toString()
* some minor proof-related cleanup
Liana Hadarean [Fri, 28 Oct 2011 19:24:38 +0000 (19:24 +0000)]
merged the proofgen3 branch into trunk:
- 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.
Tim King [Fri, 28 Oct 2011 18:35:27 +0000 (18:35 +0000)]
Adding a check in Polynomial::parsePolynomial to better enforce the arithmetic normal form when assertions are enabled.
Kshitij Bansal [Tue, 25 Oct 2011 07:40:44 +0000 (07:40 +0000)]
Initialize resource limit and millisecond limit options
Morgan Deters [Sun, 23 Oct 2011 00:45:57 +0000 (00:45 +0000)]
Implement changes from yesterday morning's meeting (10/21/2011):
* 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.
Morgan Deters [Fri, 21 Oct 2011 04:44:14 +0000 (04:44 +0000)]
some printing and parser fixes for problems recently uncovered
Morgan Deters [Fri, 21 Oct 2011 04:25:19 +0000 (04:25 +0000)]
add gcc version information to Configuration, and warn when building with v4.5.1 which has a buggy optimizer (resolves bug #266)
Morgan Deters [Thu, 20 Oct 2011 17:40:26 +0000 (17:40 +0000)]
add support for QF_AUFLIA and QF_AUFLIRA logic strings in SMT inputs, for testing
Morgan Deters [Wed, 19 Oct 2011 23:36:21 +0000 (23:36 +0000)]
fix configure step on Ubuntu oneiric (11.10)-- related to bug #284
Morgan Deters [Wed, 19 Oct 2011 21:35:50 +0000 (21:35 +0000)]
fix bug #264: competition / other static library builds when readline isn't available
Tim King [Wed, 19 Oct 2011 18:50:41 +0000 (18:50 +0000)]
Adding support for QF_UFLIA to the smt2 parser.
Tim King [Wed, 19 Oct 2011 17:25:00 +0000 (17:25 +0000)]
Merging the branch branches/arithmetic/push-pop-support from r2247 to r2256 into trunk. Arithmetic should now be closer to being able to support push and pop.
Dejan Jovanović [Mon, 17 Oct 2011 03:12:17 +0000 (03:12 +0000)]
Sharing work
Morgan Deters [Thu, 13 Oct 2011 15:27:27 +0000 (15:27 +0000)]
fix make dist
Morgan Deters [Thu, 13 Oct 2011 04:14:38 +0000 (04:14 +0000)]
Interruption, time-out, and deterministic time-out ("resource-out") features.
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.
Morgan Deters [Fri, 7 Oct 2011 14:57:38 +0000 (14:57 +0000)]
Some new Datatype public functionality, as per Chris Conway's suggestions on the dev mailing list.
Morgan Deters [Thu, 6 Oct 2011 00:09:25 +0000 (00:09 +0000)]
don't build language bindings unless expressly requested with --enable-language-bindings
Morgan Deters [Wed, 5 Oct 2011 23:58:57 +0000 (23:58 +0000)]
Reverting a fix from earlier today that fixed a Mac OS warning but completely broke Linux. :-(
Morgan Deters [Wed, 5 Oct 2011 23:51:57 +0000 (23:51 +0000)]
ensureLiteral() in CNF stream to support Andy's quantifiers work; an update to model gen on booleans; and a little cleanup
Morgan Deters [Wed, 5 Oct 2011 19:03:23 +0000 (19:03 +0000)]
minor visibility fixes
Morgan Deters [Wed, 5 Oct 2011 17:52:06 +0000 (17:52 +0000)]
remove some debugging code that slowed down last night's regressions
Tim King [Tue, 4 Oct 2011 22:21:55 +0000 (22:21 +0000)]
Disabling the variable removal hueristic by default.
Morgan Deters [Tue, 4 Oct 2011 16:16:02 +0000 (16:16 +0000)]
also add test case
Morgan Deters [Tue, 4 Oct 2011 16:15:47 +0000 (16:15 +0000)]
fixes to context-dependent caching substitutions
Morgan Deters [Tue, 4 Oct 2011 15:48:03 +0000 (15:48 +0000)]
add a guard for history saving, to enable building without GNU history library
Morgan Deters [Tue, 4 Oct 2011 14:40:01 +0000 (14:40 +0000)]
compatibility, bindings
Morgan Deters [Tue, 4 Oct 2011 14:36:57 +0000 (14:36 +0000)]
cvc3 compatibility layer; and another libantlr3c v3.4 incompatibility fix
Morgan Deters [Tue, 4 Oct 2011 06:25:36 +0000 (06:25 +0000)]
compat layer cleanup
Morgan Deters [Tue, 4 Oct 2011 01:54:38 +0000 (01:54 +0000)]
oops, one more fix, hopefully the last
Morgan Deters [Tue, 4 Oct 2011 01:42:45 +0000 (01:42 +0000)]
Yet Another Antlr3 Mod---this time, all my fault: for configuration 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.
Morgan Deters [Tue, 4 Oct 2011 01:25:35 +0000 (01:25 +0000)]
Oh, here's another cute compatibility fix for libantlr3c 3.4-beta4. They #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.
Morgan Deters [Tue, 4 Oct 2011 01:06:41 +0000 (01:06 +0000)]
mimicking Chris's recent contribution to QueryResult in CVC3 in the compatibility layer
Morgan Deters [Tue, 4 Oct 2011 00:59:29 +0000 (00:59 +0000)]
more fixes for libantlr3c v3.4
Morgan Deters [Tue, 4 Oct 2011 00:26:35 +0000 (00:26 +0000)]
support for configure-discovery of antlr3-3.4-beta4
Morgan Deters [Mon, 3 Oct 2011 22:07:38 +0000 (22:07 +0000)]
user push/pop support in minisat and simplification; also bindings work
Morgan Deters [Mon, 3 Oct 2011 18:24:57 +0000 (18:24 +0000)]
Importing Chris's recent changes to CVC3's ValidityChecker into the compatibility layer
Morgan Deters [Fri, 30 Sep 2011 23:35:31 +0000 (23:35 +0000)]
fix to CNF undoTranslate(), to support incrementality
Morgan Deters [Fri, 30 Sep 2011 23:20:23 +0000 (23:20 +0000)]
forgot to put some things in the distro
Morgan Deters [Fri, 30 Sep 2011 23:01:58 +0000 (23:01 +0000)]
interfaces fixes and cleanups...and examples of each interface!
Morgan Deters [Fri, 30 Sep 2011 03:33:56 +0000 (03:33 +0000)]
more push/pop infrastructure, some SAT stuff
Morgan Deters [Fri, 30 Sep 2011 02:29:00 +0000 (02:29 +0000)]
fixes to incremental simplification, cnf routines, other stuff in preparation of user push/pop in SAT solver
Morgan Deters [Thu, 29 Sep 2011 18:38:00 +0000 (18:38 +0000)]
compatibility work, documentation
Morgan Deters [Thu, 29 Sep 2011 06:40:27 +0000 (06:40 +0000)]
build system fixes
Morgan Deters [Thu, 29 Sep 2011 05:15:30 +0000 (05:15 +0000)]
Some base infrastructure for user push/pop; a few bugfixes to user push/pop 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
Morgan Deters [Thu, 29 Sep 2011 02:24:28 +0000 (02:24 +0000)]
some test fixes
Morgan Deters [Wed, 28 Sep 2011 23:57:12 +0000 (23:57 +0000)]
another make dist fix for java compat bindings
Morgan Deters [Wed, 28 Sep 2011 23:53:57 +0000 (23:53 +0000)]
variety of visibility fixes (should clean up some of the many warnings on MacOS-production-dynamic builds)
Morgan Deters [Wed, 28 Sep 2011 22:38:31 +0000 (22:38 +0000)]
CVC4::Integer was not marked CVC4_PUBLIC, causing dynamic link errors on MacOS in production builds. Fixed.
Morgan Deters [Wed, 28 Sep 2011 22:32:05 +0000 (22:32 +0000)]
fixes for make dist ; make install
Morgan Deters [Wed, 28 Sep 2011 19:46:53 +0000 (19:46 +0000)]
better fix for #281, also fix issue with command line options not existing on older g++en, like Apple's 4.2 on Snow Leopard.
Morgan Deters [Wed, 28 Sep 2011 18:46:29 +0000 (18:46 +0000)]
Regular expressions in shell scripts on MacOS are inconsistent... again. :-( Fixing a problem with Debug_tags and Trace_tags, closes bug #281
Morgan Deters [Wed, 28 Sep 2011 00:45:46 +0000 (00:45 +0000)]
removed "typename" keyword (fix to bug 280)
Morgan Deters [Tue, 27 Sep 2011 00:34:30 +0000 (00:34 +0000)]
more interface work; adding legacy C interface
Morgan Deters [Sun, 25 Sep 2011 08:18:45 +0000 (08:18 +0000)]
first crack at compatibility java interface (not built by default)
Morgan Deters [Sat, 24 Sep 2011 18:04:08 +0000 (18:04 +0000)]
Fix to building and linking for unit tests. (This should fix the segfaulting units in optimized-dynamic. The problem was that the code incorrectly determined the address of one of the thread-scoped global variables, and I think it's because the same library was linked twice into the unit test in two different ways, confusing the runtime support code.)
Morgan Deters [Fri, 23 Sep 2011 23:37:42 +0000 (23:37 +0000)]
interface cleanup, java bindings work
Morgan Deters [Wed, 21 Sep 2011 05:02:58 +0000 (05:02 +0000)]
Java binding now working. Some interface types still need some work (e.g. iterators aren't functional). Also, output isn't very flexible yet, as I told SWIG to ignore all the operator<<'s.
Morgan Deters [Wed, 21 Sep 2011 03:26:13 +0000 (03:26 +0000)]
considerable bindings interface work, some improvements to build
Morgan Deters [Tue, 20 Sep 2011 17:45:00 +0000 (17:45 +0000)]
fix build
Morgan Deters [Tue, 20 Sep 2011 14:58:30 +0000 (14:58 +0000)]
Merge from "swig" branch: language binding for Java is compiling and linking. Enable with --enable-language-bindings=java
Morgan Deters [Sun, 18 Sep 2011 21:13:34 +0000 (21:13 +0000)]
cleaned up the mechanism for library versioning
Morgan Deters [Sat, 17 Sep 2011 01:57:27 +0000 (01:57 +0000)]
--show-debug-tags and --show-trace-tags now supported by Configuration API; also, the information is only recompiled and relinked when it has changed, avoiding unnecessary relinking
Morgan Deters [Fri, 16 Sep 2011 21:54:21 +0000 (21:54 +0000)]
dump define-funs correctly with "--dump declarations", whether the function is defined via API or through input language
Morgan Deters [Fri, 16 Sep 2011 21:52:25 +0000 (21:52 +0000)]
include example theory (former "UF-Tim") that's included in the dist but not built for the library
Morgan Deters [Fri, 16 Sep 2011 21:36:07 +0000 (21:36 +0000)]
final(?) documentation fixes
Morgan Deters [Fri, 16 Sep 2011 21:32:37 +0000 (21:32 +0000)]
fix up more documentation
Morgan Deters [Fri, 16 Sep 2011 21:30:27 +0000 (21:30 +0000)]
some minor fixes to the cvc3 compatibility library and test case
Morgan Deters [Fri, 16 Sep 2011 20:53:36 +0000 (20:53 +0000)]
new, improved doxygen config file
Morgan Deters [Fri, 16 Sep 2011 20:53:19 +0000 (20:53 +0000)]
fix serious issue with copyright-updating script
Morgan Deters [Fri, 16 Sep 2011 20:53:00 +0000 (20:53 +0000)]
fix numerous documentation issues; doxygen complains much less, now
Morgan Deters [Fri, 16 Sep 2011 20:49:58 +0000 (20:49 +0000)]
fix an oversight in the language printers
Morgan Deters [Fri, 16 Sep 2011 20:19:25 +0000 (20:19 +0000)]
fix debian build without breaking anything (i hope)
Dejan Jovanović [Thu, 15 Sep 2011 21:48:42 +0000 (21:48 +0000)]
tim's fixes for context-dependent pre-registration
Dejan Jovanović [Thu, 15 Sep 2011 18:17:11 +0000 (18:17 +0000)]
adding --show-debug-tags to list all available debug tracing tags
Dejan Jovanović [Thu, 15 Sep 2011 06:53:33 +0000 (06:53 +0000)]
additional stuff for sharing,
Dejan Jovanović [Wed, 7 Sep 2011 16:25:15 +0000 (16:25 +0000)]
fixes for uf/equality engine from the quantifiers branch. mainly backtracking issues.
Morgan Deters [Sat, 3 Sep 2011 18:31:24 +0000 (18:31 +0000)]
this should fix the build; doxygen documentation now gets built in srcdir/doc/doxygen
Morgan Deters [Sat, 3 Sep 2011 18:13:04 +0000 (18:13 +0000)]
Disable a warning to address bug 277. (This doesn't really resolve the issue, but the warning isn't dangerous here. See the bugzilla comments.)
Dejan Jovanović [Sat, 3 Sep 2011 00:42:34 +0000 (00:42 +0000)]
removing an assert i forgot to remove that andy found
Morgan Deters [Fri, 2 Sep 2011 20:41:08 +0000 (20:41 +0000)]
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Morgan Deters [Fri, 2 Sep 2011 19:23:18 +0000 (19:23 +0000)]
Ensure that assignment gestures through CDMap iterators like:
(*myCDMap.find(foo)).second = bar;
fail with a compile-time error (rather than being silently ignored, like
they had been).
Resolves bug #276.
Morgan Deters [Fri, 2 Sep 2011 17:56:43 +0000 (17:56 +0000)]
Partial merge of integers work; this is simple B&B and some pseudoboolean
infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.
Dejan Jovanović [Fri, 2 Sep 2011 12:39:23 +0000 (12:39 +0000)]
* Changing pre-registration to be context dependent -- it is called from the SAT solver on every backtrack
* Updated UF to handle the context dependent pre-registration
* Additionally some small changes in order to satisfy warnings of the eclipse code analysis tool