summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt1
-rw-r--r--src/theory/arrays/theory_arrays_type_rules.cpp3
-rw-r--r--src/theory/booleans/theory_bool_type_rules.cpp76
-rw-r--r--src/theory/booleans/theory_bool_type_rules.h62
4 files changed, 93 insertions, 49 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 95fa90fe3..c03c2d591 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -498,6 +498,7 @@ libcvc5_add_sources(
theory/booleans/theory_bool.h
theory/booleans/theory_bool_rewriter.cpp
theory/booleans/theory_bool_rewriter.h
+ theory/booleans/theory_bool_type_rules.cpp
theory/booleans/theory_bool_type_rules.h
theory/booleans/type_enumerator.h
theory/builtin/proof_checker.cpp
diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp
index e0c27419f..04a2f1a74 100644
--- a/src/theory/arrays/theory_arrays_type_rules.cpp
+++ b/src/theory/arrays/theory_arrays_type_rules.cpp
@@ -15,7 +15,8 @@
#include "theory/arrays/theory_arrays_type_rules.h"
-#include "theory/arrays/theory_arrays_rewriter.h" // for array-constant attributes
+// for array-constant attributes
+#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/type_enumerator.h"
namespace cvc5 {
diff --git a/src/theory/booleans/theory_bool_type_rules.cpp b/src/theory/booleans/theory_bool_type_rules.cpp
new file mode 100644
index 000000000..11210a869
--- /dev/null
+++ b/src/theory/booleans/theory_bool_type_rules.cpp
@@ -0,0 +1,76 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ * Dejan Jovanovic, Morgan Deters, Christopher L. Conway
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Typing and cardinality rules for the theory of boolean.
+ */
+
+#include "theory/booleans/theory_bool_type_rules.h"
+
+#include <sstream>
+
+namespace cvc5 {
+namespace theory {
+namespace boolean {
+
+TypeNode BooleanTypeRule::computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+{
+ TypeNode booleanType = nodeManager->booleanType();
+ if (check)
+ {
+ for (const auto& child : n)
+ {
+ if (!child.getType(check).isBoolean())
+ {
+ Debug("pb") << "failed type checking: " << child << std::endl;
+ Debug("pb") << " integer: " << child.getType(check).isInteger()
+ << std::endl;
+ Debug("pb") << " real: " << child.getType(check).isReal() << std::endl;
+ throw TypeCheckingExceptionPrivate(n,
+ "expecting a Boolean subexpression");
+ }
+ }
+ }
+ return booleanType;
+}
+
+TypeNode IteTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check)
+{
+ TypeNode thenType = n[1].getType(check);
+ TypeNode elseType = n[2].getType(check);
+ TypeNode iteType = TypeNode::leastCommonTypeNode(thenType, elseType);
+ if (check)
+ {
+ TypeNode booleanType = nodeManager->booleanType();
+ if (n[0].getType(check) != booleanType)
+ {
+ throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
+ }
+ if (iteType.isNull())
+ {
+ std::stringstream ss;
+ ss << "Both branches of the ITE must be a subtype of a common type."
+ << std::endl
+ << "then branch: " << n[1] << std::endl
+ << "its type : " << thenType << std::endl
+ << "else branch: " << n[2] << std::endl
+ << "its type : " << elseType << std::endl;
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ }
+ return iteType;
+}
+
+} // namespace boolean
+} // namespace theory
+} // namespace cvc5
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 6c9aea0ae..6d8eb0a6d 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -10,9 +10,7 @@
* directory for licensing information.
* ****************************************************************************
*
- * [[ Add brief comments here ]]
- *
- * [[ Add file-specific comments here ]]
+ * Typing and cardinality rules for the theory of boolean.
*/
#include "cvc5_private.h"
@@ -20,56 +18,24 @@
#ifndef CVC5__THEORY_BOOL_TYPE_RULES_H
#define CVC5__THEORY_BOOL_TYPE_RULES_H
+#include "expr/node.h"
+#include "expr/type_node.h"
+
namespace cvc5 {
namespace theory {
namespace boolean {
-class BooleanTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- TypeNode booleanType = nodeManager->booleanType();
- if( check ) {
- TNode::iterator child_it = n.begin();
- TNode::iterator child_it_end = n.end();
- for(; child_it != child_it_end; ++child_it) {
- if(!(*child_it).getType(check).isBoolean()) {
- Debug("pb") << "failed type checking: " << *child_it << std::endl;
- Debug("pb") << " integer: " << (*child_it).getType(check).isInteger() << std::endl;
- Debug("pb") << " real: " << (*child_it).getType(check).isReal() << std::endl;
- throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression");
- }
- }
- }
- return booleanType;
- }
-};/* class BooleanTypeRule */
+class BooleanTypeRule
+{
+ public:
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
-class IteTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- TypeNode thenType = n[1].getType(check);
- TypeNode elseType = n[2].getType(check);
- TypeNode iteType = TypeNode::leastCommonTypeNode(thenType, elseType);
- if( check ) {
- TypeNode booleanType = nodeManager->booleanType();
- if (n[0].getType(check) != booleanType) {
- throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
- }
- if (iteType.isNull()) {
- std::stringstream ss;
- ss << "Both branches of the ITE must be a subtype of a common type." << std::endl
- << "then branch: " << n[1] << std::endl
- << "its type : " << thenType << std::endl
- << "else branch: " << n[2] << std::endl
- << "its type : " << elseType << std::endl;
- throw TypeCheckingExceptionPrivate(n, ss.str());
- }
- }
- return iteType;
- }
-};/* class IteTypeRule */
+class IteTypeRule
+{
+ public:
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
} // namespace boolean
} // namespace theory
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback