diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-23 00:45:57 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-23 00:45:57 +0000 |
| commit | 18f710cbfb5ce1ea13c8e929445abc211c732a81 (patch) | |
| tree | 69e4517ad67d6afd82c4b48a886e828ed84070f1 /src/theory/arith/arith_static_learner.cpp | |
| parent | 9039185001b789eadd8b20149455fe778a80fb69 (diff) | |
Implement changes from yesterday morning's meeting (10/21/2011):
* OutputChannel::lemma() now returns an unsigned int. This facility isn't functional yet, but the signature is there. For now, it always returns the current user level (which is "correct" from the interface point of view, but not what we want).
* Pseudobooleans disabled. This should fix some quantifier benchmarks Andy's been working with on the quantifiers2 branch.
* --limit / --time-limit options renamed --rlimit and --tlimit.
There may be slowdown from disabling pseudobooleans.
Diffstat (limited to 'src/theory/arith/arith_static_learner.cpp')
| -rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index a5fa428c6..d4d495486 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -242,6 +242,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet void ArithStaticLearner::replaceWithPseudoboolean(TNode var) { AssertArgument(var.getMetaKind() == kind::metakind::VARIABLE, var); + // [MGD 10/21/2011] disable pseudobooleans for now (as discussed in today's meeting) + /* TypeNode pbType = NodeManager::currentNM()->pseudobooleanType(); Node pbVar = NodeManager::currentNM()->mkVar(string("PB[") + var.toString() + ']', pbType); d_pbSubstitutions.addSubstitution(var, pbVar); @@ -250,6 +252,7 @@ void ArithStaticLearner::replaceWithPseudoboolean(TNode var) { Expr::printtypes::Scope pts(Debug("pb"), true); Debug("pb") << "will replace " << var << " with " << pbVar << endl; } + */ } void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ |