| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
post-rewrite, another full rewrite is performed and the results
compared).
Also added another response code to rewriters. Theories return a
CVC4::theory::RewriteResponse from preRewrite() and postRewrite().
This class has nice subclasses to make the theory rewriters somewhat
self-documenting in termination behavior. They look like
tail-recursive rewriting calls, but they're not; they are
instantiations of the RewriteResponse result code, which carries the
Node being returned:
// Flags the node as DONE pre- or post-rewriting, though this is
// ignored if n belongs to another theory.
//
// NOTE this just changed name from RewritingComplete(), which
// didn't match RewriteAgain().
//
return RewriteComplete(n);
// Flags the node as needing another pre-rewrite (if returned from a
// preRewrite()) or post-rewrite (if returned from a postRewrite()).
//
return RewriteAgain(n);
// Flags the node as needing another FULL rewrite. This is the same
// as RewriteAgain() if returned from preRewrite(). If it's returned
// from postRewrite(), however, this causes a full preRewrite() and
// postRewrite() of the Node and all its children (though the cache is
// still in effect, which might elide some rewriting calls).
//
// This would have been another fix for bug #168. Its use should be
// discouraged in practice, but there are places where it will
// probably be necessary, where a theory rewrites a Node into
// something in another theory about which it knows nothing.
// A common case is where the returned Node is expressed as a
// conjuction or disjunction of EQUALs, or a negation of EQUAL,
// where the EQUAL is across terms in another theory, and that EQUAL
// subterm should be seen by the owning theory.
//
return FullRewriteNeeded(n);
|
|
|
|
|
|
building with CLN or with GMP, the contrib/switch-config script
(enabling "fast switching" of different configurations in the same
builds/ directory), and also some minor changes.
./configure --with-gmp (or --without-cln) forces building with GMP
and doesn't even look for CLN. Configure fails if GMP isn't installed.
./configure --with-cln (or --without-gmp) forces building with CLN
and doesn't even look for GMP. Configure fails if CLN isn't installed.
./configure [no arguments] will detect what's installed. CLN is
default, if it isn't installed, or is too old, GMP is looked for (and
configure fails if neither is available).
It is an error to specify --with-gmp --with-cln (or --without-* for
both) at the same time.
Building with CLN (whether forced or detected) adds a note to the
configure output mentioning the fact that the build of CVC4 will be
linked against a GPLed library and notifying the user of the
--without-cln option.
Building with GMP (whether forced or detected) affects the build
directory, so CLN and GMP builds are kept separate.
./configure --with-cln debug builds in builds/$arch/debug
./configure --with-gmp debug builds in builds/$arch/debug-gmp
The final binaries are linked explicitly against either gmp or cln,
but not both. If linked against cln, cln pulls in gmp as a
dependency, so the result will be linked against both.
=== Details that you probably don't care about ===
The headers src/util/{integer,rational}.h are generated from the
corresponding .in versions. A user installing a CVC4-devel package
will get the headers for rational and integer that match the library
that s/he installs.
The preprocessor #defines CVC4_GMP_IMP and CVC4_CLN_IMP are added to
cvc4autoconfig.h. Only one is ever #defined. cvc4autoconfig.h
doesn't need to be #included directly; you get it through #including
cvc4_private.h (or the parser version).
AM_CONDITIONALs are also defined so that Makefiles get the cln/gmp
configuration. AC_SUBSTs are defined so that public headers (see
src/util/{integer,rational}.h.in) can use the setting.
*Public* headers that need to depend on the cln/gmp configuration
can't use cvc4autoconfig.h, because we're keeping that in the private,
internal-only space, never to be installed on users' machines. Here,
something special is required, like the configure-level generation of
headers that I used for src/util/{integer,rational}.h.in.
Tim's Integer and Rational wrappers are the only bits of code that
should care which library is used (and also src/util/configuration.h,
which gives the user of the library information about how CVC4 is
built), and possibly some unit tests (?).
|
|
The current commit allows for switching in between GMP and CLN by changing a flag manually in configure.ac. A configure time flag has not yet been added for deciding between the two.
To get this to work you will need to install cln in some form (for Ubuntu users the packages are libcln6(lucid)/libcln5 on karmic and libcln-dev). You will also need to install pkg-config. You will need to rerun ./autogen.sh, and reconfigure.
|
|
|
|
* Added regression documentation to test/regress/README
* Added ability to print types of vars in expr printouts
with iomanipulator Node::printtypes(true)... for example,
Warning() << Node::printtypes(true) << n << std::endl;
* Types-printing can be specified on the command line with
--print-expr-types
* Improved type handling facilities and theoryOf().
For now, SORT_TYPE moved from builtin theory to UF theory
to match old behavior.
* Additional gdb debug functionality. Now we have:
debugPrintNode(Node) debugPrintRawNode(Node)
debugPrintTNode(TNode) debugPrintRawTNode(TNode)
debugPrintTypeNode(TypeNode) debugPrintRawTypeNode(TypeNode)
debugPrintNodeValue(NodeValue*) debugPrintRawNodeValue(NodeValue*)
they all print a {Node,TNode,NodeValue*} from the debugger.
The "Raw" versions print a very low-level AST-like form.
The regular versions do the same as operator<<, but force
full printing on (no depth-limiting).
* Other trivial fixes
|
|
additional output). If the benchmark file has '% EXPECT: ' gestures,
like for cvc regressions, that is used (after being stripped out so that
the cvc4 smt parser never sees these special lines). However, this can
be a pain, since then you can't run the regression manually on the
command line (since it fails to parse). So if there is another file
in the same directory as $benchmark called $benchmark.expect, that is
scanned for '% EXPECT: ' etc., and the benchmark file is used verbatim.
|
|
* added TheoryArith::preRewrite() to test and demonstrate
the use of pre-rewriting.
* array types and type checking now supported
* array type checking now supported
* theoryOf() dispatching properly to arrays now
* theories now required to implement a (simple) identify()
function that returns a string identifying them for
debugging/user output purposes
* added "builtin" theory to hold all built-in kinds and their
type rules and rewriting (currently only exploding distinct)
* fixed production build failure (regarding NodeSetDepth)
* removed an errant "using namespace std" in util/bitvector.h
(and made associated trivial fixes elsewhere)
* fixes to make unexpected exceptions more verbose in debug builds
* fixes to make multiple, cascading assertion fails simpler
* minor other fixes to comments etc.
|
|
expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.
|
|
data into a CDMap. Such a key doesn't disappear from the map on pop,
but rather returns to its "initializing" state, set by
insertAtContextLevelZero(). This can be used for lazy assignment,
among other things, and has been added to support some exploratory
coding by Tim in arithmetic.
* Made internal CDOmap<> copy constructor private (it should always have
been). This is necessary to avoid CxxTest (or others) doing nasty
generic programming things that cause context invariants to be broken.
* Added unit testing for this feature, and in general beef up the unit
testing for CDMap<>.
* src/expr/node_manager.cpp: Better output for unhandled cases in getType().
|
|
documentation
|
|
|
|
|
|
|
|
** file-level documentation at the top of the sources. **
This is the "make bugzilla stop bugging me" bugfix commit.
* Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy.
Updated documentation in the file. Resolves bug #99.
* Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.)
moved into a separate file. Partially resolves bug #100.
* Moved isAssociative(Kind) into kind.h (and into the CVC4::kind
namespace) instead of metakind.h (where it was in CVC4::metakind).
This clears up a warning (private #inclusion) from the SMT and SMT2
parsers, and maybe makes more sense anyways, since this is based on
the kind (and not the metakind) of an operator.
* Documentation improvement; doxygen top-level \file gestures, \brief
gestures for files, etc. Changed contrib/update-copyright.pl for
this change, and post-processed to add \brief. Resolves bug #98.
* Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind).
They no longer made sense. Resolves bug #91.
|
|
|
|
|
|
assignment for slack variables once solving has begun. (They cannot just be 0.) The second has to do with how assignments are backttacked. Assignments are now tracked all of the time, and are frozen once they are known to be consistent, i.e. after a successful updateInconsistentVars(). Also added a fuzz test that shows both of these problems to the regressions.
|
|
with that of Node.
* If NodeBuilder<> hasn't yet been assigned a Kind, several member functions
related to children now throw an IllegalArgumentException:
* getNumChildren()
* begin()
* end()
* operator[]
* getChild()
This is because if you later assign the NodeBuilder<> a PARAMETERIZED kind,
the children are "reinterpreted" -- the first being an operator. Interface-wise,
it doesn't make sense to return one thing for nb[0], then later, after setting
the kind, to return another thing for nb[0].
* Fixed unit tests depending on this behavior.
* Added a warning to the testing summary if unit tests didn't run (because this
is likely due to compilation problems, and without a warning it looks kind of
like a test success)
* VERBOSE wasn't exported to the environment for unit test "make check." Fixed.
|
|
|
|
|
|
translation must indeed be a clause (if possible). I've changed the top level CNF conversion to generate clauses, instead of introducing unit clauses for each assertion.
|
|
|
|
|
|
|
|
potential design for later. Resolves bug 113, invalidates bugs 93 and 94.
|
|
|
|
revision were in conflict.)
|
|
smt and smt2 regressions; resolves bug 132
|
|
support has been added. Also a few bug fixes to Tableau.
|
|
* keeps test logs around
* provides parallel testing functionality (with make -jN).
I've also added new functionality in test/Makefile.am which deletes old test logs, ensures that ALL tests are tried (even if units fail), and provides a color-coded summary at the end of the test run, which shows how many units, regressions (per level), and system tests failed (or passed), and provides a link to the log file for further information.
Resolves bug 117.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Rational and Integer constructors are now explicit. This means that 'Integer = 3;' and so on are no longer permitted. This closes bug 121.
|
|
Real. See Bug 127 for a discussion of the hack. I am also adding a regression test that does not work (bug 128). It is not enabled so make check should still be fine.
|
|
TheoryArith. Also directly hacked in support for theoryOf() to work for equalities where the left hand is a variable of type real.
|
|
fixes and organizational changes. The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.
|
|
|
