cvc5.git
14 years agoWith "-d extra-checking", rewrites are now checked (after
Morgan Deters [Sun, 4 Jul 2010 03:59:36 +0000 (03:59 +0000)]
With "-d extra-checking", rewrites are now checked (after
post-rewrite, another full rewrite is performed and the results
compared).

Also added another response code to rewriters.  Theories return a
CVC4::theory::RewriteResponse from preRewrite() and postRewrite().
This class has nice subclasses to make the theory rewriters somewhat
self-documenting in termination behavior.  They look like
tail-recursive rewriting calls, but they're not; they are
instantiations of the RewriteResponse result code, which carries the
Node being returned:

  // Flags the node as DONE pre- or post-rewriting, though this is
  // ignored if n belongs to another theory.
  //
  // NOTE this just changed name from RewritingComplete(), which
  // didn't match RewriteAgain().
  //
  return RewriteComplete(n);

  // Flags the node as needing another pre-rewrite (if returned from a
  // preRewrite()) or post-rewrite (if returned from a postRewrite()).
  //
  return RewriteAgain(n);

  // Flags the node as needing another FULL rewrite.  This is the same
  // as RewriteAgain() if returned from preRewrite().  If it's returned
  // from postRewrite(), however, this causes a full preRewrite() and
  // postRewrite() of the Node and all its children (though the cache is
  // still in effect, which might elide some rewriting calls).
  //
  // This would have been another fix for bug #168.  Its use should be
  // discouraged in practice, but there are places where it will
  // probably be necessary, where a theory rewrites a Node into
  // something in another theory about which it knows nothing.
  // A common case is where the returned Node is expressed as a
  // conjuction or disjunction of EQUALs, or a negation of EQUAL,
  // where the EQUAL is across terms in another theory, and that EQUAL
  // subterm should be seen by the owning theory.
  //
  return FullRewriteNeeded(n);

14 years agobug 168 fixed (TheoryEngine::rewrite is not fully rewriting to a fix point); problem...
Morgan Deters [Sun, 4 Jul 2010 02:18:02 +0000 (02:18 +0000)]
bug 168 fixed (TheoryEngine::rewrite is not fully rewriting to a fix point); problem had to do with the builtin theory post-rewriting DISTINCT into an arithmetic term not in normal form.  fix was to do DISTINCT rewriting in pre-rewrite.  note that this doesn't add to the amount of theory rewriting work that needs to be done, because everything is cached

14 years agomake dist && make distcheck functional, other fixes
Morgan Deters [Sun, 4 Jul 2010 02:00:42 +0000 (02:00 +0000)]
make dist && make distcheck functional, other fixes

14 years agofix warnings
Morgan Deters [Sat, 3 Jul 2010 23:09:25 +0000 (23:09 +0000)]
fix warnings

14 years agobetter config.reconfig script auto-generated
Morgan Deters [Sat, 3 Jul 2010 18:18:55 +0000 (18:18 +0000)]
better config.reconfig script auto-generated

14 years agoWith this commit come a number of changes to build system to support
Morgan Deters [Sat, 3 Jul 2010 17:59:19 +0000 (17:59 +0000)]
With this commit come a number of changes to build system to support
building with CLN or with GMP, the contrib/switch-config script
(enabling "fast switching" of different configurations in the same
builds/ directory), and also some minor changes.

./configure --with-gmp     (or --without-cln) forces building with GMP
and doesn't even look for CLN.  Configure fails if GMP isn't installed.

./configure --with-cln     (or --without-gmp) forces building with CLN
and doesn't even look for GMP.  Configure fails if CLN isn't installed.

./configure [no arguments] will detect what's installed.  CLN is
default, if it isn't installed, or is too old, GMP is looked for (and
configure fails if neither is available).

It is an error to specify --with-gmp --with-cln (or --without-* for
both) at the same time.

Building with CLN (whether forced or detected) adds a note to the
configure output mentioning the fact that the build of CVC4 will be
linked against a GPLed library and notifying the user of the
--without-cln option.

Building with GMP (whether forced or detected) affects the build
directory, so CLN and GMP builds are kept separate.

./configure --with-cln debug     builds in builds/$arch/debug
./configure --with-gmp debug     builds in builds/$arch/debug-gmp

The final binaries are linked explicitly against either gmp or cln,
but not both.  If linked against cln, cln pulls in gmp as a
dependency, so the result will be linked against both.

=== Details that you probably don't care about ===

The headers src/util/{integer,rational}.h are generated from the
corresponding .in versions.  A user installing a CVC4-devel package
will get the headers for rational and integer that match the library
that s/he installs.

The preprocessor #defines CVC4_GMP_IMP and CVC4_CLN_IMP are added to
cvc4autoconfig.h.  Only one is ever #defined.  cvc4autoconfig.h
doesn't need to be #included directly; you get it through #including
cvc4_private.h (or the parser version).

AM_CONDITIONALs are also defined so that Makefiles get the cln/gmp
configuration.  AC_SUBSTs are defined so that public headers (see
src/util/{integer,rational}.h.in) can use the setting.

*Public* headers that need to depend on the cln/gmp configuration
can't use cvc4autoconfig.h, because we're keeping that in the private,
internal-only space, never to be installed on users' machines.  Here,
something special is required, like the configure-level generation of
headers that I used for src/util/{integer,rational}.h.in.

Tim's Integer and Rational wrappers are the only bits of code that
should care which library is used (and also src/util/configuration.h,
which gives the user of the library information about how CVC4 is
built), and possibly some unit tests (?).

14 years agoMerges the cln-test branch into the main branch.
Tim King [Fri, 2 Jul 2010 18:49:47 +0000 (18:49 +0000)]
Merges the cln-test branch into the main branch.

The current commit allows for switching in between GMP and CLN by changing a flag manually in configure.ac.  A configure time flag has not yet been added for deciding between the two.

To get this to work you will need to install cln in some form (for Ubuntu users the packages are libcln6(lucid)/libcln5 on karmic and libcln-dev).  You will also need to install pkg-config. You will need to rerun ./autogen.sh, and reconfigure.

14 years agore-generated comment headers of source files
Morgan Deters [Fri, 2 Jul 2010 00:30:19 +0000 (00:30 +0000)]
re-generated comment headers of source files

14 years agoroll back a small change that made arith fail some asserts
Morgan Deters [Fri, 2 Jul 2010 00:27:49 +0000 (00:27 +0000)]
roll back a small change that made arith fail some asserts

14 years ago* Added white-box TheoryEngine test that tests the rewriter
Morgan Deters [Fri, 2 Jul 2010 00:09:52 +0000 (00:09 +0000)]
* Added white-box TheoryEngine test that tests the rewriter

* Added regression documentation to test/regress/README

* Added ability to print types of vars in expr printouts
  with iomanipulator Node::printtypes(true)... for example,
    Warning() << Node::printtypes(true) << n << std::endl;

* Types-printing can be specified on the command line with
  --print-expr-types

* Improved type handling facilities and theoryOf().
  For now, SORT_TYPE moved from builtin theory to UF theory
  to match old behavior.

* Additional gdb debug functionality.  Now we have:

    debugPrintNode(Node)            debugPrintRawNode(Node)
    debugPrintTNode(TNode)          debugPrintRawTNode(TNode)
    debugPrintTypeNode(TypeNode)    debugPrintRawTypeNode(TypeNode)
    debugPrintNodeValue(NodeValue*) debugPrintRawNodeValue(NodeValue*)

  they all print a {Node,TNode,NodeValue*} from the debugger.
  The "Raw" versions print a very low-level AST-like form.
  The regular versions do the same as operator<<, but force
  full printing on (no depth-limiting).

* Other trivial fixes

14 years agoadd documentation for additional clarity, re-add addTerm()
Morgan Deters [Wed, 30 Jun 2010 16:59:29 +0000 (16:59 +0000)]
add documentation for additional clarity, re-add addTerm()

14 years agoParsing support for SMT divisions: LRA, QF_UFLIA, QF_UFLRA, QF_UFNRA, UFNIA
Christopher L. Conway [Wed, 30 Jun 2010 16:23:47 +0000 (16:23 +0000)]
Parsing support for SMT divisions: LRA, QF_UFLIA, QF_UFLRA, QF_UFNRA, UFNIA

14 years agoAdding documentation for --strict-parsing (Closes: #166)
Christopher L. Conway [Wed, 30 Jun 2010 16:23:42 +0000 (16:23 +0000)]
Adding documentation for --strict-parsing (Closes: #166)

14 years agofix to switch fall-through; stats now off by default regardless of -d debugging optio...
Morgan Deters [Wed, 30 Jun 2010 15:26:13 +0000 (15:26 +0000)]
fix to switch fall-through; stats now off by default regardless of -d debugging options; thanks Chris for spoting this

14 years agochecking in CC module interface for reference.
Morgan Deters [Wed, 30 Jun 2010 13:56:07 +0000 (13:56 +0000)]
checking in CC module interface for reference.

14 years agoSupport for failing .smt and .smt2 regressions (and other examples with
Morgan Deters [Wed, 30 Jun 2010 13:35:53 +0000 (13:35 +0000)]
Support for failing .smt and .smt2 regressions (and other examples with
additional output).  If the benchmark file has '% EXPECT: ' gestures,
like for cvc regressions, that is used (after being stripped out so that
the cvc4 smt parser never sees these special lines).  However, this can
be a pain, since then you can't run the regression manually on the
command line (since it fails to parse).  So if there is another file
in the same directory as $benchmark called $benchmark.expect, that is
scanned for '% EXPECT: ' etc., and the benchmark file is used verbatim.

14 years ago* theory "tree" rewriting implemented and works
Morgan Deters [Wed, 30 Jun 2010 11:12:14 +0000 (11:12 +0000)]
* theory "tree" rewriting implemented and works

* added TheoryArith::preRewrite() to test and demonstrate
  the use of pre-rewriting.

* array types and type checking now supported

* array type checking now supported

* theoryOf() dispatching properly to arrays now

* theories now required to implement a (simple) identify()
  function that returns a string identifying them for
  debugging/user output purposes

* added "builtin" theory to hold all built-in kinds and their
  type rules and rewriting (currently only exploding distinct)

* fixed production build failure (regarding NodeSetDepth)

* removed an errant "using namespace std" in util/bitvector.h
  (and made associated trivial fixes elsewhere)

* fixes to make unexpected exceptions more verbose in debug builds

* fixes to make multiple, cascading assertion fails simpler

* minor other fixes to comments etc.

14 years agoadd --default-expr-depth=N command line parameter, expose setdepth() to public interface
Morgan Deters [Tue, 29 Jun 2010 22:42:40 +0000 (22:42 +0000)]
add --default-expr-depth=N command line parameter, expose setdepth() to public interface

14 years agoThis commit merges the decaying-rows branch into the main trunk.
Tim King [Tue, 29 Jun 2010 22:01:30 +0000 (22:01 +0000)]
This commit merges the decaying-rows branch into the main trunk.

14 years agoUpdate to stats.h is now back into the trunk. The code should compile once again.
Tim King [Tue, 29 Jun 2010 20:58:44 +0000 (20:58 +0000)]
Update to stats.h is now back into the trunk.  The code should compile once again.

14 years agoMerging the unate-propagator branch into the trunk. This is a big update so expect...
Tim King [Tue, 29 Jun 2010 20:53:47 +0000 (20:53 +0000)]
Merging the unate-propagator branch into the trunk.  This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.

14 years ago* Add CDMap<>::insertAtContextLevelZero(k, d) for inserting "initializing"
Morgan Deters [Tue, 29 Jun 2010 00:49:38 +0000 (00:49 +0000)]
* Add CDMap<>::insertAtContextLevelZero(k, d) for inserting "initializing"
  data into a CDMap.  Such a key doesn't disappear from the map on pop,
  but rather returns to its "initializing" state, set by
  insertAtContextLevelZero().  This can be used for lazy assignment,
  among other things, and has been added to support some exploratory
  coding by Tim in arithmetic.

* Made internal CDOmap<> copy constructor private (it should always have
  been).  This is necessary to avoid CxxTest (or others) doing nasty
  generic programming things that cause context invariants to be broken.

* Added unit testing for this feature, and in general beef up the unit
  testing for CDMap<>.

* src/expr/node_manager.cpp: Better output for unhandled cases in getType().

14 years agoAdded post_mortem.py a statistics collector for user with the smt_curnch cluster...
Tim King [Thu, 24 Jun 2010 15:12:46 +0000 (15:12 +0000)]
Added post_mortem.py a statistics collector for user with the smt_curnch cluster. Also a spelling correction for the statistic theory::conflict.

14 years agoMade ~Stat() virtual. Added some additional statistics. And added some documentation.
Tim King [Tue, 22 Jun 2010 17:25:14 +0000 (17:25 +0000)]
Made ~Stat() virtual. Added some additional statistics. And added some documentation.

14 years ago"statistics" and "staticbinary" are now tags on the build (so you get build directori...
Morgan Deters [Fri, 18 Jun 2010 23:09:29 +0000 (23:09 +0000)]
"statistics" and "staticbinary" are now tags on the build (so you get build directories like builds/x86_64-unknown-linux-gnu/debug-staticbinary-nostatistics .. etc.  This is useful to distinguish static binary builds and statistics builds from each other when you configure multiple times in the same source directory

14 years agoMerging the statistics branch into the main trunk. I'll go over how to use this Tuesd...
Tim King [Fri, 18 Jun 2010 22:24:59 +0000 (22:24 +0000)]
Merging the statistics branch into the main trunk. I'll go over how to use this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating.

14 years agobug fix (unreported on bugzilla): skolem variables failing removal from pool
Morgan Deters [Fri, 18 Jun 2010 05:40:35 +0000 (05:40 +0000)]
bug fix (unreported on bugzilla): skolem variables failing removal from pool

14 years agofix some minor annoyances in the regression test Makefiles; add some documentation
Morgan Deters [Thu, 17 Jun 2010 18:05:04 +0000 (18:05 +0000)]
fix some minor annoyances in the regression test Makefiles; add some documentation

14 years agoAdded the experimental. +bool TheoryArith::AssertEquality(TNode n, TNode original){
Tim King [Wed, 16 Jun 2010 22:29:44 +0000 (22:29 +0000)]
Added the experimental. +bool TheoryArith::AssertEquality(TNode n, TNode original){

14 years agoMore assorted changes to arithmetic in preparation for the code review.
Tim King [Wed, 16 Jun 2010 21:19:34 +0000 (21:19 +0000)]
More assorted changes to arithmetic in preparation for the code review.

14 years agoThis commit just contains miscellaneous arithmetic cleanup.
Tim King [Wed, 16 Jun 2010 20:26:14 +0000 (20:26 +0000)]
This commit just contains miscellaneous arithmetic cleanup.

14 years agofix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)
Morgan Deters [Tue, 15 Jun 2010 22:05:46 +0000 (22:05 +0000)]
fix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)

14 years agoremove warnings about unknown #pragma GCC diagnostic on older compilers
Morgan Deters [Tue, 15 Jun 2010 21:46:56 +0000 (21:46 +0000)]
remove warnings about unknown #pragma GCC diagnostic on older compilers

14 years agoI made a documentation change to get() to make explicit the contract requirements...
Tim King [Tue, 15 Jun 2010 16:36:49 +0000 (16:36 +0000)]
I made a documentation change to get() to make explicit the contract requirements for 'slurping the queue'. Closes bug 154

14 years ago(minor) fix for file documentation
Morgan Deters [Tue, 15 Jun 2010 15:55:22 +0000 (15:55 +0000)]
(minor) fix for file documentation

14 years agoAdding array select/store to SMT v1 and v2 parsers
Christopher L. Conway [Mon, 14 Jun 2010 20:45:11 +0000 (20:45 +0000)]
Adding array select/store to SMT v1 and v2 parsers

14 years agoFix to arith to make sure it only attempts to report 1 conflict per check() call.
Tim King [Mon, 14 Jun 2010 18:35:17 +0000 (18:35 +0000)]
Fix to arith to make sure it only attempts to report 1 conflict per check() call.

14 years agoStarted work on array theory
Clark Barrett [Mon, 14 Jun 2010 16:06:51 +0000 (16:06 +0000)]
Started work on array theory

14 years agoSome assorted fixes and local optimizations for theory arith.
Tim King [Sun, 6 Jun 2010 17:06:07 +0000 (17:06 +0000)]
Some assorted fixes and local optimizations for theory arith.

14 years agoAdding += and *= to Rational.
Tim King [Sun, 6 Jun 2010 16:25:19 +0000 (16:25 +0000)]
Adding += and *= to Rational.

14 years agoChanged how assignments are saved during check. These are now backed by an attribute...
Tim King [Fri, 4 Jun 2010 19:40:33 +0000 (19:40 +0000)]
Changed how assignments are saved during check.  These are now backed by an attribute.  There is now a priority queue for selecting the smallest inconsistent basic variable. normal.h has been removed.  A large chunk of the registerTerm() stuff has been moved into preregister. The lazy splitting code is now been commented out so that it stops showing up in profiling.

14 years agoChanged several arguments to const references.
Tim King [Fri, 4 Jun 2010 19:32:26 +0000 (19:32 +0000)]
Changed several arguments to const references.

14 years agoAdding QF_SAT to SMT parsers
Christopher L. Conway [Fri, 4 Jun 2010 19:19:47 +0000 (19:19 +0000)]
Adding QF_SAT to SMT parsers

14 years agoReimplementing AntlrInputStream::newStreamInputStream
Christopher L. Conway [Fri, 4 Jun 2010 19:19:42 +0000 (19:19 +0000)]
Reimplementing AntlrInputStream::newStreamInputStream

14 years ago** Don't fear the files-changed list, almost all changes are in the **
Morgan Deters [Fri, 4 Jun 2010 18:55:22 +0000 (18:55 +0000)]
** Don't fear the files-changed list, almost all changes are in the **
** file-level documentation at the top of the sources.              **

This is the "make bugzilla stop bugging me" bugfix commit.

* Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy.
  Updated documentation in the file.  Resolves bug #99.

* Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.)
  moved into a separate file.  Partially resolves bug #100.

* Moved isAssociative(Kind) into kind.h (and into the CVC4::kind
  namespace) instead of metakind.h (where it was in CVC4::metakind).
  This clears up a warning (private #inclusion) from the SMT and SMT2
  parsers, and maybe makes more sense anyways, since this is based on
  the kind (and not the metakind) of an operator.

* Documentation improvement; doxygen top-level \file gestures, \brief
  gestures for files, etc.  Changed contrib/update-copyright.pl for
  this change, and post-processed to add \brief.  Resolves bug #98.

* Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind).
  They no longer made sense.  Resolves bug #91.

14 years agoMissing files in last commit
Christopher L. Conway [Fri, 4 Jun 2010 17:15:13 +0000 (17:15 +0000)]
Missing files in last commit

14 years agoEnabling RDL/IDL in SMT v1 and adding some simple tests
Christopher L. Conway [Fri, 4 Jun 2010 17:14:04 +0000 (17:14 +0000)]
Enabling RDL/IDL in SMT v1 and adding some simple tests

14 years agoImplementing input from stdin (Fixes: #144)
Christopher L. Conway [Thu, 3 Jun 2010 22:27:16 +0000 (22:27 +0000)]
Implementing input from stdin (Fixes: #144)

14 years agoFixes 2 issues with assignments. The first is constructing an initial assignment...
Tim King [Thu, 3 Jun 2010 20:34:21 +0000 (20:34 +0000)]
Fixes 2 issues with assignments. The first is constructing an initial assignment for slack variables once solving has begun. (They cannot just be 0.) The second has to do with how assignments are backttacked.  Assignments are now tracked all of the time, and are frozen once they are known to be consistent, i.e. after a successful updateInconsistentVars().  Also added a fuzz test that shows both of these problems to the regressions.

14 years agoAdds toString to DeltaRational
Tim King [Thu, 3 Jun 2010 18:35:15 +0000 (18:35 +0000)]
Adds toString to DeltaRational

14 years agoFixes a bug where registration occurs before preregistration.
Tim King [Thu, 3 Jun 2010 18:26:15 +0000 (18:26 +0000)]
Fixes a bug where registration occurs before preregistration.

14 years agoChanging ANTLR3 detection in configure (Fixes #147)
Christopher L. Conway [Thu, 3 Jun 2010 16:47:05 +0000 (16:47 +0000)]
Changing ANTLR3 detection in configure (Fixes #147)

14 years ago* Added NodeBuilder<>::getChild() to make interface more consistent
Morgan Deters [Thu, 3 Jun 2010 13:22:57 +0000 (13:22 +0000)]
* Added NodeBuilder<>::getChild() to make interface more consistent
  with that of Node.

* If NodeBuilder<> hasn't yet been assigned a Kind, several member functions
  related to children now throw an IllegalArgumentException:

    * getNumChildren()
    * begin()
    * end()
    * operator[]
    * getChild()

  This is because if you later assign the NodeBuilder<> a PARAMETERIZED kind,
  the children are "reinterpreted" -- the first being an operator.  Interface-wise,
  it doesn't make sense to return one thing for nb[0], then later, after setting
  the kind, to return another thing for nb[0].

* Fixed unit tests depending on this behavior.

* Added a warning to the testing summary if unit tests didn't run (because this
  is likely due to compilation problems, and without a warning it looks kind of
  like a test success)

* VERBOSE wasn't exported to the environment for unit test "make check."  Fixed.

14 years agoresolving bug 139: metaKindOf() warnings still exist, but it's probably a g++ 4.3...
Morgan Deters [Thu, 3 Jun 2010 00:09:14 +0000 (00:09 +0000)]
resolving bug 139: metaKindOf() warnings still exist, but it's probably a g++ 4.3 and 4.4 issue

14 years agoadded a handful of debugTagIsOn("context") checks to resolve bug 143
Morgan Deters [Wed, 2 Jun 2010 23:18:54 +0000 (23:18 +0000)]
added a handful of debugTagIsOn("context") checks to resolve bug 143

14 years agomore VERBOSE test failures
Morgan Deters [Wed, 2 Jun 2010 21:12:18 +0000 (21:12 +0000)]
more VERBOSE test failures

14 years agoFixing test failures in production build
Christopher L. Conway [Tue, 1 Jun 2010 21:56:35 +0000 (21:56 +0000)]
Fixing test failures in production build

14 years agoThis commit adds a debugTagIsOn() guard around some extremely verbose debugging state...
Tim King [Tue, 1 Jun 2010 21:43:18 +0000 (21:43 +0000)]
This commit adds a debugTagIsOn() guard around some extremely verbose debugging statements.  There is some evidence that these debugging statements were 20% of the running time for QF_LRA/miplib/fixnet-1000.smt in debug mode.

14 years agoThis commit is a fix for a bug in removeITEs(). The check that the then branch is...
Tim King [Tue, 1 Jun 2010 21:34:43 +0000 (21:34 +0000)]
This commit is a fix for a bug in removeITEs().  The check that the then branch is a boolean should now be working. This fixes bug 138.

14 years agoAdding SMT v2 parsing support for: QF_IDL, QF_NIA, QF_RDL, QF_UFIDL
Christopher L. Conway [Tue, 1 Jun 2010 20:19:30 +0000 (20:19 +0000)]
Adding SMT v2 parsing support for: QF_IDL, QF_NIA, QF_RDL, QF_UFIDL

14 years agoChecking for executable permission on antlr3 script
Christopher L. Conway [Tue, 1 Jun 2010 20:01:07 +0000 (20:01 +0000)]
Checking for executable permission on antlr3 script

14 years agoFixed a bug in partial_model.cpp where the data was immediately deallocated before...
Tim King [Tue, 1 Jun 2010 16:39:02 +0000 (16:39 +0000)]
Fixed a bug in partial_model.cpp where the data was immediately deallocated before being used.  Fixed a bug in node_builder.h's crop where a pointer is dereferenced after a realloc call.

14 years agoFixing failing test in r521
Christopher L. Conway [Tue, 1 Jun 2010 02:02:07 +0000 (02:02 +0000)]
Fixing failing test in r521
Adding general support for associative operators in SMT v1 and v2

14 years agoIn order for splitting on demand to be able to retract clauses every translation...
Dejan Jovanović [Tue, 1 Jun 2010 01:26:24 +0000 (01:26 +0000)]
In order for splitting on demand to be able to retract clauses every translation must indeed be a clause (if possible). I've changed the top level CNF conversion to generate clauses, instead of introducing unit clauses for each assertion.

14 years agoFirst draft implementation of mkAssociative
Christopher L. Conway [Mon, 31 May 2010 21:55:40 +0000 (21:55 +0000)]
First draft implementation of mkAssociative

14 years agoAdding a couple of example from fuzzsmt to regress1.
Tim King [Sat, 29 May 2010 22:48:01 +0000 (22:48 +0000)]
Adding a couple of example from fuzzsmt to regress1.

14 years agoCouple of fixes to theory arith. pivotAndUpdate now multiplies by a_kj. And the table...
Tim King [Sat, 29 May 2010 02:58:18 +0000 (02:58 +0000)]
Couple of fixes to theory arith. pivotAndUpdate now multiplies by a_kj. And the tableau now simulates older pivots while adding a new row.

14 years agoAfter blasting the disjuncts, TheoryEngine rewrite needs to reinvoke itself. QF_LRA...
Tim King [Sat, 29 May 2010 00:14:09 +0000 (00:14 +0000)]
After blasting the disjuncts, TheoryEngine rewrite needs to reinvoke itself. QF_LRA is now no longer complaining about seeing nodes that can be rewritten to CONST_BOOLEAN.

14 years agoThis update enables TheoryArith to accept assertions that rewrite to true or false...
Tim King [Fri, 28 May 2010 22:17:04 +0000 (22:17 +0000)]
This update enables TheoryArith to accept assertions that rewrite to true or false. This is temporary and will be removed once TheoryEngine rewriting is more fully debugged.

14 years agoBug fixes for combining coefficients of rewritten nodes.
Tim King [Fri, 28 May 2010 22:09:08 +0000 (22:09 +0000)]
Bug fixes for combining coefficients of rewritten nodes.

14 years agoAdded printModel() to src/theory/arith/partial_model.cpp. This is a debugging utilit...
Tim King [Fri, 28 May 2010 22:06:58 +0000 (22:06 +0000)]
Added printModel() to src/theory/arith/partial_model.cpp.  This is a debugging utility that prints out the lower bound, upper bound, assignment, and the constraints that were asserted that caused the lower bound and upperbound to be asserted.

14 years agoA few changes to the organization of TheoryEngine rewriting. A few bug fixes for...
Tim King [Fri, 28 May 2010 22:01:18 +0000 (22:01 +0000)]
A few changes to the organization of TheoryEngine rewriting. A few bug fixes for it as well. make check should now work again.

14 years agoMoving the ITE removal from CnfStream to TheoryEngine, which is a bit closer to its...
Tim King [Fri, 28 May 2010 20:17:48 +0000 (20:17 +0000)]
Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer to its final destination. Added a basic rewriter to TheoryUF. (x=x rewrites to true.) Added DIVISION to src/expr/node_manager.cpp's getType. Fixed the theory returned for variables in theoryOf() for bool and arith. Fixed TheoryEngine rewrite children to properly handle APPLY_UFs. Removed the special case for equality in TheoryEngine rewrite. A few tests are currently broken due to deallocation errors. Morgan and I will try to commit a fix to this in a little bit.

14 years agofix bug #134: infinite deallocation loop
Morgan Deters [Thu, 27 May 2010 22:16:02 +0000 (22:16 +0000)]
fix bug #134: infinite deallocation loop

14 years agosmall cosmetic change to tests summary output
Morgan Deters [Thu, 27 May 2010 21:25:35 +0000 (21:25 +0000)]
small cosmetic change to tests summary output

14 years agoRemove isAtomic() as per 4/27/2010 meeting. Add comments about its potential design...
Morgan Deters [Thu, 27 May 2010 21:19:36 +0000 (21:19 +0000)]
Remove isAtomic() as per 4/27/2010 meeting.  Add comments about its potential design for later.  Resolves bug 113, invalidates bugs 93 and 94.

14 years agofix compiler comparison-signedness warnings
Morgan Deters [Thu, 27 May 2010 21:18:56 +0000 (21:18 +0000)]
fix compiler comparison-signedness warnings

14 years agoReverting this file to not include any comments. (Morgan's revision and my revision...
Tim King [Thu, 27 May 2010 20:57:24 +0000 (20:57 +0000)]
Reverting this file to not include any comments. (Morgan's revision and my revision were in conflict.)

14 years agoadded the ability to add custom expected stdout, stderr, and exit codes to smt and...
Morgan Deters [Thu, 27 May 2010 20:46:50 +0000 (20:46 +0000)]
added the ability to add custom expected stdout, stderr, and exit codes to smt and smt2 regressions; resolves bug 132

14 years agoPreregistration has been turned on. Highly experimental eager splitting support has...
Tim King [Thu, 27 May 2010 20:34:18 +0000 (20:34 +0000)]
Preregistration has been turned on. Highly experimental eager splitting support has been added.  Also a few bug fixes to Tableau.

14 years agoUse the newer automake test driver "parallel-tests". This driver:
Morgan Deters [Thu, 27 May 2010 19:49:17 +0000 (19:49 +0000)]
Use the newer automake test driver "parallel-tests".  This driver:

* keeps test logs around
* provides parallel testing functionality (with make -jN).

I've also added new functionality in test/Makefile.am which deletes old test logs, ensures that ALL tests are tried (even if units fail), and provides a color-coded summary at the end of the test run, which shows how many units, regressions (per level), and system tests failed (or passed), and provides a link to the log file for further information.

Resolves bug 117.

14 years agoAdding debug assertions on most TNode operations
Christopher L. Conway [Thu, 27 May 2010 18:39:36 +0000 (18:39 +0000)]
Adding debug assertions on most TNode operations

14 years agoAdding NodeManager::prepareToBeDestroyed() (Fixes: #128)
Christopher L. Conway [Thu, 27 May 2010 18:39:32 +0000 (18:39 +0000)]
Adding NodeManager::prepareToBeDestroyed() (Fixes: #128)

14 years agoAdding .cvc4_config to .gitignore
Christopher L. Conway [Thu, 27 May 2010 18:39:22 +0000 (18:39 +0000)]
Adding .cvc4_config to .gitignore

14 years agofix bug #111: errors in building lcov-all
Morgan Deters [Thu, 27 May 2010 17:55:39 +0000 (17:55 +0000)]
fix bug #111: errors in building lcov-all

14 years agofix bug 120; competition mode regression failures for intentionally-buggy input
Morgan Deters [Thu, 27 May 2010 04:08:33 +0000 (04:08 +0000)]
fix bug 120; competition mode regression failures for intentionally-buggy input

14 years ago . '+Outstanding case split in theory arith'
Tim King [Wed, 26 May 2010 22:41:54 +0000 (22:41 +0000)]
 . '+Outstanding case split in theory arith'

14 years agoAdding CnfStreamBlack tests for all Boolean connectives
Christopher L. Conway [Wed, 26 May 2010 22:10:10 +0000 (22:10 +0000)]
Adding CnfStreamBlack tests for all Boolean connectives

14 years agoFixing test failures in CnfStreamBlack (it was the test's fault)
Christopher L. Conway [Wed, 26 May 2010 21:50:18 +0000 (21:50 +0000)]
Fixing test failures in CnfStreamBlack (it was the test's fault)

14 years agoAdding documentation to my-configure
Christopher L. Conway [Wed, 26 May 2010 21:50:13 +0000 (21:50 +0000)]
Adding documentation to my-configure

14 years agoFixing my-configure
Christopher L. Conway [Wed, 26 May 2010 20:54:40 +0000 (20:54 +0000)]
Fixing my-configure

14 years agoAdding contrib/my-configure
Christopher L. Conway [Wed, 26 May 2010 20:52:42 +0000 (20:52 +0000)]
Adding contrib/my-configure

14 years agoAdding CnfStream unit tests
Christopher L. Conway [Wed, 26 May 2010 20:52:37 +0000 (20:52 +0000)]
Adding CnfStream unit tests

14 years agoCDMap<> and CDOmap<> fixes to resolve bug 123
Morgan Deters [Wed, 26 May 2010 20:29:53 +0000 (20:29 +0000)]
CDMap<> and CDOmap<> fixes to resolve bug 123

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

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

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

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

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

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

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