From: Andrew Reynolds Date: Thu, 20 Feb 2020 20:49:02 +0000 (-0600) Subject: Remove front-end support for Chain (#3767) X-Git-Tag: cvc5-1.0.0~3626 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5489ef01beb91e256e343e2fd2d734b48b42ad6e;p=cvc5.git Remove front-end support for Chain (#3767) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 871cb2f99..1063452cb 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -893,7 +893,6 @@ install(FILES expr/array.h expr/array_store_all.h expr/ascription_type.h - expr/chain.h expr/datatype.h expr/emptyset.h expr/expr_iomanip.h diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 7bdc5008b..7f8fc8097 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -76,7 +76,6 @@ const static std::unordered_map s_kinds{ {VARIABLE, CVC4::Kind::BOUND_VARIABLE}, {LAMBDA, CVC4::Kind::LAMBDA}, {CHOICE, CVC4::Kind::CHOICE}, - {CHAIN, CVC4::Kind::CHAIN}, /* Boolean ------------------------------------------------------------- */ {CONST_BOOLEAN, CVC4::Kind::CONST_BOOLEAN}, {NOT, CVC4::Kind::NOT}, @@ -313,8 +312,6 @@ const static std::unordered_map {CVC4::Kind::BOUND_VARIABLE, VARIABLE}, {CVC4::Kind::LAMBDA, LAMBDA}, {CVC4::Kind::CHOICE, CHOICE}, - {CVC4::Kind::CHAIN, CHAIN}, - {CVC4::Kind::CHAIN_OP, CHAIN}, /* Boolean --------------------------------------------------------- */ {CVC4::Kind::CONST_BOOLEAN, CONST_BOOLEAN}, {CVC4::Kind::NOT, NOT}, @@ -567,8 +564,7 @@ const static std::unordered_map /* Set of kinds for indexed operators */ const static std::unordered_set s_indexed_kinds( - {CHAIN, - RECORD_UPDATE, + {RECORD_UPDATE, DIVISIBLE, BITVECTOR_REPEAT, BITVECTOR_ZERO_EXTEND, @@ -1146,17 +1142,6 @@ std::string Op::getIndices() const return i; } -template <> -Kind Op::getIndices() const -{ - CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(!d_expr->isNull()) - << "Expecting a non-null internal expression. This Op is not indexed."; - Kind kind = intToExtKind(d_expr->getKind()); - CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN, kind) << "CHAIN"; - return intToExtKind(d_expr->getConst().getOperator()); -} - template <> uint32_t Op::getIndices() const { @@ -3195,18 +3180,6 @@ Op Solver::mkOp(Kind kind) const CVC4_API_SOLVER_TRY_CATCH_END } -Op Solver::mkOp(Kind kind, Kind k) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN, kind) << "CHAIN"; - - return Op( - kind, - *mkValHelper(CVC4::Chain(extToIntKind(k))).d_expr.get()); - - CVC4_API_SOLVER_TRY_CATCH_END; -} - Op Solver::mkOp(Kind kind, const std::string& arg) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 79c02c031..9820aeb19 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1925,15 +1925,6 @@ class CVC4_PUBLIC Solver */ Op mkOp(Kind kind) const; - /** - * Create operator of kind: - * - CHAIN - * See enum Kind for a description of the parameters. - * @param kind the kind of the operator - * @param k the kind argument to this operator - */ - Op mkOp(Kind kind, Kind k) const; - /** * Create operator of kind: * - RECORD_UPDATE diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 213dec56a..dcb05be17 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -142,25 +142,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ CHOICE, - /** - * Chained operator. - * Parameters: 1 - * -[1]: Kind of the binary operation - * Create with: - * mkOp(Kind opkind, Kind kind) - - * Apply chained operation. - * Parameters: n > 1 - * -[1]: Op of kind CHAIN (represents a binary op) - * -[2]..[n]: Arguments to that operator - * Create with: - * mkTerm(Op op, Term child1, Term child2) - * mkTerm(Op op, Term child1, Term child2, Term child3) - * mkTerm(Op op, const std::vector& children) - * Turned into a conjunction of binary applications of the operator on - * adjoining parameters. - */ - CHAIN, /* Boolean --------------------------------------------------------------- */ diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index f6b48048f..8357102b0 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -7,7 +7,6 @@ libcvc4_add_sources( attribute.cpp attribute_internals.h attribute_unique_id.h - chain.h emptyset.cpp emptyset.h expr_iomanip.cpp diff --git a/src/expr/chain.h b/src/expr/chain.h deleted file mode 100644 index 9df819b4d..000000000 --- a/src/expr/chain.h +++ /dev/null @@ -1,51 +0,0 @@ -/********************* */ -/*! \file chain.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__CHAIN_H -#define CVC4__CHAIN_H - -#include "expr/kind.h" -#include - -namespace CVC4 { - -/** A class to represent a chained, built-in operator. */ -class CVC4_PUBLIC Chain { - Kind d_kind; -public: - explicit Chain(Kind k) : d_kind(k) { } - bool operator==(const Chain& ch) const { return d_kind == ch.d_kind; } - bool operator!=(const Chain& ch) const { return d_kind != ch.d_kind; } - Kind getOperator() const { return d_kind; } -};/* class Chain */ - -inline std::ostream& operator<<(std::ostream& out, const Chain& ch) CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream& out, const Chain& ch) { - return out << ch.getOperator(); -} - -struct CVC4_PUBLIC ChainHashFunction { - size_t operator()(const Chain& ch) const { - return kind::KindHashFunction()(ch.getOperator()); - } -};/* struct ChainHashFunction */ - -}/* CVC4 namespace */ - -#endif /* CVC4__CHAIN_H */ diff --git a/src/expr/chain.i b/src/expr/chain.i deleted file mode 100644 index 8de1665ce..000000000 --- a/src/expr/chain.i +++ /dev/null @@ -1,12 +0,0 @@ -%{ -#include "expr/chain.h" -%} - -%rename(equals) CVC4::Chain::operator==(const Chain&) const; -%ignore CVC4::Chain::operator!=(const Chain&) const; - -%ignore CVC4::operator<<(std::ostream&, const Chain&); - -%rename(apply) CVC4::ChainHashFunction::operator()(const CVC4::Chain&) const; - -%include "expr/chain.h" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 32d555718..664fa209d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -515,6 +515,22 @@ Expr Parser::mkHoApply(Expr expr, std::vector& args) return expr; } +api::Term Parser::mkChain(api::Kind k, const std::vector& args) +{ + if (args.size() == 2) + { + // if this is the case exactly 1 pair will be generated so the + // AND is not required + return d_solver->mkTerm(k, args[0], args[1]); + } + std::vector children; + for (size_t i = 0, nargsmo = args.size() - 1; i < nargsmo; i++) + { + children.push_back(d_solver->mkTerm(k, args[i], args[i + 1])); + } + return d_solver->mkTerm(api::AND, children); +} + bool Parser::isDeclared(const std::string& name, SymbolType type) { switch (type) { case SYM_VARIABLE: diff --git a/src/parser/parser.h b/src/parser/parser.h index ecf1e2961..cd70fde0f 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -24,6 +24,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "expr/expr_stream.h" #include "expr/kind.h" @@ -677,6 +678,16 @@ public: */ Expr mkHoApply(Expr expr, std::vector& args); + /** make chain + * + * Given a kind k and argument terms t_1, ..., t_n, this returns the + * conjunction of: + * (k t_1 t_2) .... (k t_{n-1} t_n) + * It is expected that k is a kind denoting a predicate, and args is a list + * of terms of size >= 2 such that the terms above are well-typed. + */ + api::Term mkChain(api::Kind k, const std::vector& args); + /** * Add an operator to the current legal set. * diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index f3b66643a..11dedb259 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1887,7 +1887,9 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) || kind == kind::LEQ || kind == kind::GEQ) { /* "chainable", but CVC4 internally only supports 2 args */ - return em->mkExpr(em->mkConst(Chain(kind)), args); + api::Term ret = + mkChain(intToExtKind(kind), api::exprVectorToTerms(args)); + return ret.getExpr(); } } diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 71a3e4bee..bf699ae3c 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -326,7 +326,9 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector& args) || kind == kind::LEQ || kind == kind::GEQ) { /* "chainable", but CVC4 internally only supports 2 args */ - return em->mkExpr(em->mkConst(Chain(kind)), args); + api::Term ret = + mkChain(intToExtKind(kind), api::exprVectorToTerms(args)); + return ret.getExpr(); } } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index f8448f1e9..f3f43220c 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -283,8 +283,8 @@ void CvcPrinter::toStream( out << ")"; return; break; - case kind::CHAIN: - case kind::DISTINCT: // chain and distinct not supported directly in CVC4, blast them away with the rewriter + case kind::DISTINCT: + // distinct not supported directly, blast it away with the rewriter toStream(out, theory::Rewriter::rewrite(n), depth, types, true); return; case kind::SORT_TYPE: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index bfdaf7852..8153d6856 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -193,9 +193,6 @@ void Smt2Printer::toStream(std::ostream& out, case kind::BUILTIN: out << smtKindString(n.getConst(), d_variant); break; - case kind::CHAIN_OP: - out << smtKindString(n.getConst().getOperator(), d_variant); - break; case kind::CONST_RATIONAL: { const Rational& r = n.getConst(); toStreamRational( @@ -474,7 +471,6 @@ void Smt2Printer::toStream(std::ostream& out, out << smtKindString(k, d_variant) << " "; parametricTypeChildren = true; break; - case kind::CHAIN: break; case kind::FUNCTION_TYPE: out << "->"; for (Node nc : n) @@ -1027,7 +1023,6 @@ static string smtKindString(Kind k, Variant v) // builtin theory case kind::EQUAL: return "="; case kind::DISTINCT: return "distinct"; - case kind::CHAIN: break; case kind::SEXPR: break; // bool theory diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 88a53062a..7e2ed84b1 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -1050,42 +1050,6 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, return; } - case kind::CHAIN: { - // LFSC doesn't allow declarations with variable numbers of - // arguments, so we have to flatten chained operators, like =. - Kind op = term.getOperator().getConst().getOperator(); - std::string op_str; - bool booleanCase = false; - if (op==kind::EQUAL && term[0].getType().isBoolean()) { - booleanCase = term[0].getType().isBoolean(); - op_str = "iff"; - } else { - op_str = utils::toLFSCKind(op); - } - size_t n = term.getNumChildren(); - std::ostringstream paren; - for(size_t i = 1; i < n; ++i) { - if(i + 1 < n) { - os << "(" << utils::toLFSCKind(kind::AND) << " "; - paren << ")"; - } - os << "(" << op_str << " "; - if (booleanCase && printsAsBool(term[i - 1])) os << "(p_app "; - printBoundTerm(term[i - 1], os, map); - if (booleanCase && printsAsBool(term[i - 1])) os << ")"; - os << " "; - if (booleanCase && printsAsBool(term[i])) os << "(p_app "; - printBoundTerm(term[i], os, map); - if (booleanCase && printsAsBool(term[i])) os << ")"; - os << ")"; - if(i + 1 < n) { - os << " "; - } - } - os << paren.str(); - return; - } - default: Unhandled() << k; } } diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 15891dfad..c90419def 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -300,13 +300,6 @@ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, sec operator CHOICE 2 "a Hilbert choice (epsilon) expression; first parameter is a BOUND_VAR_LIST, second is the Hilbert choice body" -parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjunction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator" -constant CHAIN_OP \ - ::CVC4::Chain \ - ::CVC4::ChainHashFunction \ - "expr/chain.h" \ - "the chained operator; payload is an instance of the CVC4::Chain class" - constant TYPE_CONSTANT \ ::CVC4::TypeConstant \ ::CVC4::TypeConstantHashFunction \ @@ -334,8 +327,6 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule typerule CHOICE ::CVC4::theory::builtin::ChoiceTypeRule -typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule -typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule # lambda expressions that are isomorphic to array constants can be considered constants construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index d9fe2fecc..15c312080 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -18,7 +18,6 @@ #include "theory/builtin/theory_builtin_rewriter.h" #include "expr/attribute.h" -#include "expr/chain.h" #include "expr/node_algorithm.h" #include "theory/rewriter.h" @@ -53,24 +52,6 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) { return out; } -Node TheoryBuiltinRewriter::blastChain(TNode in) { - Assert(in.getKind() == kind::CHAIN); - - Kind chainedOp = in.getOperator().getConst().getOperator(); - - if(in.getNumChildren() == 2) { - // if this is the case exactly 1 pair will be generated so the - // AND is not required - return NodeManager::currentNM()->mkNode(chainedOp, in[0], in[1]); - } else { - NodeBuilder<> conj(kind::AND); - for(TNode::iterator i = in.begin(), j = i + 1; j != in.end(); ++i, ++j) { - conj << NodeManager::currentNM()->mkNode(chainedOp, *i, *j); - } - return conj; - } -} - RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) { if( node.getKind()==kind::LAMBDA ){ Trace("builtin-rewrite") << "Rewriting lambda " << node << "..." << std::endl; diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index 60a8f29f0..4b75d7e3a 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -32,18 +32,6 @@ class TheoryBuiltinRewriter : public TheoryRewriter static Node blastDistinct(TNode node); public: - /** - * Takes a chained application of a binary operator and returns a conjunction - * of binary applications of that operator. - * - * For example: - * - * (= x y z) ---> (and (= x y) (= y z)) - * - * @param node A node that is a chained application of a binary operator - * @return A conjunction of binary applications of the chained operator - */ - static Node blastChain(TNode node); static inline RewriteResponse doRewrite(TNode node) { @@ -51,7 +39,6 @@ class TheoryBuiltinRewriter : public TheoryRewriter { case kind::DISTINCT: return RewriteResponse(REWRITE_DONE, blastDistinct(node)); - case kind::CHAIN: return RewriteResponse(REWRITE_DONE, blastChain(node)); default: return RewriteResponse(REWRITE_DONE, node); } } diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index bb88b64ee..d49edbc8c 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -194,59 +194,6 @@ class ChoiceTypeRule } }; /* class ChoiceTypeRule */ -class ChainTypeRule { - public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::CHAIN); - - if(!check) { - return nodeManager->booleanType(); - } - - TypeNode tn; - try { - tn = nodeManager->getType(TheoryBuiltinRewriter::blastChain(n), check); - } catch(TypeCheckingExceptionPrivate& e) { - std::stringstream ss; - ss << "Cannot typecheck the expansion of chained operator `" << n.getOperator() << "':" - << std::endl; - // indent the sub-exception for clarity - std::stringstream ss2; - ss2 << e; - std::string eStr = ss2.str(); - for(size_t i = eStr.find('\n'); i != std::string::npos; i = eStr.find('\n', i)) { - eStr.insert(++i, "| "); - } - ss << "| " << eStr; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - - // This check is intentionally != booleanType() rather than - // !(...isBoolean()): if we ever add a type compatible with - // Boolean (pseudobooleans or whatever), we have to revisit - // the above "!check" case where booleanType() is returned - // directly. Putting this check here will cause a failure if - // it's ever relevant. - if(tn != nodeManager->booleanType()) { - std::stringstream ss; - ss << "Chains can only be formed over predicates; " - << "the operator here returns `" << tn << "', expected `" - << nodeManager->booleanType() << "'."; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - - return nodeManager->booleanType(); - } -};/* class ChainTypeRule */ - -class ChainedOperatorTypeRule { - public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::CHAIN_OP); - return nodeManager->getType(nodeManager->operatorOf(n.getConst().getOperator()), check); - } -};/* class ChainedOperatorTypeRule */ - class SortProperties { public: inline static bool isWellFounded(TypeNode type) { diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2 index 9b5ffe747..017479871 100644 --- a/test/regress/regress0/printer/let_shadowing.smt2 +++ b/test/regress/regress0/printer/let_shadowing.smt2 @@ -1,9 +1,9 @@ ; REQUIRES: dumping ; COMMAND-LINE: --dump raw-benchmark --preprocess-only ; SCRUBBER: grep assert -; EXPECT: (assert (let ((_let_1 (* x y))) (= _let_1 _let_1 _let_0))) -; EXPECT: (assert (let ((_let_1 (and a b))) (= _let_1 _let_1 (forall ((_let_0 Int)) (= 0 _let_0) )))) -; EXPECT: (assert (let ((_let_1 (and a b))) (= _let_1 _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_2 (and b a))) (and _let_1 _let_2 _let_2 (= 0 _let_0))) ) )))) +; EXPECT: (assert (let ((_let_1 (* x y))) (and (= _let_1 _let_1) (= _let_1 _let_0)))) +; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((_let_0 Int)) (= 0 _let_0) ))))) +; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_2 (and b a))) (and _let_1 _let_2 _let_2 (= 0 _let_0))) ) ))))) (set-logic NIA) (declare-const _let_0 Int) (declare-const x Int) diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.h index dcad8b649..6fb7e839c 100644 --- a/test/unit/api/op_black.h +++ b/test/unit/api/op_black.h @@ -29,7 +29,6 @@ class OpBlack : public CxxTest::TestSuite void testIsNull(); void testOpFromKind(); void testGetIndicesString(); - void testGetIndicesKind(); void testGetIndicesUint(); void testGetIndicesPairUint(); @@ -88,14 +87,6 @@ void OpBlack::testGetIndicesString() TS_ASSERT_THROWS(record_update_ot.getIndices(), CVC4ApiException&); } -void OpBlack::testGetIndicesKind() -{ - Op chain_ot = d_solver.mkOp(CHAIN, AND); - TS_ASSERT(chain_ot.isIndexed()); - Kind chain_idx = chain_ot.getIndices(); - TS_ASSERT(chain_idx == AND); -} - void OpBlack::testGetIndicesUint() { Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index bf992d2d5..aea41a42b 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -461,7 +461,6 @@ void SolverBlack::testMkPosZero() void SolverBlack::testMkOp() { // mkOp(Kind kind, Kind k) - TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(CHAIN, EQUAL)); TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException&); // mkOp(Kind kind, const std::string& arg) @@ -622,10 +621,10 @@ void SolverBlack::testMkTermFromOp() std::vector v1 = {d_solver->mkReal(1), d_solver->mkReal(2)}; std::vector v2 = {d_solver->mkReal(1), Term()}; std::vector v3 = {}; + std::vector v4 = {d_solver->mkReal(5)}; // simple operator terms Op opterm1 = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1); Op opterm2 = d_solver->mkOp(DIVISIBLE, 1); - Op opterm3 = d_solver->mkOp(CHAIN, EQUAL); // list datatype Sort sort = d_solver->mkParamSort("T"); @@ -679,33 +678,33 @@ void SolverBlack::testMkTermFromOp() CVC4ApiException&); // mkTerm(Op op, Term child1, Term child2) const - TS_ASSERT_THROWS_NOTHING( - d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2))); + TS_ASSERT_THROWS( + d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)), + CVC4ApiException&); TS_ASSERT_THROWS_NOTHING( d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0), d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1))); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()), + TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkReal(1), Term()), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)), + TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkReal(1)), CVC4ApiException&); // mkTerm(Op op, Term child1, Term child2, Term child3) // const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( - opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2))); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&); TS_ASSERT_THROWS( d_solver->mkTerm( - opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()), + opterm2, d_solver->mkReal(1), d_solver->mkReal(1), Term()), CVC4ApiException&); // mkTerm(Op op, const std::vector& children) const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm3, v1)); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v3), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, v4)); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v3), CVC4ApiException&); } void SolverBlack::testMkTrue()