cvc5.git
13 years agoFix for Mac OS breakage (x86 didn't crash, but probably would, eventually, on some...
Morgan Deters [Mon, 6 Jun 2011 21:37:23 +0000 (21:37 +0000)]
Fix for Mac OS breakage (x86 didn't crash, but probably would, eventually, on some problems---valgrind gave many complaints): the problem was that calloc() (in the Backtracker) wasn't allocating enough space for the type located at the resulting address.  Resolves bug #263.

Also, some debugging improvements.

13 years agofixed various bugs related to ambiguous parametric datatype constructors, parametric...
Andrew Reynolds [Fri, 3 Jun 2011 19:56:12 +0000 (19:56 +0000)]
fixed various bugs related to ambiguous parametric datatype constructors, parametric datatype versions of paper benchmarks are now working

13 years agodatatypes work
Morgan Deters [Fri, 3 Jun 2011 05:30:54 +0000 (05:30 +0000)]
datatypes work

13 years agominor fix to build system for system tests
Morgan Deters [Thu, 2 Jun 2011 22:17:56 +0000 (22:17 +0000)]
minor fix to build system for system tests

13 years agoadded (temporary) support for ensuring that all ambiguously typed constructor nodes...
Andrew Reynolds [Thu, 2 Jun 2011 15:23:16 +0000 (15:23 +0000)]
added (temporary) support for ensuring that all ambiguously typed constructor nodes created internally are given a type ascription

13 years agominor fix, and better output for type errors
Morgan Deters [Wed, 1 Jun 2011 01:13:21 +0000 (01:13 +0000)]
minor fix, and better output for type errors

13 years agotype ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]
Morgan Deters [Wed, 1 Jun 2011 00:49:37 +0000 (00:49 +0000)]
type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]

13 years agoThis commit contains the code for allowing arbitrary equalities in the theory of...
Tim King [Tue, 31 May 2011 01:06:16 +0000 (01:06 +0000)]
This commit contains the code for allowing arbitrary equalities in the theory of arithmetic.
* This code has been partially tested. (My testing situation is currently not so great.)  The code for testing not preregistering equalities can be compile time enabled by setting the boolean turnOffEqualityPreRegister. Don't be shocked by slowdowns or failures.  This does pass make regress as well as a fresh checkout does. (The Mac version has issues.)
* I need to disable the permanent row removal heuristic by default.  We need to discuss why this needs to happen.  We should probably detect pure QF_LRA/QF_RDL problems and enable this when this can safely be done.
* I have disabled the arithmetic rewrite equality flag.  This code needs to be added to the parser.
* For all of the above changes, I have annotated the code with the key word BREADCRUMB.
* I have renamed ArithUnatePropagator to ArithAtomDatabase.

13 years agofix unit test linking issue
Morgan Deters [Sat, 28 May 2011 06:44:07 +0000 (06:44 +0000)]
fix unit test linking issue

13 years agoinclude subversion information used for each build in the --show-config output and...
Morgan Deters [Sat, 28 May 2011 05:51:01 +0000 (05:51 +0000)]
include subversion information used for each build in the --show-config output and as a banner in --interactive mode; intended to resolve confusion in cases where you don't know where a CVC4 binary came from

13 years agoapply arithmetic static learner's miplibtrick in a consistent order (for easier repli...
Morgan Deters [Thu, 26 May 2011 05:04:34 +0000 (05:04 +0000)]
apply arithmetic static learner's miplibtrick in a consistent order (for easier replication of experiment)

13 years agofixes for "make dist" and "make doc", minor cleanups
Morgan Deters [Mon, 23 May 2011 23:15:25 +0000 (23:15 +0000)]
fixes for "make dist" and "make doc", minor cleanups

13 years agoMerge from arrays2 branch.
Morgan Deters [Mon, 23 May 2011 21:58:12 +0000 (21:58 +0000)]
Merge from arrays2 branch.

13 years agofix production-build compiler warning
Morgan Deters [Sat, 14 May 2011 19:51:41 +0000 (19:51 +0000)]
fix production-build compiler warning

