cvc5.git
14 years agoFix for bug 131. Added some additional debugging assertions for the arith rewriter.
Tim King [Wed, 26 May 2010 19:58:36 +0000 (19:58 +0000)]
Fix for bug 131. Added some additional debugging assertions for the arith rewriter.

14 years agoCDMap: fix bug 130
Morgan Deters [Wed, 26 May 2010 18:02:59 +0000 (18:02 +0000)]
CDMap: fix bug 130

14 years agoPrevent lexer errors being raised if a parser error is pending.
Christopher L. Conway [Wed, 26 May 2010 17:53:33 +0000 (17:53 +0000)]
Prevent lexer errors being raised if a parser error is pending.
This fixes a bug Dejan has often whined about but never filed.

14 years agoAdded Rational constructors that only take a numerator. The const char* Rational...
Tim King [Tue, 25 May 2010 21:45:18 +0000 (21:45 +0000)]
Added Rational constructors that only take a numerator. The const char* Rational and Integer constructors are now explicit. This means that 'Integer = 3;' and so on are no longer permitted.  This closes bug 121.

14 years agoSome initial changes to allow for lemmas on demand.
Dejan Jovanović [Tue, 25 May 2010 05:30:40 +0000 (05:30 +0000)]
Some initial changes to allow for lemmas on demand.

To be done:
* Add erasable map Clause* to bool to minisat (backtracks with the solver)
* Add map from Clause* to Node (clauses that came from a node)
* Add reference counting Literal -> Node to CNFManager
* If Literal -> Node refcount goes to zero, the clauses of Node can be erased (if eresable)
* If clause is erased for each L in clause L -> Node refcount goes down

14 years agoSmall fixes to TheoryArith. Added a hack to make Integers a subtype of Real. See...
Tim King [Fri, 21 May 2010 19:27:18 +0000 (19:27 +0000)]
Small fixes to TheoryArith.  Added a hack to make Integers a subtype of Real. See Bug 127 for a discussion of the hack.  I am also adding a regression test that does not work (bug 128). It is not enabled so make check should still be fine.

14 years agoAdded the division symbol to the parser, and minimal support for it in TheoryArith...
Tim King [Thu, 20 May 2010 22:51:48 +0000 (22:51 +0000)]
Added the division symbol to the parser, and minimal support for it in TheoryArith.  Also directly hacked in support for theoryOf() to work for equalities where the left hand is a variable of type real.

14 years agoSignificant revision to theory/arith. The new draft has a lot of small bug fixes...
Tim King [Wed, 19 May 2010 21:20:54 +0000 (21:20 +0000)]
Significant revision to theory/arith.  The new draft has a lot of small bug fixes and organizational changes.  The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.

14 years agoAdding debugging code in PropEngine/CnfStream
Christopher L. Conway [Fri, 14 May 2010 22:50:17 +0000 (22:50 +0000)]
Adding debugging code in PropEngine/CnfStream

14 years agoAdding ITE tests
Christopher L. Conway [Fri, 14 May 2010 22:50:13 +0000 (22:50 +0000)]
Adding ITE tests

14 years agoAdding rudimentary ITE handling in CnfStream
Christopher L. Conway [Fri, 14 May 2010 03:02:40 +0000 (03:02 +0000)]
Adding rudimentary ITE handling in CnfStream

14 years agoVirtualizing interface between CnfStream and SatSolver
Christopher L. Conway [Fri, 14 May 2010 02:58:36 +0000 (02:58 +0000)]
Virtualizing interface between CnfStream and SatSolver

14 years agoMinor refactorings to PropEngine, SatSolver
Christopher L. Conway [Thu, 13 May 2010 05:30:30 +0000 (05:30 +0000)]
Minor refactorings to PropEngine, SatSolver

14 years agoMinor refactorings and corrections to comments
Christopher L. Conway [Thu, 13 May 2010 05:30:20 +0000 (05:30 +0000)]
Minor refactorings and corrections to comments

14 years agoAdding ParserBuilder, reducing visibility of Parser and Input constructors
Christopher L. Conway [Wed, 12 May 2010 20:29:24 +0000 (20:29 +0000)]
Adding ParserBuilder, reducing visibility of Parser and Input constructors
Adding Smt2 subclass of Parser
Checking for multiple calls to set-logic in SMT v2

14 years agotrue and false are only defined if the core theory is loaded in SMT v2 strict mode
Christopher L. Conway [Wed, 12 May 2010 20:29:17 +0000 (20:29 +0000)]
true and false are only defined if the core theory is loaded in SMT v2 strict mode

14 years agoRefactoring parser tests
Christopher L. Conway [Wed, 12 May 2010 15:15:58 +0000 (15:15 +0000)]
Refactoring parser tests

14 years agoAdding class Smt2 to handle declaration of logic and theory symbols
Christopher L. Conway [Wed, 12 May 2010 15:15:53 +0000 (15:15 +0000)]
Adding class Smt2 to handle declaration of logic and theory symbols

14 years agoTightening lexer rules for numerals in SMT v2
Christopher L. Conway [Fri, 7 May 2010 19:44:05 +0000 (19:44 +0000)]
Tightening lexer rules for numerals in SMT v2

