diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-11 14:28:06 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-11 14:28:06 -0700 |
commit | a2dd85d1042b71cbc9fbdc4bd54b08e5d96e6b4c (patch) | |
tree | 4fdb6f6c6f3e8bbf14b6955571df35134c4b7e5a | |
parent | 33453c7c9fb917cad471592da31bd9f39c6e14b7 (diff) |
Fallbackeval
-rw-r--r-- | src/theory/evaluator.cpp | 7 | ||||
-rw-r--r-- | src/theory/evaluator.h | 8 |
2 files changed, 11 insertions, 4 deletions
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index b50b811bf..1d5b56bd4 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -199,8 +199,11 @@ Node Evaluator::eval(TNode n, } default: - std::cout << "Not supported: " << currNodeVal << std::endl; - std::exit(1); + { + Debug("evaluator") << "Kind " << currNodeVal.getKind() + << " not supported" << std::endl; + d_results[currNode] = Result(); + } } } } diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index 35ba2b3d9..17aeb4381 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -93,9 +93,13 @@ struct Result switch (d_tag) { case Result::BITVECTOR: return nm->mkConst(d_bv); + case Result::BOOL: return nm->mkConst(d_bool); default: - std::cout << "Not supported:( " << d_tag << std::endl; - std::exit(1); + { + Debug("evaluator") << "Missing conversion from " << d_tag << " to node" + << std::endl; + return Node(); + } } return Node(); |