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.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index be7c5c665a74f5929850a90269561f1081b148aa..b4d3b013dfcd86aa32b1805a8a3c00b46dda314e 100644 (file)
--- 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 fc07a1cd7cccf669ff892685309e1da2e19f8344..aebeffb0df545d986802c801acc5612f0e56f194 100644 (file)
--- 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.

diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 90d34f7c6a8ba4d052ca11e651d77cd95b483af3..025575e41bc1c6d1fb1e927f62593d5d91cfb87d 100644 (file)
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -2,3 +2,4 @@
 # Add unit tests
 
 cvc4_add_unit_test_black(api_guards_black api)
+cvc4_add_unit_test_black(term_black api)

diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
new file mode 100644 (file)
index 0000000..c2ca1cb
--- /dev/null
+++ b/test/unit/api/term_black.h
@@ -0,0 +1,37 @@
+/*********************                                                        */
+/*! \file term_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** 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 Black box testing of the Term class
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+class TermBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override {}
+  void tearDown() override {}
+
+  void testTermAssignment()
+  {
+    Term t1 = d_solver.mkReal(1);
+    Term t2 = t1;
+    t2 = d_solver.mkReal(2);
+    TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
+  }
+
+ private:
+  Solver d_solver;
+};