13 years agore-add a removed Datatype constructor that was causing a unit test failure, so nightl...
Morgan Deters [Sat, 14 May 2011 03:38:18 +0000 (03:38 +0000)]
re-add a removed Datatype constructor that was causing a unit test failure, so nightlies go through tonight

13 years agoreverting node manager change from 1881; also part of parameterized datatypes review
Morgan Deters [Sat, 14 May 2011 00:17:20 +0000 (00:17 +0000)]
reverting node manager change from 1881; also part of parameterized datatypes review

13 years agoadd AscriptionType stuff to support nullary parameterized datatypes; also, review...
Morgan Deters [Sat, 14 May 2011 00:15:43 +0000 (00:15 +0000)]
add AscriptionType stuff to support nullary parameterized datatypes; also, review of Andy's earlier commit, with some minor code clean-up and documentation

13 years agoadded support for parametric datatypes, updated cvc parser to handle parametric datat...
Andrew Reynolds [Fri, 13 May 2011 22:02:52 +0000 (22:02 +0000)]
added support for parametric datatypes, updated cvc parser to handle parametric datatypes, type ascriptions are not implemented yet

13 years ago* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio
Morgan Deters [Fri, 13 May 2011 20:42:57 +0000 (20:42 +0000)]
* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio
  branch)
* add Theory::isSharedTermFact() -- it currently always returns false,
  pending theory combination work
* Add "unknown" cardinalities to Cardinality class
* Fix run_regression script to handle CRLF line terminators on Macs
  (where sed is non-GNU)
* Convert CRLF line terminators in datatypes regressions to LF

13 years agoDeleting dead code.
Tim King [Fri, 6 May 2011 21:23:38 +0000 (21:23 +0000)]
Deleting dead code.

13 years agoadded 10 benchmarks to regress/regress0/datatypes from paper
Andrew Reynolds [Fri, 6 May 2011 20:38:29 +0000 (20:38 +0000)]
added 10 benchmarks to regress/regress0/datatypes from paper

13 years agosignificant revisions/improvements to code for theory datatypes solver
Andrew Reynolds [Fri, 6 May 2011 20:17:57 +0000 (20:17 +0000)]
significant revisions/improvements to code for theory datatypes solver

13 years agoMerge from nonclausal-simplification-v2 branch:
Morgan Deters [Thu, 5 May 2011 22:23:50 +0000 (22:23 +0000)]
Merge from nonclausal-simplification-v2 branch:

* Preprocessing-time, non-clausal, Boolean simplification round to
  support "quasi-non-linear rewrites" as discussed at last few meetings.

* --simplification=none is the default for now, but we'll probably
  change that to --simplification=incremental.  --simplification=batch
  is also a possibility.  See --simplification=help for details.

* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.

13 years agoluby sequence generator; can use to plot MiniSat's restart sequence
Morgan Deters [Thu, 5 May 2011 21:34:52 +0000 (21:34 +0000)]
luby sequence generator; can use to plot MiniSat's restart sequence

13 years agoStronger support for zero-performance-penalty output, and fixes and
Morgan Deters [Wed, 4 May 2011 00:21:34 +0000 (00:21 +0000)]
Stronger support for zero-performance-penalty output, and fixes and
simplifications for the "muzzled" (i.e. competition) design, which had
been broken.  Addition of some new unit test bits to ensure that
nothing is ever called in muzzled builds, e.g. things like

  Warning() << expensiveFunction();

Also, fix some compiler warnings.

13 years agooutput fixes for performance
Morgan Deters [Tue, 3 May 2011 04:33:09 +0000 (04:33 +0000)]
output fixes for performance

13 years agominor updates to exp manager, fixed 32bit vs 64bit issues in transitive closure modul...
Andrew Reynolds [Mon, 2 May 2011 21:40:06 +0000 (21:40 +0000)]
minor updates to exp manager, fixed 32bit vs 64bit issues in transitive closure module, theory datatypes now uses transitive closure for cycle detection, bug 261 fixed

13 years agofix for configure
Morgan Deters [Mon, 2 May 2011 21:22:13 +0000 (21:22 +0000)]
fix for configure

