cvc5.git
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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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