cvc5.git
11 years agoadded several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExtend...
lianah [Tue, 30 Apr 2013 17:42:50 +0000 (13:42 -0400)]
added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExtend) and bvurem lemma

11 years agoadded bvule, bvsle operator elimination rulesl; added bvurem lemma generation
lianah [Thu, 25 Apr 2013 22:43:12 +0000 (18:43 -0400)]
added bvule, bvsle operator elimination rulesl; added bvurem lemma generation

11 years agoadded some bv rewrite rules
lianah [Sun, 21 Apr 2013 23:00:09 +0000 (19:00 -0400)]
added some bv rewrite rules

11 years agoinnd examples are solved fast, but destruction assertion fail
lianah [Wed, 17 Apr 2013 19:34:16 +0000 (15:34 -0400)]
innd examples are solved fast, but destruction assertion fail

11 years agofixed compile error
Liana Hadarean [Tue, 16 Apr 2013 15:17:36 +0000 (11:17 -0400)]
fixed compile error

11 years agouncompiling new bv to bool lifting
lianah [Tue, 16 Apr 2013 14:57:04 +0000 (10:57 -0400)]
uncompiling new bv to bool lifting

11 years agofinished implementing bv to bool lifting and added --bv-to-bool option
lianah [Fri, 12 Apr 2013 20:15:30 +0000 (16:15 -0400)]
finished implementing bv to bool lifting and added --bv-to-bool option

11 years agomore work on boolean lifting
Liana Hadarean [Wed, 10 Apr 2013 04:03:02 +0000 (00:03 -0400)]
more work on boolean lifting

11 years agostarted work on bv1 to boolean lifting
lianah [Wed, 10 Apr 2013 00:30:06 +0000 (20:30 -0400)]
started work on bv1 to boolean lifting

11 years agoadded support for dumping the SAT problem the sat solver is working on
lianah [Mon, 8 Apr 2013 19:31:08 +0000 (15:31 -0400)]
added support for dumping the SAT problem the sat solver is working on

11 years agoAdd option in quantifiers for clause splitting
Andrew Reynolds [Tue, 30 Apr 2013 17:56:17 +0000 (12:56 -0500)]
Add option in quantifiers for clause splitting

11 years agoadd decision_attributes.h for make dist
Kshitij Bansal [Tue, 30 Apr 2013 14:10:38 +0000 (10:10 -0400)]
add decision_attributes.h for make dist

11 years agoSome fixes for GCC 4.2, and for Java on Mac
Morgan Deters [Mon, 29 Apr 2013 22:03:28 +0000 (18:03 -0400)]
Some fixes for GCC 4.2, and for Java on Mac

11 years agoMerge pull request #9 from kbansal/master
Kshitij Bansal [Mon, 29 Apr 2013 19:27:04 +0000 (12:27 -0700)]
Merge pull request #9 from kbansal/master

 Merge experimental decisionweight branch

11 years agoFixes to FCSimplex for some versions of compilers
Morgan Deters [Mon, 29 Apr 2013 14:50:43 +0000 (10:50 -0400)]
Fixes to FCSimplex for some versions of compilers

11 years agoFixing the failure for make distcheck.
Tim King [Sun, 28 Apr 2013 22:15:20 +0000 (18:15 -0400)]
Fixing the failure for make distcheck.

11 years agoMerge experimental decisionweight branch
Kshitij Bansal [Fri, 26 Apr 2013 22:02:02 +0000 (18:02 -0400)]
Merge experimental decisionweight branch

None of these are enabled by default, so any performance impact
counts as a bug

Options added are:

--decision-threshold=N :default 0
+ ignore all nodes greater than threshold in first attempt to pick decision

--decision-use-weight bool :default false
+ use the weight nodes (locally, by looking at children) to direct recursive search

--decision-random-weight=N int :default 0
+ assign random weights to nodes between 0 and N-1 (0: disable)

--decision-weight-internal=HOW
+ computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving)

Squashed commit of the following:

commit 0dbae066c19abde37092517b50f23255398539db
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Fri Apr 26 16:42:36 2013 -0400

    contentless cleanup