13 years agoadding some previously-failing "bug" test cases for bitvectors
Morgan Deters [Mon, 2 May 2011 20:19:55 +0000 (20:19 +0000)]
adding some previously-failing "bug" test cases for bitvectors

13 years agoupdating bv regressions
Dejan Jovanović [Mon, 2 May 2011 19:46:06 +0000 (19:46 +0000)]
updating bv regressions

13 years agoparser fixes for bug 243
Dejan Jovanović [Mon, 2 May 2011 19:45:08 +0000 (19:45 +0000)]
parser fixes for bug 243

13 years agoupdates for bitvectors
Dejan Jovanović [Mon, 2 May 2011 19:09:11 +0000 (19:09 +0000)]
updates for bitvectors

13 years agomore minor fixes related to last few commits
Morgan Deters [Mon, 2 May 2011 16:06:19 +0000 (16:06 +0000)]
more minor fixes related to last few commits

13 years agoanother small fix
Morgan Deters [Mon, 2 May 2011 15:00:42 +0000 (15:00 +0000)]
another small fix

13 years agofix broken build; sorry, all!
Morgan Deters [Mon, 2 May 2011 14:55:24 +0000 (14:55 +0000)]
fix broken build; sorry, all!

13 years agofix a performance issue from last commit
Morgan Deters [Mon, 2 May 2011 05:31:00 +0000 (05:31 +0000)]
fix a performance issue from last commit

13 years agoMinor fixes to various parts of CVC4, including the removal of the uintptr_t construc...
Morgan Deters [Mon, 2 May 2011 05:04:36 +0000 (05:04 +0000)]
Minor fixes to various parts of CVC4, including the removal of the uintptr_t constructors for Type and Expr (which existed due to ANTLR limitations).  These issues are now handled (as a hack, due to said limitations) in the parser rather than the CVC4 core.

13 years agominor fixes, plus experimental readline support in InteractiveShell
Morgan Deters [Sun, 1 May 2011 22:32:32 +0000 (22:32 +0000)]
minor fixes, plus experimental readline support in InteractiveShell

13 years agorefactoring to datatypes theory, added working prototype for proof/explanation manager
Andrew Reynolds [Fri, 29 Apr 2011 22:03:59 +0000 (22:03 +0000)]
refactoring to datatypes theory, added working prototype for proof/explanation manager

13 years agomore fixes/improvements to datatypes theory and transitive closure
Andrew Reynolds [Thu, 28 Apr 2011 23:32:16 +0000 (23:32 +0000)]
more fixes/improvements to datatypes theory and transitive closure

13 years agocleaned up some of the hacks in the datatypes theory solver, working on using Transit...
Andrew Reynolds [Wed, 27 Apr 2011 00:49:02 +0000 (00:49 +0000)]
cleaned up some of the hacks in the datatypes theory solver, working on using Transitive Closure to detect cycles, added rewrite rule for disinguished ground terms

13 years agoMonday tasks:
Morgan Deters [Mon, 25 Apr 2011 23:44:00 +0000 (23:44 +0000)]
Monday tasks:

* new "well-foundedness" type property (like cardinality) specified in
  Theory kinds files; specifies well-foundedness and a ground term

* well-foundedness / finite checks in Datatypes now superseded by type
  system isFinite(), isWellFounded(), mkGroundTerm().

* new "RecursionBreaker" template class, a convenient class that keeps
  a "seen" trail without you having to pass it around (which is
  difficult in cases of mutual recursion) of the idea of passing
  around a "seen" trail

13 years agosmall unit test fix; was broken only in non-assertion, non-CLN builds
Morgan Deters [Mon, 25 Apr 2011 07:59:57 +0000 (07:59 +0000)]
small unit test fix; was broken only in non-assertion, non-CLN builds

13 years agoWeekend work. The main points:
Morgan Deters [Mon, 25 Apr 2011 06:56:14 +0000 (06:56 +0000)]
Weekend work.  The main points:

* Type::getCardinality() returns the cardinality for for all types.
  Theories give a cardinality in the their kinds file.  For
  cardinalities that depend on a type argument, a "cardinality
  computer" function is named in the kinds file, which takes a
  TypeNode and returns its cardinality.

