Age | Commit message (Collapse) | Author |
|
* test/regress/regress0/unconstrained wasn't being distributed. This caused the debian build failure last night. (It still doesn't run on "make check", but had to be distributed properly.)
* Fixing an issue where a test name was longer than 99 characters and couldn't be distributed in the "old" tar format. (Told automake to use a newer tar format.)
|
|
for portfolio)
|
|
|
|
Makefile.am files under src/prop/cryptominisat.
|
|
|
|
Dump("foo") << FooCommand(...);
now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.
If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run. This is done even if the muzzle is on.
This commit also cleans up some code that used the dump feature (in arrays,
particularly).
|
|
explicitly linked in with -l) when using CLN. Fixes a bug on recent Debian that Francois reported. Hopefully this doesn't break anything..
|
|
(Clark-requested change)
|
|
errors; threading support should only be required to build pcvc4, not cvc4
|
|
|
|
|
|
library an error; useful for builds requiring a "pcvc4" binary at the end
|
|
platforms that need it; fixes Mac builds.
|
|
and other build/documentation fixes from yesterday's portfolio merge; resolves bug 302
|
|
|
|
|
|
files can be added to it without modifying the script.
|
|
|
|
|
|
|
|
- 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.
|
|
v4.5.1 which has a buggy optimizer (resolves bug #266)
|
|
|
|
|
|
|
|
on older g++en, like Apple's 4.2 on Snow Leopard.
|
|
|
|
iterators aren't functional). Also, output isn't very flexible yet, as I told SWIG to ignore all the operator<<'s.
|
|
|
|
|
|
|
|
srcdir/doc/doxygen
|
|
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.
|
|
|
|
* compilation fixes for GCC 4.6.x
+ ptrdiff_t is now in std::
* fix some make rules that are ok in Make 3.81 but broke in Make 3.82
* look for cxxtestgen.py as well as cxxtestgen.pl, and look for cxxtest headers in /usr/include
|
|
|
|
|
|
|
|
newswire-raised documentation issues.
|
|
successful link at configure time
|
|
are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development). Dejan has now given me the go-ahead
for a merge.
=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================
Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor. The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead). This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.
TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.
Specifically:
* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
1. As described above.
2. Theories now have const access to the fact queue through base
class functions facts_begin() and facts_end(); useful for
debugging.
* Added an "Asserted" attribute so that theories can check if something
has been asserted or not (and therefore not propagate it). However, this
has been disabled for now, pending more data on the overhead of it, and
pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived! So far mainly infrastructure for having
system tests, but there is a system test aimed at improving code
coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
conformant to CVC4 policy.
Tests have been performed to demonstrate that these changes have no or
negligible effect on performance. In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).
|
|
against cudd libraries, the propositional_query class (in util/),
which uses cudd if it's available (and otherwise answers UNKNOWN for
all queries), and the arith theory support for it (currently disabled
per Tim's request, so he can clean it up).
Other changes include:
* contrib/debug-keys - script to print all used keys under Debug(), Trace()
* test/regress/run_regression - minor fix (don't export a variable)
* configure.ac - replace a comment removed by dejan's google perf commit
* some minor copyright/documentation updates, and minor changes to source
text to make 'clang --analyze' happy.
|
|
enabled at configure with
--with-google-perftools
to use it on ubuntu, you need to install packages google-perftools and libgoogle-perftools0
to run the profiling of the heap, you can run it for example with
HEAPPROFILE=/tmp/profile ./builds/bin/cvc4 test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt
this will create some files /tmp/profile* that you can then
to get the pdf of the profile you can then run
google-pprof --pdf ./builds/bin/cvc4 /tmp/profile.0001.heap > profile.pdf
or for other options check http://goog-perftools.sourceforge.net/doc/
|
|
obviates the need for a full rebuild just because you re-./configured.
|
|
graphs (but nightly build system will produce them)
|
|
documentation, and make it possible to "make doc" on a clean source tree (post-configure)
|
|
|
|
cxxtest when it wasn't found.
|
|
* Add ContextMemoryAllocator<T> allocator type, conforming to
STL allocator requirements.
* Extend the CDList<> template to take an allocator (defaults
to std::allocator<T>).
* Add a specialized version of the CDList<> template (in
src/context/cdlist_context_memory.h) that allocates a list
in segments, in context memory.
* Add "forward" headers -- cdlist_forward.h, cdmap_forward.h,
and cdset_forward.h. Use these in public headers, and other
places where you don't need the full header (just the
forward-declaration). These types justify their own header
(instead of just forward-declaring yourself), because they
are complex templated types, with default template parameters,
specializations, etc.
* theory_engine.h no longer depends on individual theory headers.
(Instead it forward-declares Theory implementations.) This is
especially important now that theory .cpp files depend on
TheoryEngine (to implement Theory::getValue()). Previously,
any modification to any theory header file required *all*
theories, and the engine, to be completely rebuilt.
* Support memory cleanup for nontrivial CONSTANT kinds. This
resolves an issue with arithmetic where memory leaked for
each distinct Rational or Integer that was wrapped in a Node.
|
|
supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command
|