cvc5.git
13 years agofix up more documentation
Morgan Deters [Fri, 16 Sep 2011 21:32:37 +0000 (21:32 +0000)]
fix up more documentation

13 years agosome minor fixes to the cvc3 compatibility library and test case
Morgan Deters [Fri, 16 Sep 2011 21:30:27 +0000 (21:30 +0000)]
some minor fixes to the cvc3 compatibility library and test case

13 years agonew, improved doxygen config file
Morgan Deters [Fri, 16 Sep 2011 20:53:36 +0000 (20:53 +0000)]
new, improved doxygen config file

13 years agofix serious issue with copyright-updating script
Morgan Deters [Fri, 16 Sep 2011 20:53:19 +0000 (20:53 +0000)]
fix serious issue with copyright-updating script

13 years agofix numerous documentation issues; doxygen complains much less, now
Morgan Deters [Fri, 16 Sep 2011 20:53:00 +0000 (20:53 +0000)]
fix numerous documentation issues; doxygen complains much less, now

13 years agofix an oversight in the language printers
Morgan Deters [Fri, 16 Sep 2011 20:49:58 +0000 (20:49 +0000)]
fix an oversight in the language printers

13 years agofix debian build without breaking anything (i hope)
Morgan Deters [Fri, 16 Sep 2011 20:19:25 +0000 (20:19 +0000)]
fix debian build without breaking anything (i hope)

13 years agotim's fixes for context-dependent pre-registration
Dejan Jovanović [Thu, 15 Sep 2011 21:48:42 +0000 (21:48 +0000)]
tim's fixes for context-dependent pre-registration

13 years agoadding --show-debug-tags to list all available debug tracing tags
Dejan Jovanović [Thu, 15 Sep 2011 18:17:11 +0000 (18:17 +0000)]
adding --show-debug-tags to list all available debug tracing tags

13 years agoadditional stuff for sharing,
Dejan Jovanović [Thu, 15 Sep 2011 06:53:33 +0000 (06:53 +0000)]
additional stuff for sharing,

13 years agofixes for uf/equality engine from the quantifiers branch. mainly backtracking issues.
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.

13 years agothis should fix the build; doxygen documentation now gets built in srcdir/doc/doxygen
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

13 years agoDisable a warning to address bug 277. (This doesn't really resolve the issue, but...
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.)

13 years agoremoving an assert i forgot to remove that andy found
Dejan Jovanović [Sat, 3 Sep 2011 00:42:34 +0000 (00:42 +0000)]
removing an assert i forgot to remove that andy found

13 years agoMerge from my post-smtcomp branch. Includes:
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.

13 years agoEnsure that assignment gestures through CDMap iterators like:
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.

13 years agoPartial merge of integers work; this is simple B&B and some pseudoboolean
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.

13 years ago* Changing pre-registration to be context dependent -- it is called from the SAT...
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

13 years agoFixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK will be...
Dejan Jovanović [Tue, 30 Aug 2011 02:19:58 +0000 (02:19 +0000)]
Fixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK will be reissued. Some unexpected slowdowns, but not too much.

13 years agoRemoving Theory::registerTerm() as discussed in the meeting. Now pre-register is...
Dejan Jovanović [Sat, 27 Aug 2011 00:33:22 +0000 (00:33 +0000)]
Removing Theory::registerTerm() as discussed in the meeting. Now pre-register is called on all the theory terms and the foreign-terms also. This means, if x: REAL and f:REAL, that in f(x) >= 0, arithmetic gets pre-register call with x, f(x) and f(x) >= 0, while UF gets pre-register call with x, f(x).

13 years agoFixing the broken unit tests
Dejan Jovanović [Thu, 25 Aug 2011 18:36:46 +0000 (18:36 +0000)]
Fixing the broken unit tests

13 years agoSimplification of the preregister and register throught a NodeVisitor class. The...
Dejan Jovanović [Wed, 24 Aug 2011 21:03:19 +0000 (21:03 +0000)]
Simplification of the preregister and register throught a NodeVisitor class. The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class.

13 years agosome uf cleanup
Dejan Jovanović [Tue, 23 Aug 2011 23:43:01 +0000 (23:43 +0000)]
some uf cleanup

13 years agonew implementation of lemmas on demand
Dejan Jovanović [Wed, 17 Aug 2011 15:20:19 +0000 (15:20 +0000)]
new implementation of lemmas on demand
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>

13 years agoforgot to reflect naming change in makefile. fixed
Morgan Deters [Tue, 12 Jul 2011 22:46:57 +0000 (22:46 +0000)]
forgot to reflect naming change in makefile.  fixed

13 years agofix bug 272, array unsoundness, and some array cleanup
Morgan Deters [Tue, 12 Jul 2011 22:42:15 +0000 (22:42 +0000)]
fix bug 272, array unsoundness, and some array cleanup

13 years agoremove some array regressions from "make check" so nightly regressions run
Morgan Deters [Mon, 11 Jul 2011 23:14:25 +0000 (23:14 +0000)]
remove some array regressions from "make check" so nightly regressions run

13 years agostatus of examples
Morgan Deters [Mon, 11 Jul 2011 20:42:39 +0000 (20:42 +0000)]
status of examples

13 years agonew array bugs ?
Morgan Deters [Mon, 11 Jul 2011 20:41:28 +0000 (20:41 +0000)]
new array bugs ?

13 years agofixing out of place typename (error on g++ 4.4.3-4ubuntu5)
Morgan Deters [Mon, 11 Jul 2011 20:06:20 +0000 (20:06 +0000)]
fixing out of place typename (error on g++ 4.4.3-4ubuntu5)

13 years agosubmission script
Morgan Deters [Mon, 11 Jul 2011 20:00:47 +0000 (20:00 +0000)]
submission script

13 years agoAdding static_fact_manager
Clark Barrett [Mon, 11 Jul 2011 20:00:29 +0000 (20:00 +0000)]
Adding static_fact_manager

13 years agoClark's work on array theory - can now solve all QF_AX problems
Clark Barrett [Mon, 11 Jul 2011 19:53:44 +0000 (19:53 +0000)]
Clark's work on array theory - can now solve all QF_AX problems

13 years agofix some confusing debug output (bogus counter)
Morgan Deters [Mon, 11 Jul 2011 19:34:01 +0000 (19:34 +0000)]
fix some confusing debug output (bogus counter)

13 years agomark the new minimized benchmark as unsat
Morgan Deters [Mon, 11 Jul 2011 18:50:44 +0000 (18:50 +0000)]
mark the new minimized benchmark as unsat

13 years agoif running in QF_AX, equalities over terms of uninterpreted sort go to arrays, as...
Morgan Deters [Mon, 11 Jul 2011 18:48:16 +0000 (18:48 +0000)]
if running in QF_AX, equalities over terms of uninterpreted sort go to arrays, as well as pre-registration of free constants of uninterpreted sort, etc..

13 years agominimized example
Morgan Deters [Mon, 11 Jul 2011 16:53:50 +0000 (16:53 +0000)]
minimized example

13 years agoarray benchmarks
Morgan Deters [Mon, 11 Jul 2011 16:38:38 +0000 (16:38 +0000)]
array benchmarks

13 years agoadding disequality propagation
Dejan Jovanović [Mon, 11 Jul 2011 12:45:16 +0000 (12:45 +0000)]
adding disequality propagation

relevant comparison http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2602&reference_id=2590&p=5

13 years agomerge from symmetry branch
Morgan Deters [Mon, 11 Jul 2011 03:33:14 +0000 (03:33 +0000)]
merge from symmetry branch

13 years agoReverting mistaken check-in
Clark Barrett [Sun, 10 Jul 2011 19:41:04 +0000 (19:41 +0000)]
Reverting mistaken check-in

13 years agochanging the sat solver remove clauses constants
Dejan Jovanović [Sun, 10 Jul 2011 17:23:29 +0000 (17:23 +0000)]
changing the sat solver remove clauses constants
with these we get closer to yices on uf and it seems better on lra

vs yices uf http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2590&category=&p=5&reference_id=1471
vs trunk on lra http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2591&category=&p=5&reference_id=2576

13 years agoFixed bug in default solve - wasn't returning when it was supposed to
Clark Barrett [Sun, 10 Jul 2011 16:57:38 +0000 (16:57 +0000)]
Fixed bug in default solve - wasn't returning when it was supposed to

13 years agoanother typo
Dejan Jovanović [Sun, 10 Jul 2011 12:48:42 +0000 (12:48 +0000)]
another typo

13 years agoyet another uf bug fix, hopefully the last
Dejan Jovanović [Sun, 10 Jul 2011 12:32:13 +0000 (12:32 +0000)]
yet another uf bug fix, hopefully the last

13 years agoanother bugfix for uf
Dejan Jovanović [Sun, 10 Jul 2011 12:05:47 +0000 (12:05 +0000)]
another bugfix for uf

13 years agosome immediate bug fixes
Dejan Jovanović [Sat, 9 Jul 2011 05:40:21 +0000 (05:40 +0000)]
some immediate bug fixes

