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
{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},
{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},
/* Set of kinds for indexed operators */
const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds(
- {CHAIN,
- RECORD_UPDATE,
+ {RECORD_UPDATE,
DIVISIBLE,
BITVECTOR_REPEAT,
BITVECTOR_ZERO_EXTEND,
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<Chain>().getOperator());
-}
-
template <>
uint32_t Op::getIndices() 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>(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;
*/
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
* mkTerm(Kind kind, const std::vector<Term>& 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<Term>& children)
- * Turned into a conjunction of binary applications of the operator on
- * adjoining parameters.
- */
- CHAIN,
/* Boolean --------------------------------------------------------------- */
attribute.cpp
attribute_internals.h
attribute_unique_id.h
- chain.h
emptyset.cpp
emptyset.h
expr_iomanip.cpp
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-
-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 */
+++ /dev/null
-%{
-#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"
return expr;
}
+api::Term Parser::mkChain(api::Kind k, const std::vector<api::Term>& 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<api::Term> 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:
#include <set>
#include <string>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "expr/expr_stream.h"
#include "expr/kind.h"
*/
Expr mkHoApply(Expr expr, std::vector<Expr>& 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<api::Term>& args);
+
/**
* Add an operator to the current legal set.
*
|| 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();
}
}
|| 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();
}
}
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:
case kind::BUILTIN:
out << smtKindString(n.getConst<Kind>(), d_variant);
break;
- case kind::CHAIN_OP:
- out << smtKindString(n.getConst<Chain>().getOperator(), d_variant);
- break;
case kind::CONST_RATIONAL: {
const Rational& r = n.getConst<Rational>();
toStreamRational(
out << smtKindString(k, d_variant) << " ";
parametricTypeChildren = true;
break;
- case kind::CHAIN: break;
case kind::FUNCTION_TYPE:
out << "->";
for (Node nc : n)
// builtin theory
case kind::EQUAL: return "=";
case kind::DISTINCT: return "distinct";
- case kind::CHAIN: break;
case kind::SEXPR: break;
// bool theory
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<Chain>().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;
}
}
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 \
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
#include "theory/builtin/theory_builtin_rewriter.h"
#include "expr/attribute.h"
-#include "expr/chain.h"
#include "expr/node_algorithm.h"
#include "theory/rewriter.h"
return out;
}
-Node TheoryBuiltinRewriter::blastChain(TNode in) {
- Assert(in.getKind() == kind::CHAIN);
-
- Kind chainedOp = in.getOperator().getConst<Chain>().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;
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)
{
{
case kind::DISTINCT:
return RewriteResponse(REWRITE_DONE, blastDistinct(node));
- case kind::CHAIN: return RewriteResponse(REWRITE_DONE, blastChain(node));
default: return RewriteResponse(REWRITE_DONE, node);
}
}
}
}; /* 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<Chain>().getOperator()), check);
- }
-};/* class ChainedOperatorTypeRule */
-
class SortProperties {
public:
inline static bool isWellFounded(TypeNode type) {
; 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)
void testIsNull();
void testOpFromKind();
void testGetIndicesString();
- void testGetIndicesKind();
void testGetIndicesUint();
void testGetIndicesPairUint();
TS_ASSERT_THROWS(record_update_ot.getIndices<uint32_t>(), CVC4ApiException&);
}
-void OpBlack::testGetIndicesKind()
-{
- Op chain_ot = d_solver.mkOp(CHAIN, AND);
- TS_ASSERT(chain_ot.isIndexed());
- Kind chain_idx = chain_ot.getIndices<Kind>();
- TS_ASSERT(chain_idx == AND);
-}
-
void OpBlack::testGetIndicesUint()
{
Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
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)
std::vector<Term> v1 = {d_solver->mkReal(1), d_solver->mkReal(2)};
std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
std::vector<Term> v3 = {};
+ std::vector<Term> 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");
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<Term>& 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()
projects / cvc5.git / commitdiff