* There's a bitmap for the set of "active theories" in the
  TheoryEngine.  Theories become "active" when a term that is owned by
  them, or whose type is owned by them, is pre-registered (run CVC4
  with --verbose to see theory activation).  Non-active theories don't
  get any calls for check() or propagate() or anything, and if we're
  running in single-theory mode, the shared term manager doesn't have
  to get involved.  This is really important for get() performance
  (which can only skimp on walking the entire sub-DAG only if the
  theory doesn't require it AND the shared term manager doesn't
  require it).

* TheoryEngine now does not call presolve(), registerTerm(),
  notifyRestart(), etc., on a Theory if that theory doesn't declare
  that property in its kinds file.  To avoid coding errors,
  mktheorytraits greps the theory header and gives warnings if:
  + the theory appears to declare one of the functions (check,
    propagate, etc.) that isn't listed among its kinds file properties
    (but probably should be)
  + the theory appears NOT to declare one of the functions listed in
    its kinds file properties

* some bounded token stream work

13 years agofix for parser/tests for ANTLR 3.2 (it was working fine on 3.3)
Morgan Deters [Sat, 23 Apr 2011 05:36:09 +0000 (05:36 +0000)]
fix for parser/tests for ANTLR 3.2 (it was working fine on 3.3)

13 years ago* reviewed BooleanSimplification, added documentation & unit test
Morgan Deters [Sat, 23 Apr 2011 05:15:56 +0000 (05:15 +0000)]
* reviewed BooleanSimplification, added documentation & unit test
* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work