14 years agomake CVC4::Rational public (fixes broken build)
Morgan Deters [Fri, 7 May 2010 00:41:06 +0000 (00:41 +0000)]
make CVC4::Rational public (fixes broken build)

14 years agoAdding --strict-parsing option
Christopher L. Conway [Thu, 6 May 2010 21:11:43 +0000 (21:11 +0000)]
Adding --strict-parsing option

14 years agoAdding AntlrInput::tokenTextSubstr
Christopher L. Conway [Thu, 6 May 2010 21:11:37 +0000 (21:11 +0000)]
Adding AntlrInput::tokenTextSubstr

14 years agoAdding tests for Rational::fromDecimal
Christopher L. Conway [Thu, 6 May 2010 20:08:04 +0000 (20:08 +0000)]
Adding tests for Rational::fromDecimal

14 years agoAdding tests for Integer::pow
Christopher L. Conway [Thu, 6 May 2010 20:08:00 +0000 (20:08 +0000)]
Adding tests for Integer::pow

14 years agoAdding bit-vector constants in SMT2
Christopher L. Conway [Thu, 6 May 2010 20:07:56 +0000 (20:07 +0000)]
Adding bit-vector constants in SMT2

14 years agoImplementing Rational::fromDecimal and adding support for real constants in SMT parsers
Christopher L. Conway [Thu, 6 May 2010 20:07:51 +0000 (20:07 +0000)]
Implementing Rational::fromDecimal and adding support for real constants in SMT parsers

14 years agofixing the nightly failure. TypeCheckingException is now marked with CVC4_PUBLIC
Dejan Jovanović [Thu, 6 May 2010 15:07:53 +0000 (15:07 +0000)]
fixing the nightly failure. TypeCheckingException is now marked with CVC4_PUBLIC

14 years agochanging the interface to bit-vector constant constructor
Dejan Jovanović [Wed, 5 May 2010 21:23:18 +0000 (21:23 +0000)]
changing the interface to bit-vector constant constructor

14 years agobit-vector constant constructor from string
Dejan Jovanović [Wed, 5 May 2010 21:05:30 +0000 (21:05 +0000)]
bit-vector constant constructor from string

14 years agobug fixes for types, old unit tests for types work now
Dejan Jovanović [Wed, 5 May 2010 19:06:07 +0000 (19:06 +0000)]
bug fixes for types, old unit tests for types work now

14 years agoAdding simple SMT2 parser tests
Christopher L. Conway [Tue, 4 May 2010 22:27:40 +0000 (22:27 +0000)]
Adding simple SMT2 parser tests

14 years agoDisabling semantic checks in competition mode.
Christopher L. Conway [Tue, 4 May 2010 21:57:57 +0000 (21:57 +0000)]
Disabling semantic checks in competition mode.
Adding function debugTagIsOn to safely test for tracing in any
compilation mode.
Removing irrelevant command-line options from usage message
in muzzled mode.

14 years agoMinor change to SMT v2 grammar
Christopher L. Conway [Tue, 4 May 2010 21:57:53 +0000 (21:57 +0000)]
Minor change to SMT v2 grammar

14 years agoAdding general support for SMT2 set-info command
Christopher L. Conway [Tue, 4 May 2010 19:31:24 +0000 (19:31 +0000)]
Adding general support for SMT2 set-info command

14 years agoHandling SMT 2.0 symbols and info flags
Christopher L. Conway [Tue, 4 May 2010 19:31:19 +0000 (19:31 +0000)]
Handling SMT 2.0 symbols and info flags

14 years agoType-checking classes and hooks (not tested yet).
Dejan Jovanović [Tue, 4 May 2010 03:42:56 +0000 (03:42 +0000)]
Type-checking classes and hooks (not tested yet).

14 years agomore reasonable smt 2.0 benchmark test
Morgan Deters [Mon, 3 May 2010 22:08:29 +0000 (22:08 +0000)]
more reasonable smt 2.0 benchmark test

