cvc5.git
14 years agoImplementing missing NodeBuilder::constructNode
Christopher L. Conway [Thu, 15 Apr 2010 17:26:29 +0000 (17:26 +0000)]
Implementing missing NodeBuilder::constructNode

14 years agoEnhancements to NodeManager tests, taking advantage of new Type implementation
Christopher L. Conway [Thu, 15 Apr 2010 16:56:11 +0000 (16:56 +0000)]
Enhancements to NodeManager tests, taking advantage of new Type implementation

14 years agoRemoving horrible, system-locking option from Eclipse Make preferences.
Christopher L. Conway [Thu, 15 Apr 2010 16:56:09 +0000 (16:56 +0000)]
Removing horrible, system-locking option from Eclipse Make preferences.

14 years agoMoving debug output in ~ContextObj under a conditional. Should fix most of the slowdo...
Christopher L. Conway [Thu, 15 Apr 2010 16:56:06 +0000 (16:56 +0000)]
Moving debug output in ~ContextObj under a conditional. Should fix most of the slowdown from r413.

14 years agoMarging from types 404:415, changes: Massive
Dejan Jovanović [Wed, 14 Apr 2010 19:06:53 +0000 (19:06 +0000)]
Marging from types 404:415, changes: Massive

* Types are now represented as nodes in the attribute table and are managed, i.e. you can say
    Type booleanType = d_nodeManager->booleanType();
    Type t = d_nodeManager->mkFunctionType(booleanType, booleanType);
    FunctionType ft = (FunctionType)t;
    Assert(ft.getArgTypes()[0], booleanType);
* The attributes now have a table for Nodes and a table for TNodes (both should be used with caution)
* Changes the way nodes are extracted from NodeBuilder, added several methods to
  extract a Node, NodeValue, or Node*, with corresponding methods for extraction
* Used the above in the construction of Expr and Type objects
* The NodeManager now destroys the attributes in the destructor by pausing the
  garbage collection
* To achive destruction a flag d_inDesctruction has been added to loosen the assertion
  in NodeValue::dec() (there might be -refcount TNodes leftover)
* Beginnings of the Bitvector constants using GMP

Not yet in tiptop phase, needs more documentation, and Types should be pulled out to TypeNodes eventually. Also, the types are currently defined in the builting_kinds, and I need to add these to the theory specific definitions with special 'type' constructs.

I hate branching and merging.

14 years ago* Better dependency tracking for unit test building and linking, and
Morgan Deters [Wed, 14 Apr 2010 06:21:26 +0000 (06:21 +0000)]
* Better dependency tracking for unit test building and linking, and
  auto-generated headers (metakind.h etc.), so they don't have to be
  recompiled every time.  This drastically improves build time when
  only small updates are made.

* Added "memory.h" unit test header for checking out-of-memory
  conditions.  cdlist_black uses it.

* Added helpful output when you "make lcov" in a non-coverage-enabled
  build.

* Removed strict aliasing warning when compiling metakind.h header
  with optimization on.

