From 52ee910c128e6bbcf7299a0660511deacadb14f1 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 5 Nov 2018 09:01:03 -0800
Subject: API: Fix assignment operators (#2680)

The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.

Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.
---
 src/api/cvc4cpp.cpp | 27 ---------------------------
 src/api/cvc4cpp.h   | 23 -----------------------
 2 files changed, 50 deletions(-)

(limited to 'src')

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index be7c5c665..b4d3b013d 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -749,15 +749,6 @@ Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) {}
 
 Sort::~Sort() {}
 
-Sort& Sort::operator=(const Sort& s)
-{
-  if (this != &s)
-  {
-    *d_type = *s.d_type;
-  }
-  return *this;
-}
-
 bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; }
 
 bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; }
@@ -1008,15 +999,6 @@ Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
 
 Term::~Term() {}
 
-Term& Term::operator=(const Term& t)
-{
-  if (this != &t)
-  {
-    *d_expr = *t.d_expr;
-  }
-  return *this;
-}
-
 bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
 
 bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; }
@@ -1180,15 +1162,6 @@ OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
 
 OpTerm::~OpTerm() {}
 
-OpTerm& OpTerm::operator=(const OpTerm& t)
-{
-  if (this != &t)
-  {
-    *d_expr = *t.d_expr;
-  }
-  return *this;
-}
-
 bool OpTerm::operator==(const OpTerm& t) const { return *d_expr == *t.d_expr; }
 
 bool OpTerm::operator!=(const OpTerm& t) const { return *d_expr != *t.d_expr; }
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index fc07a1cd7..aebeffb0d 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -196,13 +196,6 @@ class CVC4_PUBLIC Sort
    */
   ~Sort();
 
-  /**
-   * Assignment operator.
-   * @param s the sort to assign to this sort
-   * @return this sort after assignment
-   */
-  Sort& operator=(const Sort& s);
-
   /**
    * Comparison for structural equality.
    * @param s the sort to compare to
@@ -553,14 +546,6 @@ class CVC4_PUBLIC Term
    */
   ~Term();
 
-  /**
-   * Assignment operator, makes a copy of the given term.
-   * Both terms must belong to the same solver object.
-   * @param t the term to assign
-   * @return the reference to this term after assignment
-   */
-  Term& operator=(const Term& t);
-
   /**
    * Syntactic equality operator.
    * Return true if both terms are syntactically identical.
@@ -843,14 +828,6 @@ class CVC4_PUBLIC OpTerm
    */
   ~OpTerm();
 
-  /**
-   * Assignment operator, makes a copy of the given operator term.
-   * Both terms must belong to the same solver object.
-   * @param t the term to assign
-   * @return the reference to this operator term after assignment
-   */
-  OpTerm& operator=(const OpTerm& t);
-
   /**
    * Syntactic equality operator.
    * Return true if both operator terms are syntactically identical.
-- 
cgit v1.2.3