Create Test and Fix error due to no UFManager

Author: refactormyself

src/org/sosy_lab/java_smt/solvers/stp/StpFormulaManager.java

@@ -30,12 +30,13 @@ public final class StpFormulaManager
   @SuppressWarnings("checkstyle:parameternumber")
   protected StpFormulaManager(
       StpFormulaCreator pFormulaCreator,
+      StpUFManager pUFManager,
       StpBooleanFormulaManager pBooleanManager,
       @Nullable StpBitvectorFormulaManager pBitvectorManager,
       @Nullable StpArrayFormulaManager pArrayManager) {
     super(
         pFormulaCreator,
-        null,
+        pUFManager,
         pBooleanManager,
         null,
         null,

src/org/sosy_lab/java_smt/solvers/stp/StpSolverContext.java

@@ -81,13 +81,18 @@ public static StpSolverContext create(
 
     //use the FormulaCreator object to create FormulaManager object for all supported Theories
     StpBooleanFormulaManager booleanFrmMgr = new StpBooleanFormulaManager(formulaCreator);
+    StpUFManager functionFrmMgr = new StpUFManager(formulaCreator);
     StpArrayFormulaManager arrayFrmMgr = new StpArrayFormulaManager(formulaCreator);
     StpBitvectorFormulaManager bitvectorFrmMgr = new StpBitvectorFormulaManager(formulaCreator);
 
-    System.out.println("JUST right before");
     //Create the main FormulaManager to manage all supported Formula types
     StpFormulaManager formulaMgr =
-        new StpFormulaManager(formulaCreator, booleanFrmMgr, bitvectorFrmMgr, arrayFrmMgr);
+        new StpFormulaManager(
+            formulaCreator,
+            functionFrmMgr,
+            booleanFrmMgr,
+            bitvectorFrmMgr,
+            arrayFrmMgr);
 
     //Create the SolverContext with the FormulaCreator and main FormulaManager Objects
     return new StpSolverContext(formulaMgr, formulaCreator, logger);

src/org/sosy_lab/java_smt/solvers/stp/StpSolverTest.java

@@ -0,0 +1,52 @@
+/*
+ *  JavaSMT is an API wrapper for a collection of SMT solvers.
+ *  This file is part of JavaSMT.
+ *
+ *  Copyright (C) 2007-2019  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.stp;
+
+import org.junit.Test;
+import org.sosy_lab.common.ShutdownNotifier;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+import org.sosy_lab.common.log.BasicLogManager;
+import org.sosy_lab.common.log.LogManager;
+import org.sosy_lab.java_smt.SolverContextFactory;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
+import org.sosy_lab.java_smt.api.SolverContext;
+
+public class StpSolverTest {
+
+  @Test
+  public void testSolverContextClass() throws InvalidConfigurationException {
+
+    Configuration config = Configuration.defaultConfiguration();
+    LogManager logger = BasicLogManager.create(config);
+    ShutdownNotifier notifier = ShutdownNotifier.createDummy();
+
+    Solvers solver = Solvers.STP;
+
+    SolverContext context =
+        SolverContextFactory.createSolverContext(config, logger, notifier, solver);
+
+    System.out.println(context.getSolverName() + " ::: " + context.getVersion());
+
+    context.close();
+
+  }
+
+}

src/org/sosy_lab/java_smt/solvers/stp/StpUFManager.java

@@ -0,0 +1,30 @@
+/*
+ *  JavaSMT is an API wrapper for a collection of SMT solvers.
+ *  This file is part of JavaSMT.
+ *
+ *  Copyright (C) 2007-2019  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.stp;
+
+import org.sosy_lab.java_smt.basicimpl.AbstractUFManager;
+
+class StpUFManager extends AbstractUFManager<Long, Long, Long, Long> {
+
+  protected StpUFManager(StpFormulaCreator pCreator) {
+    super(pCreator);
+  }
+
+}