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

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

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

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

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

* fix some Make rule dependencies

* reformat node.h as per code formatting policy

* added Theory and NodeBuilder unit tests

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

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

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

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

14 years agoTheoryUFWhite is passing. I fixed 2 errors. Unfortunately, I also changed a TNode...
Tim King [Sun, 28 Feb 2010 00:43:32 +0000 (00:43 +0000)]
TheoryUFWhite is passing.  I fixed 2 errors. Unfortunately, I also changed a TNode to a Node at one point in the code. TNode failed for a completely unknown reason. I'm try to isolate the problem is a bit, but I am commiting this for now so other things can move forward.

14 years agofix compile error in black parser unit test after today's change to parser code
Morgan Deters [Sat, 27 Feb 2010 23:46:38 +0000 (23:46 +0000)]
fix compile error in black parser unit test after today's change to parser code

14 years agoA bag of unrelated fixes to bring trunk more in-line with recent
Morgan Deters [Sat, 27 Feb 2010 23:43:24 +0000 (23:43 +0000)]
A bag of unrelated fixes to bring trunk more in-line with recent
policy discussion (no dead code, no unimplemented unit tests...), and
other fixes:

* src/expr/node_builder.h: uncomment AndNodeBuilder, OrNodeBuilder,
  PlusNodeBuilder, and MultNodeBuilder.  (These had been dead code for
  awhile.)

* src/expr/node_value.cpp: toString() is much more reasonable now,
  printing S-exprs and using variable names (instead of printing raw
  pointer values).  Next, we'll want to define a pretty-printing
  theory interface and perhaps hook this up to that.

* test/unit/expr/node_black.h: implement testIterator(),
  testToString(), and testToStream().

* test/unit/expr/node_builder_black.h: implement testIterator() and
  testAppend(), and add some code to avoid the warnings on clear() for
  unused NodeBuilders.

* src/expr/node_builder.h: redefine "iterator" to be over Nodes rather
  than over NodeValues.  Doesn't make sense to expose the underlying
  NodeValues.  This shouldn't affect anyone, no one was using
  NodeBuilder iterators.

* fix some comments in source code

14 years agoAdding --mmap option to use memory-mapped file input, which provides a marginal impro...
Christopher L. Conway [Sat, 27 Feb 2010 18:34:44 +0000 (18:34 +0000)]
Adding --mmap option to use memory-mapped file input, which provides a marginal improvement (<5%) on big benchmarks.

14 years ago* test/unit/context/context_black.h: Test CDList<>. In particular,
Morgan Deters [Fri, 26 Feb 2010 21:44:42 +0000 (21:44 +0000)]
* test/unit/context/context_black.h: Test CDList<>.  In particular,
  test behavior of grow(), which was previously very broken, fixed by
  Tim earlier this afternoon.

* add the notion of a "private header".  Private header files (those
  not intended for distribution) should now #include "cvc4_private.h"
  (or "cvc4parser_private.h" for the parser code).  When not actually
  building libcvc4 (resp. libcvc4parser), or associated unit tests, a
  warning is emitted by the preprocessor.  This should make it easier
  to notice (and disentangle early) any unwanted public/private
  mixing.  Currently the warning identifies a couple places where we
  need to fix things.

* added directory infrastructure for arrays and BV theories.

* the Theory inheritance hierarchy makes some assumptions about the
  way inheritance is done.  These are checked at runtime when
  CVC4_ASSERTIONS is on.  See src/theory/theory.h's TheoryImpl<>
  definition for details.

* src/theory/booleans/theory_bool.h, src/theory/booleans/theory_def.h,
  src/theory/arith/theory_arith.h, src/theory/arith/theory_def.h,
  src/theory/uf/theory_uf.h, src/theory/uf/theory_def.h,
  src/parser/antlr_parser.h: minor code formatting fixes as per
  policy.

* src/theory/uf/theory_uf.cpp: fix for non-debug builds.

* src/util/options.h, src/util/model.h, src/util/result.h,
  src/expr/type.h: make CVC4_PUBLIC.

* src/util/decision_engine.h: no longer CVC4_PUBLIC.

* src/expr/expr_manager.cpp: ExprManager::booleanType() and
  ExprManager::kindType() weren't returning a value ?!  Fixed.

* src/expr/expr_manager.h, src/expr/node_manager.h: ExprManager no
  longer depends on NodeManager (public/private interface mixing).
  ExprManagerScope is an internal implementation detail, and is moved
  to node_manager.h.

* src/expr/node.h: mark gdb debug routines as "used" so that GCC
  always emits code for them (even though its static analysis shows
  they're unused).

14 years agoTheoryUFWhite tests are added. There are also accompanying bug fixes. These currently...
Tim King [Fri, 26 Feb 2010 18:58:17 +0000 (18:58 +0000)]
TheoryUFWhite tests are added. There are also accompanying bug fixes. These currently do not pass. (See bug 39.) I modified node.h/cpp to get gdb debug printing working again

14 years agoFixed a bug in CDList reallocation. (Also corrected a couple whitespace problems.)
Tim King [Fri, 26 Feb 2010 18:40:08 +0000 (18:40 +0000)]
Fixed a bug in CDList reallocation. (Also corrected a couple whitespace problems.)

14 years agoChanging the hashing in attributes to what Nodes do, i.e. hash on the id of the node...
Dejan Jovanović [Fri, 26 Feb 2010 02:25:52 +0000 (02:25 +0000)]
Changing the hashing in attributes to what Nodes do, i.e. hash on the id of the node-value. This keeps coming up so we should rename the .hash() method in the node-value to something else. Morgan, feel free to change, but I had to go in as we were stuck on infinite parsing again.

14 years agoAdding Node::getOperator()
Christopher L. Conway [Thu, 25 Feb 2010 22:32:03 +0000 (22:32 +0000)]
Adding Node::getOperator()
Removing references to ExprManager from Type, moving Type creation into NodeManager

14 years agoUpdated uf to reflect APPLY structure after conversation with Chris. Also corrected...
Tim King [Thu, 25 Feb 2010 21:55:17 +0000 (21:55 +0000)]
Updated uf to reflect APPLY structure after conversation with Chris. Also corrected conflict generation to reflect this morning's discussion.

14 years ago* src/expr/node_builder.h: fixed some overly-aggressive refcount decrementing.
Morgan Deters [Thu, 25 Feb 2010 18:26:22 +0000 (18:26 +0000)]
* src/expr/node_builder.h: fixed some overly-aggressive refcount decrementing.
  There remain memory leaks (and some over-decrementing of refcounts) that
  I've identified; another commit forthcoming.

* src/expr/attribute.h: keys are now NodeValue* instead of TNode

* src/theory/output_channel.h: change OutputChannel::conflict() to the
  negation of what we had before: it now takes an AND of TRUE literals
  as a conflict clause rather than an OR of FALSE ones.

* src/expr/node.cpp: (non-template) CVC4::expr::debugPrint() routine
  for use inside gdb

* src/expr/node.h: remove Node::debugPrint() member (now a function
  instead of a member function, since Node is now a template it wasn't
  being properly instantiated(?) and couldn't be called from gdb)

* src/expr/Makefile.am: add node.cpp

* src/expr/node_manager.h: code formatting

14 years ago* src/expr/node.h: add a copy constructor. Apparently GCC doesn't
Morgan Deters [Thu, 25 Feb 2010 07:48:03 +0000 (07:48 +0000)]
* src/expr/node.h: add a copy constructor.  Apparently GCC doesn't
  recognize an instantiation of the join conversion/copy ctor with
  ref_count = ref_count_1 as a copy constructor.  Problems with
  reference counts ensue.

* src/theory/theory.h, src/theory/theory.cpp: Theory base
  implementation work.  Changed from continuation-style theory calls
  to having an data member for the output channel.  registerTerm() and
  preRegisterTerm() work.

* src/theory/output_channel.h, src/theory/theory.h,
  src/theory/theory.cpp, src/theory/uf/theory_uf.h,
  src/theory/uf/theory_uf.cpp: merged ExplainOutputChannel into
  OutputChannel.

* test/unit/expr/node_black.h: remove testPlusNode(),
  testUMinusNode(), testMultNode().

* src/expr/attribute.h: new facilities ManagedAttribute<> and
  CDAttribute<>, and add new template parameters to Attribute<>.  Make
  CDAttribute<>s work with context manager.

* src/expr/attribute.h, src/expr/node_manager.h: VarNameAttr and
  TypeAttr are now "owned" (defined) by the NodeManager.  The
  AttributeManager knows nothing of specific attributes, it just as
  all the code for dealing generically with attributes.

* test/unit/expr/node_white.h: test new attribute facilities.

* src/expr/soft_node.h: removed: We now have TNode, so SoftNode goes
  away.

* src/theory/Makefile.am: fixed improper linking of theories

* src/theory/theory_engine.h: some implementation work (mainly stubs
  for now, just to make sure TheoryUF can be instantiated properly,
  etc.)

* src/expr/node_value.cpp, src/expr/node_value.h: move a number of
  function implementations to the header and make them inline

* src/expr/node_manager.cpp, src/expr/node_manager.h: move a number of
  function implementations to the header and make them inline

* src/theory/theoryof_table_prologue.h,
  src/theory/theoryof_table_epilogue.h, src/theory/mktheoryof,
  src/theory/Makefile.am: make the theoryOf() table from kinds and
  implement TheoryEngine::theoryOf().

* src/theory/arith/Makefile, src/theory/bool/Makefile: generated these
  stub Makefiles (with contrib/addsourcedir) as per policy

* src/theory/arith, src/theory/bool [directory properties]: add .deps
  to svn:ignore.

* contrib/configure-in-place: permit configuring "in-place" in the
  source directory.

* contrib/get-authors, contrib/dimacs_to_smt.pl,
  contrib/update-copyright.pl, contrib/get-authors,
  contrib/addsourcedir, src/expr/mkkind: copyright notice

* src/expr/node_manager.h, src/expr/node_builder.h,
  src/prop/prop_engine.h, src/prop/prop_engine.cpp,
  src/theory/theory_engine.h, src/smt/smt_engine.h, src/smt/smt_engine.cpp,
  src/theory/output_channel.h: turn "const Node&"-typed formal
  parameters into "TNode"

* src/theory/bool, src/theory/booleans: "bool" directory renamed "booleans"
  to avoid keyword clash on containing namespace

* src/theory/booleans/theory_def.h, src/theory/uf/theory_def.h,
  src/theory/arith/theory_def.h: "define" a theory simply (for automatic
  theoryOf() generator).

* src/Makefile.am: build theory subdirectory before prop, smt, etc. so that
  src/theory/theoryof_table.h header gets generated before it's needed

* src/expr/node_prologue.h, src/expr/node_middle.h: move "Kind" into a
  separate CVC4::kind namespace to avoid its contents from cluttering
  the CVC4 root namespace.  Import the symbol "Kind" into the CVC4 namespace
  but not the enum values.

* src/expr/node_manager.h, src/expr/node.h, src/expr/node_value.h,
  src/expr/node_value.cpp, src/expr/expr.cpp, src/theory/uf/theory_uf.cpp,
  src/prop/cnf_stream.cpp, src/parser/smt/smt_parser.g,
  src/parser/cvc/cvc_parser.g, src/parser/antlr_parser.cpp,
  test/unit/expr/node_white.h, test/unit/expr/node_black.h,
  test/unit/expr/kind_black.h, test/unit/expr/node_builder_black.h:
  update for having moved Kind into CVC4::kind.

* src/parser/parser.cpp: added file-does-not-exist check (was failing
  silently).

14 years agoCreated basic node builder and kind tests. Also fixed a couple of node builder problems.
Tim King [Thu, 25 Feb 2010 01:05:40 +0000 (01:05 +0000)]
Created basic node builder and kind tests. Also fixed a couple of node builder problems.

14 years agoCleaned up and documented ecdata and theory_uf.
Tim King [Wed, 24 Feb 2010 23:52:38 +0000 (23:52 +0000)]
Cleaned up and documented ecdata and theory_uf.

14 years agoCommitting small changes to attribute, and theory to avoid future merge problems...
Tim King [Wed, 24 Feb 2010 21:08:15 +0000 (21:08 +0000)]
Committing small changes to attribute, and theory to avoid future merge problems for Moragn. Also cleaned up theory uf and ecdata, and updated both to reflect attribute. Should be close now.

14 years agoMinor optimizations to parser (use const string& for ids, keep only one binding in...
Christopher L. Conway [Tue, 23 Feb 2010 17:15:44 +0000 (17:15 +0000)]
Minor optimizations to parser (use const string& for ids, keep only one binding in symtab)

14 years agocosmetic changes, comments, and renaming of Expr related stuff to Node (leftovers...
Dejan Jovanović [Tue, 23 Feb 2010 00:24:21 +0000 (00:24 +0000)]
cosmetic changes, comments, and renaming of Expr related stuff to Node (leftovers from before switching to Node)

14 years agofinally works
Dejan Jovanović [Mon, 22 Feb 2010 23:15:48 +0000 (23:15 +0000)]
finally works

14 years agoMerging from branch branches/Liana r241
Dejan Jovanović [Mon, 22 Feb 2010 23:01:16 +0000 (23:01 +0000)]
Merging from branch branches/Liana r241

14 years agoSwitching to types-as-attributes in parser
Christopher L. Conway [Mon, 22 Feb 2010 21:28:25 +0000 (21:28 +0000)]
Switching to types-as-attributes in parser

14 years ago* src/expr/attribute.h: fixed an issue with "const pointer"-valued
Morgan Deters [Mon, 22 Feb 2010 20:51:01 +0000 (20:51 +0000)]
* src/expr/attribute.h: fixed an issue with "const pointer"-valued
  attributes.

* src/expr/attribute.h, src/expr/node_manager.h, src/expr/node.h:
  hasAttribute() and getAttribute() are now const member functions.

14 years ago* configure.ac: Remove doc/ from search path for Makefile.ams
Morgan Deters [Mon, 22 Feb 2010 20:33:00 +0000 (20:33 +0000)]
* configure.ac: Remove doc/ from search path for Makefile.ams

* configure.ac, test/unit/Makefile.am: Resolved an issue where even
  when not testing, one unit test was built.

* Re-ran contrib/update-copyright.pl on all source files to ensure
  consistent and correct header comments.

* contrib/get-authors: Change definition of "minor contributor"
  to >= 10% of lines (rather than strictly greater than 10% of lines)

14 years agoRe-committing revision 232 properly:
Morgan Deters [Mon, 22 Feb 2010 19:24:43 +0000 (19:24 +0000)]
Re-committing revision 232 properly:

* Add virtual destructors to CnfStream, Theory, OutputChannel, and
  ExplainOutputChannel.  Safer and stops a compiler warning.

* node attributes: fix compiler warnings on 64-bit.

* Node: add asserts to make sure the current NodeManager is non-NULL
  when it's needed.  This can happen when public-facing functions
  don't properly set the node manager, and it can look like a bug in
  another part of the library.  Also some code format cleanup.

* configure.ac, config/cvc4.m4: added --enable-static-binary (see
  discussion on bug 33), fixed bad configure lines (bug 19), added
  documentation for some things.

* config.h.in: removed; it's auto-generated.

14 years agoundoing improperly-committed revision 232; will re-commit to get "svn blame" correct...
Morgan Deters [Mon, 22 Feb 2010 19:22:56 +0000 (19:22 +0000)]
undoing improperly-committed revision 232; will re-commit to get "svn blame" correct, etc..

14 years ago* Add virtual destructors to CnfStream, Theory, OutputChannel, and
Cesare Tinelli [Mon, 22 Feb 2010 18:59:37 +0000 (18:59 +0000)]
* Add virtual destructors to CnfStream, Theory, OutputChannel, and
  ExplainOutputChannel.  Safer and stops a compiler warning.

* node attributes: fix compiler warnings on 64-bit.

* Node: add asserts to make sure the current NodeManager is non-NULL
  when it's needed.  This can happen when public-facing functions
  don't properly set the node manager, and it can look like a bug in
  another part of the library.  Also some code format cleanup.

* configure.ac, config/cvc4.m4: added --enable-static-binary (see
  discussion on bug 32), fixed bad configure lines (bug 19), added
  documentation for some things.

* config.h.in: removed; it's auto-generated.

14 years agoSmall changes to the smt-engine, removed the assertions list.
Dejan Jovanović [Mon, 22 Feb 2010 16:57:11 +0000 (16:57 +0000)]
Small changes to the smt-engine, removed the assertions list.

14 years agoresolve bug 32; public-facing interface functions in expr package must set current...
Morgan Deters [Mon, 22 Feb 2010 07:40:23 +0000 (07:40 +0000)]
resolve bug 32; public-facing interface functions in expr package must set current NodeManager

14 years agofix bug 33 (statically link the "cvc4" binary); also main driver cleanup
Morgan Deters [Mon, 22 Feb 2010 06:54:19 +0000 (06:54 +0000)]
fix bug 33 (statically link the "cvc4" binary); also main driver cleanup

14 years agofix bug 22 (remove tracing from non-trace builds; remove all output
Morgan Deters [Mon, 22 Feb 2010 01:10:58 +0000 (01:10 +0000)]
fix bug 22 (remove tracing from non-trace builds; remove all output
from muzzled builds)

add public-facing CVC4::Configuration class that gives CVC4's (static)
configuration (whether debugging is enabled, assertions, version
information, etc...)

add some whitebox tests for assertions, output classes, and new
CVC4::Configuration class

main driver now gets about() information from CVC4::Configuration.

configure.ac now more flexible at specifying major/minor/release
versions of CVC4

add --show-config option that dumps CVC4's static configuration

commented option processing strings in src/main/getopt.cpp

fixed some compilation problems for muzzled builds.

fixed some test code for non-assertion builds (where no assertions are expected)

14 years agospecialized implementation for boolean node attributes ("flags"): they now share...
Morgan Deters [Fri, 19 Feb 2010 23:10:02 +0000 (23:10 +0000)]
specialized implementation for boolean node attributes ("flags"): they now share memory words properly; also, implementations of some output functionality

14 years ago* Attribute infrastructure -- static design. Documentation is coming.
Morgan Deters [Fri, 19 Feb 2010 20:29:58 +0000 (20:29 +0000)]
* Attribute infrastructure -- static design.  Documentation is coming.
  See test/unit/expr/node_white.h for use examples, including how to
  define new attribute kinds.

Also:

* fixes to test infrastructure
* minor changes to code formatting throughout
* attribute tests in test/unit/expr/node_white.h
* fixes to NodeManagerScope ordering
* use NodeValue::getKind() to properly deal with UNDEFINED_KIND
  (removing compiler warning)
* ExprManager: add proper NodeManagerScope to public-facing member
  functions
* store variable names and types in attributes
* SoftNode is a placeholder, not a real implementation

14 years agoChanging minArity of AND/OR to 1 in SMT parser
Christopher L. Conway [Fri, 19 Feb 2010 17:36:23 +0000 (17:36 +0000)]
Changing minArity of AND/OR to 1 in SMT parser

14 years agoAdding --no-checking option to disable semantic checks in parser
Christopher L. Conway [Thu, 18 Feb 2010 23:24:26 +0000 (23:24 +0000)]
Adding --no-checking option to disable semantic checks in parser

14 years agoRm'ing doc from SUBDIRS
Christopher L. Conway [Thu, 18 Feb 2010 21:29:17 +0000 (21:29 +0000)]
Rm'ing doc from SUBDIRS

14 years agoAdding doxygen configuration parameters and doxygen-doc Makefile target
Christopher L. Conway [Thu, 18 Feb 2010 19:53:59 +0000 (19:53 +0000)]
Adding doxygen configuration parameters and doxygen-doc Makefile target

14 years agoInitial draft of TheoryUF. Should compile without problems. A decent amount of functi...
Tim King [Wed, 17 Feb 2010 21:29:57 +0000 (21:29 +0000)]
Initial draft of TheoryUF. Should compile without problems. A decent amount of functionality is stubbed out. Still needs a bit of cleanup.

14 years agofix bug 27: --with-cxxtest-dir=(relative-path) now works
Morgan Deters [Wed, 17 Feb 2010 19:07:49 +0000 (19:07 +0000)]
fix bug 27: --with-cxxtest-dir=(relative-path) now works

14 years agoMoving parser error checking into AntlrParser
Christopher L. Conway [Tue, 16 Feb 2010 19:35:34 +0000 (19:35 +0000)]
Moving parser error checking into AntlrParser

14 years agoAdding --parse-only option
Christopher L. Conway [Tue, 16 Feb 2010 19:13:35 +0000 (19:13 +0000)]
Adding --parse-only option

14 years agoremoving assertion and warning that shouldn't be there. adding initialization of...
Dejan Jovanović [Tue, 16 Feb 2010 18:24:00 +0000 (18:24 +0000)]
removing assertion and warning that shouldn't be there. adding initialization of kind to undefined to a default constructor.

14 years agoRemoving spurious commit of configure
Christopher L. Conway [Tue, 16 Feb 2010 18:08:02 +0000 (18:08 +0000)]
Removing spurious commit of configure

14 years agoConverting semantic predicates in parser to AlwaysAssertions
Christopher L. Conway [Tue, 16 Feb 2010 18:07:41 +0000 (18:07 +0000)]
Converting semantic predicates in parser to AlwaysAssertions

14 years agosimplification minisat
Dejan Jovanović [Sat, 13 Feb 2010 21:30:18 +0000 (21:30 +0000)]
simplification minisat

14 years agoImprovements to CNF conversion when already in CNF
Dejan Jovanović [Sat, 13 Feb 2010 00:55:40 +0000 (00:55 +0000)]
Improvements to CNF conversion when already in CNF

14 years agobuild fix
Dejan Jovanović [Fri, 12 Feb 2010 20:30:24 +0000 (20:30 +0000)]
build fix

14 years agoFix to compile out Debug(...) << ... statements in optimized mode. Someone please...
Dejan Jovanović [Fri, 12 Feb 2010 20:26:56 +0000 (20:26 +0000)]
Fix to compile out Debug(...) << ... statements in optimized mode. Someone please look to see if it makes sense.

14 years agoChanges to hashing that solve the xinetd boolean benchmark in 14s (from ~25min)....
Dejan Jovanović [Fri, 12 Feb 2010 01:07:22 +0000 (01:07 +0000)]
Changes to hashing that solve the xinetd boolean benchmark in 14s (from ~25min). Switched to standard hash_set, hash_map, new hash for the vector of node values (from boost), changed the hash for nodes to be over id's, all the hash values are now size_t. The parser is down from 11s to 10s on the benchmark, so most of the solve time is parsing and we need to figure this out.

14 years agosvn ignore
Dejan Jovanović [Thu, 11 Feb 2010 21:19:48 +0000 (21:19 +0000)]
svn ignore

14 years agoAdding precedence regressions
Christopher L. Conway [Thu, 11 Feb 2010 17:10:36 +0000 (17:10 +0000)]
Adding precedence regressions

14 years agonote on setup(); for discussion at 2010.02.11 meeting
Morgan Deters [Wed, 10 Feb 2010 22:22:14 +0000 (22:22 +0000)]
note on setup(); for discussion at 2010.02.11 meeting

14 years agosvn:ignore for build stuff; add Liana to AUTHORS
Morgan Deters [Wed, 10 Feb 2010 22:21:41 +0000 (22:21 +0000)]
svn:ignore for build stuff; add Liana to AUTHORS

14 years agofixing annoying eclipse build settings, no more broken pipe errors with these settings
Dejan Jovanović [Wed, 10 Feb 2010 03:52:27 +0000 (03:52 +0000)]
fixing annoying eclipse build settings, no more broken pipe errors with these settings

14 years agoAdded calls to destructor in CDList plus optional flag to disable.
Clark Barrett [Wed, 10 Feb 2010 00:33:01 +0000 (00:33 +0000)]
Added calls to destructor in CDList plus optional flag to disable.

14 years agoChanges to the CNF conversion and the SAT solver. All regression pass now, and we...
Dejan Jovanović [Tue, 9 Feb 2010 23:07:33 +0000 (23:07 +0000)]
Changes to the CNF conversion and the SAT solver. All regression pass now, and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.

14 years agoremoving other pieces of autotools stuff to fix bug #24
Morgan Deters [Tue, 9 Feb 2010 22:02:34 +0000 (22:02 +0000)]
removing other pieces of autotools stuff to fix bug #24

14 years agomoving built-in kinds out of the kind.h prologue/middle for uniformity; added TUPLE...
Morgan Deters [Tue, 9 Feb 2010 19:20:32 +0000 (19:20 +0000)]
moving built-in kinds out of the kind.h prologue/middle for uniformity; added TUPLE built-in

14 years agoempty stubs for push and pop to fix the build fail
Dejan Jovanović [Tue, 9 Feb 2010 03:27:16 +0000 (03:27 +0000)]
empty stubs for push and pop to fix the build fail

14 years agoDisabling the failing test case for the context.
Dejan Jovanović [Mon, 8 Feb 2010 18:47:48 +0000 (18:47 +0000)]
Disabling the failing test case for the context.

14 years agoFixing the test case, it had a unary or. The cnf converter should be adapted to handl...
Dejan Jovanović [Mon, 8 Feb 2010 18:47:21 +0000 (18:47 +0000)]
Fixing the test case, it had a unary or. The cnf converter should be adapted to handle cases like this.

14 years agoPush/Pop parsing and commands
Dejan Jovanović [Mon, 8 Feb 2010 18:46:32 +0000 (18:46 +0000)]
Push/Pop parsing and commands

14 years agoMoving the template stuff back into the header in order to use CDList.
Dejan Jovanović [Mon, 8 Feb 2010 18:45:02 +0000 (18:45 +0000)]
Moving the template stuff back into the header in order to use CDList.

14 years agoDocumenting type.h/cpp
Christopher L. Conway [Sun, 7 Feb 2010 17:19:46 +0000 (17:19 +0000)]
Documenting type.h/cpp
Making Boolean and Kind types singletons

14 years agoforce sorting of AC_CONFIG_FILES, otherwise different computers generate the configur...
Morgan Deters [Sat, 6 Feb 2010 17:31:15 +0000 (17:31 +0000)]
force sorting of AC_CONFIG_FILES, otherwise different computers generate the configure script differently and we get useless commits of it; fix NodeBuilder memory leak in response to Kaustubh's expr code review (bug#15)

14 years agoPreliminary support for types in parser
Christopher L. Conway [Sat, 6 Feb 2010 03:06:07 +0000 (03:06 +0000)]
Preliminary support for types in parser

14 years agofinal fixes to addsourcedir source-directory-Makefile-generation script
Morgan Deters [Fri, 5 Feb 2010 23:21:55 +0000 (23:21 +0000)]
final fixes to addsourcedir source-directory-Makefile-generation script

14 years agoauto-generated list of AC_CONFIG_FILES so that you needn't add each recursive Makefil...
Morgan Deters [Fri, 5 Feb 2010 22:31:33 +0000 (22:31 +0000)]
auto-generated list of AC_CONFIG_FILES so that you needn't add each recursive Makefile to configure.ac

14 years agoautomatic generator script for sourcedir Makefiles and Makefile.ams
Morgan Deters [Fri, 5 Feb 2010 22:30:22 +0000 (22:30 +0000)]
automatic generator script for sourcedir Makefiles and Makefile.ams

14 years agoremove the last vestiges of support for "make build-profile" without first configurin...
Morgan Deters [Fri, 5 Feb 2010 21:16:56 +0000 (21:16 +0000)]
remove the last vestiges of support for "make build-profile" without first configuring the build-profile, simplifying the build process and closing bug 21

14 years agominor interface changes to TheoryEngine/Theory after meeting and conversation with Tim
Morgan Deters [Thu, 4 Feb 2010 23:59:41 +0000 (23:59 +0000)]
minor interface changes to TheoryEngine/Theory after meeting and conversation with Tim

14 years agofix run_regression script
Morgan Deters [Thu, 4 Feb 2010 23:50:25 +0000 (23:50 +0000)]
fix run_regression script

14 years agobeautification of the prop engine
Dejan Jovanović [Thu, 4 Feb 2010 23:50:23 +0000 (23:50 +0000)]
beautification of the prop engine

14 years agoassign expected-status to regressions
Morgan Deters [Thu, 4 Feb 2010 23:31:00 +0000 (23:31 +0000)]
assign expected-status to regressions

14 years agobuild system for multi-level regressions
Morgan Deters [Thu, 4 Feb 2010 23:29:47 +0000 (23:29 +0000)]
build system for multi-level regressions

14 years agoremove warnings from use of __gnu_cxx::hash_map<>; also spacing fixes in symbol table
Morgan Deters [Thu, 4 Feb 2010 22:14:28 +0000 (22:14 +0000)]
remove warnings from use of __gnu_cxx::hash_map<>; also spacing fixes in symbol table

14 years agoremove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing-mode...
Morgan Deters [Thu, 4 Feb 2010 22:10:47 +0000 (22:10 +0000)]
remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing-mode from contrib/editing-with-emacs

14 years agoChanged mapping from atoms to literals in the prop engine to be atoms to vars.
Tim King [Thu, 4 Feb 2010 21:03:07 +0000 (21:03 +0000)]
Changed mapping from atoms to literals in the prop engine to be atoms to vars.

14 years agoMoved regressions into various levels based on running time.
Tim King [Thu, 4 Feb 2010 21:01:04 +0000 (21:01 +0000)]
Moved regressions into various levels based on running time.

14 years agotest infrastructure updated for multiple-level regressions
Morgan Deters [Thu, 4 Feb 2010 19:01:55 +0000 (19:01 +0000)]
test infrastructure updated for multiple-level regressions

14 years agominor cleanup; give the main driver a different exit code for SAT-INVALID/UNSAT-VALID
Morgan Deters [Thu, 4 Feb 2010 03:47:41 +0000 (03:47 +0000)]
minor cleanup; give the main driver a different exit code for SAT-INVALID/UNSAT-VALID

14 years agosrc/expr/kind.h is now automatically generated.
Morgan Deters [Thu, 4 Feb 2010 03:31:38 +0000 (03:31 +0000)]
src/expr/kind.h is now automatically generated.

Build src/expr before src/util.

Moved CVC4::Command to the expr package.

Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).

Added file-level documentation to Antlr sources

When built for debug, spin on SEGV instead of aborting.  Really useful
for debugging problems that crop up only on long runs.  Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.

Updated src/main/about.h for 2010.

14 years agominor fix for update-copyright.pl; ran update-copyright.pl on all sources; regenerate...
Morgan Deters [Thu, 4 Feb 2010 02:58:12 +0000 (02:58 +0000)]
minor fix for update-copyright.pl; ran update-copyright.pl on all sources; regenerated configure script

14 years agoadded bool and arith theory makefiles to AC_CONFIG_FILES in configure.ac
Morgan Deters [Thu, 4 Feb 2010 02:47:30 +0000 (02:47 +0000)]
added bool and arith theory makefiles to AC_CONFIG_FILES in configure.ac

14 years agoAdded theory output channel interfaces and "Interrupted" exception.
Morgan Deters [Thu, 4 Feb 2010 02:46:17 +0000 (02:46 +0000)]
Added theory output channel interfaces and "Interrupted" exception.

Updated contrib/update-copyright to handle Antlr (.g) parser/lexer inputs.
Updated copyright year.

Added a new "bool" theory (right now just to hold a kind.h contribution).

Added "kinds" files to UF and the new "bool" theory.

14 years agoFixes to the cnf converter. Also a barebones utility for printing out a satisifying...
Tim King [Thu, 4 Feb 2010 00:47:45 +0000 (00:47 +0000)]
Fixes to the cnf converter. Also a barebones utility for printing out a satisifying model.

14 years agoAdding extra test to parser
Christopher L. Conway [Wed, 3 Feb 2010 23:52:16 +0000 (23:52 +0000)]
Adding extra test to parser

14 years agoadding an option to minisat to not do any debug checks/output
Dejan Jovanović [Wed, 3 Feb 2010 23:45:53 +0000 (23:45 +0000)]
adding an option to minisat to not do any debug checks/output

14 years agoFixing bad commit
Christopher L. Conway [Wed, 3 Feb 2010 23:43:43 +0000 (23:43 +0000)]
Fixing bad commit

14 years agoAdding functions/predicates to SMT grammar
Christopher L. Conway [Wed, 3 Feb 2010 22:46:36 +0000 (22:46 +0000)]
Adding functions/predicates to SMT grammar

14 years agoAddressed many of the concerns of bug 10 (build system code review).
Morgan Deters [Wed, 3 Feb 2010 22:20:25 +0000 (22:20 +0000)]
Addressed many of the concerns of bug 10 (build system code review).
Some parts split into other bugs: 19, 20, 21.

Addressed concerns of bug 11 (util package code review).

Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers

Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main().  Silenced MiniSat when
verbosity is not requested.

14 years agoELSEIF support and parser debugging with '-d parser'
Dejan Jovanović [Wed, 3 Feb 2010 22:10:21 +0000 (22:10 +0000)]
ELSEIF support and parser debugging with '-d parser'

14 years agosimple ITE parsing
Dejan Jovanović [Wed, 3 Feb 2010 19:50:44 +0000 (19:50 +0000)]
simple ITE parsing

14 years agoBy popular demand, I also added a printAst to Expr.
Tim King [Wed, 3 Feb 2010 19:41:14 +0000 (19:41 +0000)]
By popular demand, I also added a printAst to Expr.

14 years agoI hacked in a temporary way to restart minisat for multiple queries.
Tim King [Wed, 3 Feb 2010 19:25:50 +0000 (19:25 +0000)]
I hacked in a temporary way to restart minisat for multiple queries.

14 years agoWithin node I added printAst(..) for general purpose debugging use throughout the...
Tim King [Wed, 3 Feb 2010 19:23:45 +0000 (19:23 +0000)]
Within node I added printAst(..) for general purpose debugging use throughout the code. I also added debugPrint() to Node for use within gdb.