diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-28 17:31:57 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-22 18:54:52 -0400 |
commit | f44a81d1b62058fa56af952aa92be965690481e5 (patch) | |
tree | dc4b56e27701abd61ebd69675f86a9366d90998f /src/theory | |
parent | 36816ad2537a2e6163037e9592c513b9a69aa9dc (diff) |
Support for Boolean term conversion in datatypes.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/booleans/Makefile.am | 7 | ||||
-rw-r--r-- | src/theory/booleans/boolean_term_conversion_mode.cpp | 41 | ||||
-rw-r--r-- | src/theory/booleans/boolean_term_conversion_mode.h | 53 | ||||
-rw-r--r-- | src/theory/booleans/options | 3 | ||||
-rw-r--r-- | src/theory/booleans/options_handlers.h | 65 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 18 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.h | 10 | ||||
-rw-r--r-- | src/theory/model.cpp | 2 |
9 files changed, 188 insertions, 13 deletions
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index 8cb32de18..9d58ffa75 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -13,7 +13,10 @@ libbooleans_la_SOURCES = \ theory_bool_rewriter.h \ theory_bool_rewriter.cpp \ circuit_propagator.h \ - circuit_propagator.cpp + circuit_propagator.cpp \ + boolean_term_conversion_mode.h \ + boolean_term_conversion_mode.cpp EXTRA_DIST = \ - kinds + kinds \ + options_handlers.h diff --git a/src/theory/booleans/boolean_term_conversion_mode.cpp b/src/theory/booleans/boolean_term_conversion_mode.cpp new file mode 100644 index 000000000..f9d80835c --- /dev/null +++ b/src/theory/booleans/boolean_term_conversion_mode.cpp @@ -0,0 +1,41 @@ +/********************* */ +/*! \file boolean_term_conversion_mode.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include <iostream> +#include "theory/booleans/boolean_term_conversion_mode.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) { + switch(mode) { + case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: + out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS"; + break; + case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: + out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES"; + break; + case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE: + out << "BOOLEAN_TERM_CONVERT_NATIVE"; + break; + default: + out << "BooleanTermConversionMode!UNKNOWN"; + } + + return out; +} + +}/* CVC4 namespace */ diff --git a/src/theory/booleans/boolean_term_conversion_mode.h b/src/theory/booleans/boolean_term_conversion_mode.h new file mode 100644 index 000000000..6ca908df4 --- /dev/null +++ b/src/theory/booleans/boolean_term_conversion_mode.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file boolean_term_conversion_mode.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H +#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H + +#include <iostream> + +namespace CVC4 { +namespace theory { +namespace booleans { + +typedef enum { + /** + * Convert Boolean terms to bitvectors of size 1. + */ + BOOLEAN_TERM_CONVERT_TO_BITVECTORS, + /** + * Convert Boolean terms to enumerations in the Datatypes theory. + */ + BOOLEAN_TERM_CONVERT_TO_DATATYPES, + /** + * Convert Boolean terms to enumerations in the Datatypes theory IF + * used in a datatypes context, otherwise to a bitvector of size 1. + */ + BOOLEAN_TERM_CONVERT_NATIVE + +} BooleanTermConversionMode; + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */ diff --git a/src/theory/booleans/options b/src/theory/booleans/options index ae14de58b..6c571f30e 100644 --- a/src/theory/booleans/options +++ b/src/theory/booleans/options @@ -5,4 +5,7 @@ module BOOLEANS "theory/booleans/options.h" Boolean theory +option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "theory/booleans/boolean_term_conversion_mode.h" :handler CVC4::theory::booleans::stringToBooleanTermConversionMode :handler-include "theory/booleans/options_handlers.h" + policy for converting Boolean terms + endmodule diff --git a/src/theory/booleans/options_handlers.h b/src/theory/booleans/options_handlers.h new file mode 100644 index 000000000..2bf53b3d2 --- /dev/null +++ b/src/theory/booleans/options_handlers.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \file options_handlers.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H +#define __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H + +#include <string> + +namespace CVC4 { +namespace theory { +namespace booleans { + +static const std::string booleanTermConversionModeHelp = "\ +Boolean term conversion modes currently supported by the\n\ +--boolean-term-conversion-mode option:\n\ +\n\ +bitvectors [default]\n\ ++ Boolean terms are converted to bitvectors of size 1.\n\ +\n\ +datatypes\n\ ++ Boolean terms are converted to enumerations in the Datatype theory.\n\ +\n\ +native\n\ ++ Boolean terms are converted in a \"natural\" way depending on where they\n\ + are used. If in a datatype context, they are converted to an enumeration.\n\ + Elsewhere, they are converted to a bitvector of size 1.\n\ +"; + +inline BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "bitvectors") { + return BOOLEAN_TERM_CONVERT_TO_BITVECTORS; + } else if(optarg == "datatypes") { + return BOOLEAN_TERM_CONVERT_TO_DATATYPES; + } else if(optarg == "native") { + return BOOLEAN_TERM_CONVERT_NATIVE; + } else if(optarg == "help") { + puts(booleanTermConversionModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") + + optarg + "'. Try --boolean-term-conversion-mode help."); + } +} + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H */ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 352868f7b..a369fb572 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -79,7 +79,7 @@ class EqualityTypeRule { if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) { std::stringstream ss; - ss << "Subtypes must have a common type:" << std::endl; + ss << "Subexpressions must have a common base type:" << std::endl; ss << "Equation: " << n << std::endl; ss << "Type 1: " << lhsType << std::endl; ss << "Type 2: " << rhsType << std::endl; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9e4f0de75..a3bec7af0 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -24,6 +24,7 @@ #include "theory/datatypes/theory_datatypes_type_rules.h" #include "theory/model.h" #include "smt/options.h" +#include "smt/boolean_terms.h" #include "theory/quantifiers/options.h" #include <map> @@ -311,15 +312,28 @@ Node TheoryDatatypes::ppRewrite(TNode in) { return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]); } + TypeNode t = in.getType(); + // we only care about tuples and records here if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE && in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) { + if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) { + Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl; + Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl; + if(t.isTuple()) { + Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl; + Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl; + NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr())); + } else { + Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl; + Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl; + NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr())); + } + } // nothing to do return in; } - TypeNode t = in.getType(); - if(t.hasAttribute(expr::DatatypeTupleAttr())) { t = t.getAttribute(expr::DatatypeTupleAttr()); } else if(t.hasAttribute(expr::DatatypeRecordAttr())) { diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 2a74f6d15..a4facdefe 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -176,7 +176,7 @@ class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> { void newEnumerators() { d_enumerators = new TypeEnumerator*[getType().getNumChildren()]; for(size_t i = 0; i < getType().getNumChildren(); ++i) { - d_enumerators[i] = NULL; + d_enumerators[i] = new TypeEnumerator(getType()[i]); } } @@ -205,9 +205,7 @@ public: if(te.d_enumerators != NULL) { newEnumerators(); for(size_t i = 0; i < getType().getNumChildren(); ++i) { - if(te.d_enumerators[i] != NULL) { - d_enumerators[i] = new TypeEnumerator(*te.d_enumerators[i]); - } + *d_enumerators[i] = TypeEnumerator(*te.d_enumerators[i]); } } } @@ -292,9 +290,7 @@ public: if(re.d_enumerators != NULL) { newEnumerators(); for(size_t i = 0; i < getType().getNumChildren(); ++i) { - if(re.d_enumerators[i] != NULL) { - d_enumerators[i] = new TypeEnumerator(*re.d_enumerators[i]); - } + *d_enumerators[i] = TypeEnumerator(*re.d_enumerators[i]); } } } diff --git a/src/theory/model.cpp b/src/theory/model.cpp index bbc51c9e0..42a5380e4 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -57,7 +57,7 @@ Node TheoryModel::getValue( TNode n ) const{ Expr TheoryModel::getValue( Expr expr ) const{ Node n = Node::fromExpr( expr ); Node ret = getValue( n ); - return d_smt.postprocess(ret).toExpr(); + return d_smt.postprocess(ret, TypeNode::fromType(expr.getType())).toExpr(); } /** get cardinality for sort */ |