Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: Tests
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-02-11 12:22:34 -0800, Morgan Deters wrote:

At "make check" or "make regress" or "make regressN" time, support running just a subset with something like "make regress PATTERN=precedence".

On 2012-10-06 00:11:57 -0700, Morgan Deters wrote:

done some time ago.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: normal
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-02-03 13:45:10 -0800, Morgan Deters wrote:

As decided here:

http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_January_21,_2010#Notes

the build system should be simplified by removing support for building build profiles from "make" without doing a "configure" for them first.

This is in response to bug 10 (the code review of the build system).

On 2010-02-05 16:17:21 -0800, Morgan Deters wrote:

Subversion revision 171 removes the last bits of support for this.

Imported from Bugzilla
Reporter: Dejan Jovanovic
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: Tests
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2009-12-18 16:27:09 -0800, Dejan Jovanovic wrote:

When CVC4 code is changed, the CXXTEST tests are not rebuilt, and somehow use the old code. I have rebuild everything manually to see if my changes fix the tests.

On 2010-01-27 17:12:41 -0800, Morgan Deters wrote:

Fixed in rev 106. Unit tests (and in the future, system tests) will be rebuilt whenever the library is rebuilt.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: review
Assigned to: Tim King
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: All
OS: All

On 2009-12-15 14:06:38 -0800, Morgan Deters wrote:

Code review of Morgan's and Dejan's code in src/expr.

On 2009-12-16 12:48:21 -0800, Tim King wrote:

****cvc4/src/expr/expr.h ****

Near L32, Expr();
Documentation does not specify the associated memory manager?

The documentation for the _@return value does not match the description of the function. For example:
/**
* Syntactic comparison operator. Returns true if expressions belong to the
* same expression manager and are syntactically identical.
* _@param e the expression to compare to
* _@return true if expressions are syntactically the same, false otherwise
*/
The description specifies that the expression manager must be the same, but the _@return value does not mention the expression manager.

Near L70, I'm not sure what this means:
"The only invariant on the order of expressions
* is that the expressions that were created sooner will be smaller in the
* ordering than all the expressions created later."

Near L100, std::string toString() const;
I added _@return value.
TODO: Where is the string representation specified?
Is this an SMT-lib expr? Presentation?

Near L113, bool isNull() const;
"Check if this is a null expression."
What does this mean? Should be defined here.

Near L117, ExprManager* getExprManager() const;
No _@return value.

Question: Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
Is this type checked?
i.e. do we check that then_e and else_e are of the same type?

On 2009-12-16 13:00:15 -0800, Tim King wrote:

****cvc4/src/expr/expr.cpp****

Near L49, bool Expr::operator==(const Expr& e) const

On 2009-12-16 14:47:24 -0800, Tim King wrote:

****cvc4/src/expr/expr.cpp****

Near L49, bool Expr::operator==(const Expr& e) const
Refactored

Should probably have different names for the following 2 similar but different functions:
Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const {
BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const {

****cvc4/src/expr/node.h****
Author of the file?

Near L16,
Why is this "#include "expr/node_value.h" before the "#ifndef" for the header file?

The documentation says "expression" everywhere.

Should we refactor "d_ev" to "d_nv"?

ALL of the following private methods need to be documented:
inline ev_iterator ev_begin();
inline ev_iterator ev_end();
inline const_ev_iterator ev_begin() const;
inline const_ev_iterator ev_end() const;

ALL of the following public methods need to be documented:

bool operator==(const Node& e) const { return d_ev == e.d_ev; }
bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
Node& operator=(const Node&);

uint64_t hash() const;

Node eqExpr(const Node& right) const;
Node notExpr() const;
Node andExpr(const Node& right) const;
Node orExpr(const Node& right) const;
Node iteExpr(const Node& thenpart, const Node& elsepart) const;
Node iffExpr(const Node& right) const;
Node impExpr(const Node& right) const;
Node xorExpr(const Node& right) const;

Node plusExpr(const Node& right) const;
Node uMinusExpr() const;
Node multExpr(const Node& right) const;

inline Kind getKind() const;

inline size_t numChildren() const;

static Node null();

inline iterator begin();
inline iterator end();
inline const_iterator begin() const;
inline const_iterator end() const;

inline std::string toString() const;
inline void toStream(std::ostream&) const;

bool isNull() const;

**** cvc4/src/expr/node.cpp ****

I do not understand what is going on here. Good sign it should be documented.

NodeValue NodeValue::s_null;

Node Node::s_null(&NodeValue::s_null);

Node Node::null() {
return s_null;
}

Near L70, Node& Node::operator=(const Node& e) {
Does not assert that e.d_ev is not null. But it this may be referenced.
Should it?

Near L70, added parenthesis,
if((this != &e) && (d_ev != e.d_ev)) {

**** cvc4/src/expr/node_value.h ****
NodeValue::node_iterator needs documentation

No clue what is going on in computeHash
return ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId();
We do a shift-rotate 3 on hash and xor the lower 8 bits with the Id?

Again the public functions need to be documented.

Why do inc() and dec() return NodeValue*?
NodeValue* inc();
NodeValue* dec();

How are reverse iterators going to be used? Documentation? These seem to be used in the exact same way except -1 from begin() and end()
iterator rbegin();
iterator rend();

*** cvc4/src/expr/expr_manager.h ***
Changed the documentation for
Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);

Not sure what this means:
"No will be deallocated at this point,"

*** cvc4/src/expr/node_manager.h ***
Currently makes nodes using "Node mkExpr(Kind kind);" Little odd.

No documentation!

Large chunks are commented out.

*** cvc4/src/expr/node_manager.cpp ***
Node NodeManager::lookup(uint64_t hash, NodeValue* ev);
Does not assert that (ev != NULL)

Comment: Node builder notation is freaking weird.
return NodeBuilder<>(this, kind);

*** cvc4/src/expr/node_builder.h/cpp ***
These are messes. I am going to skip these as they seem to be in draft form.

*** cvc4/src/expr/attr_type.h***
Class does not meet coding guidelines: class Type_attr

Where is this typedef used? Is it nessecary?
typedef Type value_type;//Node?

*** cvc4/src/expr/attr_var_name.h***
No clue what is going on in this class.

On 2010-01-19 17:32:38 -0800, Tim King wrote:

Comments and questions will be relevant to revision 96 of cvc4.

Friendly SmtEngine:
Why is SmtEngine a friend class to Expr, ExprManager, (maybe more)?

Garbage collection of Exprs, Nodes, and NodeValue:

1. ~Expr() calls "delete d_node;".
2. This invokes turn calls ~Node.
3. This calls NodeValue::dec().
4. dec() currently has no garbage collecting done, i.e. "// FIXME gc"
   The expression manager is currently not involved with any of this explicitly.
   From group discussions, it sounds like ExprManager will need to be informed of what is getting killed.
   For most Node and NodeValue's grabbing currentNM() and deleting will be fine, but when this chain originates from an Expr the ExprManager will need to be specified somehow.

More documentation is needed near for public methods:
node_value.h::L122 "class node_iterator {..."
node_value.h::L158-L168
node_manager.h
node_builder.h

More documentation for s_null would be nice in node.cpp . I am a bit confused.

In node_manager.cpp the function
"NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {"
does a "return NULL;" near L76 and a "return 0;" near L103.

In node_manager.cpp's "lookup" and "lookupNoInsert" c2 appears to be used the same as c1 yet one is a const_ev_iterator and one is an ev_iterator. Is there a reason for this?

Test cases will be forthcoming.

On 2010-01-25 12:55:58 -0800, Tim King wrote:

Do we really want to have the following be part of Node? Seems like they are theory specific and not always well defined.

Node plusExpr(const Node& right) const;
Node uMinusExpr() const;
Node multExpr(const Node& right) const;

What are the advantages and disadvantages of including them here?

Needs to be documented. I am not sure the syntax for this is obvious.
Node iteExpr(const Node& thenpart, const Node& elsepart) const;

On 2010-01-25 15:35:19 -0800, Tim King wrote:

In order to black box test a good chunk of "class Node", NodeManager::currentNM() *MUST* be set. It is used implicitly by just about every function in this class.

I need a way to set the NodeManager. Directly setting NodeManager::s_current from NodeBlack is not possible because it is private. And making the black box unit tester a friend class to NodeManager feels icky.

Ideas?

On 2010-01-27 13:06:32 -0800, Tim King wrote:

The following do not appear to be defined in node.h or node.cpp:
Node plusExpr(const Node& right) const;
Node uMinusExpr() const;
Node multExpr(const Node& right) const;

I can't find there definition with grep either.

On 2010-02-01 14:30:04 -0800, Dejan Jovanovic wrote:

Am I missing something, or is the implementation of the hash table for expressions (NodeManager) completely unnecessary. What's wrong with using a standard STL hash_map?

On 2010-02-11 19:05:02 -0800, Dejan Jovanovic wrote:

Tim, I'm guessing you wrote the black-box tests for the expr package.

You are using debug assertions to check out of bounds indexing is caught. Unfortunately, this causes a segfault in optimized mode, since assertions are off. This particular assertion we don't want to have as always-assert, so you should either remove the case, or enclose it in some sort of IF_DEBUG block.

All the unit/regress tests should always pass both in debug and optimized mode.

On 2010-02-19 16:03:00 -0800, Tim King wrote:

Just a reminder that node_builder.h has large chunks explicitly commented out as well as a large chunk of code that is removed by the C preprocessor.

#if 0
....
#endif

On 2010-02-21 22:33:12 -0800, Morgan Deters wrote:

(In reply to comment # 9)

Tim, I'm guessing you wrote the black-box tests for the expr package.

You are using debug assertions to check out of bounds indexing is caught.
Unfortunately, this causes a segfault in optimized mode, since assertions are
off. This particular assertion we don't want to have as always-assert, so you
should either remove the case, or enclose it in some sort of IF_DEBUG block.

All the unit/regress tests should always pass both in debug and optimized mode.

I fixed this as part of my check-in from today (since I needed to push through other tests whose behavior is necessarily dependent on whether the code has assertions enabled or not).

Imported from Bugzilla
Reporter: Dejan Jovanovic
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-02-09 21:52:04 -0800, Dejan Jovanovic wrote:

Passing the location of cxxtest as a relative path doesn't work. Not an issue but it would be nice if I could config it with --with-cxxtest-path=../cxxtest, or if this was the default value to search for.

On 2010-02-17 14:07:55 -0800, Morgan Deters wrote:

Hm. This is tricky; if you ./configure, the configure script switches directories (to the appropriate build directory) before doing any configuring. So ../cxxtest is then relative to the build directory, as if you ran configure from inside of that directory.

As a fix, I use the srcdir to find cxxtest IF it's given as a relative path AND the configure script automatically entered a build directory from the source directory. This should do the Right Thing(tm).

Fixed in the repository, revision 211.

Imported from Bugzilla
Reporter: Dejan Jovanovic
Status: RESOLVED
Severity: enhancement
Assigned to: Christopher Conway
Component: Documentation
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-02-22 11:46:26 -0800, Dejan Jovanovic wrote:

void CVC4::TraceC::printf(const char *tag, const char *fmt,...) __attribute__((format(printf at line 222 of file /home/dejan/eclipse-cxx/cvc4/src/util/output.h
void void CVC4::TraceC::printf(std::string tag, const char *fmt,...) __attribute__((format(printf at line 223 of file /home/dejan/eclipse-cxx/cvc4/src/util/output.h
/home/dejan/eclipse-cxx/cvc4/src/parser/antlr_parser.h:173: Warning: Unsupported xml/html tag found
/home/dejan/eclipse-cxx/cvc4/src/parser/antlr_parser.h:173: Warning: end of comment block while expecting command
/home/dejan/eclipse-cxx/cvc4/src/parser/smt/generated/AntlrSmtParser.cpp:270: Warning: Found unknown command `\retrurn'
/home/dejan/eclipse-cxx/cvc4/src/parser/cvc/generated/AntlrCvcParser.cpp:852: Warning: argument 'what' of command _@param is not found in the argument list of AntlrCvcParser::functionSymbol(DeclarationCheck check=CHECK_NONE)
/home/dejan/eclipse-cxx/cvc4/src/parser/cvc/generated/AntlrCvcParser.cpp:852: Warning: The following parameters of AntlrCvcParser::functionSymbol(DeclarationCheck check=CHECK_NONE) are not documented:
parameter 'check'
/home/dejan/eclipse-cxx/cvc4/src/parser/smt/generated/AntlrSmtParser.cpp:270: Warning: Found unknown command `\retrurn'
/home/dejan/eclipse-cxx/cvc4/src/parser/smt/generated/AntlrSmtParser.cpp:270: Warning: Found unknown command `\retrurn'
/home/dejan/eclipse-cxx/cvc4/src/parser/smt/generated/AntlrSmtParser.cpp:404: Warning: The following parameters of AntlrSmtParser::identifier(DeclarationCheck check=CHECK_NONE, SymbolType type=SYM_VARIABLE) are not documented:

/home/dejan/eclipse-cxx/cvc4/src/parser/antlr_parser.h:173: Warning: Unsupported xml/html tag found
/home/dejan/eclipse-cxx/cvc4/src/parser/antlr_parser.h:174: Warning: end of comment block while expecting command
/home/dejan/eclipse-cxx/cvc4/src/parser/antlr_parser.h:173: Warning: Unsupported xml/html tag found
/home/dejan/eclipse-cxx/cvc4/src/parser/antlr_parser.h:174: Warning: end of comment block while expecting command
/home/dejan/eclipse-cxx/cvc4/src/parser/antlr_parser.h:182: Warning: argument 'name' of command _@param is not found in the argument list of CVC4::parser::AntlrParser::getType(std::string var_name, SymbolType type=SYM_VARIABLE)
/home/dejan/eclipse-cxx/cvc4/src/parser/antlr_parser.h:182: Warning: The following parameters of CVC4::parser::AntlrParser::getType(std::string var_name, SymbolType type=SYM_VARIABLE) are not documented:
parameter 'var_name'
/home/dejan/eclipse-cxx/cvc4/src/parser/antlr_parser.h:210: Warning: argument 'child1' of command _@param is not found in the argument list of CVC4::parser::AntlrParser::mkExpr(Kind kind, const Expr &child_1, const Expr &child_2)
/home/dejan/eclipse-cxx/cvc4/src/parser/antlr_parser.h:210: Warning: argument 'child2' of command _@param is not found in the argument list of CVC4::parser::AntlrParser::mkExpr(Kind kind, const Expr &child_1, const Expr &child_2)
/home/dejan/eclipse-cxx/cvc4/src/parser/antlr_parser.h:210: Warning: The following parameters of CVC4::parser::AntlrParser::mkExpr(Kind kind, const Expr &child_1, const Expr &child_2) are not documented:
parameter 'child_1'
parameter 'child_2'
/home/dejan/eclipse-cxx/cvc4/src/parser/parser.h:106: Warning: The following parameters of CVC4::parser::Parser::Parser(std::istream *input, AntlrParser *antlrParser, antlr::CharScanner *antlrLexer, bool deleteInput) are not documented:
parameter 'input'
parameter 'antlrLexer'
parameter 'deleteInput'

On 2010-04-06 11:34:07 -0700, Morgan Deters wrote:

Is this still relevant?

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: review
Assigned to: Clark Barrett
Component: {Internals} Driver
Milestone: ---
Version: master
Platform: All
OS: All

On 2009-12-15 14:09:12 -0800, Morgan Deters wrote:

Code review of Morgan's and Dejan's driver code in src/main.

On 2009-12-16 21:32:22 -0800, Clark Barrett wrote:

getopt.cpp: generally could use more comments! Want to make it easy for other developers to understand how to add/modify command-line options.

getopt.cpp: for some reason progName gets set to lt-cvc4 instead of cvc4. Can we fix this? Maybe just hardwire the name into the code?

getopt.cpp: line 112: intentional fallthrough? should be commented as such.

main.cpp: line 142: ok to delete file if it is &cin?

main.h: Missing file-specific comment.
I prefer to avoid #inlcude in .h files whenever possible. By declaring struct Options, we can avoid including util/options.h

about.h and usage.h:
missing file comments
I suppose the rationale for separating these out is that they are needed by both main.cpp and getopt.cpp. But they seem to really belong in getopt.cpp. In particular, if someone adds an option in getopt.cpp, are they going to remember to change usage.h? Maybe we can use extern references in main. Either that or add a comment in getopt.cpp directing developers to where the about/usage strings live.

util.cpp:
This file needs more comments. In particular, does it just set up signal handlers (in which case it ought to perhaps have a different name), or is the vision for this file to contain additional utilities as well.

On 2009-12-17 00:31:26 -0800, Morgan Deters wrote:

Added comments to getopt.cpp indicating the need to change usage.h. Added a section to the developers' guide on command-line options, and added a link on the wiki "how do I...?" faq page.

The progName is only set to "lt-cvc4" when running from a build directory through the libtool wrapper (e.g. from builds/i686-pc-linux-gnu/default/src/main/cvc4, but not from builds/bin/cvc4). This should never be an issue after cvc4 is installed. It's best to leave the program-name calculation as is, rather than to hardcode it, since the binary could be installed under a different name by a Linux distribution (smtsolver, or redhat-cvc4, or whatever).

Documented the switch fall-through. (debugging implies statistics)

Added file-specific comment to src/main/main.h.

"class Options" forward-declared in main.h instead of including "util/options.h".

The idea for util.cpp was that it might be a general repository for additional utilities. If it doesn't grow to fill that capacity, then agreed, it should be renamed.

On 2010-01-26 02:35:56 -0800, Morgan Deters wrote:

oops, closed wrong bug. reopening.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: normal
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-02-03 13:41:19 -0800, Morgan Deters wrote:

From bug 10..

Will the call to AC_CONFIG_FILES have to be edited any time we
add a source directory? Could this be automated? For example, we
could base the Makefile list off something like
`find src -type d` or
`find . -name 'Makefile.am'`

On 2010-02-05 17:26:37 -0800, Morgan Deters wrote:

Fixed, commit coming shortly. AC_CONFIG_FILES() no longer needs to be modified when you add a Makefile.am in a subdirectory of contrib/, doc/, src/, or test/.

Added a new contrib/addsourcedir script to simplify the process of adding a new source directory with standard Makefile and Makefile.am..

Developer's guide updated to reflect all these changes.

Imported from Bugzilla
Reporter: Clark Barrett
Status: RESOLVED
Severity: normal
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2009-12-16 20:52:05 -0800, Clark Barrett wrote:

If I check out a fresh copy and run configure, I get an error because mkbuilddir is not executable. I'm not sure how to tell svn that mkbuilddir should be executable.

On 2009-12-16 22:31:26 -0800, Morgan Deters wrote:

Fixed.

"svn propset svn:executable filename" is the way to set a file executable in svn.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-03-01 17:10:36 -0800, Morgan Deters wrote:

Current implementations are hacks and require knowledge of theory kinds.

On 2010-03-30 23:58:26 -0700, Morgan Deters wrote:

Fixed as of revision 351.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: review
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: All
OS: All

On 2009-12-17 12:16:06 -0800, Morgan Deters wrote:

The build system needs a review to determine where it should be improved and documented.

On 2010-01-04 17:07:53 -0800, Christopher Conway wrote:

What's the rationale for having all the autotool-generated stuff in SVN?

Rebuilding with an alternative configuration doesn't work as I would.
For example, if I do
./configure debug
make
Then
make OPTIMIZE=1
Nothing seems to be recompiled. I don't have a new directory under
builds/$target. builds/current still references
x86_64-unknown-linux-gnu/debug. What did OPTIMIZE do?

* autogen.sh

Do we really need our own customized script? Could we use buildconf?
http://sourceforge.net/projects/buildconf/

Do we really need the most up-to-date autotools? Can we restrict
ourselves to the versions in Debian stable/RHEL?

The last 8 lines need documentation: why are we doing these operations
in this order?

Running produces the following warnings:
test/unit/Makefile.am:45: filter %_white,$(TESTS: non-POSIX variable name
test/unit/Makefile.am:45: (probably a GNU make extension)
test/unit/Makefile.am:48: filter %_black,$(TESTS: non-POSIX variable name
test/unit/Makefile.am:48: (probably a GNU make extension)
test/unit/Makefile.am:51: filter %_public,$(TESTS: non-POSIX variable name
test/unit/Makefile.am:51: (probably a GNU make extension)

* configure.ac

Moved documentation of version numbers here from src/Makefile.am.
Needs clarification: what is an "interface" and how do I know if
it has been added, removed, or changed?

What does this line do?
# really irritating: AC_CANONICAL_* bash $@
config_cmdline="$@"

The build type stuff is real spaghetti. There has to be a way to
simplify this...

How does CVC4_CONFIGURE_IN_BUILDS work?

The output of config/build-type is the worst of both worlds:
not at all concise and incredibly cryptic. I think I would prefer
one-letter abbreviations all smushed together. For example,
"optimized with assertions and profiling" becomes "aop" and
"debug with tracing and coverage" becomes "cdt".

Alternatively, since this is primarily going to be used to name a
directory which the shell can tab-complete for us, we could just
use entire words instead of abbreviations. I.e., "opt-assert-profile"
and "debug-trace-coverage".

I don't see why we need user_cppflags et al. Can't we just append
the computed CPPFLAGS et al. onto whatever the user provides?

What does this line do?
_LT_SET_OPTION([LT_INIT],[win32-dll])

What's the purpose of mk_include?

Will the call to AC_CONFIG_FILES have to be edited any time we
add a source directory? Could this be automated? For example, we
could base the Makefile list off something like
`find src -type d` or
`find . -name 'Makefile.am'`

* Makefile.builds.in

This needs to be documented.

* config/cvc4.m4

Is this argument preprocessing really necessary. The implementation
is difficuilt to understand and likely to confusing errors. For example,

 $ ./configure \-\-with\-include foo
 <...>
 : error: unknown build profile: foo

Actually, it's buggy too:

$ ./configure \-\-with\-include /tmp/foo
<...>
checking for requested build profile... /tmp/foo
checking for appropriate build string... /tmp/foo
checking what dir to configure... builds/x86\_64\-unknown\-linux\-gnu//tmp/foo
<...>
cd builds/x86\_64\-unknown\-linux\-gnu//tmp/foo
../../../configure \-\-with\-include \-\-with\-build\=/tmp/foo
./configure: line 2903: /home/chris/Source/Eclipse/cvc4/builds/x86\_64\-unknown\-linux\-gnu/tmp/foo/../../../configure: No such file or directory

* src/Makefile.am

Do we want to use the -release flag for libcvc4? It seems to be in
conflict with -version-info. According to the libtool docs: "In
general, you should only use -release for package-internal libraries
or for ones whose interfaces change very frequently."

On 2010-01-28 13:16:37 -0800, Christopher Conway wrote:

I replaced autogen.sh with the buildconf version, but have otherwise left the build system unchanged.

On 2010-02-03 12:59:52 -0800, Morgan Deters wrote:

(In reply to comment # 2)

I replaced autogen.sh with the buildconf version, but have otherwise left the
build system unchanged.

...and Makefile.ins have been removed.

As noted here:

http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_January_21,_2010#Notes

it was decided by the team to remove the support for building profiles without first configuring them. This work (removing this) is still pending.

On 2010-02-03 13:37:49 -0800, Morgan Deters wrote:

(In reply to comment # 1)

Do we really need the most up-to-date autotools? Can we restrict
ourselves to the versions in Debian stable/RHEL?

Probably not-- I'm getting the CIMS guys to look at bringing the tools up to date system-wide.

Running produces the following warnings:
test/unit/Makefile.am:45: filter %_white,$(TESTS: non-POSIX variable name
test/unit/Makefile.am:45: (probably a GNU make extension)
test/unit/Makefile.am:48: filter %_black,$(TESTS: non-POSIX variable name
test/unit/Makefile.am:48: (probably a GNU make extension)
test/unit/Makefile.am:51: filter %_public,$(TESTS: non-POSIX variable name
test/unit/Makefile.am:51: (probably a GNU make extension)

This has been fixed.

What does this line do?
# really irritating: AC_CANONICAL_* bash $@
config_cmdline="$@"

Additional documentation provided.

How does CVC4_CONFIGURE_IN_BUILDS work?

Documented.

The output of config/build-type is the worst of both worlds:
not at all concise and incredibly cryptic. I think I would prefer
one-letter abbreviations all smushed together. For example,
"optimized with assertions and profiling" becomes "aop" and
"debug with tracing and coverage" becomes "cdt".

These have been changed to include the full names (the same as what is used for --enable-* or --disable-* at configure-time). So these examples become "*-optimized-assertions-profiling" and "*-debugsymbols-tracing-coverage".

I don't see why we need user_cppflags et al. Can't we just append
the computed CPPFLAGS et al. onto whatever the user provides?

Done.

What's the purpose of mk_include?

Documented.

Will the call to AC_CONFIG_FILES have to be edited any time we
add a source directory? Could this be automated? For example, we
could base the Makefile list off something like
`find src -type d` or
`find . -name 'Makefile.am'`

I'll work on this..

* Makefile.builds.in

This needs to be documented.

Documented.

* config/cvc4.m4

Is this argument preprocessing really necessary. The implementation
is difficuilt to understand and likely to confusing errors. For example,

 $ ./configure \-\-with\-include foo
 <...>
 : error: unknown build profile: foo

Actually, it's buggy too:

$ ./configure \-\-with\-include /tmp/foo
<...>
checking for requested build profile... /tmp/foo
checking for appropriate build string... /tmp/foo
checking what dir to configure... builds/x86\_64\-unknown\-linux\-gnu//tmp/foo
<...>
cd builds/x86\_64\-unknown\-linux\-gnu//tmp/foo
../../../configure \-\-with\-include \-\-with\-build\=/tmp/foo
./configure: line 2903:

/home/chris/Source/Eclipse/cvc4/builds/x86_64-unknown-linux-gnu/tmp/foo/../../../configure:
No such file or directory

I'll take a look..

* src/Makefile.am

Do we want to use the -release flag for libcvc4? It seems to be in
conflict with -version-info. According to the libtool docs: "In
general, you should only use -release for package-internal libraries
or for ones whose interfaces change very frequently."

Done.

On 2010-02-03 13:46:10 -0800, Morgan Deters wrote:

This has spawned (more specific) task bugs 19, 20, and 21. Closing the code review ticket.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: enhancement
Assigned to: Christopher Conway
Component: {Internals} Parser infrastructure
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-02-09 16:37:54 -0800, Morgan Deters wrote:

There's a need for operator precedence tests.

On 2010-02-11 12:33:01 -0800, Christopher Conway wrote:

Committed to test/regress/regress0/precedence/

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: normal
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-03-09 10:23:03 -0800, Morgan Deters wrote:

"make; make check" works as expected but "make check" with library updates does not. This is because "make check" doesn't do the top-level copying of binary/libraries before checking.

On 2010-04-04 16:12:30 -0700, Morgan Deters wrote:

Partially fixed in revision 378.

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.

On 2010-04-04 16:13:14 -0700, Morgan Deters wrote:

Lowering importance since the major symptom of this bug has been fixed.

On 2010-09-01 18:25:13 -0700, Morgan Deters wrote:

Fixed in r847.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: review
Assigned to: Dejan Jovanovic
Component: {Internals} Context manager
Milestone: ---
Version: master
Platform: All
OS: All

On 2009-12-15 14:05:32 -0800, Morgan Deters wrote:

Code review of Clark's memory management code in src/context.

On 2010-02-01 18:17:44 -0800, Dejan Jovanovic wrote:

The only comment I have with respect to the new Context/Scope code is that it might be simpler to just have a vector of Scopes indexed by levels. But I guess this is a matter of taste. I'll go ahead and write some tests.

On 2010-02-02 12:00:28 -0800, Clark Barrett wrote:

Expanding the scope of this review to include all the context package.

On 2010-02-02 17:04:49 -0800, Dejan Jovanovic wrote:

void setUp() {
d_context = new Context();
}

void testIntCDO() {
CDO a1(d_context);
}

void tearDown(){
delete d_context;
}

fails with

Program received signal SIGSEGV, Segmentation fault.
0x08053709 in CVC4::context::ContextMemoryManager::pop (this=0x8061038)
at /home/dejan/eclipse-cxx/cvc4/builds/i686-pc-linux-gnu/debug/../../../src/context/context_mm.cpp:101
101 d_nextFree = d_nextFreeStack.back();
(gdb) where
# 0 0x08053709 in CVC4::context::ContextMemoryManager::pop (this=0x8061038)
at /home/dejan/eclipse-cxx/cvc4/builds/i686-pc-linux-gnu/debug/../../../src/context/context_mm.cpp:101
# 1 0x0805153b in CVC4::context::Context::pop (this=0x8061018) at /home/dejan/eclipse-cxx/cvc4/builds/i686-pc-linux-gnu/debug/../../../src/context/context.cpp:87
# 2 0x08051594 in CVC4::context::Context::popto (this=0x8061018, toLevel=-1)
at /home/dejan/eclipse-cxx/cvc4/builds/i686-pc-linux-gnu/debug/../../../src/context/context.cpp:103
# 3 0x0805136b in ~Context (this=0x8061018, __in_chrg=)
at /home/dejan/eclipse-cxx/cvc4/builds/i686-pc-linux-gnu/debug/../../../src/context/context.cpp:36
# 4 0x0804fe79 in ContextBlack::tearDown (this=0x8060118) at /home/dejan/eclipse-cxx/cvc4/builds/i686-pc-linux-gnu/debug/../../../test/unit/context/context_black.h:41
# 5 0x0804af8b in CxxTest::RealTestDescription::tearDown (this=0x8060128) at /home/dejan/software/cxxtest/cxxtest/RealDescriptions.cpp:66
# 6 0x0804e05d in CxxTest::TestRunner::runTest (this=0xbffff73f, td=...) at /home/dejan/software/cxxtest/cxxtest/TestRunner.h:75
# 7 0x0804df73 in CxxTest::TestRunner::runSuite (this=0xbffff73f, sd=...) at /home/dejan/software/cxxtest/cxxtest/TestRunner.h:61
# 8 0x0804de5a in CxxTest::TestRunner::runWorld (this=0xbffff73f) at /home/dejan/software/cxxtest/cxxtest/TestRunner.h:46
# 9 0x0804dc54 in CxxTest::TestRunner::runAllTests (listener=...) at /home/dejan/software/cxxtest/cxxtest/TestRunner.h:23
# 10 0x0804e35d in CxxTest::ErrorFormatter::run (this=0xbffff79c) at /home/dejan/software/cxxtest/cxxtest/ErrorFormatter.h:47
# 11 0x08049c91 in main () at context/context_black.cpp:16

On 2010-02-02 17:42:24 -0800, Clark Barrett wrote:

Fixed problem from Comment # 3

Imported from Bugzilla
Reporter: Christopher Conway
Status: RESOLVED
Severity: enhancement
Assigned to: Dejan Jovanovic
Component: {Internals} Parser infrastructure
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2009-12-16 13:35:43 -0800, Christopher Conway wrote:

$ ./builds/bin/cvc4 --lang pl test/regress/bug1.cvc
CVC4 Error:
Parse Error: test/regress/bug1.cvc:1:1: unexpected char: '%'
Aborted

On 2009-12-17 13:55:00 -0800, Christopher Conway wrote:

This problem went away after I blew away my builds directory and nobody else could duplicate.

Imported from Bugzilla
Reporter: Tim King
Status: RESOLVED
Severity: major
Assigned to: Tim King
Component: Uninterpreted functions
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-02-26 13:56:04 -0800, Tim King wrote:

As it stands, there is an inconsistency between ECData and the assumption that TNodes need a ref count of zero at destruction time.

Let us say that a Node n maps to an ECData ecN.
ecN has a field Tnode rep that maps back to n.
Equivalently this is the invariant,
(n.getAttribute(ECAttr()))->rep == n
This is needed in order for there to not always be a hard link to n.
When n gets destructed, the problem is that n->d_nv.d_rc == 0, and so when (n.getAttribute(ECAttr()))->rep gets destructed the following assertion in the NodeTemplate destructor is violated,
Assert(ref_count || d_nv->d_rc > 0, "Temporary node pointing to an expired node");

We will need to make a work around for this in the near future. For now I am just disabling this assertion in my working copy of the code.

On 2010-03-23 15:44:12 -0700, Tim King wrote:

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. This allows for the rep in an ECData to be deleted.

Imported from Bugzilla
Reporter: Dejan Jovanovic
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-02-08 22:19:56 -0800, Dejan Jovanovic wrote:

Configure on a fresh svn checkout gives

checking for uint64_t... yes
checking for size_t... yes
: creating ./config.status
config.status: creating Makefile.builds
config.status: error: cannot find input file: `Makefile.in'

If I run autogen everything is fine, but as I recall we are keeping ./configure in the svn so that we don't need to autogen.

On 2010-02-09 17:03:37 -0800, Morgan Deters wrote:

Removed other parts of autotools stuff. Run autogen.sh on a clean checkout, as it says in the README. Fixed in revision 184.

Imported from Bugzilla
Reporter: Christopher Conway
Status: RESOLVED
Severity: enhancement
Assigned to: Christopher Conway
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-03-09 17:26:06 -0800, Christopher Conway wrote:

Do we want a DISTINCT kind in the Expr package, or should these just be generated as a conjunction of disequalities?

On 2010-03-09 18:44:38 -0800, Christopher Conway wrote:

Implemented in SVN, by generating the conjunction in the parser.

On 2010-03-09 19:14:30 -0800, Dejan Jovanovic wrote:

Ultimately it would be best to have a better way of dealing with DISTINCT. Until we can come up with one, exploding the dis-equalities is good.

Imported from Bugzilla
Reporter: Dejan Jovanovic
Status: RESOLVED
Severity: major
Assigned to: Morgan Deters
Component: {Internals} Utilities
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-02-12 14:02:44 -0800, Dejan Jovanovic wrote:

We've annotated the code all over with tracing information, but this expensive code is not compiled out in optimized mode. Stuff like

Debug("parser") << "newSort(" << name << ")" << std::endl;

should be compiled out in optimized mode. In the profiling I did for the parser on big examples, some of top non-parser calls are

CVC4::null_streambuf::overflow(int),
CVC4::expr::NodeValue::toStream(std::ostream&) const,

and these don't belong to the optimized build.

On 2010-02-12 16:24:00 -0800, Morgan Deters wrote:

Same as bug 22.

On 2010-02-21 17:30:06 -0800, Morgan Deters wrote:

Dejan resolved this in revision 199 to src/util/output.h.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-02-03 18:02:32 -0800, Morgan Deters wrote:

Collect Kinds from different theories and generate a kind.h.

On 2010-02-03 23:08:36 -0800, Morgan Deters wrote:

This should work (more or less?) now.

Imported from Bugzilla
Reporter: Christopher Conway
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-02-19 19:40:49 -0800, Christopher Conway wrote:

$ ./configure --disable-shared --enable-static
$ make
$ file builds/bin/cvc4
builds/bin/cvc4: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.15, not stripped
$ ldd builds/bin/cvc4
linux-vdso.so.1 => (0x00007fff19f7d000)
libgmp.so.3 => /usr/lib/libgmp.so.3 (0x00007f59fb0f9000)
libstdc++.so.6 => /usr/lib/libstdc++.so.6 (0x00007f59fade9000)
libm.so.6 => /lib/libm.so.6 (0x00007f59fab65000)
libgcc_s.so.1 => /lib/libgcc_s.so.1 (0x00007f59fa94e000)
libc.so.6 => /lib/libc.so.6 (0x00007f59fa5df000)
/lib64/ld-linux-x86-64.so.2 (0x00007f59fb35d000)

On 2010-02-22 01:54:33 -0800, Morgan Deters wrote:

This is the usual autoconf/libtool behavior (dynamically link all binaries; statically link only built libraries). But this is probably an important feature to have. Fixed in revision 229: if shared libraries are built, the binary is dynamically-linked. If static-ONLY libraries are built, the binary is statically-linked.

On 2010-02-22 10:48:50 -0800, Christopher Conway wrote:

I'm not sure I understand the resolution. Could you give examples of which configuration options lead to which outcomes?

On 2010-02-22 11:56:02 -0800, Morgan Deters wrote:

Here's the breakdown:

$ ./configure --enable-shared --enable-static builds both kinds of libraries, and the binary is dynamically linked against the shared libraries

$ ./configure --enable-shared --disable-static builds shared libraries only, and the binary is dynamically linked against them

$ ./configure --disable-shared --enable-static builds static libraries only, and the binary is statically linked against them AND statically linked against libc etc.

This resolves the original bug report rather literally. autoconf preferred, in the --disable-shared --enable-static case, to link statically against libcvc4 and libcvc4parser, but link dynamically against libm, libc, libgmp, etc. This is intentional. See, e.g.,

http://people.redhat.com/drepper/no_static_linking.html

Other teams, when they really want fully-static binaries, sometimes have an --enable-fullstatic flag or similar.

On 2010-02-22 12:34:04 -0800, Christopher Conway wrote:

I'm OK with an --enable-full-static option.

On 2010-02-22 12:52:30 -0800, Morgan Deters wrote:

(In reply to comment # 4)

I'm OK with an --enable-full-static option.

I feel it makes little sense under that wording. It would seem to conflict with dynamic linking. So you couldn't --enable-shared --enable-full-static.

Maybe --enable-static-binary ?

On 2010-02-22 14:00:51 -0800, Morgan Deters wrote:

(In reply to comment # 5)

(In reply to comment # 4)

I'm OK with an --enable-full-static option.

I feel it makes little sense under that wording. It would seem to conflict
with dynamic linking. So you couldn't --enable-shared --enable-full-static.

Maybe --enable-static-binary ?

Added --enable-static-binary option to configure in revision 232.

On 2010-02-22 14:28:09 -0800, Morgan Deters wrote:

(In reply to comment # 6)

(In reply to comment # 5)

(In reply to comment # 4)

I'm OK with an --enable-full-static option.

I feel it makes little sense under that wording. It would seem to conflict
with dynamic linking. So you couldn't --enable-shared --enable-full-static.

Maybe --enable-static-binary ?

Added --enable-static-binary option to configure in revision 232.

Make that 234; 232 was committed improperly.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: major
Assigned to: Morgan Deters
Component: {Internals} Utilities
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-02-03 14:21:01 -0800, Morgan Deters wrote:

Review the utility code to ensure that there are no traces of Trace() or Debug() support when a non-debug build is performed.

On 2010-02-21 20:11:14 -0800, Morgan Deters wrote:

Also reported as bug 30.

Dejan resolved the Debug issue in revision 199 to src/util/output.h.

I fixed the Trace issue in revision 228 to src/util/output.h.

Muzzling now compiles all output classes out of the build.

Added output unit tests.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: review
Assigned to: Morgan Deters
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-02-09 16:35:58 -0800, Morgan Deters wrote:

Perform a code review and write blackbox unit tests for the Type infrastructure under src/expr.

On 2010-04-01 02:32:58 -0700, Morgan Deters wrote:

The Type infrastructure is begin replaced, so I won't write tests against this Type stuff at this time. Chris requested comments, so I'll make a few and close the ticket.

The design is a very Java-like one, with virtual testers in the base, overridden by derived classes. (e.g. isFunction() returns false by default and true in the FunctionType derived class.) This requires knowledge of the type hierarchy in the base class, but this is probably appropriate in this case.

Some things were left undefined (that should have been), but I guess they were never called:

Type::operator==(const Type&) const;
Type::operator!=(const Type&) const;

The only real problem with the Type infrastructure, as originally written, is that Types were never freed. The current hackish reference-counting of Types (they are reference-counted in how many times they appear as values the Type attribute table) is functional, partly, but broken: the reference-counts should also be incremented/decremented if they are component Types of another Type, for example the rangeType and argTypes of FunctionType. Further, "sort" types never appear in type attribute tables, so they still leak. However, since the Type infrastructure is going to be replaced with an Expr/Node-based solution, this is probably now moot.

Closing the ticket.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: normal
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-02-03 13:39:48 -0800, Morgan Deters wrote:

From bug 10..

* config/cvc4.m4

Is this argument preprocessing really necessary. The implementation
is difficuilt to understand and likely to confusing errors. For example,

 $ ./configure \-\-with\-include foo
 <...>
 : error: unknown build profile: foo

Actually, it's buggy too:

$ ./configure \-\-with\-include /tmp/foo
<...>
checking for requested build profile... /tmp/foo
checking for appropriate build string... /tmp/foo
checking what dir to configure... builds/x86\_64\-unknown\-linux\-gnu//tmp/foo
<...>
cd builds/x86\_64\-unknown\-linux\-gnu//tmp/foo
../../../configure \-\-with\-include \-\-with\-build\=/tmp/foo
./configure: line 2903:

/home/chris/Source/Eclipse/cvc4/builds/x86_64-unknown-linux-gnu/tmp/foo/../../../configure:
No such file or directory

On 2010-02-22 13:59:53 -0800, Morgan Deters wrote:

Fixed in revision 232. Only valid build profiles { production, debug, default, competition } are permitted. "foo" won't work, "/tmp/foo" won't work, etc.

(In reply to comment # 0)

From bug 10..

* config/cvc4.m4

Is this argument preprocessing really necessary. The implementation
is difficuilt to understand and likely to confusing errors. For example,

 $ ./configure \-\-with\-include foo
 <...>
 : error: unknown build profile: foo

Actually, it's buggy too:

$ ./configure \-\-with\-include /tmp/foo
<...>
checking for requested build profile... /tmp/foo
checking for appropriate build string... /tmp/foo
checking what dir to configure... builds/x86\_64\-unknown\-linux\-gnu//tmp/foo
<...>
cd builds/x86\_64\-unknown\-linux\-gnu//tmp/foo
../../../configure \-\-with\-include \-\-with\-build\=/tmp/foo
./configure: line 2903:

/home/chris/Source/Eclipse/cvc4/builds/x86_64-unknown-linux-gnu/tmp/foo/../../../configure:
No such file or directory

On 2010-02-22 14:28:30 -0800, Morgan Deters wrote:

(In reply to comment # 1)

Fixed in revision 232. Only valid build profiles { production, debug, default,
competition } are permitted. "foo" won't work, "/tmp/foo" won't work, etc.

Make that 234. Revision 232 was committed improperly.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: minor
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-02-24 22:29:21 -0800, Morgan Deters wrote:

$as_me is not set properly in configure script thanks to some strangeness with m4 expansion and the specialized config/cvc4.m4 stuff.

config.status seems to work, oddly enough.

On 2012-10-06 00:42:05 -0700, Morgan Deters wrote:

fixed.

Imported from Bugzilla
Reporter: Tim King
Status: RESOLVED
Severity: major
Assigned to: Morgan Deters
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: PC
OS: Linux

Original attachment names and IDs:

• node_black.h (node_black.h, ID 1)

On 2010-01-25 19:20:12 -0800, Tim King wrote:

The children to an explicitly built node are NULL when accessed through an iterator. I have attached source code that produces the problem. It could be that the code should not work?

The attached file can be dropped in place of cvc4/test/unit/expr/node_black.h.
When run via 'make check' from cvc4/test/unit the bizarre test passes.

Possibly related to why cvc4/test/regression/hole6.cvc fails?

On 2010-01-25 19:20:39 -0800, Tim King wrote:

Created attachment 1
node_black.h

On 2010-01-26 02:34:37 -0800, Morgan Deters wrote:

This "bizarre test" no longer passes, and hole6.cvc gives valid.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-03-01 17:09:37 -0800, Morgan Deters wrote:

Current implementation is a "major hack!"

On 2010-04-01 01:57:36 -0700, Morgan Deters wrote:

Addressed by revision 363.

Imported from Bugzilla
Reporter: Christopher Conway
Status: RESOLVED
Severity: enhancement
Assigned to: Dejan Jovanovic
Component: {Internals} Parser infrastructure
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-01-04 18:28:24 -0800, Christopher Conway wrote:

Configured with:
./configure debug --with-cxxtest-dir=/home/chris/Tools/cxxtest

$ make check
<...>
Running 2 tests..OK!
PASS: expr/node_white
Running 2 tests..OK!
PASS: expr/node_black
Running 8 testsTesting input: ''
Testing input: 'ASSERT TRUE;'
kind TRUE
Parsed command: Assert((TRUE))
Testing input: 'QUERY TRUE;'
kind TRUE
Parsed command: Query((TRUE))
Testing input: 'CHECKSAT FALSE;'
kind FALSE
Parsed command: CheckSat((FALSE))
Testing input: 'a, b : BOOLEAN;'
kind VARIABLE
kind VARIABLE
Parsed command: Declare(a, b)
Testing input: 'a, b : BOOLEAN; QUERY (a => b) AND a => b;'
kind VARIABLE
kind VARIABLE
Parsed command: Declare(a, b)
kind IMPLIES
kind IMPLIES
kind AND
Parsed command: Query((AND 0 0))
Testing input: '%% nothing but a comment'
Testing input: '% a comment
ASSERT TRUE; %a command
% another comment'
kind TRUE
Parsed command: Assert((TRUE))
.Testing input: ';'
Testing input: 'ASSERT;'
Testing input: 'QUERY'
Testing input: 'CHECKSAT'
Testing input: 'a, b : boolean;'
Testing input: '0x : INT;'
Testing input: 'a, b : BOOLEAN
QUERY (a => b) AND a => b;'
kind VARIABLE
kind VARIABLE
Testing input: 'a : BOOLEAN; a: BOOLEAN;'
kind VARIABLE
/bin/bash: line 5: 16888 Segmentation fault ${dir}$tst
FAIL: parser/parser_black
===================
1 of 3 tests failed
===================

On 2010-02-01 18:21:28 -0800, Dejan Jovanovic wrote:

Fixed make check.

Imported from Bugzilla
Reporter: Tim King
Status: RESOLVED
Severity: enhancement
Assigned to: Christopher Conway
Component: {Internals} Parser infrastructure
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-02-11 17:20:34 -0800, Tim King wrote:

Here are a smattering of current parser failures in regress2 and regress3:

$cvc4 instance_1444.smt
CVC4 Error:
Parse Error: instance_1444.smt:1268:1: Expected at least 2 arguments for operator 'AND'. Found: 0
Aborted

$cvc4 bmc-ibm-10.smt
CVC4 Error:
Parse Error: bmc-ibm-10.smt:362873:1: Expected at most 4294967295 arguments for operator 'AND'. Found: 303804
Aborted

$ cvc4 bmc-ibm-6.smt
CVC4 Error:
Parse Error: bmc-ibm-6.smt:404526:1: Expected at most 4294967295 arguments for operator 'AND'. Found: 352874
Aborted

$ cvc4 instance_1151.smt
CVC4 Error:
Parse Error: instance_1151.smt:1432:1: Expected at least 2 arguments for operator 'AND'. Found: 0
Aborted

Preceded by
make clean ; ./autogen.sh ; ./configure ; make -j4

On 2010-02-19 12:39:28 -0800, Christopher Conway wrote:

I've committed a fix for the min arity problem on AND/OR (SMT allows AND/OR to be applied to a single argument, I had assume at least 2).

I don't get the max arity messages on my machine.

On 2010-02-19 15:43:05 -0800, Christopher Conway wrote:

Can anybody reproduce the max arity problem?

On 2010-04-01 16:08:45 -0700, Christopher Conway wrote:

The minArity problem is fixed. I've never seen the maxArity problem. Re-open if you can reproduce.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-03-01 17:55:13 -0800, Morgan Deters wrote:

Change getNumChildren(), begin(), operator[], etc., to handle children properly for APPLY nodes. Re-review the expr package to make sure internals (e.g., refcounts, etc.) are still managed ok.

On 2010-03-30 23:58:58 -0700, Morgan Deters wrote:

Fixed as of revision 351.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: review
Assigned to: Kaustubh Nimkar
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-01-12 12:03:26 -0800, Morgan Deters wrote:

Additional code review of the code under src/expr: review code, make suggestions, fix documentation, file bug reports, write black box tests.

On 2010-01-24 12:57:58 -0800, Kaustubh Nimkar wrote:

Few comments.

1. The prototype for std::copy algorithm is as follows.

template <class InputIterator, class OutputIterator>
OutputIterator copy ( InputIterator first, InputIterator last, OutputIterator result );

Sequence of arguments being passed to all the calls to std::copy() in node_builder.h file is incorrect.

2. We have following declaration for d_childrenStorage array in file node_builder.h

NodeValue *d_childrenStorage[nchild_thresh];

However in all the constructors d_childrenStorage is being initialized to 0, which I think is wrong. Also it's not clear the use of d_childrenStorage array.

3)The motivation behind using following declaration of d_children inside NodeValue class is not clear.

/** Variable number of child nodes */
NodeValue *d_children[0];

I understand the use of 0 length array, but it's not clear why we need to use this when the same thing can be implemented using simpler methods. (e.g vectors)

Also, I'm not sure if this use is standard and all the compilers support it.

On 2010-01-31 07:39:02 -0800, Kaustubh Nimkar wrote:

I think, the NodeManager::lookup(uint64_t hash, NodeValue* ev) function is buggy.

The last four lines in the else block of the function are :

// didn't find it, insert
std::vector<Node> v;
Node e(ev);
v.push\_back(e);
d\_hash.insert(std::make\_pair(hash, v));
return e;

Here we have found the hash key in the d_hash map but we could not find the NodeValue in the Node vector associated with the hash key. But while inserting we are creating a new vector, adding NodeValue and trying to insert it in d_hash map. The hash key is still the same and thus this insert would fail as the same key already exists in the map.

I think the right code is

// didn't find it, insert
Node e(ev);
i\->second.push\_back(e);
return e;

On 2010-02-01 12:17:30 -0800, Kaustubh Nimkar wrote:

Morgan,

After looking at the expr code, I have developed the following understanding of the code. Please confirm that my understanding is correct.

1. The purpose of a Node Manager is to maintain the hash map that checks if we have previously built the required expression.
   If yes, then it adjusts the NodeValue pointer of the Node being created to point to that expression which in turn avoids duplication.

2. A Node class can represent any generic expression. However Expr class is a wrapper around Node class pointer.
   A subclass of Expr will be used to create expressions from a particular theory. e.g. BoolExpr will create Boolean expressions.
   Similarly there will be subclasses for other theories. Each subclass will provide functions to build expressions only from that particular theory.
   This is the main reason for providing Expr class wrapper around Node class Pointer.

If my understanding is correct and if Tim has not already started working on black box tests for Expr package, I would like to take up that task.
Can you please confirm?

On 2010-02-01 12:28:40 -0800, Morgan Deters wrote:

(In reply to comment # 2)

I think, the NodeManager::lookup(uint64_t hash, NodeValue* ev) function is
buggy.

The last four lines in the else block of the function are :

// didn't find it, insert
std::vector<Node> v;
Node e(ev);
v.push\_back(e);
d\_hash.insert(std::make\_pair(hash, v));
return e;

Here we have found the hash key in the d_hash map but we could not find the
NodeValue in the Node vector associated with the hash key. But while inserting
we are creating a new vector, adding NodeValue and trying to insert it in
d_hash map. The hash key is still the same and thus this insert would fail as
the same key already exists in the map.

I think the right code is

// didn't find it, insert
Node e(ev);
i\->second.push\_back(e);
return e;

Fixed. Committed as Subversion revision 125.

On 2010-02-01 12:37:25 -0800, Morgan Deters wrote:

(In reply to comment # 3)

Morgan,

After looking at the expr code, I have developed the following understanding of
the code. Please confirm that my understanding is correct.

1. The purpose of a Node Manager is to maintain the hash map that checks if we
   have previously built the required expression.
   If yes, then it adjusts the NodeValue pointer of the Node being created to
   point to that expression which in turn avoids duplication.

2. A Node class can represent any generic expression. However Expr class is a
   wrapper around Node class pointer.
   A subclass of Expr will be used to create expressions from a particular theory.
   e.g. BoolExpr will create Boolean expressions.

No, however this is still in flux. Theories will use Nodes for efficiency, not Exprs.

"Expr" is intended as a "public view" into Nodes. Nodes are used internally only because they have no pointer back to their NodeManager. Exprs have a link to their ExprManager, so are safe for use outside of the cvc4 library because we can set the right Manager context on entry to the library. (With Nodes, multiple managers could be active at once and strange behavior could result..)

BoolExpr, e.g., is just an Expr known to have boolean type, and were written (I believe) before the Node/Expr split. We could just as easily have a BoolNode. This would be a lightweight subclass just intended to get some assistance from C++'s type system if we do something (obviously) wrong.

Similarly there will be subclasses for other theories. Each subclass will
provide functions to build expressions only from that particular theory.
This is the main reason for providing Expr class wrapper around Node class
Pointer.

see above

If my understanding is correct and if Tim has not already started working on
black box tests for Expr package, I would like to take up that task.
Can you please confirm?

Tim has worked on the Expr black-box tests. However, I encourage you to write some of your own, then have a look at what he has, then write some more! :-) You could put your unit tests in test/expr/expr2_black.h, or test/expr/expr_kaustubh_black.h, or something like that for now.

The Expr package is central to CVC4 and we must get it right. More test cases here, I think, will not be wasted, and serve the purpose not just of finding bugs but of having early clients (you and Tim) for Exprs so that you can point out strange things in the interface that should be addressed.

On 2010-02-06 07:04:07 -0800, Kaustubh Nimkar wrote:

I think, we have a memory leak in the NodeBuilder for the following case.

While building the node we had to allocate memory for the children using realloc() function. evIsAllocated() is true in this case. While building the node in the operator Node() function, we find that the expression being built already exists in the node manager. In this case, we set d_used = true and return a Node with a NodeValue pointer pointing to the expression in the node manager. However this causes a memory leak as we are not freeing the memory allocated for the d_ev pointer.

I think we should not set d_used = true (line no 583, node_builder.h) so that the memory is freed in the NodeBuilder destructor.

On 2010-02-06 12:31:48 -0800, Morgan Deters wrote:

(In reply to comment # 6)

I think, we have a memory leak in the NodeBuilder for the following case.

While building the node we had to allocate memory for the children using
realloc() function. evIsAllocated() is true in this case. While building the
node in the operator Node() function, we find that the expression being built
already exists in the node manager. In this case, we set d_used = true and
return a Node with a NodeValue pointer pointing to the expression in the node
manager. However this causes a memory leak as we are not freeing the memory
allocated for the d_ev pointer.

I think we should not set d_used = true (line no 583, node_builder.h) so that
the memory is freed in the NodeBuilder destructor.

Good catch! Fixed in revision 176. Added a dealloc() member to handle deallocation in the destructor, clear(), and this case.

On 2010-02-07 08:45:00 -0800, Kaustubh Nimkar wrote:

We are not setting the id of the node being created in the following case.

In Operator Node() function in NodeBuilder when evIsAllocated() is true but we don't find the expression being created in the Node Manager.

after ev = d_ev (line 601 node_builder.h)
we should have, ev->d_id = NodeValue::next_id++;

On 2010-02-07 09:05:00 -0800, Kaustubh Nimkar wrote:

In the NodeValue::hash() function we use d_kind to compute the hash value.
However while a Node is being created in the NodeBuilder we don't use d_kind of the Node to compute hash while doing any operation related to hash map in the Node Manager.

Is this expected?

Imported from Bugzilla
Reporter: Dejan Jovanovic
Status: RESOLVED
Severity: enhancement
Assigned to: Dejan Jovanovic
Component: Documentation
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-02-22 11:48:11 -0800, Dejan Jovanovic wrote:

/home/dejan/eclipse-cxx/cvc4/src/expr/type.h:226: Warning: argument 'e' of command _@param is not found in the argument list of CVC4::operator<<(std::ostream &out, const Type &t)
/home/dejan/eclipse-cxx/cvc4/src/expr/type.h:226: Warning: The following parameters of CVC4::operator<<(std::ostream &out, const Type &t) are not documented:
parameter 't'
/home/dejan/eclipse-cxx/cvc4/src/expr/expr.h:44: Warning: argument 'the' of command _@param is not found in the argument list of CVC4::Expr::Expr(const Expr &e)
/home/dejan/eclipse-cxx/cvc4/src/expr/expr.h:44: Warning: The following parameters of CVC4::Expr::Expr(const Expr &e) are not documented:
parameter 'e'
/home/dejan/eclipse-cxx/cvc4/src/expr/expr.h:117: Warning: argument 'the' of command _@param is not found in the argument list of CVC4::Expr::toStream(std::ostream &out) const
/home/dejan/eclipse-cxx/cvc4/src/expr/expr.h:117: Warning: The following parameters of CVC4::Expr::toStream(std::ostream &out) const are not documented:
parameter 'out'
/home/dejan/eclipse-cxx/cvc4/src/expr/expr.h:117: Warning: argument 'the' of command _@param is not found in the argument list of CVC4::Expr::toStream(std::ostream &out) const
/home/dejan/eclipse-cxx/cvc4/src/expr/expr.h:117: Warning: The following parameters of CVC4::Expr::toStream(std::ostream &out) const are not documented:
parameter 'out'
/home/dejan/eclipse-cxx/cvc4/src/expr/expr_manager.h:61: Warning: The following parameters of CVC4::ExprManager::mkExpr(Kind kind, const Expr &child1) are not documented:
parameter 'child1'

On 2010-04-01 01:57:39 -0700, Morgan Deters wrote:

Addressed by revision 363.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: normal
Assigned to: Morgan Deters
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-03-09 14:11:55 -0800, Morgan Deters wrote:

APPLYs should be inlined when possible. APPLY is a build-only kind mechanism, and shouldn't actually exist "in the wild" at this time.

On 2012-10-06 00:12:48 -0700, Morgan Deters wrote:

doesn't really matter anymore. probably APPLY goes away anyway.

Imported from Bugzilla
Reporter: Tim King
Status: RESOLVED
Severity: normal
Assigned to: Dejan Jovanovic
Component: {Internals} other
Milestone: ---
Version: master
Platform: PC
OS: Linux

Original attachment names and IDs:

• PEQ012_size3_seqsat.smt (Example, ID 3)

On 2010-03-09 16:04:17 -0800, Tim King wrote:

Created attachment 3
Example

I found an example that segfaults while solving in the debug build. It appears to be dereferencing a null pointer. I then found a minimal formula that maintains the same error. (I did this by hand.) Attached is the minimized example.

From the console:
#cvc4 PEQ012_size3_seqsat.smt
CVC4 suffered a segfault in DEBUG mode.
Spinning so that a debugger can be connected.
Try: gdb cvc4 5698
^CCVC4 interrupted by user.
Aborted

From gdb:
(gdb) bt
# 0 0x00007f8610ae0f20 in __nanosleep_nocancel () from /lib/libc.so.6
# 1 0x00007f8610ae0da0 in __sleep (seconds=)
at ../sysdeps/unix/sysv/linux/sleep.c:138
# 2 0x0000000000409318 in CVC4::main::segv_handler (sig=11,
info=0x7fff206facb0)
at /home/taking/src/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/main/util.cpp:58
# 3
# 4 0x00007f861187403a in CVC4::prop::minisat::Clause::learnt (this=0x0)
at /home/taking/src/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/prop/minisat/core/SolverTypes.h:136
# 5 0x00007f86118718e0 in CVC4::prop::minisat::Solver::analyze (
this=0x152e910, confl=0x0, out_learnt=..., out_btlevel=_@0x7fff206fb0b8)
at /home/taking/src/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/prop/minisat/core/Solver.C:254
# 6 0x00007f86118731c4 in CVC4::prop::minisat::Solver::search (this=0x152e910,
nof_conflicts=100, nof_learnts=7)
at /home/taking/src/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/prop/minisat/core/Solver.C:630
# 7 0x00007f86118739cb in CVC4::prop::minisat::Solver::solve (this=0x152e910,
assumps=...)
at /home/taking/src/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/prop/minisat/core/Solver.C:738

On 2010-03-10 20:03:54 -0800, Dejan Jovanovic wrote:

I had problems tracking this one down. The prablem seems to be that the theory is providing conflicts that contain non-asserted SAT literals. "How did this happen?", you might ask.

The most reasonable explanation we have so far is that the queue in the theory engine is not backtracking properly. It get's filled up during BCP and TCP, but if a Boolean conflict is found, it would not get emptied, for example.

On 2010-03-10 20:32:19 -0800, Dejan Jovanovic wrote:

Fixed in revision 310: "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)."

Imported from Bugzilla
Reporter: Tim King
Status: RESOLVED
Severity: enhancement
Assigned to: Tim King
Component: {Internals} other
Milestone: ---
Version: master
Platform: All
OS: All

Original attachment names and IDs:

• bmc-ibm-2.mod.smt (modified file, ID 2)

On 2010-01-26 13:29:22 -0800, Tim King wrote:

CNF as assertion list instead of single check sat of the same formula takes significantly different time.

I modified the dimacs2smt.pl script to generate a CNF as a list of assumptions and to use :formula true at the end.

The 2 formulas input files are:

1. CNF formula in an assumption list: comb2.shuffled-as.sat03-420.smt
   This is in cvc4/test/regress/comb2.shuffled-as.sat03-420.smt
2. CNF formula in a single formula: comb2.shuffled-as.sat03-420.unmod.smt
   This is attached.

I ran both with:
time cvc4 -v [filename]

Number 2 takes roughly 20s.
Number 1 I killed after 13 minutes.

I ran both through opensmt. (cvc3 took too long.)
Number 2 took roughly 70s.
Number 1 took roughly 90s.

If it matters, I am using the debug build profile.

On 2010-01-26 13:38:52 -0800, Tim King wrote:

File is here:

http://www.cs.nyu.edu/~taking/comb2.shuffled-as.sat03-420.unmod.smt.bz2

Turned out it is too big to be attached in Bugzilla. (Even after bzip2.)

On 2010-01-26 16:22:50 -0800, Tim King wrote:

Created attachment 2
modified file

Here is another smaller example with similar behavior.

The original is cvc4/test/regress/bmc-ibm-2.smt

On 2010-02-03 13:47:24 -0800, Morgan Deters wrote:

Closed wrong bug (oops). Reopening, though the status of this ticket isn't clear while the CNF conversion system undergoes redesign.

On 2010-02-09 17:04:33 -0800, Morgan Deters wrote:

Has this been addressed?

On 2010-02-09 18:31:34 -0800, Tim King wrote:

This has been addressed, and I am closing the bug.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: review
Assigned to: Dejan Jovanovic
Component: {Internals} Parser infrastructure
Milestone: ---
Version: master
Platform: All
OS: All

On 2009-12-15 14:08:34 -0800, Morgan Deters wrote:

Code review of Dejan's parser code in src/parser.

On 2009-12-15 16:55:38 -0800, Christopher Conway wrote:

Quick design overview:

The Parser base class defines the interface between the CVC4 core and an input language parser. It has derived classes CvcParser and SmtParser.

The AntlrParser base class defines the interface between a generated parser and ExprManager. The generated parsers AntlrCvcParser and AntlrSmtParser are derived from it. The XParser classes have AntlrXParser and AntlrXLexer fields.

The separation into similarly-named class hierarchies is confusing. Does the division need to exist? I.e., could Parser and AntlrParser be merged? If the division is useful or necessary, can we find other names that are less similar?

Detailed comments:

- Field names don't follow the coding standard, e.g., "d_expr_manager" instead of "d_exprManager," "d_antlr_parser" instead of "d_antlrParser," etc.

- Brackets are missing on blocks, everywhere.

- I think rules in the grammars should following general naming convention: CamelCase, descriptive, no unnecessary abbreviations. E.g., "predSymbol" and "annotAtom" (or even "predicateSymbol" and "annotatedAtom") instead of "pred_symb" and "an_atom."

- Why does Parser::parseNextCommand() return a Command pointer?

- Comment on Parser::done(): "Check if we are done -- either the end of input has been reached." Or what? Should the method be isDone()?

- AntlrParser::newExpression should be mkExpr, for consistency.

- AntlrParser::newPredicate(std::string p_name, const std::vectorstd::string& p_sorts)
Why "p_name" and "p_sorts"? Aren't we using "p" as a Hungarian prefix for pointers? Should be "name" and "sorts".
Aside: IMO we should require a Hungarian prefix for vectors and lists, e.g., "vSorts". This is especially helpful for nested structures.

- AntlrParser::addExtraSorts(). Is this supposed to be virtual? Throw an exception or print out a message that this is unimplemented. (Or implement it.)

- AntlrParser::createPrecedenceExpr(). I think we should go over this in the meeting: (1) to decide whether it is correct; (2) to discuss whether there is a better way to do it.

- SymbolTable is a template over the binding type. Will we ever have symbol table bindings that aren't Exprs? If so, would we like to be able to mix different kind of bindings in the same symbol table?

- SymbolTable::unbindName. Where will this get used?

- smt_lexer.g:
- What is the "C_" in "C_IDENTIFIER," "C_LOGIC," etc. supposed to stand for? In Lisp, these are called "slots." In SMT-LIB, they are called "attributes." I wonder if the lexer should tokenize this as " ," " ," etc.?
- Should USER_VALUE forbid braces? Is there an escape syntax?
- STRING_LITERAL forbids double quotes. It should accept " as an escape.

- smt_parser.g:
- "an_" in "an_atom," "an_formula," "an_formulas" stands for "annotated"? Where are the annotations?
- Since the parser generates a CommandSequence, should :status, :extrasorts, and :extrapreds processing be deferred to preserve ordering?
- The definition of bench_attributes is counter-intuitive and merits some comments.

- SmtParser::parseNextCommand(). Should we assert(isDone()) after parsing, instead of just calling setDone()?

- Can't Cvc/SmtParser::d_antlr_lexer/parser (ahem, d_antlrLexer/Parser) live in Parser, as protected fields of type AntlrParser/CharScanner?

- smt_lexer.g: comment char for CVC is '%' (I fixed this)

- smt_parser.g: Instead of an EmptyCommand for a declaration list, why not a DeclCommand? This could help with the ordering of command sequences.

On 2009-12-17 15:43:01 -0800, Christopher Conway wrote:

Something I missed: I prefer grammar definitions to be in a top-down breadth-first style, where the start symbol is at the top, with nonterminals it depends on coming just after it, and so on. The ordering can be a bit loose down near the leaves... This is basically what you do in cvc_parser.g, but in smt_parser.g you do the opposite.

On 2010-01-19 10:26:54 -0800, Morgan Deters wrote:

Reassigning to Dejan: tests are written, etc. Just need resolution.

On 2010-02-01 18:36:25 -0800, Dejan Jovanovic wrote:

(In reply to comment # 1)

- Field names don't follow the coding standard, e.g., "d_expr_manager" instead
of "d_exprManager," "d_antlr_parser" instead of "d_antlrParser," etc.

Fixed

- Brackets are missing on blocks, everywhere.

Fixed

- I think rules in the grammars should following general naming convention:
CamelCase, descriptive, no unnecessary abbreviations. E.g., "predSymbol" and
"annotAtom" (or even "predicateSymbol" and "annotatedAtom") instead of
"pred_symb" and "an_atom."

Fixed

- Why does Parser::parseNextCommand() return a Command pointer?

Because it's an polymorphic object created within the parser.

- Comment on Parser::done(): "Check if we are done -- either the end of input
has been reached." Or what? Should the method be isDone()?

The isDone() method tells whether the parsing is no longer possible. One should always check to see if the last parse method returned a meaningful thing, i.e. isNull for parseExpr() and == NULL for parseCommand.

- AntlrParser::newExpression should be mkExpr, for consistency.

Fixed

- AntlrParser::newPredicate(std::string p_name, const std::vectorstd::string&
p_sorts)
Why "p_name" and "p_sorts"? Aren't we using "p" as a Hungarian prefix for
pointers? Should be "name" and "sorts".
Aside: IMO we should require a Hungarian prefix for vectors and lists, e.g.,
"vSorts". This is especially helpful for nested structures.

p is for predicate

- AntlrParser::addExtraSorts(). Is this supposed to be virtual? Throw an
exception or print out a message that this is unimplemented. (Or implement it.)

Removed

- AntlrParser::createPrecedenceExpr(). I think we should go over this in the
meeting: (1) to decide whether it is correct; (2) to discuss whether there is a
better way to do it.

Removed and moved all the parsing in a classical recursive descent into the grammar.

- SymbolTable is a template over the binding type. Will we ever have symbol
table bindings that aren't Exprs? If so, would we like to be able to mix
different kind of bindings in the same symbol table?

This is not a big deal, but it gives the flexibility to use it if possible. For example, keeping different symbol tables for variables, functions... depending on how we decide to type our language.

- SymbolTable::unbindName. Where will this get used?

When parsing nested structures, such as quantifiers.

- smt_lexer.g:
- What is the "C_" in "C_IDENTIFIER," "C_LOGIC," etc. supposed to stand for?
In Lisp, these are called "slots." In SMT-LIB, they are called "attributes." I
wonder if the lexer should tokenize this as " ," " ,"
etc.?

These are just prefixes for COLON

- Should USER_VALUE forbid braces? Is there an escape syntax?
- STRING_LITERAL forbids double quotes. It should accept " as an escape.

These two are noted, I just have to find the right way to implement it.

- smt_parser.g:
- "an_" in "an_atom," "an_formula," "an_formulas" stands for "annotated"?
Where are the annotations?

These are never used in practice, so we don't use them.

- Since the parser generates a CommandSequence, should :status, :extrasorts,
and :extrapreds processing be deferred to preserve ordering?

No, we need to create the variables in order to create the exprs for the parsed expressions.

- Can't Cvc/SmtParser::d_antlr_lexer/parser (ahem, d_antlrLexer/Parser) live in
Parser, as protected fields of type AntlrParser/CharScanner?

Now they do.

- smt_lexer.g: comment char for CVC is '%' (I fixed this)

- smt_parser.g: Instead of an EmptyCommand for a declaration list, why not a
DeclCommand? This could help with the ordering of command sequences.

Fixed.

On 2010-02-02 15:13:10 -0800, Christopher Conway wrote:

- SymbolTable::unbindName. Where will this get used?

When parsing nested structures, such as quantifiers.

Can you comment this. I don't find this description intuitive at all.

- smt_parser.g:
- "an_" in "an_atom," "an_formula," "an_formulas" stands for "annotated"?
Where are the annotations?

These are never used in practice, so we don't use them.

I would suggest either:

1. Make a note that we do not and will not support annotations, and rename these productions "atom", "formula", etc.
2. Insert a TODO comment on each production.

Imported from Bugzilla
Reporter: Tim King
Status: RESOLVED
Severity: major
Assigned to: Clark Barrett
Component: {Internals} Context manager
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-03-04 15:09:04 -0800, Tim King wrote:

When the destructor of a class inheriting from context obj is destroyed at a context level that is not 0, the following error occurs:
pure virtual method called
terminate called without an active exception
Aborted

The example that causes this bug is calling the destructor of TheoryUF when the context level is not zero and one of TheoryUF CDLists gets modified at least once.

1. ~TheoryUF() is called. TheoryUF contains a CDList.
2. ~CDList is called when ~TheoryUF exits (as the destructor of internal data structures get called implicitly before exiting)
3. ~ContextObj() is called when ~CDList exits as CDList extends ContextObj and the destructor for the parent class is implicitly called when ContextObj exits.
4. ~ContextObj() calls restoreAndContinue() as we are not at context level 0 and the data has been modified.
5. restoreAndContinue() calls restore(...). This will not be resolved into CDList::restore() because C++ reverts to the base class within destructors. This is resolved to ContextObj::

This behavior can be reproduced by commenting out the line
d_context->pop();
in function void testPushPopA()
in the unit test cvc4/test/unit/theory/theory_uf/theory_uf_white.h .
This can be compiled using make check. The binary is then cvc4/builds/test/unit/theory/theory_uf_white . This can be executed alone or with gdb.

On 2010-03-10 19:59:10 -0800, Dejan Jovanovic wrote:

This also happens when throwing a proper Assert exception anywhere -- the main driver is supposed to catch it and print out the message. But, during the unwinding of the stack, the CDObjects are destructed (withouth being level 0) and everything crashes. So, until this is fixed we can't get meaningful assert messages.

Destructing the PropEngine
pure virtual method called

CVC4 was terminated by the C++ runtime.
Perhaps an exception was thrown during stack unwinding. (Don't do that.)
terminate called without an active exception
Aborted

On 2010-03-12 20:57:53 -0800, Clark Barrett wrote:

I didn't get a chance to test it much, but I think it's fixed.

Imported from Bugzilla
Reporter: Christopher Conway
Status: RESOLVED
Severity: enhancement
Assigned to: Dejan Jovanovic
Component: {Internals} Parser infrastructure
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2009-12-17 13:51:54 -0800, Christopher Conway wrote:

"make check" fails with:

terminate called after throwing an instance of 'CVC4::AssertionException'
/bin/bash: line 5: 22257 Aborted ${dir}$tst
FAIL: parser/cvc/cvc_parser_black

Here's the backtrace:

# 1 0x080792e7 in Node (this=0x80a1f58, ev=0x0)
at /home/chris/workspace/cvc4/builds/i686-pc-linux-gnu/default/../../../src/expr/node.cpp:48
# 2 0x08077cce in CVC4::NodeBuilder<10u>::operator CVC4::Node (this=0xbfffeab8)
at /home/chris/workspace/cvc4/builds/i686-pc-linux-gnu/default/../../../src/expr/node_builder.h:498
# 3 0x080777ed in CVC4::NodeManager::mkExpr (this=0x80a1370, kind=CVC4::TRUE)
at /home/chris/workspace/cvc4/builds/i686-pc-linux-gnu/default/../../../src/expr/node_manager.cpp:101
# 4 0x080738e0 in CVC4::ExprManager::mkExpr (this=0x80a1360, kind=CVC4::TRUE)
at /home/chris/workspace/cvc4/builds/i686-pc-linux-gnu/default/../../../src/expr/expr_manager.cpp:26
# 5 0x08056df4 in CVC4::parser::AntlrParser::getTrueExpr (this=0x80a1930)
at /home/chris/workspace/cvc4/builds/i686-pc-linux-gnu/default/../../../src/parser/antlr_parser.cpp:76
# 6 0x0805faca in CVC4::parser::AntlrCvcParser::bool_atom (this=0x80a1930)
at cvc_parser.g:105
# 7 0x08060802 in CVC4::parser::AntlrCvcParser::primary_bool_formula (
this=0x80a1930) at AntlrCvcParser.cpp:215
# 8 0x080603dc in CVC4::parser::AntlrCvcParser::bool_formula (this=0x80a1930)
at AntlrCvcParser.cpp:173
# 9 0x08060997 in CVC4::parser::AntlrCvcParser::formula (this=0x80a1930)
at AntlrCvcParser.cpp:121
# 10 0x08060cbd in CVC4::parser::AntlrCvcParser::command (this=0x80a1930)
at AntlrCvcParser.cpp:61
# 11 0x0805562b in CVC4::parser::CvcParser::parseNextCommand (this=0xbfffef84)
at /home/chris/workspace/cvc4/builds/i686-pc-linux-gnu/default/../../../src/parser/cvc/cvc_parser.cpp:34
# 12 0x080517d4 in CvcParserBlack::testGoodInputs (this=0x80a0300)
at /home/chris/workspace/cvc4/builds/i686-pc-linux-gnu/default/../../../test/unit/parser/cvc/cvc_parser_black.h:44
# 13 TestDescription_CvcParserBlack_testGoodInputs::runTest (this=0x80a0300)
at parser/cvc/cvc_parser_black.cpp:28
# 14 0x0804fbe5 in CxxTest::RealTestDescription::run (this=0x80a0300)
at /home/chris/tools/cxxtest/cxxtest/RealDescriptions.cpp:96
# 15 0x080524e8 in CxxTest::TestRunner::runTest (this=0xbffff09f)
at /home/chris/tools/cxxtest/cxxtest/TestRunner.h:74
# 16 CxxTest::TestRunner::runSuite (this=0xbffff09f)
at /home/chris/tools/cxxtest/cxxtest/TestRunner.h:61
# 17 CxxTest::TestRunner::runWorld (this=0xbffff09f)
at /home/chris/tools/cxxtest/cxxtest/TestRunner.h:46
# 18 0x0805074b in CxxTest::TestRunner::runAllTests ()
at /home/chris/tools/cxxtest/cxxtest/TestRunner.h:23
# 19 CxxTest::ErrorFormatter::run ()
at /home/chris/tools/cxxtest/cxxtest/ErrorFormatter.h:47
# 20 main () at parser/cvc/cvc_parser_black.cpp:16

On 2010-02-01 18:20:49 -0800, Dejan Jovanovic wrote:

This has apparently been fixed. The 'make check' passes for now.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-01-27 17:59:00 -0800, Morgan Deters wrote:

When a mkNode(UNDEFINED_KIND) is requested, an assertion fails (you can't create an UNDEFINED-kinded node), and this causes destruction of the NodeBuilder, which has d_used == false, causing another assertion to fail (unused NodeBuilder destructed), masking the first assertion failure.

Probably NodeBuilders that fail during construction should get d_used set to true.

On 2010-02-03 12:49:24 -0800, Morgan Deters wrote:

Addressed by making NodeBuilder-destruction-without-being-used a non-fatal error.

Imported from Bugzilla
Reporter: Dejan Jovanovic
Status: RESOLVED
Severity: enhancement
Assigned to: Dejan Jovanovic
Component: Documentation
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-02-22 11:49:14 -0800, Dejan Jovanovic wrote:

/home/dejan/eclipse-cxx/cvc4/src/prop/cnf_stream.h:118: Warning: argument 'whether' of command _@param is not found in the argument list of CVC4::prop::CnfStream::convertAndAssert(const Node &node)
/home/dejan/eclipse-cxx/cvc4/src/prop/cnf_stream.h:86: Warning: argument 'node' of command _@param is not found in the argument list of CVC4::prop::CnfStream::lookupInCache(const Node &n) const
/home/dejan/eclipse-cxx/cvc4/src/prop/cnf_stream.h:86: Warning: The following parameters of CVC4::prop::CnfStream::lookupInCache(const Node &n) const are not documented:
parameter 'n'
/home/dejan/eclipse-cxx/cvc4/src/prop/cnf_stream.h:86: Warning: argument 'node' of command _@param is not found in the argument list of CVC4::prop::CnfStream::lookupInCache(const Node &n) const
/home/dejan/eclipse-cxx/cvc4/src/prop/cnf_stream.h:86: Warning: The following parameters of CVC4::prop::CnfStream::lookupInCache(const Node &n) const are not documented:
parameter 'n'
/home/dejan/eclipse-cxx/cvc4/src/theory/uf/ecdata.h:67: Warning: The following parameters of CVC4::theory::ECData::addPredecessor(Node n, context::Context *context) are not documented:
parameter 'context'

Imported from Bugzilla
Reporter: Christopher Conway
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: {Internals} Driver
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2009-12-16 13:42:57 -0800, Christopher Conway wrote:

I've got a default build of CVC4. When I tried to debug Bug # 7, I couldn't effectively load the binary into GDB.

Using GDB inside Emacs, the line number information appears to be scrambled so that breakpoints don't work properly.

In the Eclipse debugger, I got the error:

The current source language is "auto; currently c".
Stopped due to shared library event
warning: static field's value depends on the current frame - bad debug info?
/build/buildd/gdb-7.0/gdb/findvar.c:420: internal-error: read_var_value: Assertion `frame' failed.
A problem internal to GDB has been detected,
further debugging may prove unreliable.

On 2009-12-17 13:57:27 -0800, Christopher Conway wrote:

Same deal as Bug # 7. Disappeared and couldn't reproduce.

Imported from Bugzilla
Reporter: Dejan Jovanovic
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: Tests
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-03-03 18:18:40 -0800, Dejan Jovanovic wrote:

As our unit-test database is growing the time to compile all the tests is getting increasingly unbearable, specially as every change in the source spawns recompilation of all tests. I know it might be impossible, but I would be wonderful if we could get around this somehow.

On 2010-03-04 16:49:12 -0800, Morgan Deters wrote:

See bug 13, "Test not rebuilding on code changes". We can't have it both ways! :)

Fortunately, the answer is yes, you can avoid this rebuilding.

But let me stress that before any commit, you should always let the build tree rebuild, relink, and rerun all tests.

First, the preferred method, which involves partial rebuilding: You can run subsets of unit tests (rebuilding only those necessary for the subset). Let's say I have an up-to-date build tree (including all unit tests). You make a small change to "src/theory/theory.h" and want to run _just_ the theory tests. Run "make" to rebuild the libraries, then:

$ make -C src/theory check

By the way, -C isn't anything magical, it just chdir's into src/theory first. So the same results from:

$ (cd src/theory && make check)

With the current build tree, this will rebuild ONLY the "theory_black" and "theory_uf_white" tests and then run them.

THE SECOND METHOD (not preferred):

IF you are using dynamic linking (--enable-shared, the default), and you make a change to libcvc4/libcvc4parser that shouldn't require relinking (a small change to a non-inlined function, for example), you can "make" to rebuild the libraries, then "make -t check" to mark the tests up-to-date even though they aren't, then "make check" to run them.

If you change interface, data layout, or inline-able function implementations, you'll run into problems and the tests should be rebuilt, so use good judgment and ** always rebuild, relink, and rerun all unit tests ** before a commit.

Also, if you use this "make -t check" method, your build tree may become out-of-sync with itself. If you see strange behavior (unexpected segfaults, weird debugger behavior, etc.), rebuild and relink all tests.

I've been meaning to write a blurb about this on the "How do I..." and Developer's Guide. I'll do so, and forward this message to cvc4-devel.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: review
Assigned to: Liana Hadarean
Component: {Internals} Utilities
Milestone: ---
Version: master
Platform: All
OS: All

On 2009-12-17 12:16:54 -0800, Morgan Deters wrote:

All classes in the utilities package under src/util need to be reviewed.

On 2010-02-01 14:36:57 -0800, Liana Hadarean wrote:

Design overview

The Exception base class is a superclass of the AssertionException class and provides a way to handle exceptions in cvc4. It has as subclasses UnreachableCodeException (with derived class UnhandledCaseException), UnimplementedOperationException and llegalArgumentException.

output.h contains all the Debug, Trace etc. classes.
command.h handles command by invoking the SmtEngine methods on them.
Most of the other files, seem to be stubs to be implemented.

** Assert.h **

_@line 45:
The construct method is defined several times with different arguments:

void construct(const char* header, const char* extra,
const char* function, const char* file,
unsigned line, const char* fmt, ...) {
va_list args;
va_start(args, fmt);
construct(header, extra, function, file, line, fmt, args);
va_end(args);
}
void construct(const char* header, const char* extra,
const char* function, const char* file,
unsigned line, const char* fmt, va_list args);

However, I noticed that throughout the code you never call the first definition, just the 2nd one, and just have the va_list args again. Why do you need the first definition?

** output.h **

_@line 31:
I found the null_streambuf class a bit confusing initially, and I think it would be helpful to have an explanation in the comments as well.

_@line 35:
What does overflow do in the null_streambuf class?

_@line 50:
What were the Yeting options? Do we still need them in the comments?

_@line 164:
I noticed that in Assert.cpp in the construct method (line 71) you try to build the exception with a small buffer and then increase the size. However, in TraceC you have a buffer of constant size 1024. Will that potentially lead to an overflow?

** command.h **

_@line 13:
In the comments, what's generated by the parser?

_@line 25:
Why do you need these lines:
namespace CVC4 {
class SmtEngine;
class Command;
}/* CVC4 namespace */

_@line 129:
I found it a bit confusing that the index of the next command to be executed is called d_last_index.

** command.cpp **

It's missing file specific comments.
I found the layout too spread out and a bit confusing. Maybe some comments or grouping the methods for the same class together. The file alltogether seems to have few comments.

On 2010-02-03 15:54:47 -0800, Morgan Deters wrote:

(In reply to comment # 1)

** Assert.h **

_@line 45:
The construct method is defined several times with different arguments:

void construct(const char* header, const char* extra,
const char* function, const char* file,
unsigned line, const char* fmt, ...) {
va_list args;
va_start(args, fmt);
construct(header, extra, function, file, line, fmt, args);
va_end(args);
}
void construct(const char* header, const char* extra,
const char* function, const char* file,
unsigned line, const char* fmt, va_list args);

However, I noticed that throughout the code you never call the first
definition, just the 2nd one, and just have the va_list args again. Why do you
need the first definition?

It wasn't being used (but it is now :)... by UnhandledCaseException)

** output.h **

_@line 31:
I found the null_streambuf class a bit confusing initially, and I think it
would be helpful to have an explanation in the comments as well.

Documented.

_@line 35:
What does overflow do in the null_streambuf class?

Documented.

_@line 50:
What were the Yeting options? Do we still need them in the comments?

Documented. It's a method of having a non-tagged Debug() output just for temporary debugging while developing.

_@line 164:
I noticed that in Assert.cpp in the construct method (line 71) you try to build
the exception with a small buffer and then increase the size. However, in
TraceC you have a buffer of constant size 1024. Will that potentially lead to
an overflow?

It shouldn't. These are different buffers:
* in Assert.cpp, the buffer grows dynamically if it needs more space. Assertion exceptions are somewhat "user-facing," so this is good, no output is lost.
* in TraceC, for simplicity, the per-call to TraceC::printf() is cut off at 1024 bytes. There isn't overflow because the size of the buffer is passed to vsnprintf(). 1024's probably sufficient; if not, too bad, the output is truncated. :) Perhaps it shouldn't be, but tracing isn't as "user-facing," so this seemed ok..

Thoughts? Did I not calculate the buffer size in the vsnprintf() calls correctly?

** command.h **

_@line 13:
In the comments, what's generated by the parser?

Commands. :) Better documented.

_@line 25:
Why do you need these lines:
namespace CVC4 {
class SmtEngine;
class Command;
}/* CVC4 namespace */

Forward declarations. We prefer forward-declaring to #include'ing when possible (to avoid unnecessary dependences). Also, forward declarations are necessary to break circular references, which is the case here with SmtEngine. "class Command;" is forward-declared so that the operator<<() declaration can go before the class definition for Command. I chose that location for operator<<() so that it was easy to find (and didn't get lost at the bottom of the header file).

_@line 129:
I found it a bit confusing that the index of the next command to be executed is
called d_last_index.

Renamed to "d_index" -- it's unclear to me why this is a member and not a local variable in "invoke", perhaps Dejan could explain? Maybe the invocation of a Command in the CommandSequence can add another item to the sequence? Not sure..

** command.cpp **

It's missing file specific comments.

Added.

I found the layout too spread out and a bit confusing. Maybe some comments or
grouping the methods for the same class together. The file alltogether seems to
have few comments.

I've reorganized these member function implementations and put suitable candidates for inlining in command.h instead.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: major
Assigned to: Morgan Deters
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-02-25 13:30:30 -0800, Morgan Deters wrote:

Review NodeBuilder<> again and ensure there aren't any leaks or improper decrements.

The way that d_nv (allocated) and d_inlineEv hand off is complicated and should be explicitly documented, also making invariants easier to verify.

On 2010-03-08 14:09:53 -0800, Morgan Deters wrote:

This is ongoing work; some issues have been fixed in recent commits, but there are still problems with regress levels >= 1 due to (I think) NodeBuilder<> issues.

Recoding of NodeBuilder<>, with better documentation and more careful handling of internal reference-counting-related invariants, is nearly complete.

On 2010-03-08 18:50:05 -0800, Morgan Deters wrote:

Fixed in revision 297.

Imported from Bugzilla
Reporter: Dejan Jovanovic
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-02-19 16:45:58 -0800, Dejan Jovanovic wrote:

a:BOOLEAN;
b:BOOLEAN;
ASSERT(a);
QUERY(a OR b);

results with an failure in printing the name (attribute) somewhere

On 2010-02-22 02:40:41 -0800, Morgan Deters wrote:

All public-facing functions in the expr package (e.g. in Expr and ExprManager) need to set the current node manager. If they don't, NodeManager::currentNM() is NULL causing a null-pointer dereference trying to get to the AttributeManager (which holds the hash tables).

Fixed in revision 230 by adding some ExprManagerScope lines.

Imported from Bugzilla
Reporter: Dejan Jovanovic
Status: RESOLVED
Severity: major
Assigned to: Morgan Deters
Component: Build system (configure, make, make install)
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-02-16 14:38:33 -0800, Dejan Jovanovic wrote:

The Assert.h structure is not conforming to what we agreed at in the meetings. If we are using AlwaysAsserts in code, these should get compiled out in the competition build.

On 2010-02-17 14:10:58 -0800, Morgan Deters wrote:

After a conversation with Dejan 2/17/2010:

AlwaysAssert() should always assert, regardless of build, even in competition. Accordingly, it should test only cheap-to-test and highly-important things.

In the case of the parser, another kind of check should be performed on input (rather than an assertion): (1) it doesn't make much sense for bad input to cause an assertion failure (rather than a ParseException or whatever), and (2) it would be possible to provide an --assume-input-well-formed flag (or similar) to disable a check if it was thought to be expensive. (And perhaps the check is compiled out in "competition" builds).

Imported from Bugzilla
Reporter: Christopher Conway
Status: RESOLVED
Severity: enhancement
Assigned to: Christopher Conway
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-03-09 17:24:45 -0800, Christopher Conway wrote:

This requires some detailed design discussion regarding how bindings should be represented at the Node level. Let bindings correspond exactly to substructure sharing in the expression DAG, so there's no technical need for them inside the NodeManager. But presumably we want to preserve the original structure of the input in some form, including let bindings.

On 2010-03-09 21:35:09 -0800, Christopher Conway wrote:

This is fixed in SVN, the hacky way: by binding the variable to its definition and just replacing the variable everywhere it appears with the definition.

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: {Internals} Context manager
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-03-09 12:06:40 -0800, Morgan Deters wrote:

Rename orderedIterator -> iterator
remove (old) hash_map<>-backed iterator

On 2010-03-13 20:53:43 -0800, Morgan Deters wrote:

Fixed in revision 324.

Imported from Bugzilla
Reporter: Tim King
Status: RESOLVED
Severity: enhancement
Assigned to: Christopher Conway
Component: {Internals} Parser infrastructure
Milestone: ---
Version: master
Platform: PC
OS: Linux

On 2010-03-09 16:17:26 -0800, Tim King wrote:

The file attached to bug 49
( http://goedel.cims.nyu.edu/cgi-bin/bugzilla3/show_bug.cgi?id=49 )
will not parse unless the line ":extrasorts (U)" is included. If this is taken out, CVC4 fails to parse it. Other smt solvers (CVC3 and opensmt) refuse to parse it with this line included.

On 2010-03-09 17:00:49 -0800, Dejan Jovanovic wrote:

This is the first break on the SMTLIB problems. I've added the smallest ones to the repository and they break on isDeclared()...

test/regress/regress0/uf/eq_diamond1.smt
CVC4 Error:
Assertion failure.
const CVC4::Type* CVC4::parser::AntlrParser::getSort(const std::string&)
/home/dejan/eclipse-cxx/cvc4/builds/i686-pc-linux-gnu/debug/../../../src/parser/antlr_parser.cpp:84:

isDeclared(name, SYM_SORT)

Aborted
test/regress/regress0/uf/iso_brn001.smt
CVC4 Error:
Parse Error: test/regress/regress0/uf/iso_brn001.smt:19:1: unexpected token: (
Aborted
test/regress/regress0/uf/NEQ016_size5.smt
CVC4 Error:
Assertion failure.
const CVC4::Type* CVC4::parser::AntlrParser::getSort(const std::string&)
/home/dejan/eclipse-cxx/cvc4/builds/i686-pc-linux-gnu/debug/../../../src/parser/antlr_parser.cpp:84:

isDeclared(name, SYM_SORT)

Aborted
test/regress/regress0/uf/PEQ018_size4.smt
CVC4 Error:
Assertion failure.
const CVC4::Type* CVC4::parser::AntlrParser::getSort(const std::string&)
/home/dejan/eclipse-cxx/cvc4/builds/i686-pc-linux-gnu/debug/../../../src/parser/antlr_parser.cpp:84:

isDeclared(name, SYM_SORT)

Aborted
test/regress/regress0/uf/SEQ032_size2.smt
CVC4 Error:
Assertion failure.
const CVC4::Type* CVC4::parser::AntlrParser::getSort(const std::string&)
/home/dejan/eclipse-cxx/cvc4/builds/i686-pc-linux-gnu/debug/../../../src/parser/antlr_parser.cpp:84:

isDeclared(name, SYM_SORT)

Aborted

On 2010-03-09 17:04:10 -0800, Christopher Conway wrote:

So far as I can tell, we're right and the benchmark is wrong: the extrafuns have no business referring to a sort that has not been declared. It's dead simple to add a rule implicitly declaring a sort whenever it appears in a extrafuns or extrapreds declaration, but that could lead to subtle errors in benchmarks (e.g., imagine a single typo in the middle of a list of several hundred new variables). This behavior could be enabled by --no-checking.

On 2010-03-09 17:41:32 -0800, Tim King wrote:

Some sorts are predefined in the SMT specification. ":sorts (U)" is defined in the Empty Theory, which is part of the QF_UF logic, http://combination.cs.uiowa.edu/smtlib/theories/Empty.smt and http://combination.cs.uiowa.edu/smtlib/logics/QF_UF.smt .

Other Theories such as Reals have ":sorts (...)" predefined.

(Morgan figured this out.)

On 2010-03-09 17:44:26 -0800, Christopher Conway wrote:

Ah. I looked at the definition of QF_UF, but I assumed the Empty theory was, you know, empty. I'll have the parser declare "U" when it sees QF_UF.

On 2010-03-09 18:11:16 -0800, Christopher Conway wrote:

":logic QF_UF" causes sort "U" to be declared

Imported from Bugzilla
Reporter: Morgan Deters
Status: RESOLVED
Severity: enhancement
Assigned to: Morgan Deters
Component: {Internals} Expression package
Milestone: ---
Version: master
Platform: All
OS: All

On 2010-03-01 17:35:36 -0800, Morgan Deters wrote:

Doxygen-style comments should be permitted in the theory "kinds" files and included in kind.h for Doxygen parsing.

On 2010-04-01 03:23:40 -0700, Morgan Deters wrote:

This is fixed as of last week; it is tested and works in revision 363.