commit 62bb99b33deceb803ba5afc563fd322b4b5d1b7e
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Tue Apr 16 21:43:55 2013 -0400

    bugfixes in usr1 auto weight computation

commit 9f039cba805bfd722466734920e758d48ae3b23e
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Fri Mar 29 15:01:33 2013 -0400

    DECISION_WEIGHT_INTERNAL_USR1

commit 744e16d514594e5f1c69b36473b03cf501d9b9d1
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Mar 27 11:05:43 2013 -0400

    split theory and decision requests

commit f379d8a821df31c74b42a7722e891abc5c944f16
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Mar 27 09:51:58 2013 -0400

    fix potential bug with threshold

commit 3dcb45eb5ee648d3edbeddf76b838076afea3d12
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Feb 27 20:29:38 2013 -0500

    stat bv::weightComputationTimer

commit 2ab97d063e221357d2bb017af4589105777fd5a3
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Sat Feb 23 17:02:43 2013 -0500

    decision: option to auto compute weight of boolean structure

commit 0a8c29e699ad96d5f73bc14d31ad9254f6711ae8
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Sat Feb 23 14:53:50 2013 -0500

    decision: fix design to do partial explorations

    * make findSplitterRec and all related helper functions' return
      type trivalued, to be able to distinguish between
      "partial exploration" vs "done exploration but found nothing"

    * keep additional data structure to remember to what extent the
      partial exploration has been completed so not to repeat it. we
      can use this to make multiple passes on formula with arbritrary
      order of thresholds for exploration

commit 0815991fc1b0f1d63f0e8124d4672d782e89d671
Author: lianah <lianahady@gmail.com>
Date:   Fri Feb 22 17:55:40 2013 -0500

    added simple node weight computation for bv.

commit e4c507e2e2fdc8794fd04c31093660a80c7f44c3
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Feb 20 02:35:21 2013 -0500

    --decision-use-weight, --decision-random-weight=N

commit 0624177d66d6ed2b3cc7fdb13df775990cfe50c2
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Tue Feb 19 23:36:49 2013 -0500

    decisionThreshold option

commit ac3579a52e452e3118ce116ff1823d6c6885544b
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Tue Feb 19 20:22:51 2013 -0500

    DecisionWeightAttr

11 years agoFCSimplex branch merge
Tim King [Fri, 26 Apr 2013 21:10:21 +0000 (17:10 -0400)]
FCSimplex branch merge

11 years agoAdd ability to run different regression levels with "make check"
Morgan Deters [Thu, 25 Apr 2013 19:43:16 +0000 (15:43 -0400)]
Add ability to run different regression levels with "make check"

11 years agoTheory "alternates" support
Morgan Deters [Wed, 24 Apr 2013 03:03:37 +0000 (23:03 -0400)]
Theory "alternates" support

* This is a feature that Dejan and I want for the upcoming tutorial.
  It allows rapid prototyping of new decision procedure implementations
  (which we may choose to demonstrate), and a new --use-theory command-line
  option to select from different available implementations.  It has no
  affect on the current set of theories, as no "alternates" are defined.

* Also update the new-theory script, which was broken and incomplete.

11 years agoadd bit0 and bit1 constants to smt-lib v1 parser
Morgan Deters [Mon, 22 Apr 2013 13:49:46 +0000 (09:49 -0400)]
add bit0 and bit1 constants to smt-lib v1 parser

11 years agomaking sure sat context is zero when user context is popped to 0 in SmtEngine destructor
lianah [Thu, 18 Apr 2013 23:03:32 +0000 (19:03 -0400)]
making sure sat context is zero when user context is popped to 0 in SmtEngine destructor

11 years agofixing destruction order in SmtEngine
lianah [Thu, 18 Apr 2013 21:02:22 +0000 (17:02 -0400)]
fixing destruction order in SmtEngine

11 years agobool flatten: node num_children workaround
Kshitij Bansal [Wed, 17 Apr 2013 20:27:45 +0000 (16:27 -0400)]
bool flatten: node num_children workaround

11 years agoboolean flatten: bug fix in dfs search
Kshitij Bansal [Wed, 17 Apr 2013 17:30:41 +0000 (13:30 -0400)]
boolean flatten: bug fix in dfs search

(this is not intended to (and doesn't) address the issue with
NodeBuilder limit)

11 years agoboolean flatten rewrite: dont re-rewrite
Kshitij Bansal [Wed, 17 Apr 2013 00:55:47 +0000 (20:55 -0400)]
boolean flatten rewrite: dont re-rewrite

11 years agogeneralize to handle and
Kshitij Bansal [Wed, 17 Apr 2013 00:49:25 +0000 (20:49 -0400)]
generalize to handle and

11 years agoflatten or nodes
Kshitij Bansal [Tue, 16 Apr 2013 23:26:28 +0000 (19:26 -0400)]
flatten or nodes

11 years agoImproved speed of no redundant lemma assertion by using hash set
Clark Barrett [Thu, 11 Apr 2013 16:47:47 +0000 (12:47 -0400)]
Improved speed of no redundant lemma assertion by using hash set

11 years agoFixes for getModelVal in bv theory
Clark Barrett [Thu, 11 Apr 2013 15:50:41 +0000 (11:50 -0400)]
Fixes for getModelVal in bv theory

11 years agoAdded check for infinite lemma loop
Clark Barrett [Thu, 11 Apr 2013 04:31:22 +0000 (00:31 -0400)]
Added check for infinite lemma loop

11 years agofixed getModelValue to only query the value of leaves and evaluate more complex bv...
lianah [Thu, 11 Apr 2013 01:40:37 +0000 (21:40 -0400)]
fixed getModelValue to only query the value of leaves and evaluate more complex bv terms

11 years agoChange TPTP parser to not use the STRING type; this necessary to repurpose strings...
Morgan Deters [Tue, 9 Apr 2013 20:29:59 +0000 (16:29 -0400)]
Change TPTP parser to not use the STRING type; this necessary to repurpose strings for the upcoming string theory

11 years agoFix unit test (compile error) for new SatSolver interface
Morgan Deters [Fri, 5 Apr 2013 20:35:42 +0000 (16:35 -0400)]
Fix unit test (compile error) for new SatSolver interface

11 years ago* changing the bitblast-eager to bitblast on pre-register
Dejan Jovanović [Wed, 3 Apr 2013 21:55:58 +0000 (17:55 -0400)]
* changing the bitblast-eager to bitblast on pre-register
* the newVar interface of the sat solver now changed to include (isTheoryLiteral, preRegister, canEliminate)
* when bitblast-eager all bv atoms are (theory=false, prereg = true, canelim = true)
* bitblast-eager implies decision=internal

11 years agoPrerelease versioning for master.
Morgan Deters [Wed, 3 Apr 2013 18:37:54 +0000 (14:37 -0400)]
Prerelease versioning for master.

11 years agoPre-release versioning
Morgan Deters [Wed, 3 Apr 2013 18:36:22 +0000 (14:36 -0400)]
Pre-release versioning

11 years agoCutting release 1.1.
Morgan Deters [Wed, 3 Apr 2013 18:19:41 +0000 (14:19 -0400)]
Cutting release 1.1.

11 years agoSome final minor changes before cutting 1.1.
Morgan Deters [Wed, 3 Apr 2013 17:08:00 +0000 (13:08 -0400)]
Some final minor changes before cutting 1.1.

* update documentation
* update the cut-release script
* spelling/wording updates
* add a (previously-failing) fuzzer regression

11 years agoupdated NEWS to include inequality solver
Liana Hadarean [Wed, 3 Apr 2013 16:53:15 +0000 (12:53 -0400)]
updated NEWS to include inequality solver

11 years agoabort quantifiers check if master equality engine is inconsistent.
Andrew Reynolds [Wed, 3 Apr 2013 07:09:17 +0000 (02:09 -0500)]
abort quantifiers check if master equality engine is inconsistent.

11 years agoMaking arithmetic model reversion on unsat checks an option.
Tim King [Tue, 2 Apr 2013 18:51:06 +0000 (14:51 -0400)]
Making arithmetic model reversion on unsat checks an option.

11 years agoRegenerated copyrights: canonicalized names, no emails
Morgan Deters [Tue, 2 Apr 2013 18:31:53 +0000 (14:31 -0400)]
Regenerated copyrights: canonicalized names, no emails

11 years agoRemove old README file from rewrite-rules left over from new-theory script long ago
Morgan Deters [Tue, 2 Apr 2013 17:59:58 +0000 (13:59 -0400)]
Remove old README file from rewrite-rules left over from new-theory script long ago

11 years agoFix get-authors script to not extract email addresses, canonicalize names, add .mailmap
Morgan Deters [Tue, 2 Apr 2013 17:34:55 +0000 (13:34 -0400)]
Fix get-authors script to not extract email addresses, canonicalize names, add .mailmap

11 years agoOne final fix to "make submission" rule
Morgan Deters [Tue, 2 Apr 2013 14:44:24 +0000 (10:44 -0400)]
One final fix to "make submission" rule

11 years agoupdate copyrights
Morgan Deters [Tue, 2 Apr 2013 03:32:39 +0000 (23:32 -0400)]
update copyrights

11 years agoAdjust release Makefile rules, new run script
Morgan Deters [Tue, 2 Apr 2013 03:26:46 +0000 (23:26 -0400)]
Adjust release Makefile rules, new run script

11 years agoFix regression error by turning off model-based solver when models are on
Clark Barrett [Tue, 2 Apr 2013 03:06:13 +0000 (23:06 -0400)]
Fix regression error by turning off model-based solver when models are on
(ironic, yes, but model-based solver doesn't yet produce models)

11 years agoTurning on model based array solver for QF_AX
Clark Barrett [Tue, 2 Apr 2013 02:38:52 +0000 (22:38 -0400)]
Turning on model based array solver for QF_AX

11 years agoMade eager lemmas an option, enabled for QF_AX
Clark Barrett [Tue, 2 Apr 2013 02:27:17 +0000 (22:27 -0400)]
Made eager lemmas an option, enabled for QF_AX

11 years agoDisabling eager array index splitting for QF_AX
Clark Barrett [Tue, 2 Apr 2013 00:06:09 +0000 (20:06 -0400)]
Disabling eager array index splitting for QF_AX

11 years agoFixes for two bugs:
Morgan Deters [Mon, 1 Apr 2013 21:34:27 +0000 (17:34 -0400)]
Fixes for two bugs:

* one that Tim found in model generation for records containing Booleans
* another that the fuzzer found in quantifiers + check-models

Test cases enabled/added for both.

11 years agoCleaning up the demand restart code.
Tim King [Mon, 1 Apr 2013 23:42:43 +0000 (19:42 -0400)]
Cleaning up the demand restart code.

11 years agoAdding a restart test strategy to integers.
Tim King [Mon, 1 Apr 2013 15:26:57 +0000 (11:26 -0400)]
Adding a restart test strategy to integers.

11 years agoAdding demand restart.
Tim King [Mon, 1 Apr 2013 15:26:14 +0000 (11:26 -0400)]
Adding demand restart.

11 years agoAdding tests for the previous commit.
Tim King [Mon, 1 Apr 2013 21:26:13 +0000 (17:26 -0400)]
Adding tests for the previous commit.

11 years agoMerging some cleanup work:
Morgan Deters [Wed, 20 Mar 2013 22:16:26 +0000 (18:16 -0400)]
Merging some cleanup work:

* Comment cleanup
* Spelling fixes
* Fix warnings
* Documentation updates
* References in docs to cryptominisat removed
* Unneeded scope resolutions removed
* Old, unused regression removed

11 years agoFix for iff terms over equalities between the same term and differing constants.
Tim King [Mon, 1 Apr 2013 19:39:25 +0000 (15:39 -0400)]
Fix for iff terms over equalities between the same term and differing constants.

11 years agoFix bug 491 and related issues with checkModel() and quantifiers. Enabling previousl...
Morgan Deters [Thu, 7 Feb 2013 23:13:01 +0000 (18:13 -0500)]
Fix bug 491 and related issues with checkModel() and quantifiers.  Enabling previously-failing testcase.

11 years agofixed TheoryBool rewriter bug
lianah [Mon, 1 Apr 2013 19:23:46 +0000 (15:23 -0400)]
fixed TheoryBool rewriter bug

11 years agofixed bug 502; now the core bv solver only gives the model for variables and shared...
lianah [Mon, 1 Apr 2013 18:04:58 +0000 (14:04 -0400)]
fixed bug 502; now the core bv solver only gives the model for variables and shared terms.

11 years agochanged option to run inequality solver by default
Liana Hadarean [Sun, 31 Mar 2013 03:47:03 +0000 (23:47 -0400)]
changed option to run inequality solver by default

11 years agoDisabling eager array index splitting for QF_AUFLIA
Clark Barrett [Sun, 31 Mar 2013 00:27:37 +0000 (20:27 -0400)]
Disabling eager array index splitting for QF_AUFLIA
Minor changes to model-based array solver

11 years agodo simple ite rewriting within quantifiers
Andrew Reynolds [Sat, 30 Mar 2013 22:29:34 +0000 (17:29 -0500)]
do simple ite rewriting within quantifiers

11 years agomake Boolean term conversion partially non-recursive (resolves bug 501)
Morgan Deters [Fri, 29 Mar 2013 20:50:13 +0000 (16:50 -0400)]
make Boolean term conversion partially non-recursive (resolves bug 501)

11 years agoMerge branch 'master' of github.com:CVC4/CVC4
Dejan Jovanović [Fri, 29 Mar 2013 14:57:50 +0000 (10:57 -0400)]
Merge branch 'master' of github.com:CVC4/CVC4

11 years agoremoving cryptominisat since we're not using it
Dejan Jovanović [Fri, 29 Mar 2013 14:57:22 +0000 (10:57 -0400)]
removing cryptominisat since we're not using it

11 years agofix memory corruption in arrays destructor
Morgan Deters [Thu, 28 Mar 2013 16:37:37 +0000 (12:37 -0400)]
fix memory corruption in arrays destructor

11 years agosome Java bindings fixes (fixes Debian build problems)
Morgan Deters [Thu, 28 Mar 2013 03:42:13 +0000 (23:42 -0400)]
some Java bindings fixes (fixes Debian build problems)

11 years agoFixed a warning, made eager-index default to true (better for QF_AUFBV)
Clark Barrett [Thu, 28 Mar 2013 03:02:29 +0000 (23:02 -0400)]
Fixed a warning, made eager-index default to true (better for QF_AUFBV)

11 years agoFixed bug in arrays
Clark Barrett [Thu, 28 Mar 2013 02:43:18 +0000 (22:43 -0400)]
Fixed bug in arrays

11 years agoAdded assertion
Clark Barrett [Thu, 28 Mar 2013 00:34:18 +0000 (20:34 -0400)]
Added assertion

11 years agoUpdates to model-based array solver
Clark Barrett [Wed, 27 Mar 2013 20:38:41 +0000 (16:38 -0400)]
Updates to model-based array solver
Minor fixes to bv and theory_engine

11 years agoNew model-based array procedure
Clark Barrett [Wed, 27 Mar 2013 00:12:47 +0000 (20:12 -0400)]
New model-based array procedure

11 years agoreverted the core solver to do static slicing, added option --bv-core-solver
lianah [Wed, 27 Mar 2013 21:48:39 +0000 (17:48 -0400)]
reverted the core solver to do static slicing, added option --bv-core-solver

11 years agofixed inequality checkDisequalities inefficiency
lianah [Wed, 27 Mar 2013 19:10:57 +0000 (15:10 -0400)]
fixed inequality checkDisequalities inefficiency

11 years agoMerge branch 'master' into bv-core
lianah [Wed, 27 Mar 2013 18:07:59 +0000 (14:07 -0400)]
Merge branch 'master' into bv-core

11 years agofixed some model stuff
lianah [Wed, 27 Mar 2013 18:05:49 +0000 (14:05 -0400)]
fixed some model stuff

11 years agofixed model generation bug; commented out attempt at inequality propagation
lianah [Wed, 27 Mar 2013 04:29:18 +0000 (00:29 -0400)]
fixed  model generation bug; commented out attempt at inequality propagation

11 years agoinequality solver now only splits on disequalities when complete
lianah [Wed, 27 Mar 2013 03:34:25 +0000 (23:34 -0400)]
inequality solver now only splits on disequalities when complete

11 years agoadded model generation for bv subtheories and bv-inequality solver option
lianah [Wed, 27 Mar 2013 02:14:24 +0000 (22:14 -0400)]
added model generation for bv subtheories and bv-inequality solver option

11 years agoFixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac
Morgan Deters [Tue, 26 Mar 2013 21:58:39 +0000 (17:58 -0400)]
Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac

11 years agoMake --incremental the default when running interactively
Morgan Deters [Tue, 26 Mar 2013 21:58:33 +0000 (17:58 -0400)]
Make --incremental the default when running interactively

11 years agocore theory currently disabled
lianah [Tue, 26 Mar 2013 20:55:29 +0000 (16:55 -0400)]
core theory currently disabled

11 years agogetModelValue implementation in bitvectors
Dejan Jovanović [Tue, 26 Mar 2013 20:52:21 +0000 (16:52 -0400)]
getModelValue implementation in bitvectors

11 years agoadding
Dejan Jovanović [Tue, 26 Mar 2013 20:47:47 +0000 (16:47 -0400)]
adding
* getModelValue to valuation
* getModelValue to theory engine
* getModelValue to theory
implemented getModelValue in bitvector

the purpose of getModelValue is to ask for a concrete value of a shared term

11 years agoMerge branch 'master' of git@github.com:CVC4/CVC4.git
Dejan Jovanović [Tue, 26 Mar 2013 20:17:40 +0000 (16:17 -0400)]
Merge branch 'master' of git@github.com:CVC4/CVC4.git

11 years agomoving bv before arrays
Dejan Jovanović [Tue, 26 Mar 2013 20:17:27 +0000 (16:17 -0400)]
moving bv before arrays

11 years agofixed inequality bugs due to improper explanation
lianah [Tue, 26 Mar 2013 19:36:47 +0000 (15:36 -0400)]
fixed inequality bugs due to improper explanation

11 years agocleaned up the bv subtheory interface; added check for inequality theory completeness
lianah [Tue, 26 Mar 2013 00:37:31 +0000 (20:37 -0400)]
cleaned up the bv subtheory interface; added check for inequality theory completeness

11 years agojava input stream adapters working
Morgan Deters [Fri, 1 Mar 2013 23:31:10 +0000 (18:31 -0500)]
java input stream adapters working

11 years agogetEqualityStatus now also queries the inequality solver
lianah [Mon, 25 Mar 2013 22:24:29 +0000 (18:24 -0400)]
getEqualityStatus now also queries the inequality solver

11 years agoFix for SCM detection
Morgan Deters [Mon, 25 Mar 2013 22:14:37 +0000 (18:14 -0400)]
Fix for SCM detection

11 years agoMerge pull request #7 from kbansal/portfolio
Kshitij Bansal [Mon, 25 Mar 2013 21:16:31 +0000 (14:16 -0700)]
Merge pull request #7 from kbansal/portfolio

finish removal of separateOutput

11 years agofinish removal of separateOutput
Kshitij Bansal [Mon, 25 Mar 2013 21:15:11 +0000 (17:15 -0400)]
finish removal of separateOutput

11 years agoadded support for disequalities in the inequality solver
Liana Hadarean [Mon, 25 Mar 2013 03:38:33 +0000 (23:38 -0400)]
added support for disequalities in the inequality solver

11 years agoincremental inequality solver implemented
lianah [Sun, 24 Mar 2013 22:50:39 +0000 (18:50 -0400)]
incremental inequality solver implemented

11 years agoFix bug in portfolio executor output; fixes nightly portfolio-checking runs.
Morgan Deters [Sun, 24 Mar 2013 01:38:55 +0000 (21:38 -0400)]
Fix bug in portfolio executor output; fixes nightly portfolio-checking runs.

11 years agonon-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)
lianah [Sat, 23 Mar 2013 21:19:21 +0000 (17:19 -0400)]
non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)