cvc5.git
14 years agorenaming minisat .C to .cc
Dejan Jovanović [Fri, 13 Aug 2010 17:47:56 +0000 (17:47 +0000)]
renaming minisat .C to .cc

14 years agoAdding the changes to the original copy
Dejan Jovanović [Fri, 13 Aug 2010 17:27:12 +0000 (17:27 +0000)]
Adding the changes to the original copy

14 years agoImporting MiniSat2 070721 into trunk
Christopher L. Conway [Fri, 13 Aug 2010 17:22:46 +0000 (17:22 +0000)]
Importing MiniSat2 070721 into trunk

14 years agoRemoving newer version of MiniSat for Dejan's preferred import
Christopher L. Conway [Fri, 13 Aug 2010 17:21:24 +0000 (17:21 +0000)]
Removing newer version of MiniSat for Dejan's preferred import

14 years agoImporting MiniSat2 2.2.0 into trunk
Christopher L. Conway [Fri, 13 Aug 2010 17:20:19 +0000 (17:20 +0000)]
Importing MiniSat2 2.2.0 into trunk

14 years agoRemoving old version of MiniSat for proper vendor import
Christopher L. Conway [Fri, 13 Aug 2010 17:19:28 +0000 (17:19 +0000)]
Removing old version of MiniSat for proper vendor import

14 years agoAdding configuration_private.h to allow inlining of configuration checks
Christopher L. Conway [Thu, 29 Jul 2010 18:33:33 +0000 (18:33 +0000)]
Adding configuration_private.h to allow inlining of configuration checks

14 years agofix TheoryEngineWhite, add documentation; related to bug #188
Morgan Deters [Thu, 29 Jul 2010 16:52:14 +0000 (16:52 +0000)]
fix TheoryEngineWhite, add documentation; related to bug #188

14 years agoAdding TypeCheckingException to throws clause in SMT parsers
Christopher L. Conway [Wed, 28 Jul 2010 23:04:44 +0000 (23:04 +0000)]
Adding TypeCheckingException to throws clause in SMT parsers

