From 01e84d511e40604b01328b1e96ecdbe2b818b3c3 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 8 Aug 2019 17:19:05 -0700
Subject: New C++ API: Add checks and tests for Solver::simplify. (#3170)

---
 test/unit/api/solver_black.h | 77 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 77 insertions(+)

(limited to 'test/unit/api/solver_black.h')

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 37eccb94c..3a90f7ed2 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -89,6 +89,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testPop1();
   void testPop2();
   void testPop3();
+  void testSimplify();
 
   void testSetInfo();
   void testSetLogic();
@@ -950,6 +951,82 @@ void SolverBlack::testSetInfo()
   TS_ASSERT_THROWS(d_solver->setInfo("status", "asdf"), CVC4ApiException&);
 }
 
+void SolverBlack::testSimplify()
+{
+  TS_ASSERT_THROWS(d_solver->simplify(Term()), CVC4ApiException&);
+
+  Sort bvSort = d_solver->mkBitVectorSort(32);
+  Sort uSort = d_solver->mkUninterpretedSort("u");
+  Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
+
+  DatatypeDecl consListSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver->getIntegerSort());
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(head);
+  cons.addSelector(tail);
+  consListSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  consListSpec.addConstructor(nil);
+  Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
+
+  Term x = d_solver->mkConst(bvSort, "x");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x));
+  Term a = d_solver->mkConst(bvSort, "a");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(a));
+  Term b = d_solver->mkConst(bvSort, "b");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b));
+  Term x_eq_x = d_solver->mkTerm(EQUAL, x, x);
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x_eq_x));
+  TS_ASSERT(d_solver->mkTrue() != x_eq_x);
+  TS_ASSERT(d_solver->mkTrue() == d_solver->simplify(x_eq_x));
+  Term x_eq_b = d_solver->mkTerm(EQUAL, x, b);
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x_eq_b));
+  TS_ASSERT(d_solver->mkTrue() != x_eq_b);
+  TS_ASSERT(d_solver->mkTrue() != d_solver->simplify(x_eq_b));
+
+  Term i1 = d_solver->mkConst(d_solver->getIntegerSort(), "i1");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i1));
+  Term i2 = d_solver->mkTerm(MULT, i1, d_solver->mkReal("23"));
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i2));
+  TS_ASSERT(i1 != i2);
+  TS_ASSERT(i1 != d_solver->simplify(i2));
+  Term i3 = d_solver->mkTerm(PLUS, i1, d_solver->mkReal(0));
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i3));
+  TS_ASSERT(i1 != i3);
+  TS_ASSERT(i1 == d_solver->simplify(i3));
+
+  Datatype consList = consListSort.getDatatype();
+  Term dt1 = d_solver->mkTerm(
+      APPLY_CONSTRUCTOR,
+      consList.getConstructorTerm("cons"),
+      d_solver->mkReal(0),
+      d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1));
+  Term dt2 = d_solver->mkTerm(
+      APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1);
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt2));
+
+  Term b1 = d_solver->mkVar(bvSort, "b1");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b1));
+  Term b2 = d_solver->mkVar(bvSort, "b1");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b2));
+  Term b3 = d_solver->mkVar(uSort, "b3");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b3));
+  Term v1 = d_solver->mkConst(bvSort, "v1");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(v1));
+  Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(v2));
+  Term f1 = d_solver->mkConst(funSort1, "f1");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f1));
+  Term f2 = d_solver->mkConst(funSort2, "f2");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
+  d_solver->defineFunsRec({f1, f2}, {{b1, b2}, {b3}}, {v1, v2});
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
+}
+
 void SolverBlack::testSetLogic()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->setLogic("AUFLIRA"));
-- 
cgit v1.2.3