13 years agofix submission makefile
Morgan Deters [Sat, 9 Jul 2011 03:11:58 +0000 (03:11 +0000)]
fix submission makefile

13 years agominor fixups
Morgan Deters [Sat, 9 Jul 2011 02:35:19 +0000 (02:35 +0000)]
minor fixups

13 years agosurprize surprize
Dejan Jovanović [Sat, 9 Jul 2011 01:38:48 +0000 (01:38 +0000)]
surprize surprize

13 years agoremoving duplicate clauses in ite cnf conversion
Dejan Jovanović [Thu, 7 Jul 2011 14:03:14 +0000 (14:03 +0000)]
removing duplicate clauses in ite cnf conversion

13 years agocudd-building prefs with --with-cudd / --without-cudd
Morgan Deters [Thu, 7 Jul 2011 05:31:13 +0000 (05:31 +0000)]
cudd-building prefs with --with-cudd / --without-cudd

13 years agoFixing two bugs:
Dejan Jovanović [Wed, 6 Jul 2011 23:42:04 +0000 (23:42 +0000)]
Fixing two bugs:

1) arithmetic should check for subterms when solving equations, for instance x = if b then x + 1 else x -1 is not a valid substitution
2) a memory problem in minisat - explanations are constructed during conflict analysis, so the clause database might resize and relocate, which invalidates any references to clauses

13 years agomissing test case
Dejan Jovanović [Tue, 5 Jul 2011 17:56:45 +0000 (17:56 +0000)]
missing test case

13 years agoupdated preprocessing and rewriting input equalities into inequalities for LRA
Dejan Jovanović [Tue, 5 Jul 2011 16:21:50 +0000 (16:21 +0000)]
updated preprocessing and rewriting input equalities into inequalities for LRA

13 years agoAllow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),
Morgan Deters [Thu, 30 Jun 2011 21:03:52 +0000 (21:03 +0000)]
Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),
when --strict-parsing is off (which it is by default).  The danoint benchmarks
have such monsters.

13 years agoChanged the defaults for arithPivotThreshold and arithPropagateMaxLength to 16. Enabl...
Tim King [Thu, 30 Jun 2011 19:06:57 +0000 (19:06 +0000)]
Changed the defaults for arithPivotThreshold and arithPropagateMaxLength to 16. Enabled arithmetic propagation and variable removal by default. Changed the command line arguments for both propagation and variable removal allow for disabling these.

13 years agoMerging the playground branch upto r1957 into trunk.
Tim King [Thu, 30 Jun 2011 18:40:29 +0000 (18:40 +0000)]
Merging the playground branch upto r1957 into trunk.

13 years agoonly use theory registration if (1) a theory requests it, or (2) if there's more...
Morgan Deters [Thu, 30 Jun 2011 06:06:30 +0000 (06:06 +0000)]
only use theory registration if (1) a theory requests it, or (2) if there's more than one "real" theory (not BUILTIN or BOOL) active

13 years agosome things I had laying around in a directory but never got committed; minor fix...
Morgan Deters [Thu, 30 Jun 2011 03:56:58 +0000 (03:56 +0000)]
some things I had laying around in a directory but never got committed; minor fix-ups to documentation and some node stuff

13 years agoFixed spelling mistake and documentation for --enable-variable-removal.
Tim King [Wed, 29 Jun 2011 19:32:04 +0000 (19:32 +0000)]
Fixed spelling mistake and documentation for --enable-variable-removal.

13 years agoSome fixes inspired by Fedora 15:
Morgan Deters [Sat, 18 Jun 2011 02:44:41 +0000 (02:44 +0000)]
Some fixes inspired by Fedora 15:
* 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

13 years agocompilation fix for x86 (from previous commit)
Morgan Deters [Mon, 6 Jun 2011 22:12:21 +0000 (22:12 +0000)]
compilation fix for x86 (from previous commit)