* Removed const version of NodeBuilder::operator Node()---it was
  poorly performing, better to not permit it---and fixed the
  convenience builders to use the non-const version
  (re: code review #63)

* Color-coded test output on capable terminals.

* Fixed some warnings in unit tests.

14 years agoMerging from branches/decl-scopes (r401:411)
Christopher L. Conway [Tue, 13 Apr 2010 22:50:07 +0000 (22:50 +0000)]
Merging from branches/decl-scopes (r401:411)

14 years agoDoxygen fixes
Christopher L. Conway [Tue, 13 Apr 2010 22:50:03 +0000 (22:50 +0000)]
Doxygen fixes

14 years agominor fixes to lcov build target, better contextobj testing
Morgan Deters [Fri, 9 Apr 2010 18:46:16 +0000 (18:46 +0000)]
minor fixes to lcov build target, better contextobj testing

14 years agoadded experimental "make lcov" target (it runs only unit tests); better coverage...
Morgan Deters [Fri, 9 Apr 2010 16:25:32 +0000 (16:25 +0000)]
added experimental "make lcov" target (it runs only unit tests); better coverage for util and context classes; implemented some output functionality that was missing; reclassified some tests white -> black or black -> public; other minor fixes

14 years agoA handful of build system fixes:
Morgan Deters [Thu, 8 Apr 2010 20:49:11 +0000 (20:49 +0000)]
A handful of build system fixes:

* (test/unit/Makefile.am) libtool was being passed relative paths of
  sources in .cpp, confusing lcov if -b wasn't given.  Fixed.
  Closes bug #102.

* (configure.ac) --enable-coverage now implies --enable-static
  --enable-static-binary --disable-shared.

* (configure.ac) Create top-level config.status for informational and
  re-configuration purposes.

* (configure.ac) Remove -fvisibility=hidden for debug builds.
  Closes bug #104.

* (test/unit/Makefile.am) Build unit tests with -Wall.

* (various unit tests) Fixed trivially-fixable warnings in building
  unit tests.  (Signedness in comparison, unused variables, etc.)

* (Makefile.builds.in) Copy the binary correctly if it is static.
  (It was failing, but only with --enable-static --enable-shared
  --enable-static-binary.)  Closes bug #103.

* (src/parser/Makefile.am) libcvc4parser.so now links with libcvc4.so.

* Other minor cleanups to the build system.

14 years agoThis update contains more black-box tests as part of the attributes code review....
Tim King [Wed, 7 Apr 2010 22:14:10 +0000 (22:14 +0000)]
This update contains more black-box tests as part of the attributes code review. I have confirmed by eyeball that every executable line of attributes.h is now getting hit in coverage testing. This can only be eyeballed at the moment because of templates. (There is 1 function that is not being touched, something included from NodeTemplate: _ZNK4CVC44expr4attr16AttributeManager12getAttributeINS0_9AttributeINS_6theory15RewriteCacheTagENS_12NodeTemplateILb0EEENS1_19NullCleanupStrategyELb0EEEEENT_10value_typeEPNS0_9NodeValueERKSB_)

14 years ago* Add some protected ContextObj accessors for ContextObj-derived classes:
Morgan Deters [Tue, 6 Apr 2010 06:39:01 +0000 (06:39 +0000)]
* Add some protected ContextObj accessors for ContextObj-derived classes:
  + Context* getContext() -- gets the context
  + ContextMemoryManager* getCMM() -- gets the CMM
  + int getLevel() -- the scope level of the ContextObj's most recent update
  + bool isCurrent() -- true iff the most recent update is the current top level

  In particular, the ContextObj::getCMM() call cleans up by TheoryUF's
  ECData::addPredecessor() function substantially (re: code review bug #64).

* Fix serious bugs in context operations that corrupted the ContextObj
  linked lists.  Closes bug #85.

* Identified a bug in the way objects of the "Link" class are
  allocated; see bug #96.

* Re-enable context white-box tests that ensure proper links in linked
  lists.  Closes bug #86.

* Re-enable CDMap<>::emptyTrash().  Closes bug #87.

* Add a tracing option (-t foo or --trace foo) to the driver to enable
  Trace("foo") output stream.  -d foo implies -t foo.

* Minor clean-up of some TheoryUF code; addition of some documentation
  (re: code review bug #64).

* Address some things that caused Doxygen discomfort.

* Address an issue raised in NodeManager's code review (bug #65).

* Remove an inaccurate comment in Attribute code (re: code review bug #61).

14 years agoAdding black-box tests for NodeManager (Closes bug #65)
Christopher L. Conway [Mon, 5 Apr 2010 22:28:41 +0000 (22:28 +0000)]
Adding black-box tests for NodeManager (Closes bug #65)

14 years agoRemoving unused functions that were causing compiler warnings
Christopher L. Conway [Mon, 5 Apr 2010 20:04:48 +0000 (20:04 +0000)]
Removing unused functions that were causing compiler warnings

14 years agoSimplifying ANTLR3 overrides
Christopher L. Conway [Mon, 5 Apr 2010 20:04:45 +0000 (20:04 +0000)]
Simplifying ANTLR3 overrides

14 years agoupdating COPYING file to reflect that antlr_input_imports.cpp is not under CVC4 copyright
Morgan Deters [Mon, 5 Apr 2010 19:23:37 +0000 (19:23 +0000)]
updating COPYING file to reflect that antlr_input_imports.cpp is not under CVC4 copyright

14 years agoUpdating copyright exclusion
Christopher L. Conway [Mon, 5 Apr 2010 19:10:42 +0000 (19:10 +0000)]
Updating copyright exclusion

14 years agoMoving sources copied from libantlr3c to separate file
Christopher L. Conway [Mon, 5 Apr 2010 19:10:39 +0000 (19:10 +0000)]
Moving sources copied from libantlr3c to separate file

14 years agoIgnoring gcov files
Christopher L. Conway [Mon, 5 Apr 2010 19:10:36 +0000 (19:10 +0000)]
Ignoring gcov files

14 years agoMoving code imported from libantlr3c to separate file and adding copyright exception
Christopher L. Conway [Mon, 5 Apr 2010 19:10:33 +0000 (19:10 +0000)]
Moving code imported from libantlr3c to separate file and adding copyright exception

14 years agofix most of the warnings in the parser by (1) quieting unused-function and unused...
Morgan Deters [Mon, 5 Apr 2010 17:17:38 +0000 (17:17 +0000)]
fix most of the warnings in the parser by (1) quieting unused-function and unused-variable warnings in the generated code, which aren't useful, and (2) not #including our autoheader stuff in the parser, which was conflicting with antlr3's

14 years agoAdding match override to AntlrInput, in attempt to workaround Bug #76
Christopher L. Conway [Mon, 5 Apr 2010 16:21:27 +0000 (16:21 +0000)]
Adding match override to AntlrInput, in attempt to workaround Bug #76

14 years agoMinor refactorings, in response to code review (Bug #73)
Christopher L. Conway [Mon, 5 Apr 2010 14:28:55 +0000 (14:28 +0000)]
Minor refactorings, in response to code review (Bug #73)

14 years agoTypos and renames for code review
Christopher L. Conway [Mon, 5 Apr 2010 14:28:41 +0000 (14:28 +0000)]
Typos and renames for code review

14 years agominor formatting and code guidelines, related to parser code review (bug #73)
Morgan Deters [Mon, 5 Apr 2010 00:05:47 +0000 (00:05 +0000)]
minor formatting and code guidelines, related to parser code review (bug #73)

14 years ago* Addressed issues brought up in Chris's review of Morgan's
Morgan Deters [Sun, 4 Apr 2010 23:03:52 +0000 (23:03 +0000)]
* Addressed issues brought up in Chris's review of Morgan's
  NodeManager (bug #65).  Better documentation, etc.

* As part of this, removed NodeManager::mkVar() (which created a
  variable of unknown type).  This requires changes to lots of unit
  tests, which were using this function.

* Performed some review of parser code (my code review #73).

  + I changed the way exceptions were caught and rethrown in
    src/parser/input.cpp.

  + ParserExceptions weren't being properly constructed (d_line and
    d_column weren't intiialized and could contain junk, leading to
    weird error messages).  Fixed.

* Fix to the current working directory used by run_regression script.
  Makes exceptional output easier to match against (in expected error
  output).

* (configure.ac) Ensure that CFLAGS has -fexceptions in it, in case we
  compile any C code and don't use the C++ compiler.

14 years ago* Node::isAtomic() now looks at an "atomic" attribute of arguments
Morgan Deters [Sun, 4 Apr 2010 19:55:47 +0000 (19:55 +0000)]
* Node::isAtomic() now looks at an "atomic" attribute of arguments
  instead of assuming it's atomic based on kind.  Atomicity is
  determined at node building time.  Fixes bug #81.  If this is
  determined to make node building too slow, we can allocate another
  attribute "AtomicHasBeenComputed" to lazily compute atomicity.

* TheoryImpl<> has gone away.  Theory implementations now derive from
  Theory directly and share a single RegisteredAttr attribute for term
  registration (which shouldn't overlap: every term is "owned" by
  exactly one Theory).  Fixes bug #79.

* Additional atomicity tests in ExprBlack unit test.

* More appropriate whitebox testing for attribute ID assignment
  (AttributeWhite unit test).

* Better (and more correct) assertion checking in NodeBuilderBlack.

* run-regression script now checks exit status against what's provided
  in "% EXIT: " gesture in .cvc input files, and stderr against
  "% EXPECT-ERROR: ".  These can be used to support intended failures.
  Fixes bug #84.  Also add "% EXIT: " gestures to all .cvc regressions
  in repository.

* Solved some "control reaches end of non-void function" warnings in
  src/parser/bounded_token_buffer.cpp by replacing
  "AlwaysAssert(false)" with "Unreachable()" (which is known
  statically to never return normally).

* Regression tests now use the cvc4 binary under
  builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which
  may not be properly installed yet at that point of the build.
  (Partially fixes bug #46.)

* -fvisibility=hidden is now included by configure.ac instead of each
   Makefile.am, which will make it easier to support platforms
   (e.g. cygwin) that do things a different way.

* TheoryUF code formatting.  (re: my code review bug #64)

* CDMap<> is leaking memory again, pending a fix for bug #85 in the
  context subsystem.  (To avoid serious errors, can't free context
  objects.)

* add ContextWhite unit test for bug #85 (though it's currently
  "defanged," awaiting the bugfix)

* Minor documentation, other cleanup.

14 years agoRecommit revision 365 (undoing revision 375, which reverted revision 365).
Morgan Deters [Sun, 4 Apr 2010 19:36:56 +0000 (19:36 +0000)]
Recommit revision 365 (undoing revision 375, which reverted revision 365).
Fix the case in NodeBuilderBlack that triggered bug #82.  (Fixes bug #82.)

This also fixes regression failures from this morning (2010 Apr 4), in
the optimized builds, for which a fix was included in 365 and reverted
in 375.  They looked like this:

  In ExprBlack::testGetConst:
  /usr/local/share/cvc4/src/cvc4-2010-04-04/builds/x86_64-unknown-linux-gnu/production/../../../test/unit/expr/expr_black.h:377: Error: Expected (a->getConst<Kind>()) to throw (IllegalArgumentException) but it didn't throw
  /usr/local/share/cvc4/src/cvc4-2010-04-04/builds/x86_64-unknown-linux-gnu/production/../../../test/unit/expr/expr_black.h:378: Error: Expected (b->getConst<Kind>()) to throw (IllegalArgumentException) but it didn't throw
  [etc..]

14 years agoReverting r365
Christopher L. Conway [Sat, 3 Apr 2010 15:17:50 +0000 (15:17 +0000)]
Reverting r365

14 years agoOverriding ANTLR3 error recovery routine
Christopher L. Conway [Fri, 2 Apr 2010 20:04:34 +0000 (20:04 +0000)]
Overriding ANTLR3 error recovery routine

14 years agoFixing double delete bug in main.cpp
Christopher L. Conway [Fri, 2 Apr 2010 18:40:51 +0000 (18:40 +0000)]
Fixing double delete bug in main.cpp

14 years agoFixed the 32 bit vs. 64 bit problem in the rational and integer tests.
Tim King [Fri, 2 Apr 2010 17:17:35 +0000 (17:17 +0000)]
Fixed the 32 bit vs. 64 bit problem in the rational and integer tests.

14 years agoChanging min/maxArity to use metakind info.
Christopher L. Conway [Thu, 1 Apr 2010 20:06:10 +0000 (20:06 +0000)]
Changing min/maxArity to use metakind info.

14 years agoParser tweaks to address review
Christopher L. Conway [Thu, 1 Apr 2010 19:55:45 +0000 (19:55 +0000)]
Parser tweaks to address review
Private members of Input moved to new class ParserState

14 years agoAdding newly generated files
Christopher L. Conway [Thu, 1 Apr 2010 19:55:40 +0000 (19:55 +0000)]
Adding newly generated files

14 years agoRemoving Expr::operator=(uintptr_t n), as it's no longer used by the parser.
Christopher L. Conway [Thu, 1 Apr 2010 19:55:38 +0000 (19:55 +0000)]
Removing Expr::operator=(uintptr_t n), as it's no longer used by the parser.

14 years agocvc4 --show-config now gives library version
Morgan Deters [Thu, 1 Apr 2010 07:26:37 +0000 (07:26 +0000)]
cvc4 --show-config now gives library version

14 years agoreran update-copyright.pl to get new contributors and add new header comments to...
Morgan Deters [Thu, 1 Apr 2010 07:19:41 +0000 (07:19 +0000)]
reran update-copyright.pl to get new contributors and add new header comments to files without them

14 years ago* Minor code formatting stuff in src/expr/type.{h,cpp}. Concluded
Morgan Deters [Thu, 1 Apr 2010 06:59:18 +0000 (06:59 +0000)]
* Minor code formatting stuff in src/expr/type.{h,cpp}.  Concluded
  Type code review and closed bug #25.

* Do assertions on Expr creation (public library interface) even when
  assertions are off.  Also a similar check for proper kind (in public
  interface) when Expr::getConst<>() is called.  This fixes a unit
  test that was failing in production builds (an exception wasn't
  thrown but should have been).

* kind::XOR must have exactly 2 arguments, not 2-or-more.

14 years agominor forgotten things in last commit
Morgan Deters [Thu, 1 Apr 2010 06:00:17 +0000 (06:00 +0000)]
minor forgotten things in last commit

14 years agoPARSER STUFF:
Morgan Deters [Thu, 1 Apr 2010 05:54:26 +0000 (05:54 +0000)]
PARSER STUFF:

* Other minor changes to the new parser to match coding guidelines,
  add documentation, ....

* Add CFLAGS stuff to configure.ac parser Makefile.ams.  This ensures
  that profiling, coverage, optimization, debugging, and warning
  level options will apply to the new parser as well (which is in C,
  not C++).  This fixes the deprecated warning we were seeing this
  evening.

* Now, if you have ANTLR_HOME set in your environment, you don't need
  to specify --with-antlr-dir to ./configure or have libantlr3c
  installed in standard places.  --with-antlr-dir still overrides
  $ANTLR_HOME, and if the installation in $ANTLR_HOME is missing or
  doesn't work, the standard places are still tried.

* Extend "silent make" to new parser stuff.

* Added src/parser/bounded_token_buffer.{h,cpp} to the list of
  exclusions in contrib/update-copyright.pl and mention them as
  excluded from CVC4 copyright in COPYING.  They are antlr3-derived
  works, covered under a BSD license.

OTHER STUFF:

* expr_manager.h, expr.h, expr_manager.cpp, and expr.cpp are now
  auto-generated by a "mkexpr" script.  This provides the correct
  instantiations of mkConst() for public use, e.g., by the parser.

* Fix doxygen documentation in expr, expr_manager.. closes bug #35

* Node::isAtomic() implemented in a better way, based on theory kinds
  files.  Fixes bug #40.  To support this, a "nonatomic_operator"
  command has been added.  All other "parameterized" or "operator"
  kinds are atomic.

* Added expr_black test

* Remove kind::TRUE and kind::FALSE and make a new CONST_BOOLEAN kind
  that takes a "bool" payload; for example, to make "true" you now do
  nodeManager->mkConst(true).

* Make new "cvc4_public.h" and "cvc4parser_public.h" headers.  Private
  headers should include "cvc4_private.h"
  (resp. "cvc4parser_private.h"), which existed previously.  Public
  headers should include the others.  **No one** should include the
  autoheader #include (which has been renamed "cvc4autoconfig.h")
  directly, and public CVC4 headers can't access its #defines.  This
  is to avoid us having the same distribution problem as libantlr3c.

* Preliminary fixes based on Tim's code review of attributes (bug #61).
  This includes splitting hairy template internals into
  attribute_internals.h, for which another code review ticket will be
  opened.  Bug is still outstanding, but pending further
  refactoring/documentation.

* Some *HashFcns renamed to *HashStrategy to match refactoring done
  elsewhere (done by Chris?) earlier this week.

* Simplified creation of make rules for generated files (expr.cpp,
  expr.h, expr_manager.cpp, expr_manager.h, theoryof_table.h, kind.h,
  metakind.h).

* CVC4::Configuration interface and implementation split (so private
  stuff doesn't leak into public headers).

* Some documentation/code formatting fixes.

* Add required versions of autotools to autogen.sh.

* src/expr/mkmetakind: fix a nonportable thing in invocation of "expr"
  that was causing warnings on Red Hat.

* src/context/cdmap.h: add workaround to what appears to be a g++ 4.1
  parsing bug.

14 years agoAdding check for --disable-shared on --enable-coverage
Christopher L. Conway [Thu, 1 Apr 2010 03:02:01 +0000 (03:02 +0000)]
Adding check for --disable-shared on --enable-coverage

14 years agoFix bug in SMT-LIB with let/flet bindings
Christopher L. Conway [Wed, 31 Mar 2010 23:07:14 +0000 (23:07 +0000)]
Fix bug in SMT-LIB with let/flet bindings

14 years agoFinishing parser cleanup. Code is now review-ready.
Christopher L. Conway [Wed, 31 Mar 2010 23:07:12 +0000 (23:07 +0000)]
Finishing parser cleanup. Code is now review-ready.

14 years agoMore parser cleanup. Should fix problems with last commit.
Christopher L. Conway [Wed, 31 Mar 2010 20:45:31 +0000 (20:45 +0000)]
More parser cleanup. Should fix problems with last commit.

14 years agoCode cleanup in parser
Christopher L. Conway [Wed, 31 Mar 2010 19:53:41 +0000 (19:53 +0000)]
Code cleanup in parser

14 years agoAdding 'generated/' to .gitignore
Christopher L. Conway [Wed, 31 Mar 2010 19:53:38 +0000 (19:53 +0000)]
Adding 'generated/' to .gitignore

14 years agoRemoving unnecessary .gitignores
Christopher L. Conway [Tue, 30 Mar 2010 20:51:08 +0000 (20:51 +0000)]
Removing unnecessary .gitignores

14 years agoMerging from branches/antlr3 (r246:354)
Christopher L. Conway [Tue, 30 Mar 2010 20:22:33 +0000 (20:22 +0000)]
Merging from branches/antlr3 (r246:354)

14 years agoagain, re-enabling integer/rational tests (though they still fail to compile on 32...
Morgan Deters [Tue, 30 Mar 2010 08:28:22 +0000 (08:28 +0000)]
again, re-enabling integer/rational tests (though they still fail to compile on 32-bit)

14 years agoI think this finishes off the CDMap<>/Attribute leaks
Morgan Deters [Tue, 30 Mar 2010 08:22:06 +0000 (08:22 +0000)]
I think this finishes off the CDMap<>/Attribute leaks

14 years agofixing mistaken commit to unit test Makefile.am which removed tests
Morgan Deters [Tue, 30 Mar 2010 04:59:53 +0000 (04:59 +0000)]
fixing mistaken commit to unit test Makefile.am which removed tests

14 years agoHighlights of this commit are:
Morgan Deters [Tue, 30 Mar 2010 04:59:16 +0000 (04:59 +0000)]
Highlights of this commit are:

* add NodeManagerWhite unit test

* change kind::APPLY to kind::APPLY_UF

* better APPLY handling: operators are no longer considered children

* more efficient pool lookup; the NodeValue doesn't have to be as fully constructed for the lookup to proceed

* extend DSL for kind declarations
  + new "theory" command declares a theory and its header.  theory_def.h no longer required.
  + arity enforced on operators
  + constant mapping, hashing, equality

* CONSTANT metakinds supported (via Node::getConst<T>(), for example, Node::getConst<CVC4::Rational>() gets a Rational out of a Node (assuming it is of CONST_RATIONAL kind)

* added CONST_RATIONAL and CONST_INTEGER kinds

* builtin operators (AND, OR, PLUS, etc..) returned by Node::getOperator() are now CONSTANT metakind and are created by NodeManager

* Pretty-printing of Nodes now has a depth limit settable by a stream manipulator (e.g. "cout << Node::setdepth(5) << m << endl;" prints DAG rooted at m to a depth of 5)

* getters added to Node, TNode, NodeValue, etc., for operators and metakinds

* build-time generators for kind.h, metakind.h, and theoryof_table.h headers now have a simpler design and flag errors better, and the templates (kind_template.h etc.) are easier to understand.

* DISTINCT is now a kind, and the SMT parser now passes through DISTINCT nodes instead of blowing them up into ANDs.  Until theory rewriting is online, though, DISTINCTs are directly blown up into conjunctions in TheoryEngine::rewrite().

* add gmpxx detection and inclusion

* better Asserts throughout, some documentation, cleanup

14 years agoImproved the documentation and testing for Rational.
Tim King [Sun, 28 Mar 2010 21:39:39 +0000 (21:39 +0000)]
Improved the documentation and testing for Rational.

14 years agoRm'ing test file (sorry for spam)
Christopher L. Conway [Sun, 28 Mar 2010 19:56:59 +0000 (19:56 +0000)]
Rm'ing test file (sorry for spam)

14 years agoAdding test file
Christopher L. Conway [Sun, 28 Mar 2010 19:51:48 +0000 (19:51 +0000)]
Adding test file

14 years agoAdded GMP backed Rational and Integer classes, and white box tests for them. You...
Tim King [Fri, 26 Mar 2010 22:37:12 +0000 (22:37 +0000)]
Added GMP backed Rational and Integer classes, and white box tests for them.  You may have to reconfigure after this update.

14 years agoMerging let/flet rules in SMT parser
Christopher L. Conway [Thu, 25 Mar 2010 20:25:04 +0000 (20:25 +0000)]
Merging let/flet rules in SMT parser

14 years agoAdding comments to NodeManager
Christopher L. Conway [Thu, 25 Mar 2010 20:20:29 +0000 (20:20 +0000)]
Adding comments to NodeManager
Minor name changes for cleanup and hash function templates

14 years agonew domain-specific language for kinds files: permits characterization of different...
Morgan Deters [Thu, 25 Mar 2010 05:03:55 +0000 (05:03 +0000)]
new domain-specific language for kinds files: permits characterization of different "kinds of kinds" (special, operator, parameterized, and constant), and permits doxygen comments on them

14 years agoDocumented that ContextObj::destroy() only restores back to context level 0.
Clark Barrett [Tue, 23 Mar 2010 21:30:27 +0000 (21:30 +0000)]
Documented that ContextObj::destroy() only restores back to context level 0.
If there is more cleanup to do, it has to be done by the destructor.

14 years agoFixed some memory cleanup and destruction issues with ContextObj, ECData, CDList...
Tim King [Tue, 23 Mar 2010 19:41:49 +0000 (19:41 +0000)]
Fixed some memory cleanup and destruction issues with ContextObj, ECData, CDList, and CDMap. Added the d_underTheShotgun field to NodeManager to keep track of which NodeValue is currently being deleted. If a Node or TNode has this node value, it can always be deleted.  This avoids the need for introducing SoftNodes.  Currently passes Debug and Production make check

14 years ago* test/unit/Makefile.am, test/unit/expr/attribute_white.h,
Morgan Deters [Tue, 16 Mar 2010 20:24:37 +0000 (20:24 +0000)]
* test/unit/Makefile.am, test/unit/expr/attribute_white.h,
  test/unit/expr/node_white.h: add whitebox attribute test (pulled out
  attribute stuff from node_white)

* test/unit/parser/parser_black.h: fix memory leaks uncovered by
  valgrind

* src/theory/interrupted.h: actually make this "lightweight" (not
  derived from CVC4::Exception), as promised in my last commit

* src/theory/uf/theory_uf.h, test/unit/expr/attribute_black.h: match
  the new-style cleanup function definition

* src/expr/attribute.cpp, src/expr/attribute.h: support for attribute
  deletion, custom cleanup functions, clearer cleanup function
  definition.

* src/expr/node_manager.h, src/expr/node_manager.cpp: reclaim
  remaining zombies in dtor, rename NodeValueSet ==> "NodeValuePool",
  and enable freeing of NodeValues

* src/expr/type.h, src/expr/type.cpp: reference-counting for types,
  customized cleanup function for types, also code cleanup

* (various): changed "const Type*" to "Type*" (to enable
  reference-counting etc.  Types are still immutable.)

* src/util/output.h: add ::isOn()-- which queries whether a
  Debug/Trace flag is currently on or not.

* src/smt/smt_engine.cpp, src/parser/antlr_parser.cpp,
  src/expr/type.cpp, src/expr/expr_manager.cpp, various others:
  minor code cleanup

14 years agoThis checkin resolves bug #57.
Morgan Deters [Mon, 15 Mar 2010 21:10:29 +0000 (21:10 +0000)]
This checkin resolves bug #57.

* CVC4::theory::Interrupted no longer derives CVC4::Exception.

* Interrupted is only thrown if "safe" parameter is TRUE !

* UF returns one conflict (instead of waiting for Interrupted to be thrown).

* Minor build system work (quieter builds if V=0, better handling of build
  profiles in configure)

14 years ago* test/unit/context/context_black.h: added a test for Clark's fix to bug #45.
Morgan Deters [Sun, 14 Mar 2010 01:55:36 +0000 (01:55 +0000)]
* test/unit/context/context_black.h: added a test for Clark's fix to bug #45.
* test/unit/context/cdlist_black.h: comment fix

14 years agoFix for bug 45
Clark Barrett [Sat, 13 Mar 2010 01:57:01 +0000 (01:57 +0000)]
Fix for bug 45

14 years ago* src/context/cdmap.h: rename orderedIterator to iterator, do away
Morgan Deters [Fri, 12 Mar 2010 23:52:14 +0000 (23:52 +0000)]
* src/context/cdmap.h: rename orderedIterator to iterator, do away
  with old iterator (closes bug #47).

* src/context/cdset.h: implemented.

* src/expr/node_builder.h: fixed all the strict-aliasing warnings.

* Remove Node::hash() and Expr::hash() (they had been aliases for
  getId()).  There's now a NodeValue::internalHash(), for internal
  expr package purposes only, that doesn't depend on the ID.  That's
  the only hashing of Nodes or Exprs.

* Automake-quiet generation of kind.h, theoryof_table.h, and CVC and
  SMT parsers.

* various minor code cleanups.

14 years agoFixing unnecessary construction of NOT nodes when generating conflict clauses and:
Dejan Jovanović [Fri, 12 Mar 2010 23:41:12 +0000 (23:41 +0000)]
Fixing unnecessary  construction of NOT nodes when generating conflict clauses and:
* adding the smallest test case (eq_diamond23.smt) that memouts in 50s
* adding the initial attributes black box test

14 years ago* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,
Morgan Deters [Fri, 12 Mar 2010 19:41:04 +0000 (19:41 +0000)]
* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,
  DecisionEngine, and Theory.  These are triggered from the SmtEngine
  dtor before the other engines are deleted.  This is important
  because of potential issues with outstanding TNodes in Theory
  implementations (which fail if the destruction is done in the wrong
  order, in certain cases).

* Favor "FactQueueResetter" instead of clearAssertionQueues() for
  resetting facts queue in Theory implementations.

* Better theory-rewriting code.

* Minor cleanups.

14 years agonaive rewriting to fix minisat invariant; rewrite x == x ==> TRUE
Morgan Deters [Thu, 11 Mar 2010 21:53:38 +0000 (21:53 +0000)]
naive rewriting to fix minisat invariant; rewrite  x == x  ==>  TRUE

14 years agoChanging const TNode& to TNode in the CNF conversion + a new small benchmark that...
Dejan Jovanović [Thu, 11 Mar 2010 20:53:41 +0000 (20:53 +0000)]
Changing const TNode& to TNode in the CNF conversion + a new small benchmark that fail on "x != x"

14 years agoAdded some hand generated UF tests. Unfortunartely all of them work. Also fixed some...
Tim King [Thu, 11 Mar 2010 18:23:31 +0000 (18:23 +0000)]
Added some hand generated UF tests. Unfortunartely all of them work. Also fixed some cleanup stuff.

14 years agoBoolean variables were marked as theory literals by mistake. Fixed, should give us...
Dejan Jovanović [Thu, 11 Mar 2010 06:15:32 +0000 (06:15 +0000)]
Boolean variables were marked as theory literals by mistake. Fixed, should give us back the SAT performance we had before the theory stuff.

14 years agoFix for the main bug that was bugging me -- Bug 49. The assertions queue in the theor...
Dejan Jovanović [Thu, 11 Mar 2010 01:30:37 +0000 (01:30 +0000)]
Fix for the main bug that was bugging me -- Bug 49. The assertions queue in the theories didn't get cleared on SatSolver backtracking so there were unasserted literals being returned as part of some conflicts. Sat solver now explicitely calls in the theory engine after it backtracks in order to clear the queues (clearAssertionQueues).

Also, changed the let.smt as it used to exibit "single literal conflict" problem. The sat solve can not except conflicts similar to (x != x), these should be rewritten to false during pre-processing.

Adding 3 more small problems from the library that we can solve now to the regressions.

14 years agofix production-build unit testing errors (they assumed that assertions were on)
Morgan Deters [Wed, 10 Mar 2010 17:23:21 +0000 (17:23 +0000)]
fix production-build unit testing errors (they assumed that assertions were on)

14 years agoLexical scoping for let-bound variables (Bug #53)
Christopher L. Conway [Wed, 10 Mar 2010 03:58:23 +0000 (03:58 +0000)]
Lexical scoping for let-bound variables (Bug #53)

14 years agoAdding preliminary let/flet support to SMT parser (Bug #51)
Christopher L. Conway [Wed, 10 Mar 2010 02:34:04 +0000 (02:34 +0000)]
Adding preliminary let/flet support to SMT parser (Bug #51)

14 years agoAdding support for "distinct" builtin in SMT parser
Christopher L. Conway [Tue, 9 Mar 2010 23:43:35 +0000 (23:43 +0000)]
Adding support for "distinct" builtin in SMT parser

14 years agoAdding support for sort U in QF_UF.
Christopher L. Conway [Tue, 9 Mar 2010 23:10:13 +0000 (23:10 +0000)]
Adding support for sort U in QF_UF.

14 years agoAdding the smallest of test cases from the smtlib.
Dejan Jovanović [Tue, 9 Mar 2010 21:56:35 +0000 (21:56 +0000)]
Adding the smallest of test cases from the smtlib.

14 years agoremoving makefile.in
Dejan Jovanović [Tue, 9 Mar 2010 18:06:25 +0000 (18:06 +0000)]
removing makefile.in

14 years agoFixed non-debug build problems
Tim King [Tue, 9 Mar 2010 14:38:51 +0000 (14:38 +0000)]
Fixed non-debug build problems

14 years agoone more simple test for uf
Dejan Jovanović [Tue, 9 Mar 2010 05:25:31 +0000 (05:25 +0000)]
one more simple test for uf

14 years ago(no commit message)
Dejan Jovanović [Tue, 9 Mar 2010 05:19:22 +0000 (05:19 +0000)]

14 years agoThis fixes regressions at levels >= 1 which were failing
Morgan Deters [Mon, 8 Mar 2010 23:49:47 +0000 (23:49 +0000)]
This fixes regressions at levels >= 1 which were failing

* implement zombification and garbage collection of NodeValues
  (but GC not turned on yet)

* implement removal of key nodes from all attribute tables

* audit NodeBuilder and fix memory leaks and improper reference-count
  management.  This is in many places a re-write.  Clearly documented
  invariants on NodeBuilder state.  (Closes Bug 38)

* created a "BackedNodeBuilder" that can be used to construct
  NodeBuilders with a stack-based backing store for a size that's not
  a compile-time constant.

* NodeValues no longer depend on Node for toStream()'ing

* make unit test-building "silent" with --enable-silent-rules

* (Makefile.am, Makefile.builds.in) fix top-level build system so that
  "make regressN" works with unbuilt/out-of-date source trees in the
  expected way.

* (various) code cleanup, documentation, formatting

14 years agoadding simple-uf to the regressions, and the code that apparently solves it
Dejan Jovanović [Mon, 8 Mar 2010 23:03:48 +0000 (23:03 +0000)]
adding simple-uf to the regressions, and the code that apparently solves it

14 years agoFixing Debug("prop") => Debug("node") typo
Dejan Jovanović [Mon, 8 Mar 2010 22:35:56 +0000 (22:35 +0000)]
Fixing Debug("prop") => Debug("node") typo

14 years agoImproved output for theory uf
Tim King [Mon, 8 Mar 2010 21:29:50 +0000 (21:29 +0000)]
Improved output for theory uf

14 years agosome more sat stuff for tim: assertions now go to theory_uf
Dejan Jovanović [Mon, 8 Mar 2010 21:08:40 +0000 (21:08 +0000)]
some more sat stuff for tim: assertions now go to theory_uf

14 years agoAdding quiet output of make by default. There are two additional options to configure
Dejan Jovanović [Mon, 8 Mar 2010 16:40:29 +0000 (16:40 +0000)]
Adding quiet output of make by default. There are two additional options to configure
  --enable-silent-rules          less verbose build output (undo: `make V=1')
  --disable-silent-rules         verbose build output (undo: `make V=0')
If you need the verbose output, you can either reconfigure with --disable-silent-rules, or do a make V=0.

14 years ago* public/private code untangled (smt/smt_engine.h no longer #includes
Morgan Deters [Fri, 5 Mar 2010 08:26:37 +0000 (08:26 +0000)]
* public/private code untangled (smt/smt_engine.h no longer #includes
  expr/node.h).  This removes the warnings we had during compilation,
  and heads off a number of potential linking errors due to improper
  inlining of private (library-only) stuff in client (out-of-library)
  code.

* "configure" now takes some options as part of a "bare-option" build
  type (e.g., "./configure debug-coverage" or "./configure production-muzzle").

* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h

* split cdlist_black unit test from context_black

* implement CDMap<>.

* give ExprManagers ownership of the context (and have SmtEngine share
  that one)

* fix main driver to properly report file-not-found

* fix MemoryMappedInputBuffer class to report reasons for
  "errno"-returned system errors

* src/expr/attribute.h: context-dependent attribute kinds now
  supported

* test/unit/expr/node_white.h: context-dependent attribute tests

* src/prop/cnf_conversion.h and associated parts of src/util/options.h
  and src/main/getopt.cpp: obsolete command-line option, removed.

* src/util/Assert.h: assertions are now somewhat more useful (in debug
  builds, anyway) during stack unwinding.

* test/unit/theory/theory_black.h: test context-dependent behavior of
  registerTerm() attribute for theories

* src/expr/node_builder.h: formatting, fixes for arithmetic
  convenience node builders, check memory allocations

* test/unit/expr/node_builder_black.h: add tessts for addition,
  subtraction, unary minus, and multiplication convenience node
  builders

* src/expr/attribute.h: more comments

* (various) code formatting, comment cleanup, added throws specifier
  to some destructors

* contrib/code-checker: prototype perl script to test (some) code policy

* contrib/indent-settings: command line for GNU indent to indent using
  CVC4 style (sort of; this is a work in progress)

* COPYING: legal stuff

* DESIGN_QUESTIONS: obsolete, removed

14 years agoCommitting a bug fix from Dejan. This resolves an issue with restoring ECData.
Tim King [Thu, 4 Mar 2010 20:10:46 +0000 (20:10 +0000)]
Committing a bug fix from Dejan. This resolves an issue with restoring ECData.

14 years agoAdding phase-caching to minisat.
Dejan Jovanović [Thu, 4 Mar 2010 18:45:15 +0000 (18:45 +0000)]
Adding phase-caching to minisat.
(A Lightweight Component Caching Scheme for Satisfiability Solvers <http://www.springerlink.com/content/y802q03263x84159/>)

14 years agoSome SAT stuff, not doing anything special yet, just to keep it in sync.
Dejan Jovanović [Wed, 3 Mar 2010 23:39:43 +0000 (23:39 +0000)]
Some SAT stuff, not doing anything special yet, just to keep it in sync.

14 years ago* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"
Morgan Deters [Tue, 2 Mar 2010 20:33:26 +0000 (20:33 +0000)]
* NodeBuilder work: specifically, convenience builders.  "a && b && c || d && e"
  (etc.) now work for Nodes a, b, c, d, e.  Also refcounting fixes for
  NodeBuilder in certain cases

* (various places) don't overload __gnu_cxx::hash<>, instead provide
  an explicit hash function to hash_maps and hash_sets.

* add a new kind of assert, DtorAssert(), which doesn't throw
  exceptions (right now it operates like a usual C assert()).  For use
  in destructors.

* don't import NodeValue into CVC4 namespace (leave under CVC4::expr::).

* fix some Make rule dependencies

* reformat node.h as per code formatting policy

* added Theory and NodeBuilder unit tests

14 years agoAdded theory black box test.
Tim King [Mon, 1 Mar 2010 21:28:52 +0000 (21:28 +0000)]
Added theory black box test.

14 years agoNode builder tests that targetted properly detecting and handling expections have...
Tim King [Mon, 1 Mar 2010 20:19:48 +0000 (20:19 +0000)]
Node builder tests that targetted properly detecting and handling expections have been changed to be debug mode. (The Assert(..) calls these checks rely on get compiled out of production mode.) Production and debug mode should now both pass make check on everything.

14 years agoAdded some documentation to theory_uf.
Tim King [Mon, 1 Mar 2010 20:14:53 +0000 (20:14 +0000)]
Added some documentation to theory_uf.

14 years ago* context.h - Changed cdlist::push_back to use a new copy constructor instead of...
Dejan Jovanović [Sun, 28 Feb 2010 00:57:25 +0000 (00:57 +0000)]
* context.h - Changed cdlist::push_back to use a new copy constructor instead of the assignment operator. This is important as Nodes, for example, check that d_nv != NULL in the assignemnt operator.
* node.h - Simplified the constructors, apparently it's ok to write ~ref_count in the template declaration. All the constructed nodes are now the ref-counted ones, i.e. eqNode() will return a ref-counted node.