14 years agoForcing a type check on Node construction in debug mode (Fixes: #188)
Christopher L. Conway [Wed, 28 Jul 2010 22:57:36 +0000 (22:57 +0000)]
Forcing a type check on Node construction in debug mode (Fixes: #188)
NOTE: mkNode/mkExpr/parsing functions can now throw type checking exceptions

14 years agofixed theory engine white test for new (old) theoryOf() behavior (re: bug 188)
Morgan Deters [Wed, 28 Jul 2010 02:57:22 +0000 (02:57 +0000)]
fixed theory engine white test for new (old) theoryOf() behavior (re: bug 188)

14 years agoMoving EQ->IFF handling from TheoryEngine to parser/type checker
Christopher L. Conway [Tue, 27 Jul 2010 20:55:10 +0000 (20:55 +0000)]
Moving EQ->IFF handling from TheoryEngine to parser/type checker

14 years agoAdding optional 'check' parameter to getType() methods
Christopher L. Conway [Tue, 27 Jul 2010 20:54:33 +0000 (20:54 +0000)]
Adding optional 'check' parameter to getType() methods

14 years agoincorporate a fix from smtcomp2010 version for handling CNF of (= bool bool); also...
Morgan Deters [Thu, 22 Jul 2010 21:55:28 +0000 (21:55 +0000)]
incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool); also make theoryOf(= t1 t2) return theoryOf(t1.getType()), rather than theoryOf(t1), as the latter gives different results for (= (geq x1 x2) (leq x2 x1)) and (= a (leq x2 x1)), which is strange and causes problems.  should discuss at tuesday meeting.  resolves bug 187.

14 years agoAdded test file for fuzzsmt bug, bug187.smt2.
Tim King [Thu, 22 Jul 2010 20:24:27 +0000 (20:24 +0000)]
Added test file for fuzzsmt bug, bug187.smt2.

14 years agoadd >, <=, and >= comparisons for Exprs and Nodes
Morgan Deters [Sat, 10 Jul 2010 05:46:41 +0000 (05:46 +0000)]
add >, <=, and >= comparisons for Exprs and Nodes

14 years agoFix for the type in sat propagation.
Dejan Jovanović [Sat, 10 Jul 2010 04:32:03 +0000 (04:32 +0000)]
Fix for the type in sat propagation.

14 years agothe tableaux optimization
Dejan Jovanović [Fri, 9 Jul 2010 15:47:24 +0000 (15:47 +0000)]
the tableaux optimization

14 years agoMoving cluster-qf_lra-full to scripts project
Christopher L. Conway [Thu, 8 Jul 2010 20:29:20 +0000 (20:29 +0000)]
Moving cluster-qf_lra-full to scripts project

14 years agoMoving cluster-qf_lra-benchmark to scripts project
Christopher L. Conway [Thu, 8 Jul 2010 20:28:36 +0000 (20:28 +0000)]
Moving cluster-qf_lra-benchmark to scripts project

14 years agoAdding missing operators in SMT2 parser: UMINUS, DIVISION, GEQ, LEQ
Christopher L. Conway [Thu, 8 Jul 2010 19:12:41 +0000 (19:12 +0000)]
Adding missing operators in SMT2 parser: UMINUS, DIVISION, GEQ, LEQ

14 years agoFixing Array type in SMT v1.2
Christopher L. Conway [Thu, 8 Jul 2010 19:12:32 +0000 (19:12 +0000)]
Fixing Array type in SMT v1.2

14 years agoI am adding my smt-crunch scripts to source control. Others may find them useful...
Tim King [Thu, 8 Jul 2010 17:25:12 +0000 (17:25 +0000)]
I am adding my smt-crunch scripts to source control.  Others may find them useful. To use them, log into goedel, sudo su acsys-user, and run ./cluster-script PATH_TO_EXECUTABLE. Be sure to change the email address in the script before using it. Improvements are of course welcome.

14 years agocontext work to support cdmaps with elements allocated in context memory
Morgan Deters [Thu, 8 Jul 2010 04:33:10 +0000 (04:33 +0000)]
context work to support cdmaps with elements allocated in context memory

14 years agoUpdates to the post_mortem.py script.
Tim King [Thu, 8 Jul 2010 01:24:34 +0000 (01:24 +0000)]
Updates to the post_mortem.py script.

14 years agoShared term manager tested and working
Clark Barrett [Wed, 7 Jul 2010 21:55:11 +0000 (21:55 +0000)]
Shared term manager tested and working
It is currently tracking all asserted equalities for simplicity.
Might want to check if this is a performance hit

14 years agoMaking plus-mult.cvc test a bit more torturous (as enabled by r744)
Christopher L. Conway [Wed, 7 Jul 2010 16:25:36 +0000 (16:25 +0000)]
Making plus-mult.cvc test a bit more torturous (as enabled by r744)

14 years agoFixes arith rewriter to allow for division by a constant. It previously only allowed...
Tim King [Wed, 7 Jul 2010 16:23:22 +0000 (16:23 +0000)]
Fixes arith rewriter to allow for division by a constant. It previously only allowed for a constant divided by a constant.

14 years agoFixing test plus-mult.cvc by making it linear (Fixes: #184)
Christopher L. Conway [Wed, 7 Jul 2010 16:02:10 +0000 (16:02 +0000)]
Fixing test plus-mult.cvc by making it linear (Fixes: #184)

14 years agominor changes to cdmap/cdset interface for detection of duplicate inserts
Morgan Deters [Wed, 7 Jul 2010 05:39:04 +0000 (05:39 +0000)]
minor changes to cdmap/cdset interface for detection of duplicate inserts

14 years agochris and i committed the same fix; reverting the (now duplicated) fix
Morgan Deters [Wed, 7 Jul 2010 05:38:01 +0000 (05:38 +0000)]
chris and i committed the same fix; reverting the (now duplicated) fix

14 years agoUpdated headers
Clark Barrett [Wed, 7 Jul 2010 02:26:38 +0000 (02:26 +0000)]
Updated headers

14 years agoAdded shared term manager. Basic mechanism for identifying shared terms is
Clark Barrett [Wed, 7 Jul 2010 02:18:42 +0000 (02:18 +0000)]
Added shared term manager.  Basic mechanism for identifying shared terms is
working.  Still need to implement theory-specific shared term propagation.

14 years agoDisabling failing tests
Christopher L. Conway [Wed, 7 Jul 2010 02:02:08 +0000 (02:02 +0000)]
Disabling failing tests

14 years agoadd exit status to regression that was failing
Morgan Deters [Wed, 7 Jul 2010 01:12:40 +0000 (01:12 +0000)]
add exit status to regression that was failing

14 years agosome build system changes reverted after the CLN build system work a few days ago...
Morgan Deters [Wed, 7 Jul 2010 00:57:48 +0000 (00:57 +0000)]
some build system changes reverted after the CLN build system work a few days ago, these are now fixed:  competition configurations build with -O9 (as they used to); they are static-binary by default and shared libs are not built; also the default autoconf compiler flags "-g -O2" is removed from builds

14 years agocompetition submission should be fully static
Morgan Deters [Wed, 7 Jul 2010 00:36:20 +0000 (00:36 +0000)]
competition submission should be fully static

14 years agofixed submission target
Morgan Deters [Wed, 7 Jul 2010 00:11:05 +0000 (00:11 +0000)]
fixed submission target

14 years agothings for competition upload: new "make submission" target
Morgan Deters [Wed, 7 Jul 2010 00:04:41 +0000 (00:04 +0000)]
things for competition upload: new "make submission" target

14 years agoAdding tests for precedence of arithmetic in CVC inputs
Christopher L. Conway [Wed, 7 Jul 2010 00:01:13 +0000 (00:01 +0000)]
Adding tests for precedence of arithmetic in CVC inputs

14 years agoAdding config.reconfig to .gitignore
Christopher L. Conway [Wed, 7 Jul 2010 00:01:03 +0000 (00:01 +0000)]
Adding config.reconfig to .gitignore

14 years agoFixed exit status for competition mode.
Tim King [Tue, 6 Jul 2010 23:48:49 +0000 (23:48 +0000)]
Fixed exit status for competition mode.

14 years agoDon't eagerly collect zombies. This should speed up things for competition but might...
Morgan Deters [Tue, 6 Jul 2010 20:19:34 +0000 (20:19 +0000)]
Don't eagerly collect zombies.  This should speed up things for competition but might flush out some memory issues.  Passes all regressions so far..

14 years agoadd Configuration::isCompetitionBuild() and some main driver fixes
Morgan Deters [Tue, 6 Jul 2010 19:36:59 +0000 (19:36 +0000)]
add Configuration::isCompetitionBuild() and some main driver fixes

14 years agofix crash on command line parsing
Morgan Deters [Tue, 6 Jul 2010 19:32:50 +0000 (19:32 +0000)]
fix crash on command line parsing

14 years agoMoved registration to theory engine
Clark Barrett [Tue, 6 Jul 2010 18:37:06 +0000 (18:37 +0000)]
Moved registration to theory engine

14 years agoAdding Array types to SMT2 parser
Christopher L. Conway [Tue, 6 Jul 2010 17:10:53 +0000 (17:10 +0000)]
Adding Array types to SMT2 parser

14 years agoAdding arithmetic symbols to CVC parser (Fixes: #176)
Christopher L. Conway [Tue, 6 Jul 2010 16:21:27 +0000 (16:21 +0000)]
Adding arithmetic symbols to CVC parser (Fixes: #176)

14 years agomerge from CC work: pieces of the parser need to be declared to throw AssertionExcept...
Morgan Deters [Tue, 6 Jul 2010 15:52:10 +0000 (15:52 +0000)]
merge from CC work: pieces of the parser need to be declared to throw AssertionException, and language enum should have stream insertion op

14 years agoFixes for doubled-statistics (bug 171), a fix to muzzled builds and some minor code
Morgan Deters [Tue, 6 Jul 2010 04:00:42 +0000 (04:00 +0000)]
Fixes for doubled-statistics (bug 171), a fix to muzzled builds and some minor code
cleanup found while searching for additional cases.  Closes bug 171.

14 years agoadd regressions from bug reports
Morgan Deters [Tue, 6 Jul 2010 00:44:14 +0000 (00:44 +0000)]
add regressions from bug reports

14 years agobetter exception wording, assertion-handling in multiple-exception case; resolves...
Morgan Deters [Mon, 5 Jul 2010 23:02:05 +0000 (23:02 +0000)]
better exception wording, assertion-handling in multiple-exception case; resolves bug 175.  also newer URL for config/pkg.m4

14 years agobetter exception wording, assertion-handling in multiple-exception case; resolves...
Morgan Deters [Mon, 5 Jul 2010 23:01:36 +0000 (23:01 +0000)]
better exception wording, assertion-handling in multiple-exception case; resolves bug 175.  also newer URL for config/pkg.m4

14 years agoworkaround for strange CIMS installation of automake; resolves bug 172: autogen fails...
Morgan Deters [Mon, 5 Jul 2010 21:47:05 +0000 (21:47 +0000)]
workaround for strange CIMS installation of automake; resolves bug 172: autogen fails on CIMS machines

14 years agoAdded Cesare to list of authors
Clark Barrett [Mon, 5 Jul 2010 17:29:16 +0000 (17:29 +0000)]
Added Cesare to list of authors

14 years agoChanged AUTHORS - removed references to earlier CVC tool authors
Clark Barrett [Mon, 5 Jul 2010 16:49:48 +0000 (16:49 +0000)]
Changed AUTHORS - removed references to earlier CVC tool authors

14 years agoConsiderably simplified the way output streams are used. This commit
Morgan Deters [Sun, 4 Jul 2010 18:36:22 +0000 (18:36 +0000)]
Considerably simplified the way output streams are used.  This commit
should have no impact on production performance and speed up debug
performance considerably, while making the code much cleaner.  On some
benchmarks, debug builds now run _much_ faster.

We no longer have to sprinkle our code with things like:

  if(debugTagIsOn("context")) {
    Debug("context") << theContext << std::endl;
  }

which we had to do to get around performance problems previously.
Now just writing:

  Debug("context") << theContext << std::endl;

does the same in production and debug builds.  That is, if "context"
debugging is off, theContext isn't converted to a string, nor is it
output to a "/dev/null" ostream.  I've confirmed this.  In production
builds, the whole statement inlines to nothing.  I've confirmed this
too.

Also, "Debug" is no longer a #definition, so you can use it directly
in production builds where you couldn't previously, e.g.

  if(Debug.isOn("paranoid:check_tableau")) {
    checkTableau();
  }

I'm leaving debugTagIsOn() for now, but marking it as deprecated.

14 years agoassigning benchmark statuses
Morgan Deters [Sun, 4 Jul 2010 18:34:02 +0000 (18:34 +0000)]
assigning benchmark statuses

14 years agobetter detection for static binary building
Morgan Deters [Sun, 4 Jul 2010 18:06:57 +0000 (18:06 +0000)]
better detection for static binary building

14 years agofix to production build
Morgan Deters [Sun, 4 Jul 2010 06:31:05 +0000 (06:31 +0000)]
fix to production build

14 years agoenable arrays
Morgan Deters [Sun, 4 Jul 2010 04:38:58 +0000 (04:38 +0000)]
enable arrays

14 years agodon't do extra-checking for all regressions; that's probably a bad default
Morgan Deters [Sun, 4 Jul 2010 04:04:23 +0000 (04:04 +0000)]
don't do extra-checking for all regressions; that's probably a bad default

14 years agoWith "-d extra-checking", rewrites are now checked (after
Morgan Deters [Sun, 4 Jul 2010 03:59:36 +0000 (03:59 +0000)]
With "-d extra-checking", rewrites are now checked (after
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);

14 years agobug 168 fixed (TheoryEngine::rewrite is not fully rewriting to a fix point); problem...
Morgan Deters [Sun, 4 Jul 2010 02:18:02 +0000 (02:18 +0000)]
bug 168 fixed (TheoryEngine::rewrite is not fully rewriting to a fix point); problem had to do with the builtin theory post-rewriting DISTINCT into an arithmetic term not in normal form.  fix was to do DISTINCT rewriting in pre-rewrite.  note that this doesn't add to the amount of theory rewriting work that needs to be done, because everything is cached

14 years agomake dist && make distcheck functional, other fixes
Morgan Deters [Sun, 4 Jul 2010 02:00:42 +0000 (02:00 +0000)]
make dist && make distcheck functional, other fixes

14 years agofix warnings
Morgan Deters [Sat, 3 Jul 2010 23:09:25 +0000 (23:09 +0000)]
fix warnings

14 years agobetter config.reconfig script auto-generated
Morgan Deters [Sat, 3 Jul 2010 18:18:55 +0000 (18:18 +0000)]
better config.reconfig script auto-generated

14 years agoWith this commit come a number of changes to build system to support
Morgan Deters [Sat, 3 Jul 2010 17:59:19 +0000 (17:59 +0000)]
With this commit come a number of changes to build system to support
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 (?).

14 years agoMerges the cln-test branch into the main branch.
Tim King [Fri, 2 Jul 2010 18:49:47 +0000 (18:49 +0000)]
Merges the cln-test branch into the main branch.

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.

14 years agore-generated comment headers of source files
Morgan Deters [Fri, 2 Jul 2010 00:30:19 +0000 (00:30 +0000)]
re-generated comment headers of source files

14 years agoroll back a small change that made arith fail some asserts
Morgan Deters [Fri, 2 Jul 2010 00:27:49 +0000 (00:27 +0000)]
roll back a small change that made arith fail some asserts

14 years ago* Added white-box TheoryEngine test that tests the rewriter
Morgan Deters [Fri, 2 Jul 2010 00:09:52 +0000 (00:09 +0000)]
* Added white-box TheoryEngine test that tests the rewriter

* 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

14 years agoadd documentation for additional clarity, re-add addTerm()
Morgan Deters [Wed, 30 Jun 2010 16:59:29 +0000 (16:59 +0000)]
add documentation for additional clarity, re-add addTerm()

14 years agoParsing support for SMT divisions: LRA, QF_UFLIA, QF_UFLRA, QF_UFNRA, UFNIA
Christopher L. Conway [Wed, 30 Jun 2010 16:23:47 +0000 (16:23 +0000)]
Parsing support for SMT divisions: LRA, QF_UFLIA, QF_UFLRA, QF_UFNRA, UFNIA

14 years agoAdding documentation for --strict-parsing (Closes: #166)
Christopher L. Conway [Wed, 30 Jun 2010 16:23:42 +0000 (16:23 +0000)]
Adding documentation for --strict-parsing (Closes: #166)

14 years agofix to switch fall-through; stats now off by default regardless of -d debugging optio...
Morgan Deters [Wed, 30 Jun 2010 15:26:13 +0000 (15:26 +0000)]
fix to switch fall-through; stats now off by default regardless of -d debugging options; thanks Chris for spoting this

14 years agochecking in CC module interface for reference.
Morgan Deters [Wed, 30 Jun 2010 13:56:07 +0000 (13:56 +0000)]
checking in CC module interface for reference.

14 years agoSupport for failing .smt and .smt2 regressions (and other examples with
Morgan Deters [Wed, 30 Jun 2010 13:35:53 +0000 (13:35 +0000)]
Support for failing .smt and .smt2 regressions (and other examples with
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.

14 years ago* theory "tree" rewriting implemented and works
Morgan Deters [Wed, 30 Jun 2010 11:12:14 +0000 (11:12 +0000)]
* theory "tree" rewriting implemented and works

* 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.

14 years agoadd --default-expr-depth=N command line parameter, expose setdepth() to public interface
Morgan Deters [Tue, 29 Jun 2010 22:42:40 +0000 (22:42 +0000)]
add --default-expr-depth=N command line parameter, expose setdepth() to public interface

14 years agoThis commit merges the decaying-rows branch into the main trunk.
Tim King [Tue, 29 Jun 2010 22:01:30 +0000 (22:01 +0000)]
This commit merges the decaying-rows branch into the main trunk.

14 years agoUpdate to stats.h is now back into the trunk. The code should compile once again.
Tim King [Tue, 29 Jun 2010 20:58:44 +0000 (20:58 +0000)]
Update to stats.h is now back into the trunk.  The code should compile once again.

14 years agoMerging the unate-propagator branch into the trunk. This is a big update so expect...
Tim King [Tue, 29 Jun 2010 20:53:47 +0000 (20:53 +0000)]
Merging the unate-propagator branch into the trunk.  This is a big update so 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.

14 years ago* Add CDMap<>::insertAtContextLevelZero(k, d) for inserting "initializing"
Morgan Deters [Tue, 29 Jun 2010 00:49:38 +0000 (00:49 +0000)]
* Add CDMap<>::insertAtContextLevelZero(k, d) for inserting "initializing"
  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().

14 years agoAdded post_mortem.py a statistics collector for user with the smt_curnch cluster...
Tim King [Thu, 24 Jun 2010 15:12:46 +0000 (15:12 +0000)]
Added post_mortem.py a statistics collector for user with the smt_curnch cluster. Also a spelling correction for the statistic theory::conflict.

14 years agoMade ~Stat() virtual. Added some additional statistics. And added some documentation.
Tim King [Tue, 22 Jun 2010 17:25:14 +0000 (17:25 +0000)]
Made ~Stat() virtual. Added some additional statistics. And added some documentation.

14 years ago"statistics" and "staticbinary" are now tags on the build (so you get build directori...
Morgan Deters [Fri, 18 Jun 2010 23:09:29 +0000 (23:09 +0000)]
"statistics" and "staticbinary" are now tags on the build (so you get build directories like builds/x86_64-unknown-linux-gnu/debug-staticbinary-nostatistics .. etc.  This is useful to distinguish static binary builds and statistics builds from each other when you configure multiple times in the same source directory

14 years agoMerging the statistics branch into the main trunk. I'll go over how to use this Tuesd...
Tim King [Fri, 18 Jun 2010 22:24:59 +0000 (22:24 +0000)]
Merging the statistics branch into the main trunk. I'll go over how to use this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating.

14 years agobug fix (unreported on bugzilla): skolem variables failing removal from pool
Morgan Deters [Fri, 18 Jun 2010 05:40:35 +0000 (05:40 +0000)]
bug fix (unreported on bugzilla): skolem variables failing removal from pool

14 years agofix some minor annoyances in the regression test Makefiles; add some documentation
Morgan Deters [Thu, 17 Jun 2010 18:05:04 +0000 (18:05 +0000)]
fix some minor annoyances in the regression test Makefiles; add some documentation

14 years agoAdded the experimental. +bool TheoryArith::AssertEquality(TNode n, TNode original){
Tim King [Wed, 16 Jun 2010 22:29:44 +0000 (22:29 +0000)]
Added the experimental. +bool TheoryArith::AssertEquality(TNode n, TNode original){

14 years agoMore assorted changes to arithmetic in preparation for the code review.
Tim King [Wed, 16 Jun 2010 21:19:34 +0000 (21:19 +0000)]
More assorted changes to arithmetic in preparation for the code review.

14 years agoThis commit just contains miscellaneous arithmetic cleanup.
Tim King [Wed, 16 Jun 2010 20:26:14 +0000 (20:26 +0000)]
This commit just contains miscellaneous arithmetic cleanup.

14 years agofix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)
Morgan Deters [Tue, 15 Jun 2010 22:05:46 +0000 (22:05 +0000)]
fix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)

14 years agoremove warnings about unknown #pragma GCC diagnostic on older compilers
Morgan Deters [Tue, 15 Jun 2010 21:46:56 +0000 (21:46 +0000)]
remove warnings about unknown #pragma GCC diagnostic on older compilers

14 years agoI made a documentation change to get() to make explicit the contract requirements...
Tim King [Tue, 15 Jun 2010 16:36:49 +0000 (16:36 +0000)]
I made a documentation change to get() to make explicit the contract requirements for 'slurping the queue'. Closes bug 154

14 years ago(minor) fix for file documentation
Morgan Deters [Tue, 15 Jun 2010 15:55:22 +0000 (15:55 +0000)]
(minor) fix for file documentation

14 years agoAdding array select/store to SMT v1 and v2 parsers
Christopher L. Conway [Mon, 14 Jun 2010 20:45:11 +0000 (20:45 +0000)]
Adding array select/store to SMT v1 and v2 parsers

14 years agoFix to arith to make sure it only attempts to report 1 conflict per check() call.
Tim King [Mon, 14 Jun 2010 18:35:17 +0000 (18:35 +0000)]
Fix to arith to make sure it only attempts to report 1 conflict per check() call.

14 years agoStarted work on array theory
Clark Barrett [Mon, 14 Jun 2010 16:06:51 +0000 (16:06 +0000)]
Started work on array theory