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

13 years agofix typo
Morgan Deters [Sat, 26 Mar 2011 02:38:08 +0000 (02:38 +0000)]
fix typo

13 years agoThis is a merge from the "theoryfixes+cdattrhash" branch. The changes
Morgan Deters [Fri, 25 Mar 2011 05:32:31 +0000 (05:32 +0000)]
This is a merge from the "theoryfixes+cdattrhash" branch.  The changes
are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development).  Dejan has now given me the go-ahead
for a merge.

=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================

Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor.  The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead).  This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.

TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.

Specifically:

* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
  1. As described above.
  2. Theories now have const access to the fact queue through base
     class functions facts_begin() and facts_end(); useful for
     debugging.
* Added an "Asserted" attribute so that theories can check if something
  has been asserted or not (and therefore not propagate it).  However, this
  has been disabled for now, pending more data on the overhead of it, and
  pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
  that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
  regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
  attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived!  So far mainly infrastructure for having
  system tests, but there is a system test aimed at improving code
  coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
  conformant to CVC4 policy.

Tests have been performed to demonstrate that these changes have no or
negligible effect on performance.  In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).

13 years agoFix for a bug Andrew Reynolds found for iterators that affects empty CDList<> objects...
Morgan Deters [Fri, 25 Mar 2011 05:20:56 +0000 (05:20 +0000)]
Fix for a bug Andrew Reynolds found for iterators that affects empty CDList<> objects that allocate from ContextMemoryAllocator<>.  Iterators were broken in that begin() != end() for empty lists (again---only those that allocated space from ContextMemoryAllocator<>).  Added a unit test for this, too.  Thanks Andy!

13 years agoMerges the small changes on the queue-period branch into trunk. This branch importan...
Tim King [Tue, 22 Mar 2011 13:37:11 +0000 (13:37 +0000)]
Merges the small changes on the queue-period branch into trunk.  This branch importantly removes an unintentional line of code that had it pivoting more times than intended before rechecking the queue. Importantly, it does this without losing any examples with rewrite-equality enabled. This adds a parameter NUM_CHECKS which determines how many times the queue chould be checked during difference mode.  A value of 10 for NUM_CHECKS has been empirically determined to be good in practice. See jobs 1815, 1824, 1825, 1821, 1814.

13 years agoupdating debug output usage to eliviate impact of bug 252
Dejan Jovanović [Tue, 22 Mar 2011 02:11:09 +0000 (02:11 +0000)]
updating debug output usage to eliviate impact of bug 252

13 years agomore bugfixes, some basic propagation, and testcases to cover them
Dejan Jovanović [Mon, 21 Mar 2011 18:55:05 +0000 (18:55 +0000)]
more bugfixes, some basic propagation, and testcases to cover them

13 years agofixing a bug in the BV rewrite, off by one error when merging constants
Dejan Jovanović [Mon, 21 Mar 2011 17:43:22 +0000 (17:43 +0000)]
fixing a bug in the BV rewrite, off by one error when merging constants

13 years agoagain a typo
Dejan Jovanović [Sun, 20 Mar 2011 19:58:51 +0000 (19:58 +0000)]
again a typo

13 years agomore bugfixes for bitvectors
Dejan Jovanović [Sun, 20 Mar 2011 19:50:48 +0000 (19:50 +0000)]
more bugfixes for bitvectors

13 years agofixing the failure from last nigth, due to using a reference to an element in a growi...
Dejan Jovanović [Sun, 20 Mar 2011 16:31:19 +0000 (16:31 +0000)]
fixing the failure from last nigth, due to using a reference to an element in a growing vector

13 years agomissed one case
Dejan Jovanović [Sun, 20 Mar 2011 01:41:48 +0000 (01:41 +0000)]
missed one case

13 years agocommit for the version of bitvectors that passes all the unit tests
Dejan Jovanović [Sun, 20 Mar 2011 01:12:31 +0000 (01:12 +0000)]
commit for the version of bitvectors that passes all the unit tests