14 years agomain driver supports .smt2 input, added an smt2 regression (currently broken, so...
Morgan Deters [Mon, 3 May 2010 22:05:44 +0000 (22:05 +0000)]
main driver supports .smt2 input, added an smt2 regression (currently broken, so it doesn't run with "make check")

14 years agotheory detection fixes; fixes build breakage when you delete build directories
Morgan Deters [Mon, 3 May 2010 21:31:55 +0000 (21:31 +0000)]
theory detection fixes; fixes build breakage when you delete build directories

14 years agoSmall mistake in previous commit
Christopher L. Conway [Mon, 3 May 2010 21:25:47 +0000 (21:25 +0000)]
Small mistake in previous commit

14 years agoImporting ANTLR3 lexer nextToken function to avoid escaped exceptions.
Christopher L. Conway [Mon, 3 May 2010 20:52:41 +0000 (20:52 +0000)]
Importing ANTLR3 lexer nextToken function to avoid escaped exceptions.

14 years agosmt parser for bit-vectors
Dejan Jovanović [Sun, 2 May 2010 02:20:17 +0000 (02:20 +0000)]
smt parser for bit-vectors

14 years agoFix for the last night's build errors (type that broke proper expression generation).
Dejan Jovanović [Sat, 1 May 2010 21:00:41 +0000 (21:00 +0000)]
Fix for the last night's build errors (type that broke proper expression generation).

14 years agoAdding missed antlr_input files
Christopher L. Conway [Sat, 1 May 2010 20:45:47 +0000 (20:45 +0000)]
Adding missed antlr_input files

14 years agoFixing private/public header warnings in parser library
Christopher L. Conway [Sat, 1 May 2010 20:44:09 +0000 (20:44 +0000)]
Fixing private/public header warnings in parser library

14 years agoAdding comments to bounded token files
Christopher L. Conway [Sat, 1 May 2010 20:43:30 +0000 (20:43 +0000)]
Adding comments to bounded token files

14 years agoFix for bug 115, mapping was going in the wrong direction.
Dejan Jovanović [Fri, 30 Apr 2010 23:55:18 +0000 (23:55 +0000)]
Fix for bug 115, mapping was going in the wrong direction.

14 years agoAdded the capability to construct expressions by passing the operator instead of...
Dejan Jovanović [Thu, 29 Apr 2010 23:42:41 +0000 (23:42 +0000)]
Added the capability to construct expressions by passing the operator instead of the kind, i.e.

Expr op = ..."f"...
em.mkExpr(op, children);

Operator kinds are automatically associated with the enclosing expression kind in the DSL and generated.

14 years ago(Not) Handling parameterized sorts in SMT v2
Christopher L. Conway [Thu, 29 Apr 2010 19:45:24 +0000 (19:45 +0000)]
(Not) Handling parameterized sorts in SMT v2

14 years agoMinor fix to SMT v2 parser tests
Christopher L. Conway [Thu, 29 Apr 2010 19:45:21 +0000 (19:45 +0000)]
Minor fix to SMT v2 parser tests

14 years agoFirst draft implementation of SMT v2 parser
Christopher L. Conway [Thu, 29 Apr 2010 16:53:19 +0000 (16:53 +0000)]
First draft implementation of SMT v2 parser

14 years agoSMT parser has to map 'Real' to RealType
Christopher L. Conway [Wed, 28 Apr 2010 20:19:29 +0000 (20:19 +0000)]
SMT parser has to map 'Real' to RealType

14 years agoMerging the arithmetic theory draft (lra-init) back into the main trunk. This should...
Tim King [Wed, 28 Apr 2010 20:14:17 +0000 (20:14 +0000)]
Merging the arithmetic theory draft (lra-init) back into the main trunk.  This should not affect other parts of the system. This code is untested, and is volatile.  It is going to be improved in the future so don't pick on it too much.  I am merging this code in its current state back into the main trunk because it was getting unruly to keep merging the updated trunk back into the branch.

14 years agoadding integer and real types to the public interface
Dejan Jovanović [Wed, 28 Apr 2010 19:51:34 +0000 (19:51 +0000)]
adding integer and real types to the public interface

14 years agoBuild fix for parser
Dejan Jovanović [Wed, 28 Apr 2010 19:42:52 +0000 (19:42 +0000)]
Build fix for parser

14 years agoRefactoring Input/Parser code to support external manipulation of the parser state.
Christopher L. Conway [Wed, 28 Apr 2010 18:34:11 +0000 (18:34 +0000)]
Refactoring Input/Parser code to support external manipulation of the parser state.

14 years agoAdded theory/arith/kind and enabled the smt parser to read in these symbols. Also...
Tim King [Wed, 28 Apr 2010 14:52:22 +0000 (14:52 +0000)]
Added theory/arith/kind and enabled the smt parser to read in these symbols. Also a bug fix to a couple of unit tests.

14 years agoAdding Integer and Rational constants to SMT
Christopher L. Conway [Tue, 27 Apr 2010 20:44:47 +0000 (20:44 +0000)]
Adding Integer and Rational constants to SMT

14 years agoAdding a bit of documentation to the SMT parser
Christopher L. Conway [Tue, 27 Apr 2010 16:54:39 +0000 (16:54 +0000)]
Adding a bit of documentation to the SMT parser

14 years agoSome cleanup. Also added the integer and real types.
Dejan Jovanović [Mon, 26 Apr 2010 23:16:18 +0000 (23:16 +0000)]
Some cleanup. Also added the integer and real types.

14 years agoAdding the intermediary TypeNode to represent (and separate) the Types at the Node...
Dejan Jovanović [Mon, 26 Apr 2010 21:37:34 +0000 (21:37 +0000)]
Adding the intermediary TypeNode to represent (and separate) the Types at the Node level.

14 years agoFixing compiler error for optimized builds
Christopher L. Conway [Sat, 17 Apr 2010 00:43:42 +0000 (00:43 +0000)]
Fixing compiler error for optimized builds

14 years agoAdding info in the minisat README
Dejan Jovanović [Thu, 15 Apr 2010 19:07:50 +0000 (19:07 +0000)]
Adding info in the minisat README

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.