13 years agoFix for Mac OS breakage (x86 didn't crash, but probably would, eventually, on some...
Morgan Deters [Mon, 6 Jun 2011 21:37:23 +0000 (21:37 +0000)]
Fix for Mac OS breakage (x86 didn't crash, but probably would, eventually, on some problems---valgrind gave many complaints): the problem was that calloc() (in the Backtracker) wasn't allocating enough space for the type located at the resulting address.  Resolves bug #263.

Also, some debugging improvements.

13 years agofixed various bugs related to ambiguous parametric datatype constructors, parametric...
Andrew Reynolds [Fri, 3 Jun 2011 19:56:12 +0000 (19:56 +0000)]
fixed various bugs related to ambiguous parametric datatype constructors, parametric datatype versions of paper benchmarks are now working

13 years agodatatypes work
Morgan Deters [Fri, 3 Jun 2011 05:30:54 +0000 (05:30 +0000)]
datatypes work

13 years agominor fix to build system for system tests
Morgan Deters [Thu, 2 Jun 2011 22:17:56 +0000 (22:17 +0000)]
minor fix to build system for system tests

13 years agoadded (temporary) support for ensuring that all ambiguously typed constructor nodes...
Andrew Reynolds [Thu, 2 Jun 2011 15:23:16 +0000 (15:23 +0000)]
added (temporary) support for ensuring that all ambiguously typed constructor nodes created internally are given a type ascription

13 years agominor fix, and better output for type errors
Morgan Deters [Wed, 1 Jun 2011 01:13:21 +0000 (01:13 +0000)]
minor fix, and better output for type errors

13 years agotype ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]
Morgan Deters [Wed, 1 Jun 2011 00:49:37 +0000 (00:49 +0000)]
type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]

13 years agoThis commit contains the code for allowing arbitrary equalities in the theory of...
Tim King [Tue, 31 May 2011 01:06:16 +0000 (01:06 +0000)]
This commit contains the code for allowing arbitrary equalities in the theory of arithmetic.
* This code has been partially tested. (My testing situation is currently not so great.)  The code for testing not preregistering equalities can be compile time enabled by setting the boolean turnOffEqualityPreRegister. Don't be shocked by slowdowns or failures.  This does pass make regress as well as a fresh checkout does. (The Mac version has issues.)
* I need to disable the permanent row removal heuristic by default.  We need to discuss why this needs to happen.  We should probably detect pure QF_LRA/QF_RDL problems and enable this when this can safely be done.
* I have disabled the arithmetic rewrite equality flag.  This code needs to be added to the parser.
* For all of the above changes, I have annotated the code with the key word BREADCRUMB.
* I have renamed ArithUnatePropagator to ArithAtomDatabase.

13 years agofix unit test linking issue
Morgan Deters [Sat, 28 May 2011 06:44:07 +0000 (06:44 +0000)]
fix unit test linking issue

13 years agoinclude subversion information used for each build in the --show-config output and...
Morgan Deters [Sat, 28 May 2011 05:51:01 +0000 (05:51 +0000)]
include subversion information used for each build in the --show-config output and as a banner in --interactive mode; intended to resolve confusion in cases where you don't know where a CVC4 binary came from

13 years agoapply arithmetic static learner's miplibtrick in a consistent order (for easier repli...
Morgan Deters [Thu, 26 May 2011 05:04:34 +0000 (05:04 +0000)]
apply arithmetic static learner's miplibtrick in a consistent order (for easier replication of experiment)

13 years agofixes for "make dist" and "make doc", minor cleanups
Morgan Deters [Mon, 23 May 2011 23:15:25 +0000 (23:15 +0000)]
fixes for "make dist" and "make doc", minor cleanups

13 years agoMerge from arrays2 branch.
Morgan Deters [Mon, 23 May 2011 21:58:12 +0000 (21:58 +0000)]
Merge from arrays2 branch.

13 years agofix production-build compiler warning
Morgan Deters [Sat, 14 May 2011 19:51:41 +0000 (19:51 +0000)]
fix production-build compiler warning

13 years agore-add a removed Datatype constructor that was causing a unit test failure, so nightl...
Morgan Deters [Sat, 14 May 2011 03:38:18 +0000 (03:38 +0000)]
re-add a removed Datatype constructor that was causing a unit test failure, so nightlies go through tonight

13 years agoreverting node manager change from 1881; also part of parameterized datatypes review
Morgan Deters [Sat, 14 May 2011 00:17:20 +0000 (00:17 +0000)]
reverting node manager change from 1881; also part of parameterized datatypes review

13 years agoadd AscriptionType stuff to support nullary parameterized datatypes; also, review...
Morgan Deters [Sat, 14 May 2011 00:15:43 +0000 (00:15 +0000)]
add AscriptionType stuff to support nullary parameterized datatypes; also, review of Andy's earlier commit, with some minor code clean-up and documentation

13 years agoadded support for parametric datatypes, updated cvc parser to handle parametric datat...
Andrew Reynolds [Fri, 13 May 2011 22:02:52 +0000 (22:02 +0000)]
added support for parametric datatypes, updated cvc parser to handle parametric datatypes, type ascriptions are not implemented yet

13 years ago* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio
Morgan Deters [Fri, 13 May 2011 20:42:57 +0000 (20:42 +0000)]
* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio
  branch)
* add Theory::isSharedTermFact() -- it currently always returns false,
  pending theory combination work