13 years agoMerges the pqueue-set branch into trunk. During VarOrder mode and Collection mode...
Tim King [Sat, 19 Mar 2011 22:59:39 +0000 (22:59 +0000)]
Merges the pqueue-set branch into trunk.  During VarOrder mode and Collection mode, the arithmetic priority queue is maintained as a set. Compare jobs 1781 and 1782 for the expected performance change.

13 years ago- The learned clauses from the miplib trick were being added twice. This was slowing...
Tim King [Fri, 18 Mar 2011 22:22:28 +0000 (22:22 +0000)]
- The learned clauses from the miplib trick were being added twice. This was slowing down the search. (The effect can be seen in the difference between jobs 1765 and 1755). This happened during commit -r1480 when adding the ArithStaticLearner.  This has been fixed.

13 years agoSwitched SimplexDecisionProcedure::d_delayedLemmas from a vector to a queue.
Tim King [Thu, 17 Mar 2011 21:28:50 +0000 (21:28 +0000)]
Switched SimplexDecisionProcedure::d_delayedLemmas from a vector to a queue.

13 years agoSimplexDecisionProcedure no longer takes an OutputChannel as a parameter.
Tim King [Thu, 17 Mar 2011 21:20:28 +0000 (21:20 +0000)]
SimplexDecisionProcedure no longer takes an OutputChannel as a parameter.

13 years ago- Removes arith_constants.h
Tim King [Thu, 17 Mar 2011 20:38:32 +0000 (20:38 +0000)]
- Removes arith_constants.h
- Adds ArithStaticLearner.  Consolidates and cleans up the code for static learning in arithmetic.  Static learning is now associated with a small amount of state between calls. This is used to track the data for the miplib trick.  The goal is to make this inference work without relying on the fact that all of the miplib problem is asserted under the same AND node.
- This commit contains miscellaneous other arithmetic cleanup.

13 years agoAdds debugging output to EngineOutputChannel::lemma.
Tim King [Thu, 17 Mar 2011 20:24:05 +0000 (20:24 +0000)]
Adds debugging output to EngineOutputChannel::lemma.

13 years agoFix for the bug introduced in 1477. The stuff that was added to CVC4ostream::operato...
Tim King [Thu, 17 Mar 2011 15:23:53 +0000 (15:23 +0000)]
Fix for the bug introduced in 1477.  The stuff that was added to CVC4ostream::operator<< should only be executed when d_os != NULL. This was the cause of the NULL pointer dereference in debug builds.

13 years agopush and pop manipulators for output stream so that one can indent the output
Dejan Jovanović [Thu, 17 Mar 2011 03:48:53 +0000 (03:48 +0000)]
push and pop manipulators for output stream so that one can indent the output
ueful for me, maybe someone else finds it useful also

13 years ago- Turns on the excluded middle assertions during the miplibTrick. If it is known...
Tim King [Wed, 16 Mar 2011 22:08:15 +0000 (22:08 +0000)]
- Turns on the excluded middle assertions during the miplibTrick. If it is known that x \in {c_i}, then x is not in the interval (c_{i}, c_{i+1}) (assuming the c_i's are sorted). (Compare jobs 1742 and 1739 for the expected performance change on trunk. Compare jobs 1740 and 1738 for the expected performance change with the rewrite-equality patch.)

13 years ago- Turns on the miplibTrick. This detects during the static learning phase a set...
Tim King [Wed, 16 Mar 2011 15:36:45 +0000 (15:36 +0000)]
- Turns on the miplibTrick.  This detects during the static learning phase a set of nodes that are asserted to the theory of the form (=> p_i (= x c_i)). If (or p_1 p_2 ...) is a tautology, then x \in {c_1, c_2, ...}. (This tautology check currently requires CUDD to be installed.)  Right now all this does is assert x \leq max{c_i} and x \geq min{c_i}. (Compare jobs 1728 to 1626 for how this affects the miplib examples.)

13 years agoreal fix for bug 245, previous one was faulty
Dejan Jovanović [Tue, 15 Mar 2011 22:08:46 +0000 (22:08 +0000)]
real fix for bug 245, previous one was faulty

13 years agosmall fixes for run_regression script to workaround bug in old mktemp, was causing...
Morgan Deters [Tue, 15 Mar 2011 21:06:47 +0000 (21:06 +0000)]
small fixes for run_regression script to workaround bug in old mktemp, was causing a hang in bug220.smt2

13 years agofix for bug 254, lemmas were propagating at lower levels, and the conflict clauses...
Dejan Jovanović [Tue, 15 Mar 2011 20:48:57 +0000 (20:48 +0000)]
fix for bug 254, lemmas were propagating at lower levels, and the conflict clauses asserting literal  would overwrite the propagated literal
let's see if i break the build again

13 years agoMerge from cudd branch. This mostly just adds support for linking
Morgan Deters [Tue, 15 Mar 2011 20:32:13 +0000 (20:32 +0000)]
Merge from cudd branch.  This mostly just adds support for linking
against cudd libraries, the propositional_query class (in util/),
which uses cudd if it's available (and otherwise answers UNKNOWN for
all queries), and the arith theory support for it (currently disabled
per Tim's request, so he can clean it up).

Other changes include:

* contrib/debug-keys - script to print all used keys under Debug(), Trace()
* test/regress/run_regression - minor fix (don't export a variable)
* configure.ac - replace a comment removed by dejan's google perf commit
* some minor copyright/documentation updates, and minor changes to source
  text to make 'clang --analyze' happy.

13 years agoadding support for google performance tools to the build sytem, it can be enabled...
Dejan Jovanović [Mon, 14 Mar 2011 22:14:47 +0000 (22:14 +0000)]
adding support for google performance tools to the build sytem, it can be enabled at configure with
--with-google-perftools

to use it on ubuntu, you need to install packages google-perftools and libgoogle-perftools0

to run the profiling of the heap, you can run it for example with

HEAPPROFILE=/tmp/profile ./builds/bin/cvc4 test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt

this will create some files  /tmp/profile* that you can then

to get the pdf of the profile you can then run

google-pprof --pdf ./builds/bin/cvc4 /tmp/profile.0001.heap > profile.pdf

or for other options check http://goog-perftools.sourceforge.net/doc/

13 years agochange to the run_regression script to better manage temporary files; hopefully this...
Morgan Deters [Mon, 14 Mar 2011 21:00:34 +0000 (21:00 +0000)]
change to the run_regression script to better manage temporary files; hopefully this will somewhat alleviate the problem with all the junk files in /tmp

13 years agoFix to bug 251 (non-spurious warnings in builds) by shifting metakind array by 1...
Morgan Deters [Mon, 14 Mar 2011 19:51:26 +0000 (19:51 +0000)]
Fix to bug 251 (non-spurious warnings in builds) by shifting metakind array by 1 to handle the UNDEFINED_KIND case.

13 years agoFix bug 246 (occasional buffer overflow related to varargs in assertion-failure strin...
Morgan Deters [Thu, 10 Mar 2011 21:05:13 +0000 (21:05 +0000)]
Fix bug 246 (occasional buffer overflow related to varargs in assertion-failure string construction) and addition of an assert_white unit test check for the issue

13 years agoITE removal in TheoryEngine was not properly handling PARAMETERIZED kinds. Fixed...
Morgan Deters [Thu, 10 Mar 2011 07:28:32 +0000 (07:28 +0000)]
ITE removal in TheoryEngine was not properly handling PARAMETERIZED kinds.  Fixed and added bug regression.  Thanks Andrew Reynolds for the bug report!

13 years agoClean up Theory base class as per code review bug #60; also fixes to CodeTimer statis...
Morgan Deters [Tue, 8 Mar 2011 21:43:45 +0000 (21:43 +0000)]
Clean up Theory base class as per code review bug #60; also fixes to CodeTimer statistic, and adding a CodeTimer to TheoryEngine::EngineOutputChannel::newFact() for investigation into (possible) slow or redundant theory registration.

13 years ago- Merges queue-interrogation branch into the trunk. This branch adds extra phases...
Tim King [Tue, 8 Mar 2011 01:46:31 +0000 (01:46 +0000)]
- Merges queue-interrogation branch into the trunk. This branch adds extra phases of looking for additional conflicts during and after the heuristic pivoting stage. (For the expected performance gain, comparing jobs 1676 and 1643 gives a rough idea.)

13 years agoMerges branches/arithmetic/tableau-reset into the trunk. The tableau is now heuristi...
Tim King [Mon, 7 Mar 2011 19:10:16 +0000 (19:10 +0000)]
Merges branches/arithmetic/tableau-reset into the trunk.  The tableau is now heuristically reset to its initial state during restarts.

13 years ago- Adds PermissiveBackArithVarSet. This is very similar to ArithVarSet. The differenc...
Tim King [Sat, 5 Mar 2011 23:10:41 +0000 (23:10 +0000)]
- Adds PermissiveBackArithVarSet.  This is very similar to ArithVarSet. The difference is that set.isMember(x) for an ArithVar x s.t. x > set.allocated() returns false for PermissiveBackArithVarSet and is an assertion failure for ArithVarSet.  This cuts down on the memory usage of the ColumnMatrix slightly.

13 years agoEnables the PreferenceFunction minBoundAndRowCount.
Tim King [Sat, 5 Mar 2011 19:30:06 +0000 (19:30 +0000)]
Enables the PreferenceFunction minBoundAndRowCount.

13 years ago- Adds "PreferenceFunction" to SimplexDecisionProcedure. A PreferenceFunction allows...
Tim King [Sat, 5 Mar 2011 17:33:01 +0000 (17:33 +0000)]
- Adds "PreferenceFunction" to SimplexDecisionProcedure.  A PreferenceFunction allows for specifying how to choose between two nonbasic variables for which should become basic during the selectSlack(...) function. This partially addresses a point brought up by Dejan during the Code Review.  (Unfortunately, function pointers are involved in the implementation. Because of this, I have had Morgan review this code before check-in.)

13 years ago- Made Rational::sgn() function const.
Tim King [Sat, 5 Mar 2011 16:59:13 +0000 (16:59 +0000)]
- Made Rational::sgn() function const.

13 years agoadding three features to CVC parser that drastically improve its support for the...
Morgan Deters [Sat, 5 Mar 2011 00:03:08 +0000 (00:03 +0000)]
adding three features to CVC parser that drastically improve its support for the language: LET now supported (but not "type-lets" yet), OPTION now supported, and ^ operator (exponentiation) supported for nonnegative integer exponents.  The latter simply expands to MULT, and of course fails assertions in arithmetic if a variable is raised to n >= 2.  Also other CVC parser clean-up.

13 years agofix for bug #244, "Segfault if file cannot be found and --stats is on"
Morgan Deters [Thu, 3 Mar 2011 18:35:17 +0000 (18:35 +0000)]
fix for bug #244, "Segfault if file cannot be found and --stats is on"

13 years ago- Creates a queue for lemmas discovered during the simplex procedure. Lemmas are...
Tim King [Thu, 3 Mar 2011 18:00:35 +0000 (18:00 +0000)]
- Creates a queue for lemmas discovered during the simplex procedure. Lemmas are sent to the sat solver during theory propagation. The lemmas currently come from additional conflicts that are discovered by findConflictOnTheQueue(...).

13 years agoresurrecting triple.h from r1023 (after which it was removed)
Morgan Deters [Thu, 3 Mar 2011 17:49:15 +0000 (17:49 +0000)]
resurrecting triple.h from r1023 (after which it was removed)

13 years agoMerged the tableau-copy branch into trunk. This adds a copy constructor and operator...
Tim King [Thu, 3 Mar 2011 16:34:48 +0000 (16:34 +0000)]
Merged the tableau-copy branch into trunk. This adds a copy constructor and operator=(...) to Tableau.

13 years agofixing a type that caused the segfaults in the regressions
Dejan Jovanović [Thu, 3 Mar 2011 14:04:38 +0000 (14:04 +0000)]
fixing a type that caused the segfaults in the regressions