-/********************* */
-/*! \file normal_form.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King, Morgan Deters, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 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_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H
-#define __CVC4__THEORY__ARITH__NORMAL_FORM_H
+/******************************************************************************
+ * Top contributors (to current version):
+ * Tim King, Morgan Deters, Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__ARITH__NORMAL_FORM_H
+#define CVC5__THEORY__ARITH__NORMAL_FORM_H
#include <algorithm>
-#include <list>
#include "base/output.h"
#include "expr/node.h"
#include "theory/arith/delta_rational.h"
#include "util/rational.h"
-
-namespace CVC4 {
+namespace cvc5 {
namespace theory {
namespace arith {
class Variable : public NodeWrapper {
public:
- Variable(Node n) : NodeWrapper(n) {
- Assert(isMember(getNode()));
- }
-
- // TODO: check if it's a theory leaf also
- static bool isMember(Node n) {
- Kind k = n.getKind();
- switch(k){
- case kind::CONST_RATIONAL:
- return false;
- case kind::INTS_DIVISION:
- case kind::INTS_MODULUS:
- case kind::DIVISION:
- case kind::INTS_DIVISION_TOTAL:
- case kind::INTS_MODULUS_TOTAL:
- case kind::DIVISION_TOTAL:
- return isDivMember(n);
- case kind::EXPONENTIAL:
- case kind::SINE:
- case kind::COSINE:
- case kind::TANGENT:
- case kind::COSECANT:
- case kind::SECANT:
- case kind::COTANGENT:
- case kind::ARCSINE:
- case kind::ARCCOSINE:
- case kind::ARCTANGENT:
- case kind::ARCCOSECANT:
- case kind::ARCSECANT:
- case kind::ARCCOTANGENT:
- case kind::SQRT:
- case kind::PI:
- return isTranscendentalMember(n);
- case kind::ABS:
- case kind::TO_INTEGER:
- // Treat to_int as a variable; it is replaced in early preprocessing
- // by a variable.
- return true;
- default:
- return isLeafMember(n);
- }
- }
+ Variable(Node n) : NodeWrapper(n) { Assert(isMember(getNode())); }
+
+ // TODO: check if it's a theory leaf also
+ static bool isMember(Node n)
+ {
+ Kind k = n.getKind();
+ switch (k)
+ {
+ case kind::CONST_RATIONAL: return false;
+ case kind::INTS_DIVISION:
+ case kind::INTS_MODULUS:
+ case kind::DIVISION:
+ case kind::INTS_DIVISION_TOTAL:
+ case kind::INTS_MODULUS_TOTAL:
+ case kind::DIVISION_TOTAL: return isDivMember(n);
+ case kind::IAND: return isIAndMember(n);
+ case kind::POW2: return isPow2Member(n);
+ case kind::EXPONENTIAL:
+ case kind::SINE:
+ case kind::COSINE:
+ case kind::TANGENT:
+ case kind::COSECANT:
+ case kind::SECANT:
+ case kind::COTANGENT:
+ case kind::ARCSINE:
+ case kind::ARCCOSINE:
+ case kind::ARCTANGENT:
+ case kind::ARCCOSECANT:
+ case kind::ARCSECANT:
+ case kind::ARCCOTANGENT:
+ case kind::SQRT:
+ case kind::PI: return isTranscendentalMember(n);
+ case kind::ABS:
+ case kind::TO_INTEGER:
+ // Treat to_int as a variable; it is replaced in early preprocessing
+ // by a variable.
+ return true;
+ default: return isLeafMember(n);
+ }
+ }
static bool isLeafMember(Node n);
+ static bool isIAndMember(Node n);
+ static bool isPow2Member(Node n);
static bool isDivMember(Node n);
bool isDivLike() const{
return isDivMember(getNode());
if(n < m){
return -1;
}else{
- Assert( n != m );
+ Assert(n != m);
return 1;
}
}else{
size_t getComplexity() const;
};/* class Variable */
-
class Constant : public NodeWrapper {
public:
- Constant(Node n) : NodeWrapper(n) {
- Assert(isMember(getNode()));
- }
+ Constant(Node n) : NodeWrapper(n) { Assert(isMember(getNode())); }
- static bool isMember(Node n) {
- return n.getKind() == kind::CONST_RATIONAL;
- }
+ static bool isMember(Node n) { return n.getKind() == kind::CONST_RATIONAL; }
- bool isNormalForm() { return isMember(getNode()); }
+ bool isNormalForm() { return isMember(getNode()); }
- static Constant mkConstant(Node n) {
- Assert(n.getKind() == kind::CONST_RATIONAL);
- return Constant(n);
- }
+ static Constant mkConstant(Node n)
+ {
+ Assert(n.getKind() == kind::CONST_RATIONAL);
+ return Constant(n);
+ }
static Constant mkConstant(const Rational& rat);
template <class GetNodeIterator>
inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
- NodeBuilder<> nb(k);
+ NodeBuilder nb(k);
while(start != end) {
nb << (*start).getNode();
public:
- class iterator : public std::iterator<std::input_iterator_tag, Variable> {
+ class iterator {
private:
internal_iterator d_iter;
public:
+ /* The following types are required by trait std::iterator_traits */
+
+ /** Iterator tag */
+ using iterator_category = std::forward_iterator_tag;
+
+ /** The type of the item */
+ using value_type = Variable;
+
+ /** The pointer type of the item */
+ using pointer = Variable*;
+
+ /** The reference type of the item */
+ using reference = Variable&;
+
+ /** The type returned when two iterators are subtracted */
+ using difference_type = std::ptrdiff_t;
+
+ /* End of std::iterator_traits required types */
+
explicit iterator(internal_iterator i) : d_iter(i) {}
inline Variable operator*() {
Monomial(Node n, const Constant& c, const VarList& vl):
NodeWrapper(n), constant(c), varList(vl)
{
- Assert(!c.isZero() || vl.empty() );
- Assert( c.isZero() || !vl.empty() );
+ Assert(!c.isZero() || vl.empty());
+ Assert(c.isZero() || !vl.empty());
Assert(!c.isOne() || !multStructured(n));
}
Monomial(const VarList& vl):
NodeWrapper(vl.getNode()), constant(Constant::mkConstant(1)), varList(vl)
{
- Assert( !varList.empty() );
+ Assert(!varList.empty());
}
Monomial(const Constant& c, const VarList& vl):
NodeWrapper(makeMultNode(c,vl)), constant(c), varList(vl)
{
- Assert( !c.isZero() );
- Assert( !c.isOne() );
- Assert( !varList.empty() );
+ Assert(!c.isZero());
+ Assert(!c.isOne());
+ Assert(!varList.empty());
Assert(multStructured(getNode()));
}
public:
static bool isMember(TNode n);
- class iterator : public std::iterator<std::input_iterator_tag, Monomial> {
+ class iterator {
private:
internal_iterator d_iter;
public:
+ /* The following types are required by trait std::iterator_traits */
+
+ /** Iterator tag */
+ using iterator_category = std::forward_iterator_tag;
+
+ /** The type of the item */
+ using value_type = Monomial;
+
+ /** The pointer type of the item */
+ using pointer = Monomial*;
+
+ /** The reference type of the item */
+ using reference = Monomial&;
+
+ /** The type returned when two iterators are subtracted */
+ using difference_type = std::ptrdiff_t;
+
+ /* End of std::iterator_traits required types */
+
explicit iterator(internal_iterator i) : d_iter(i) {}
inline Monomial operator*() {
Polynomial(const std::vector<Monomial>& m):
NodeWrapper(makePlusNode(m)), d_singleton(false)
{
- Assert( m.size() >= 2);
- Assert( Monomial::isStrictlySorted(m) );
+ Assert(m.size() >= 2);
+ Assert(Monomial::isStrictlySorted(m));
}
static Polynomial mkPolynomial(const Constant& c){
}
Polynomial getTail() const {
- Assert(! singleton());
+ Assert(!singleton());
iterator tailStart = begin();
++tailStart;
/** Returns true if the polynomial contains a non-linear monomial.*/
bool isNonlinear() const;
+ /** Check whether this polynomial is only a single variable. */
+ bool isVariable() const
+ {
+ return singleton() && getHead().getVarList().singleton()
+ && getHead().coefficientIsOne();
+ }
+ /** Return the variable, given that isVariable() holds. */
+ Variable getVariable() const
+ {
+ Assert(isVariable());
+ return getHead().getVarList().getHead();
+ }
/**
* Selects a minimal monomial in the polynomial by the absolute value of
return NodeManager::currentNM()->mkNode(kind::PLUS, p.getNode(), c.getNode());
}
- SumPair(TNode n) :
- NodeWrapper(n)
- {
- Assert(isNormalForm());
- }
-
-public:
+ SumPair(TNode n) : NodeWrapper(n) { Assert(isNormalForm()); }
+ public:
SumPair(const Polynomial& p):
NodeWrapper(toNode(p, Constant::mkConstant(0)))
{
Polynomial normalizedVariablePart() const;
DeltaRational normalizedDeltaRational() const;
+ /**
+ * Transforms a Comparison object into a stronger normal form:
+ * Polynomial ~Kind~ Constant
+ *
+ * From the comparison, this method resolved a negation (if present) and
+ * moves everything to the left side.
+ * If split_constant is false, the constant is always zero.
+ * If split_constant is true, the polynomial has no constant term and is
+ * normalized to have leading coefficient one.
+ */
+ std::tuple<Polynomial, Kind, Constant> decompose(
+ bool split_constant = false) const;
+
};/* class Comparison */
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace arith
+} // namespace theory
+} // namespace cvc5
-#endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */
+#endif /* CVC5__THEORY__ARITH__NORMAL_FORM_H */
projects / cvc5.git / blobdiff