cvc5.git
14 years agofix statistics-registry-related memory leaks
Morgan Deters [Tue, 21 Sep 2010 21:51:25 +0000 (21:51 +0000)]
fix statistics-registry-related memory leaks

14 years agopart of review (bug #197): coding conventions, file-level documentation, re-ran updat...
Morgan Deters [Tue, 21 Sep 2010 21:50:26 +0000 (21:50 +0000)]
part of review (bug #197): coding conventions, file-level documentation, re-ran update-copyright.pl, etc.

14 years agosvn:ignore properties for new bv stuff
Morgan Deters [Tue, 21 Sep 2010 21:37:30 +0000 (21:37 +0000)]
svn:ignore properties for new bv stuff

14 years agosome code cleanup, documentation, review of "kinded-iterator" code, and addition...
Morgan Deters [Tue, 21 Sep 2010 21:36:22 +0000 (21:36 +0000)]
some code cleanup, documentation, review of "kinded-iterator" code, and addition of a unit test

14 years agoiterators for tim, begin<PLUS>() and end<PLUS>() should give him what he wants
Dejan Jovanović [Tue, 21 Sep 2010 17:33:06 +0000 (17:33 +0000)]
iterators for tim, begin<PLUS>() and end<PLUS>() should give him what he wants

14 years agoRm'ing Makefile.in's
Christopher L. Conway [Tue, 21 Sep 2010 16:36:48 +0000 (16:36 +0000)]
Rm'ing Makefile.in's

14 years agoMoving automatic type check to NodeBuilder (Fixes: #199)
Christopher L. Conway [Tue, 21 Sep 2010 16:36:42 +0000 (16:36 +0000)]
Moving automatic type check to NodeBuilder (Fixes: #199)

14 years agohooking up the bitvector tests
Dejan Jovanović [Mon, 20 Sep 2010 16:47:38 +0000 (16:47 +0000)]
hooking up the bitvector tests

14 years agobitvector rewriting for the core theory and testcases
Dejan Jovanović [Mon, 20 Sep 2010 01:08:32 +0000 (01:08 +0000)]
bitvector rewriting for the core theory and testcases

14 years agoBug fix to CVC4::theory::arith::VarList as well as some superficial changes. test...
Tim King [Thu, 16 Sep 2010 21:16:59 +0000 (21:16 +0000)]
Bug fix to CVC4::theory::arith::VarList as well as some superficial changes. test/regress/regress0/arith/arith.03.cvc now passes and is turned on by default.  Tiny documentation fix for the arithmetic normal form.

14 years ago* added test/regress/regress0/arith for easy arithmetic regress tests.
Tim King [Tue, 14 Sep 2010 19:37:31 +0000 (19:37 +0000)]
* added test/regress/regress0/arith for easy arithmetic regress tests.

14 years agoensure uf/congruence closure debugging stuff isn't called in production builds
Morgan Deters [Tue, 14 Sep 2010 03:22:51 +0000 (03:22 +0000)]
ensure uf/congruence closure debugging stuff isn't called in production builds

14 years agomake Node iterators more STL-friendly, resolves bug #196
Morgan Deters [Mon, 13 Sep 2010 23:35:30 +0000 (23:35 +0000)]
make Node iterators more STL-friendly, resolves bug #196

14 years agobuild system consistency in target names for unit test targets
Morgan Deters [Mon, 13 Sep 2010 23:34:47 +0000 (23:34 +0000)]
build system consistency in target names for unit test targets

14 years agostatistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is given
Morgan Deters [Mon, 13 Sep 2010 22:13:36 +0000 (22:13 +0000)]
statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is given

14 years agolink TAGS file into builds/ directory, when built. Resolves bug #195
Morgan Deters [Mon, 13 Sep 2010 17:27:15 +0000 (17:27 +0000)]
link TAGS file into builds/ directory, when built.  Resolves bug #195

14 years ago* New normal form for arithmetic is in place.
Tim King [Mon, 13 Sep 2010 16:08:21 +0000 (16:08 +0000)]
* New normal form for arithmetic is in place.
* src/theory/arith/normal_form.{h,cpp} contains the description for the new
  normal form as well as utilities for dealing with the normal form.
* src/theory/arith/next_arith_rewriter.{h,cpp} contains the new rewriter.
  The new rewriter implements preRewrite() and postRewrite() for arithmetic.
* src/theory/arith/arith_rewriter.{h,cpp} have been removed.
* TheoryArith::rewrite() has been removed.
* Arithmetic with the new normal form outperforms the trunk where the branch
  occurred (-r797) on 46% of the examples in QF_LRA. (33% have no noticeable
  difference.) Some important optimizations are stilling pending to the code
  for handling the new normal form. (Bug 196.)

14 years ago"Leftist NodeBuilders" are now supported.
Morgan Deters [Thu, 2 Sep 2010 09:05:26 +0000 (09:05 +0000)]
"Leftist NodeBuilders" are now supported.

That is, "nb << a << b << c << OR << d << AND" turns into
  (AND (OR a b c) d)

The rule is:  pushing a kind onto a NodeBuilder with a nonzero
number of child Nodes in it, the action "collapses" it.  If a
kind is already associated to the NodeBuilder, it is an error.

Thus:
  NodeBuilder<> nb(AND); nb << AND;
and
  NodeBuilder<> nb; nb << AND << OR;
are both errors (if assertions are on).

In reality, though, the implementation is trickier, as the collapsing
is done lazily on the following push.  This complicates things a bit,
but by placing an Assert(false), I found that we aren't depending on
the old behavior (at least for any unit tests or regressions in the
source tree).  The Assert(false) is now removed and leftist
NodeBuilders are in business.

Fixes bug 101.

14 years agorecategorize eq_diamond14 as a regress2 test (instead of regress0)
Morgan Deters [Thu, 2 Sep 2010 08:24:12 +0000 (08:24 +0000)]
recategorize eq_diamond14 as a regress2 test (instead of regress0)

14 years agofix an error in TimerStat
Morgan Deters [Thu, 2 Sep 2010 08:16:28 +0000 (08:16 +0000)]
fix an error in TimerStat

14 years agoneglected build system update from r848 (last commit)
Morgan Deters [Thu, 2 Sep 2010 07:32:00 +0000 (07:32 +0000)]
neglected build system update from r848 (last commit)

14 years ago* add TimerStat statistic type
Morgan Deters [Thu, 2 Sep 2010 07:31:04 +0000 (07:31 +0000)]
* add TimerStat statistic type
* add Stats black-box unit test
* new make target: "make units" now runs unit tests only
* revised make target: "make regress" now runs regressions only
* configure.ac: pull in librt for clock_gettime()

14 years ago"make check" now places binaries in the proper place before doing the checks; this...
Morgan Deters [Wed, 1 Sep 2010 22:24:55 +0000 (22:24 +0000)]
"make check" now places binaries in the proper place before doing the checks; this closes bug 46 finally, though the major annoyances related to this bug already had been fixed long ago

14 years agoreflect in build strings that -gmp is now the default and -cln is an option
Morgan Deters [Wed, 1 Sep 2010 22:20:43 +0000 (22:20 +0000)]
reflect in build strings that -gmp is now the default and -cln is an option

14 years agoadded documentation, closes bug 97
Morgan Deters [Wed, 1 Sep 2010 21:02:07 +0000 (21:02 +0000)]
added documentation, closes bug 97

14 years agoMaking GMP default, CLN opt-in with --with-cln
Christopher L. Conway [Tue, 24 Aug 2010 17:09:40 +0000 (17:09 +0000)]
Making GMP default, CLN opt-in with --with-cln

14 years agoupdating the minisat restart parameters after running some experiments
Dejan Jovanović [Fri, 20 Aug 2010 18:23:53 +0000 (18:23 +0000)]
updating the minisat restart parameters after running some experiments

14 years agoturn off extra-checking (which does extra theory-rewriter checking); it was enabled...
Morgan Deters [Fri, 20 Aug 2010 00:00:09 +0000 (00:00 +0000)]
turn off extra-checking (which does extra theory-rewriter checking); it was enabled by mistake in the last commit

14 years agoUF theory bug fixes, code cleanup, and extra debugging output.
Morgan Deters [Thu, 19 Aug 2010 23:49:58 +0000 (23:49 +0000)]
UF theory bug fixes, code cleanup, and extra debugging output.
Enabled new UF theory by default.

Added some UF regressions.

Some work on the whole equality-over-bool-removed-in-favor-of-IFF
thing.  (Congruence closure module and other things have to handle
IFF as a special case of equality, etc..)

Added pre-rewriting to TheoryBool which rewrites:

  * (IFF true x)          =>  x
  * (IFF false x)         =>  (NOT x)
  * (IFF x true)          =>  x
  * (IFF x false)         =>  (NOT x)
  * (IFF x x)             =>  true
  * (IFF x (NOT x))       =>  false
  * (IFF (NOT x) x)       =>  false

  * (ITE true x y)        =>  x
  * (ITE false x y)       =>  y
  * (ITE cond x x)        =>  x

Added post-rewriting that does all of the above, plus normalize IFF and ITE:

  * (IFF x y)             =>  (IFF y x), if y < x
  * (ITE (NOT cond) x y)  =>  (ITE cond y x)

(Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.)

A little more debugging output from CNF stream, context pushes/pops,
ITE removal.

Some more documentation.

Fixed some typos.

14 years agomore tests, configuration for UF
Morgan Deters [Wed, 18 Aug 2010 03:59:26 +0000 (03:59 +0000)]
more tests, configuration for UF

14 years agoMerge from "cc" branch:
Morgan Deters [Tue, 17 Aug 2010 22:24:26 +0000 (22:24 +0000)]
Merge from "cc" branch:

CongruenceClosure implementation; CongruenceClosure white-box test.

New UF theory implementation based on new CC module.  This one
supports predicates.  The two UF implementations exist in parallel
(they can be selected at runtime via the new command line option
"--uf").

Added type infrastructure for TUPLE.

Fixes to unit tests that failed in 16-August-2010 regressions.
Needed to instantiate TheoryEngine with an Options structure, and
explicitly call ->shutdown() on it before destruction (like the
SMTEngine does).

Fixed test makefiles to (1) perform all tests even in the presence of
failures, (2) give proper summaries of subdirectory tests
(e.g. regress0/uf and regress0/precedence)

Other minor changes.

14 years agoAdd "no trash" CDMap elements, so that CDMap elements can themselves
Morgan Deters [Tue, 17 Aug 2010 05:06:09 +0000 (05:06 +0000)]
Add "no trash" CDMap elements, so that CDMap elements can themselves
be allocated in context memory.  CDMap black-box test extended.

14 years agoChange TheoryEngine to use pointers to theories instead of
Morgan Deters [Tue, 17 Aug 2010 05:05:54 +0000 (05:05 +0000)]
Change TheoryEngine to use pointers to theories instead of
calling them directly.  In tests this doesn't appear to
lead to slowdown.

14 years agoadd zlib checks to configure (new minisat requires it?)
Morgan Deters [Mon, 16 Aug 2010 22:07:05 +0000 (22:07 +0000)]
add zlib checks to configure (new minisat requires it?)

14 years agoFixing failures in minisat
Dejan Jovanović [Mon, 16 Aug 2010 21:49:42 +0000 (21:49 +0000)]
Fixing failures in minisat

14 years ago(no commit message)
Dejan Jovanović [Sun, 15 Aug 2010 21:35:42 +0000 (21:35 +0000)]

14 years ago(no commit message)
Dejan Jovanović [Sun, 15 Aug 2010 21:25:21 +0000 (21:25 +0000)]

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);