* Add "unknown" cardinalities to Cardinality class
* Fix run_regression script to handle CRLF line terminators on Macs
  (where sed is non-GNU)
* Convert CRLF line terminators in datatypes regressions to LF

13 years agoDeleting dead code.
Tim King [Fri, 6 May 2011 21:23:38 +0000 (21:23 +0000)]
Deleting dead code.

13 years agoadded 10 benchmarks to regress/regress0/datatypes from paper
Andrew Reynolds [Fri, 6 May 2011 20:38:29 +0000 (20:38 +0000)]
added 10 benchmarks to regress/regress0/datatypes from paper

13 years agosignificant revisions/improvements to code for theory datatypes solver
Andrew Reynolds [Fri, 6 May 2011 20:17:57 +0000 (20:17 +0000)]
significant revisions/improvements to code for theory datatypes solver

13 years agoMerge from nonclausal-simplification-v2 branch:
Morgan Deters [Thu, 5 May 2011 22:23:50 +0000 (22:23 +0000)]
Merge from nonclausal-simplification-v2 branch:

* Preprocessing-time, non-clausal, Boolean simplification round to
  support "quasi-non-linear rewrites" as discussed at last few meetings.

* --simplification=none is the default for now, but we'll probably
  change that to --simplification=incremental.  --simplification=batch
  is also a possibility.  See --simplification=help for details.

* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.

13 years agoluby sequence generator; can use to plot MiniSat's restart sequence
Morgan Deters [Thu, 5 May 2011 21:34:52 +0000 (21:34 +0000)]
luby sequence generator; can use to plot MiniSat's restart sequence

13 years agoStronger support for zero-performance-penalty output, and fixes and
Morgan Deters [Wed, 4 May 2011 00:21:34 +0000 (00:21 +0000)]
Stronger support for zero-performance-penalty output, and fixes and
simplifications for the "muzzled" (i.e. competition) design, which had
been broken.  Addition of some new unit test bits to ensure that
nothing is ever called in muzzled builds, e.g. things like

  Warning() << expensiveFunction();

Also, fix some compiler warnings.

13 years agooutput fixes for performance
Morgan Deters [Tue, 3 May 2011 04:33:09 +0000 (04:33 +0000)]
output fixes for performance

13 years agominor updates to exp manager, fixed 32bit vs 64bit issues in transitive closure modul...
Andrew Reynolds [Mon, 2 May 2011 21:40:06 +0000 (21:40 +0000)]
minor updates to exp manager, fixed 32bit vs 64bit issues in transitive closure module, theory datatypes now uses transitive closure for cycle detection, bug 261 fixed

13 years agofix for configure
Morgan Deters [Mon, 2 May 2011 21:22:13 +0000 (21:22 +0000)]
fix for configure

13 years agoadding some previously-failing "bug" test cases for bitvectors
Morgan Deters [Mon, 2 May 2011 20:19:55 +0000 (20:19 +0000)]
adding some previously-failing "bug" test cases for bitvectors

13 years agoupdating bv regressions
Dejan Jovanović [Mon, 2 May 2011 19:46:06 +0000 (19:46 +0000)]
updating bv regressions

13 years agoparser fixes for bug 243
Dejan Jovanović [Mon, 2 May 2011 19:45:08 +0000 (19:45 +0000)]
parser fixes for bug 243

13 years agoupdates for bitvectors
Dejan Jovanović [Mon, 2 May 2011 19:09:11 +0000 (19:09 +0000)]
updates for bitvectors

13 years agomore minor fixes related to last few commits
Morgan Deters [Mon, 2 May 2011 16:06:19 +0000 (16:06 +0000)]
more minor fixes related to last few commits

13 years agoanother small fix
Morgan Deters [Mon, 2 May 2011 15:00:42 +0000 (15:00 +0000)]
another small fix

13 years agofix broken build; sorry, all!
Morgan Deters [Mon, 2 May 2011 14:55:24 +0000 (14:55 +0000)]
fix broken build; sorry, all!

13 years agofix a performance issue from last commit
Morgan Deters [Mon, 2 May 2011 05:31:00 +0000 (05:31 +0000)]
fix a performance issue from last commit

13 years agoMinor fixes to various parts of CVC4, including the removal of the uintptr_t construc...
Morgan Deters [Mon, 2 May 2011 05:04:36 +0000 (05:04 +0000)]
Minor fixes to various parts of CVC4, including the removal of the uintptr_t constructors for Type and Expr (which existed due to ANTLR limitations).  These issues are now handled (as a hack, due to said limitations) in the parser rather than the CVC4 core.