Introduce a public interface for Sygus commands. (#4204)

This commit addresses issue #38 in cvc4-projects by introducing public API for Sygus commands. It also includes two simple examples of how to use the API.

1 files changed, 119 insertions, 0 deletions

diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h
new file mode 100644
index 000000000..abf37f210
--- /dev/null
+++ b/test/unit/api/grammar_black.h
@@ -0,0 +1,119 @@
+/*********************                                                        */
+/*! \file grammar_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed, Andrew Reynolds
+ ** 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 Black box testing of the guards of the C++ API functions.
+ **
+ ** Black box testing of the guards of the C++ API functions.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+class GrammarBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override;
+  void tearDown() override;
+
+  void testAddRule();
+  void testAddRules();
+  void testAddAnyConstant();
+  void testAddAnyVariable();
+
+ private:
+  std::unique_ptr<Solver> d_solver;
+};
+
+void GrammarBlack::setUp() { d_solver.reset(new Solver()); }
+
+void GrammarBlack::tearDown() {}
+
+void GrammarBlack::testAddRule()
+{
+  Sort boolean = d_solver->getBooleanSort();
+  Sort integer = d_solver->getIntegerSort();
+
+  Term nullTerm;
+  Term start = d_solver->mkVar(boolean);
+  Term nts = d_solver->mkVar(boolean);
+
+  Grammar g = d_solver->mkSygusGrammar({}, {start});
+
+  TS_ASSERT_THROWS_NOTHING(g.addRule(start, d_solver->mkBoolean(false)));
+
+  TS_ASSERT_THROWS(g.addRule(nullTerm, d_solver->mkBoolean(false)),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(start, nullTerm), CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(nts, d_solver->mkBoolean(false)),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(start, d_solver->mkReal(0)), CVC4ApiException&);
+}
+
+void GrammarBlack::testAddRules()
+{
+  Sort boolean = d_solver->getBooleanSort();
+  Sort integer = d_solver->getIntegerSort();
+
+  Term nullTerm;
+  Term start = d_solver->mkVar(boolean);
+  Term nts = d_solver->mkVar(boolean);
+
+  Grammar g = d_solver->mkSygusGrammar({}, {start});
+
+  TS_ASSERT_THROWS_NOTHING(g.addRules(start, {d_solver->mkBoolean(false)}));
+
+  TS_ASSERT_THROWS(g.addRules(nullTerm, {d_solver->mkBoolean(false)}),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(start, {nullTerm}), CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(nts, {d_solver->mkBoolean(false)}),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(start, {d_solver->mkReal(0)}), CVC4ApiException&);
+}
+
+void GrammarBlack::testAddAnyConstant()
+{
+  Sort boolean = d_solver->getBooleanSort();
+
+  Term nullTerm;
+  Term start = d_solver->mkVar(boolean);
+  Term nts = d_solver->mkVar(boolean);
+
+  Grammar g = d_solver->mkSygusGrammar({}, {start});
+
+  TS_ASSERT_THROWS_NOTHING(g.addAnyConstant(start));
+  TS_ASSERT_THROWS_NOTHING(g.addAnyConstant(start));
+
+  TS_ASSERT_THROWS(g.addAnyConstant(nullTerm), CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addAnyConstant(nts), CVC4ApiException&);
+}
+
+void GrammarBlack::testAddAnyVariable()
+{
+  Sort boolean = d_solver->getBooleanSort();
+
+  Term nullTerm;
+  Term x = d_solver->mkVar(boolean);
+  Term start = d_solver->mkVar(boolean);
+  Term nts = d_solver->mkVar(boolean);
+
+  Grammar g1 = d_solver->mkSygusGrammar({x}, {start});
+  Grammar g2 = d_solver->mkSygusGrammar({}, {start});
+
+  TS_ASSERT_THROWS_NOTHING(g1.addAnyVariable(start));
+  TS_ASSERT_THROWS_NOTHING(g1.addAnyVariable(start));
+  TS_ASSERT_THROWS_NOTHING(g2.addAnyVariable(start));
+
+  TS_ASSERT_THROWS(g1.addAnyConstant(nullTerm), CVC4ApiException&);
+  TS_ASSERT_THROWS(g1.addAnyConstant(nts), CVC4ApiException&);
+}