13 years agomake run_regression script robust to DOS newlines :(
Morgan Deters [Sat, 23 Apr 2011 04:00:02 +0000 (04:00 +0000)]
make run_regression script robust to DOS newlines :(

13 years agoadded fixes for datatype theory solver to account for rewriting before finite/well...
Andrew Reynolds [Fri, 22 Apr 2011 22:24:29 +0000 (22:24 +0000)]
added fixes for datatype theory solver to account for rewriting before finite/well-founded check.

13 years agofix to last commit
Morgan Deters [Fri, 22 Apr 2011 22:02:46 +0000 (22:02 +0000)]
fix to last commit

13 years agoFixing SmtEngine::getValue() by adding a NodeManagerScope (thanks Tim for finding...
Morgan Deters [Fri, 22 Apr 2011 22:01:36 +0000 (22:01 +0000)]
Fixing SmtEngine::getValue() by adding a NodeManagerScope (thanks Tim for finding this)

13 years agonumerous bugfixes
Morgan Deters [Wed, 20 Apr 2011 11:19:50 +0000 (11:19 +0000)]
numerous bugfixes

13 years agoincorrect usage of C++ std::string caused a test to fail
Morgan Deters [Wed, 20 Apr 2011 08:07:07 +0000 (08:07 +0000)]
incorrect usage of C++ std::string caused a test to fail

13 years agoMinor mixed-bag commit. Expected performance impact negligible.
Morgan Deters [Wed, 20 Apr 2011 07:57:28 +0000 (07:57 +0000)]
Minor mixed-bag commit.  Expected performance impact negligible.

* Fixed hole in arrays typechecking.
* Fixed "make dist".
* Better ouroborous test, and some printer fixes.
* Continued cleanup in CVC parser, removed some warnings.
* Better output.

13 years agoTuesday end-of-day commit.
Morgan Deters [Wed, 20 Apr 2011 05:37:38 +0000 (05:37 +0000)]
Tuesday end-of-day commit.

Expected performance impact outside of datatypes/CVC parser is
negligible.

* CVC language LAMBDA, functional LET, type LET, precedence fixes,
  bitvectors, and arrays, with partial parsing support also for
  quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
    tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
  these are complicated because they have to be left unresolved
  at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
  (not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items

13 years agoRemoving dead code that came in on commit r1740.
Tim King [Mon, 18 Apr 2011 20:19:29 +0000 (20:19 +0000)]
Removing dead code that came in on commit r1740.

13 years agomore work on CVC language
Morgan Deters [Mon, 18 Apr 2011 19:08:11 +0000 (19:08 +0000)]
more work on CVC language

13 years agomostly CVC presentation language parsing and printing
Morgan Deters [Mon, 18 Apr 2011 18:05:39 +0000 (18:05 +0000)]
mostly CVC presentation language parsing and printing

13 years agoThis commit merges the branch arithmetic/propagation-again into trunk.
Tim King [Mon, 18 Apr 2011 16:48:52 +0000 (16:48 +0000)]
This commit merges the branch arithmetic/propagation-again into trunk.
- This adds code for bounds refinement, and conflict weakening.
- This adds util/boolean_simplification.h.
- This adds a propagation manager to theory of arithmetic.
- Propagation is disabled by default.
- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.

13 years agoPartial merge from datatypes-merge branch:
Morgan Deters [Mon, 18 Apr 2011 08:59:09 +0000 (08:59 +0000)]
Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.

13 years agoFixing output for EOF token in parser errors
Christopher L. Conway [Mon, 18 Apr 2011 03:10:55 +0000 (03:10 +0000)]
Fixing output for EOF token in parser errors

13 years agoalso a fix for a system test related to ParserBuilder
Morgan Deters [Sat, 16 Apr 2011 00:12:01 +0000 (00:12 +0000)]
also a fix for a system test related to ParserBuilder

13 years agounit test fixes for new NodeManager constructor (related to previous two trunk commits)
Morgan Deters [Sat, 16 Apr 2011 00:10:57 +0000 (00:10 +0000)]
unit test fixes for new NodeManager constructor (related to previous two trunk commits)

13 years agoparser/driver fixes for last commit
Morgan Deters [Fri, 15 Apr 2011 22:17:22 +0000 (22:17 +0000)]
parser/driver fixes for last commit

13 years agopartial merge from portfolio branch, adding conversions (library-internal-only of...
Morgan Deters [Fri, 15 Apr 2011 22:11:11 +0000 (22:11 +0000)]
partial merge from portfolio branch, adding conversions (library-internal-only of course) between Exprs and Nodes, Types and TypeNodes, ExprManagers and NodeManagers.

13 years agoreverting back the minisat code and adding a simpler one that shouldn't change the...
Dejan Jovanović [Thu, 14 Apr 2011 20:57:28 +0000 (20:57 +0000)]
reverting back the minisat code and adding a simpler one that shouldn't change the search

13 years agoThree things:
Morgan Deters [Thu, 14 Apr 2011 20:41:19 +0000 (20:41 +0000)]
Three things:
1. Infrastructure for unit T-conflicts added to SAT proxy
   (and also the theory output channel documentation);
   previously theories could not communicate unit T-conflicts
   with the SAT layer because that layer had an implicit
   assumption (not asserted) that the conflict nodes were an AND.
2. UF now pre-rewrites trivial equalities to "true".  These could
   conceivably occur in artificial benchmarks in this form:
     (let (?x BIG-HUGE-TERM) ... (= ?x ?x) ... )
3. The SMT-LIBv2 printer now properly prints Bool constants.

13 years agofixing an uninitialized literal variable
Dejan Jovanović [Thu, 14 Apr 2011 19:11:42 +0000 (19:11 +0000)]
fixing an uninitialized literal variable

13 years agoadding support for unit conflicts in minisat...
Dejan Jovanović [Wed, 13 Apr 2011 21:15:48 +0000 (21:15 +0000)]
adding support for unit conflicts in minisat...

13 years agofix compiler warning in non-replay builds
Morgan Deters [Wed, 13 Apr 2011 06:25:37 +0000 (06:25 +0000)]
fix compiler warning in non-replay builds

13 years agocache the LET rewriting (and defined-function expansion too)---it wasn't before,...
Morgan Deters [Wed, 13 Apr 2011 06:10:55 +0000 (06:10 +0000)]
cache the LET rewriting (and defined-function expansion too)---it wasn't before, leading to terrible slowdown on heavily-nested LETs (and defined functions)

13 years agoadd disequality token ("/=") and rules to CVC parser
Morgan Deters [Wed, 13 Apr 2011 05:27:42 +0000 (05:27 +0000)]
add disequality token ("/=") and rules to CVC parser

13 years agoanother small fix to "make dist" that can lead to a misconfigured tarball
Morgan Deters [Tue, 12 Apr 2011 18:45:44 +0000 (18:45 +0000)]
another small fix to "make dist" that can lead to a misconfigured tarball

13 years agoTransitive closure module is working
Clark Barrett [Mon, 11 Apr 2011 17:33:07 +0000 (17:33 +0000)]
Transitive closure module is working

13 years agofix "make dist" issues in makefiles
Morgan Deters [Mon, 11 Apr 2011 05:55:37 +0000 (05:55 +0000)]
fix "make dist" issues in makefiles

13 years agomerge from replay branch
Morgan Deters [Sun, 10 Apr 2011 00:44:20 +0000 (00:44 +0000)]
merge from replay branch

13 years agoAdd -lprofiler when --with-google-perftools is offered; also fix some newswire-raised...
Morgan Deters [Sun, 10 Apr 2011 00:14:49 +0000 (00:14 +0000)]
Add -lprofiler when --with-google-perftools is offered; also fix some newswire-raised documentation issues.

13 years agochanging the sat solver to assert propagated literals back to the theories
Dejan Jovanović [Sat, 9 Apr 2011 03:06:53 +0000 (03:06 +0000)]
changing the sat solver to assert propagated literals back to the theories

13 years agoAdded util class
Clark Barrett [Fri, 8 Apr 2011 13:22:18 +0000 (13:22 +0000)]
Added util class

13 years agoMade Valuation::getValue() and Valuation::getSatValue() const.
Tim King [Thu, 7 Apr 2011 19:28:25 +0000 (19:28 +0000)]
Made Valuation::getValue() and Valuation::getSatValue() const.

13 years agoMemory fix for congruence closure; affects many UF benchmarks, probably AX too.
Morgan Deters [Tue, 5 Apr 2011 18:31:38 +0000 (18:31 +0000)]
Memory fix for congruence closure; affects many UF benchmarks, probably AX too.

13 years agoAdded options for setting the random decision frequency and random seed for the sat...
Tim King [Tue, 5 Apr 2011 15:58:59 +0000 (15:58 +0000)]
Added options for setting the random decision frequency and random seed for the sat solver.  Also added command line options for setting both.

13 years agoMinor adjustments to the Registrar commit in 1644, documentation.
Morgan Deters [Tue, 5 Apr 2011 04:06:10 +0000 (04:06 +0000)]
Minor adjustments to the Registrar commit in 1644, documentation.

13 years agoMerging the satliteral-before-prereg branch into trunk. Theory preregistration is...
Tim King [Mon, 4 Apr 2011 20:42:23 +0000 (20:42 +0000)]
Merging the satliteral-before-prereg branch into trunk. Theory preregistration is now called during the conversion to cnf. This fixes bug 257.

13 years agoReverts previous commit r1636.
Tim King [Mon, 4 Apr 2011 20:18:11 +0000 (20:18 +0000)]
Reverts previous commit r1636.

13 years agoAdd documentation to Node and TNode (closes bug #201).
Morgan Deters [Mon, 4 Apr 2011 18:59:33 +0000 (18:59 +0000)]
Add documentation to Node and TNode (closes bug #201).
Also, only build doxygen documentation on stuff in src/,
not test/ or contrib/ or anywhere else.  Hopefully this
turns our 3000+ page user manual into something a little
more useful!

13 years agoDelayed the addition of unate propagation lemmas until propagation is called. The...
Tim King [Sat, 2 Apr 2011 21:05:47 +0000 (21:05 +0000)]
Delayed the addition of unate propagation lemmas until propagation is called.  The OutputChannel is now untouched by TheoryArith during preregistration.

13 years agowith --with-google-perftools, don't just take it on blind faith, require a successful...
Morgan Deters [Sat, 2 Apr 2011 05:43:24 +0000 (05:43 +0000)]
with --with-google-perftools, don't just take it on blind faith, require a successful link at configure time

13 years agominor fixes
Morgan Deters [Sat, 2 Apr 2011 04:24:17 +0000 (04:24 +0000)]
minor fixes

13 years agominor bugfixes (fixes broken dynamic-library build from last night)
Morgan Deters [Fri, 1 Apr 2011 21:35:50 +0000 (21:35 +0000)]
minor bugfixes (fixes broken dynamic-library build from last night)

13 years agodocumentation fix
Morgan Deters [Fri, 1 Apr 2011 01:49:09 +0000 (01:49 +0000)]
documentation fix

13 years agoThis commit is a merge from the "betterstats" branch, which:
Morgan Deters [Fri, 1 Apr 2011 00:56:42 +0000 (00:56 +0000)]
This commit is a merge from the "betterstats" branch, which:

* Makes Options an "omnipresent thread-local global" (like the notion
  of the "current NodeManager" was already).  Options::current() accesses
  this structure.
* Removes Options from constructors and data structures everywhere
  (this cleans up a lot of things).
* No longer uses StatisticsRegistry statically.  An instance of the
  registry is created and linked to a NodeManager.
* StatisticsRegistry::current() is similar to Options::current(), but
  the pointer is stowed in the NodeManager (rather than stored)
* The static functions of StatisticsRegistry have been left, for backward
  compatibility; they now use the "current" statistics registry.
* SmtEngine::getStatisticsRegistry() is a public accessor for the
  registry; this is needed by main() to reach in and get the registry,
  for flushing statistics at the end.

13 years agoFixes to Valuation.
Tim King [Thu, 31 Mar 2011 18:35:45 +0000 (18:35 +0000)]
Fixes to Valuation.

13 years agoimprove recent low-coverage complaints
Morgan Deters [Wed, 30 Mar 2011 21:53:15 +0000 (21:53 +0000)]
improve recent low-coverage complaints

13 years agoadding CVC4:: qualifier to the #define for debugging so that it can be used outside...
Dejan Jovanović [Wed, 30 Mar 2011 21:47:12 +0000 (21:47 +0000)]
adding CVC4:: qualifier to the #define for debugging so that it can be used outside of CVC4 namespace (like minisat)

13 years agoMoved the constructor for Options out of the header and into the cpp. For people...
Tim King [Wed, 30 Mar 2011 17:32:50 +0000 (17:32 +0000)]
Moved the constructor for Options out of the header and into the cpp. For people who fiddle with default values set by the Options constructor, this will require significantly less recompiling.

13 years agoAdded the command line flag --rewrite-arithmetic-equalities. This sets a static...
Tim King [Wed, 30 Mar 2011 15:07:02 +0000 (15:07 +0000)]
Added the command line flag --rewrite-arithmetic-equalities.  This sets a static flag in Options that the ArithRewriter uses to determine the equality rewriting policy.

13 years agoAdd Valuation::getSatValue() so that theories can access the current
Morgan Deters [Wed, 30 Mar 2011 03:59:05 +0000 (03:59 +0000)]
Add Valuation::getSatValue() so that theories can access the current
(propositional) assignment for theory atoms.

Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list.
This implementation leads to some compiler warnings in production builds,
but these will be corrected in coming days.  There appears to be a small
speedup in the parser as a result of this fix:

  http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5

Cleaned up a few CD Boolean attribute things.

Various small fixes to coding guidelines / test coverage.

This commit:
* Resolves bug 252 (tracing not disabled in production builds)
* Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())

13 years agoMerged the branch sparse-tableau into trunk.
Tim King [Wed, 30 Mar 2011 01:06:37 +0000 (01:06 +0000)]
Merged the branch sparse-tableau into trunk.

13 years agofixes to attribute-internals warnings on 64-bit; also some GCC function attribute...
Morgan Deters [Sun, 27 Mar 2011 19:02:02 +0000 (19:02 +0000)]
fixes to attribute-internals warnings on 64-bit; also some GCC function attribute cleanup; nothing major

13 years agofix for bug 253, was propagating an asserted literal
Dejan Jovanović [Sat, 26 Mar 2011 22:26:06 +0000 (22:26 +0000)]
fix for bug 253, was propagating an asserted literal
also fixing some compile warnings in attributes