diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 19 | ||||
| -rw-r--r-- | src/expr/node_manager.cpp | 65 | ||||
| -rw-r--r-- | src/expr/node_manager.h | 88 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 16 | ||||
| -rw-r--r-- | test/unit/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/unit/printer/CMakeLists.txt | 14 | ||||
| -rw-r--r-- | test/unit/printer/smt2_printer_black.h | 68 |
7 files changed, 195 insertions, 76 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index e16d8c519..2c694dbed 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3386,6 +3386,7 @@ Sort Solver::getNullSort(void) const Sort Solver::getBooleanSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->booleanType()); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3393,6 +3394,7 @@ Sort Solver::getBooleanSort(void) const Sort Solver::getIntegerSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->integerType()); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3400,6 +3402,7 @@ Sort Solver::getIntegerSort(void) const Sort Solver::getRealSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->realType()); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3407,6 +3410,7 @@ Sort Solver::getRealSort(void) const Sort Solver::getRegExpSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->regExpType()); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3414,6 +3418,7 @@ Sort Solver::getRegExpSort(void) const Sort Solver::getStringSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->stringType()); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3421,6 +3426,7 @@ Sort Solver::getStringSort(void) const Sort Solver::getRoundingModeSort(void) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; @@ -3432,6 +3438,7 @@ Sort Solver::getRoundingModeSort(void) const Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!indexSort.isNull(), indexSort) << "non-null index sort"; @@ -3448,6 +3455,7 @@ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const Sort Solver::mkBitVectorSort(uint32_t size) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0"; @@ -3458,6 +3466,7 @@ Sort Solver::mkBitVectorSort(uint32_t size) const Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; @@ -3503,6 +3512,7 @@ std::vector<Sort> Solver::mkDatatypeSorts( Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain) << "non-null codomain sort"; @@ -3522,6 +3532,7 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for function sort"; @@ -3553,6 +3564,7 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const Sort Solver::mkParamSort(const std::string& symbol) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort( this, @@ -3562,6 +3574,7 @@ Sort Solver::mkParamSort(const std::string& symbol) const Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for predicate sort"; @@ -3610,6 +3623,7 @@ Sort Solver::mkRecordSort( Sort Solver::mkSetSort(Sort elemSort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; @@ -3622,6 +3636,7 @@ Sort Solver::mkSetSort(Sort elemSort) const Sort Solver::mkBagSort(Sort elemSort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; @@ -3634,6 +3649,7 @@ Sort Solver::mkBagSort(Sort elemSort) const Sort Solver::mkSequenceSort(Sort elemSort) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort) << "non-null element sort"; @@ -3646,6 +3662,7 @@ Sort Solver::mkSequenceSort(Sort elemSort) const Sort Solver::mkUninterpretedSort(const std::string& symbol) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; return Sort(this, getNodeManager()->mkSort(symbol)); CVC4_API_SOLVER_TRY_CATCH_END; @@ -3654,6 +3671,7 @@ Sort Solver::mkUninterpretedSort(const std::string& symbol) const Sort Solver::mkSortConstructorSort(const std::string& symbol, size_t arity) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0"; @@ -3664,6 +3682,7 @@ Sort Solver::mkSortConstructorSort(const std::string& symbol, Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const { + NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = sorts.size(); i < size; ++i) { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e9f121047..7c847d8ce 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -105,6 +105,71 @@ NodeManager::NodeManager(ExprManager* exprManager) init(); } +TypeNode NodeManager::booleanType() +{ + return mkTypeConst<TypeConstant>(BOOLEAN_TYPE); +} + +TypeNode NodeManager::integerType() +{ + return mkTypeConst<TypeConstant>(INTEGER_TYPE); +} + +TypeNode NodeManager::realType() +{ + return mkTypeConst<TypeConstant>(REAL_TYPE); +} + +TypeNode NodeManager::stringType() +{ + return mkTypeConst<TypeConstant>(STRING_TYPE); +} + +TypeNode NodeManager::regExpType() +{ + return mkTypeConst<TypeConstant>(REGEXP_TYPE); +} + +TypeNode NodeManager::roundingModeType() +{ + return mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE); +} + +TypeNode NodeManager::boundVarListType() +{ + return mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE); +} + +TypeNode NodeManager::instPatternType() +{ + return mkTypeConst<TypeConstant>(INST_PATTERN_TYPE); +} + +TypeNode NodeManager::instPatternListType() +{ + return mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE); +} + +TypeNode NodeManager::builtinOperatorType() +{ + return mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE); +} + +TypeNode NodeManager::mkBitVectorType(unsigned size) +{ + return mkTypeConst<BitVectorSize>(BitVectorSize(size)); +} + +TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) +{ + return mkTypeConst<FloatingPointSize>(FloatingPointSize(exp, sig)); +} + +TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) +{ + return mkTypeConst<FloatingPointSize>(fs); +} + void NodeManager::init() { // `mkConst()` indirectly needs the correct NodeManager in scope because we // call `NodeValue::inc()` which uses `NodeManager::curentNM()` diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5cf19aab9..99db9feb2 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -808,37 +808,37 @@ class NodeManager { const typename AttrKind::value_type& value); /** Get the (singleton) type for Booleans. */ - inline TypeNode booleanType(); + TypeNode booleanType(); /** Get the (singleton) type for integers. */ - inline TypeNode integerType(); + TypeNode integerType(); /** Get the (singleton) type for reals. */ - inline TypeNode realType(); + TypeNode realType(); /** Get the (singleton) type for strings. */ - inline TypeNode stringType(); + TypeNode stringType(); /** Get the (singleton) type for RegExp. */ - inline TypeNode regExpType(); + TypeNode regExpType(); /** Get the (singleton) type for rounding modes. */ - inline TypeNode roundingModeType(); + TypeNode roundingModeType(); /** Get the bound var list type. */ - inline TypeNode boundVarListType(); + TypeNode boundVarListType(); /** Get the instantiation pattern type. */ - inline TypeNode instPatternType(); + TypeNode instPatternType(); /** Get the instantiation pattern type. */ - inline TypeNode instPatternListType(); + TypeNode instPatternListType(); /** * Get the (singleton) type for builtin operators (that is, the type * of the Node returned from Node::getOperator() when the operator * is built-in, like EQUAL). */ - inline TypeNode builtinOperatorType(); + TypeNode builtinOperatorType(); /** * Make a function type from domain to range. @@ -906,11 +906,11 @@ class NodeManager { /** Make the type of floating-point with <code>exp</code> bit exponent and <code>sig</code> bit significand */ - inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig); - inline TypeNode mkFloatingPointType(FloatingPointSize fs); + TypeNode mkFloatingPointType(unsigned exp, unsigned sig); + TypeNode mkFloatingPointType(FloatingPointSize fs); /** Make the type of bitvectors of size <code>size</code> */ - inline TypeNode mkBitVectorType(unsigned size); + TypeNode mkBitVectorType(unsigned size); /** Make the type of arrays with the given parameterization */ inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); @@ -1129,56 +1129,6 @@ public: } };/* class NodeManagerScope */ -/** Get the (singleton) type for booleans. */ -inline TypeNode NodeManager::booleanType() { - return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE)); -} - -/** Get the (singleton) type for integers. */ -inline TypeNode NodeManager::integerType() { - return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE)); -} - -/** Get the (singleton) type for reals. */ -inline TypeNode NodeManager::realType() { - return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE)); -} - -/** Get the (singleton) type for strings. */ -inline TypeNode NodeManager::stringType() { - return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE)); -} - -/** Get the (singleton) type for regexps. */ -inline TypeNode NodeManager::regExpType() { - return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE)); -} - -/** Get the (singleton) type for rounding modes. */ -inline TypeNode NodeManager::roundingModeType() { - return TypeNode(mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE)); -} - -/** Get the bound var list type. */ -inline TypeNode NodeManager::boundVarListType() { - return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE)); -} - -/** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternType() { - return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE)); -} - -/** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternListType() { - return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE)); -} - -/** Get the (singleton) type for builtin operators. */ -inline TypeNode NodeManager::builtinOperatorType() { - return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE)); -} - inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) { std::vector<TypeNode> typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { @@ -1187,18 +1137,6 @@ inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) { return mkTypeNode(kind::SEXPR_TYPE, typeNodes); } -inline TypeNode NodeManager::mkBitVectorType(unsigned size) { - return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size))); -} - -inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) { - return TypeNode(mkTypeConst<FloatingPointSize>(FloatingPointSize(exp,sig))); -} - -inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) { - return TypeNode(mkTypeConst<FloatingPointSize>(fs)); -} - inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { CheckArgument(!indexType.isNull(), indexType, diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index cdaa61295..5ef1eca2b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -367,6 +367,13 @@ void Smt2Printer::toStream(std::ostream& out, out << "(_ fp.to_sbv_total " << n.getConst<FloatingPointToSBVTotal>().bvs.d_size << ")"; break; + case kind::REGEXP_REPEAT_OP: + out << "(_ re.^ " << n.getConst<RegExpRepeat>().d_repeatAmount << ")"; + break; + case kind::REGEXP_LOOP_OP: + out << "(_ re.loop " << n.getConst<RegExpLoop>().d_loopMinOcc << " " + << n.getConst<RegExpLoop>().d_loopMaxOcc << ")"; + break; default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant @@ -669,7 +676,6 @@ void Smt2Printer::toStream(std::ostream& out, case kind::REGEXP_PLUS: case kind::REGEXP_OPT: case kind::REGEXP_RANGE: - case kind::REGEXP_LOOP: case kind::REGEXP_COMPLEMENT: case kind::REGEXP_DIFF: case kind::REGEXP_EMPTY: @@ -677,6 +683,13 @@ void Smt2Printer::toStream(std::ostream& out, case kind::SEQ_UNIT: case kind::SEQ_NTH: case kind::SEQUENCE_TYPE: out << smtKindString(k, d_variant) << " "; break; + case kind::REGEXP_REPEAT: + case kind::REGEXP_LOOP: + { + out << n.getOperator() << ' '; + stillNeedToPrintParams = false; + break; + } case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break; case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break; @@ -1262,6 +1275,7 @@ static string smtKindString(Kind k, Variant v) case kind::REGEXP_PLUS: return "re.+"; case kind::REGEXP_OPT: return "re.opt"; case kind::REGEXP_RANGE: return "re.range"; + case kind::REGEXP_REPEAT: return "re.^"; case kind::REGEXP_LOOP: return "re.loop"; case kind::REGEXP_COMPLEMENT: return "re.comp"; case kind::REGEXP_DIFF: return "re.diff"; diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index f29785a56..bb53c15b0 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -116,6 +116,7 @@ add_subdirectory(context) add_subdirectory(expr) add_subdirectory(main) add_subdirectory(parser) +add_subdirectory(printer) add_subdirectory(prop) add_subdirectory(theory) add_subdirectory(preprocessing) diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt new file mode 100644 index 000000000..3b040d1fc --- /dev/null +++ b/test/unit/printer/CMakeLists.txt @@ -0,0 +1,14 @@ +##################### +## CMakeLists.txt +## Top contributors (to current version): +## Andres Noetzli +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 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. +## +#-----------------------------------------------------------------------------# +# Add unit tests + +cvc4_add_unit_test_black(smt2_printer_black printer) diff --git a/test/unit/printer/smt2_printer_black.h b/test/unit/printer/smt2_printer_black.h new file mode 100644 index 000000000..8540c3cc8 --- /dev/null +++ b/test/unit/printer/smt2_printer_black.h @@ -0,0 +1,68 @@ +/********************* */ +/*! \file smt2_printer_black.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief Black box testing of the SMT2 printer + ** + ** Black box testing of the SMT2 printer. + **/ + +#include <cxxtest/TestSuite.h> + +#include <iostream> + +#include "api/cvc4cpp.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "options/language.h" +#include "smt/smt_engine.h" + +using namespace CVC4; +using namespace CVC4::kind; + +class Smt2PrinterBlack : public CxxTest::TestSuite +{ + public: + void setUp() override + { + d_slv.reset(new api::Solver()); + d_nm = d_slv->getSmtEngine()->getNodeManager(); + } + + void tearDown() override { d_slv.reset(); } + + void checkToString(TNode n, const std::string& expected) + { + std::stringstream ss; + ss << Node::setdepth(-1) + << Node::setlanguage(language::output::LANG_SMTLIB_V2_6) << n; + TS_ASSERT_EQUALS(ss.str(), expected); + } + + void testRegexpRepeat() + { + Node n = d_nm->mkNode( + d_nm->mkConst(RegExpRepeat(5)), + d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("x")))); + checkToString(n, "((_ re.^ 5) (str.to_re \"x\"))"); + } + + void testRegexpLoop() + { + Node n = d_nm->mkNode( + d_nm->mkConst(RegExpLoop(1, 3)), + d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("x")))); + checkToString(n, "((_ re.loop 1 3) (str.to_re \"x\"))"); + } + + private: + std::unique_ptr<api::Solver> d_slv; + NodeManager* d_nm; +}; |