diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
| commit | 3cbb76ef86a769cfe3dac5976a14e1bc43c42ca6 (patch) | |
| tree | e08efdc63abd663de4f5750db9326b69c79829e5 /src/expr/node_manager.h | |
| parent | 3a7aafccadbfa1543c435b7dfe4f53116224a11f (diff) | |
Interruption, time-out, and deterministic time-out ("resource-out") features.
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.
Also implemented TheoryEngine::properPropagation().
Other minor things.
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 6adcb62a9..84ed78662 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1191,7 +1191,7 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, TypeNode child2, TypeNode child3) { - return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();; + return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode(); } // N-ary version for types |