Add portfolio solving. (#185)

This adds a PortfolioSolver that uses threads for the solvers. A future version should use processes instead, as mentioned in #206

CMakeLists.txt

@@ -19,26 +19,27 @@ if (NOT SMT_SWITCH_LIB_TYPE)
   set(SMT_SWITCH_LIB_TYPE SHARED)
 endif()
 
-set(SOURCES
-  "${PROJECT_SOURCE_DIR}/src/ops.cpp"
-  "${PROJECT_SOURCE_DIR}/src/result.cpp"
-  "${PROJECT_SOURCE_DIR}/src/sort.cpp"
-  "${PROJECT_SOURCE_DIR}/src/term.cpp"
-  "${PROJECT_SOURCE_DIR}/src/solver.cpp"
-  "${PROJECT_SOURCE_DIR}/src/solver_enums.cpp"
-  "${PROJECT_SOURCE_DIR}/src/term_translator.cpp"
+set (SOURCES "${SMT_SWITCH_LIB_TYPE}"
+  "${PROJECT_SOURCE_DIR}/include/smtlib_utils.h"
+  "${PROJECT_SOURCE_DIR}/src/generic_solver.cpp"
+  "${PROJECT_SOURCE_DIR}/src/generic_sort.cpp"
+  "${PROJECT_SOURCE_DIR}/src/generic_term.cpp"
   "${PROJECT_SOURCE_DIR}/src/identity_walker.cpp"
-  "${PROJECT_SOURCE_DIR}/src/substitution_walker.cpp"
-  "${PROJECT_SOURCE_DIR}/src/sort_inference.cpp"
-  "${PROJECT_SOURCE_DIR}/src/term_hashtable.cpp"
   "${PROJECT_SOURCE_DIR}/src/logging_sort.cpp"
   "${PROJECT_SOURCE_DIR}/src/logging_term.cpp"
   "${PROJECT_SOURCE_DIR}/src/logging_solver.cpp"
-  "${PROJECT_SOURCE_DIR}/src/generic_solver.cpp"
-  "${PROJECT_SOURCE_DIR}/src/generic_sort.cpp"
-  "${PROJECT_SOURCE_DIR}/src/generic_term.cpp"
+  "${PROJECT_SOURCE_DIR}/src/ops.cpp"
   "${PROJECT_SOURCE_DIR}/src/printing_solver.cpp"
-  "${PROJECT_SOURCE_DIR}/include/smtlib_utils.h"
+  "${PROJECT_SOURCE_DIR}/src/portfolio_solver.cpp"
+  "${PROJECT_SOURCE_DIR}/src/result.cpp"
+  "${PROJECT_SOURCE_DIR}/src/solver_enums.cpp"
+  "${PROJECT_SOURCE_DIR}/src/solver.cpp"
+  "${PROJECT_SOURCE_DIR}/src/sort_inference.cpp"
+  "${PROJECT_SOURCE_DIR}/src/sort.cpp"
+  "${PROJECT_SOURCE_DIR}/src/substitution_walker.cpp"
+  "${PROJECT_SOURCE_DIR}/src/term.cpp"
+  "${PROJECT_SOURCE_DIR}/src/term_hashtable.cpp"
+  "${PROJECT_SOURCE_DIR}/src/term_translator.cpp"
   "${PROJECT_SOURCE_DIR}/src/utils.cpp")
 
 if (SMTLIB_READER)
@@ -80,6 +81,10 @@ include_directories (${INCLUDE_DIRS})
 
 add_library(smt-switch "${SMT_SWITCH_LIB_TYPE}" ${SOURCES})
 
+set(THREADS_PREFER_PTHREAD_FLAG True)
+find_package(Threads)
+target_link_libraries( smt-switch PRIVATE Threads::Threads)
+
 # Should we build python bindings
 option (BUILD_PYTHON_BINDINGS
    "Build Python bindings")

contrib/yices2_instructions.txt

@@ -10,7 +10,7 @@ https://github.com/SRI-CSL/yices2 and place the directory in ./deps.
 Then, build the yices2 library:
 cd deps/yices2
 autoconf
-./configure
+./configure --enable-thread-safety
 make build_dir=build BUILD=build
 
 Now you should be able to build smt-switch with Yices2 as a backend solver by configuring

include/portfolio_solver.h

@@ -0,0 +1,56 @@
+/*********************                                                        */
+/*! \file portfolio_solver.h
+** \verbatim
+** Top contributors (to current version):
+**   Amalee Wilson
+** This file is part of the smt-switch project.
+** Copyright (c) 2021 by the authors listed in the file AUTHORS
+** in the top-level source directory) and their institutional affiliations.
+** All rights reserved.  See the file LICENSE in the top-level source
+** directory for licensing information.\endverbatim
+**
+** \brief Header for a portfolio solving function that takes a vector
+**        of solvers and a term, and returns check_sat from the first solver
+**        that finishes.
+**/
+#pragma once
+
+#include <condition_variable>
+#include <mutex>
+#include <thread>
+
+#include "smt.h"
+
+namespace smt {
+
+class PortfolioSolver
+{
+ public:
+  PortfolioSolver(std::vector<SmtSolver> slvrs, Term trm);
+
+  /** Launch many solvers and return whether the term is satisfiable when one of
+   *  them has finished.
+   *  @param solvers The solvers to run.
+   *  @param t The term to be checked.
+   */
+  smt::Result portfolio_solve();
+
+ private:
+  smt::Result result;
+  std::vector<SmtSolver> solvers;
+  Term portfolio_term;
+  // Once a solver is done, result has been set,
+  // and the main thread can terminate the others.
+  bool a_solver_is_done = false;
+
+  // Used for synchronization.
+  std::mutex m;
+  std::condition_variable cv;
+
+  /** Translate the term t to the solver s, and check_sat.
+   *  @param s The solver to translate the term t to.
+   *  @param t The term being translated to solver s.
+   */
+  void run_solver(SmtSolver s);
+};
+}  // namespace smt

src/portfolio_solver.cpp

@@ -0,0 +1,67 @@
+/*********************                                                        */
+/*! \file portfolio_solver.cpp
+** \verbatim
+** Top contributors (to current version):
+**   Amalee Wilson
+** This file is part of the smt-switch project.
+** Copyright (c) 2021 by the authors listed in the file AUTHORS
+** in the top-level source directory) and their institutional affiliations.
+** All rights reserved.  See the file LICENSE in the top-level source
+** directory for licensing information.\endverbatim
+**
+** \brief Implementation of a portfolio solving function that takes a vector
+**        of solvers and a term, and returns check_sat from the first solver
+**        that finishes.
+**/
+
+#include "portfolio_solver.h"
+
+#include <unistd.h>
+namespace smt {
+
+PortfolioSolver::PortfolioSolver(std::vector<SmtSolver> slvrs, Term trm)
+    : solvers(slvrs), portfolio_term(trm)
+{
+}
+/** Translate the term t to the solver s, and check_sat.
+ *  @param s The solver to translate the term t to.
+ *  @param t The term being translated to solver s.
+ */
+void PortfolioSolver::run_solver(SmtSolver s)
+{
+  TermTranslator to_s(s);
+  Term a = to_s.transfer_term(portfolio_term, smt::BOOL);
+  s->assert_formula(a);
+  result = s->check_sat();
+  std::lock_guard<std::mutex> lk(m);
+  a_solver_is_done = true;
+
+  cv.notify_all();
+}
+
+/** Launch many solvers and return whether the term is satisfiable when one of
+ *  them has finished.
+ *  @param solvers The solvers to run.
+ *  @param t The term to be checked.
+ */
+smt::Result PortfolioSolver::portfolio_solve()
+{
+  // We must maintain a vector of pthreads in order to stop the threads that are
+  // still running once one of the solvers finish because pthreads is assumed to
+  // be the underlying implementation.
+  for (auto s : solvers)
+  {
+    // Start a thread, store its handle, and detach the thread because we are
+    // not interested in waiting for all of them to finish.
+    std::thread t1(&PortfolioSolver::run_solver, this, s);
+    t1.detach();
+  }
+
+  // Wait until a solver is done to cancel the threads that are still running.
+  std::unique_lock<std::mutex> lk(m);
+  while (!a_solver_is_done) cv.wait(lk);
+
+  return result;
+}
+
+}  // namespace smt

tests/CMakeLists.txt

@@ -50,6 +50,10 @@ if (BUILD_YICES2)
   add_subdirectory(yices2)
 endif()
 
+if (${BUILD_YICES2} AND ${BUILD_BTOR} AND ${BUILD_MSAT} AND ${BUILD_CVC4})
+  add_subdirectory(portfolio)
+endif()
+
 if (BUILD_Z3)
   add_subdirectory(z3)
 endif()

tests/portfolio/CMakeLists.txt

@@ -0,0 +1,23 @@
+set(PORTFOLIO_TESTS
+  test-portfolio-solver
+)
+
+foreach(test ${PORTFOLIO_TESTS})
+  add_executable(${test}.out ${test}.cpp)
+  target_include_directories (${test}.out PUBLIC "${PROJECT_SOURCE_DIR}/include")
+  target_link_libraries(${test}.out smt-switch)
+  if (SMT_SWITCH_LIB_TYPE STREQUAL STATIC)
+    # make sure to use the repacked cvc4 static lib if built statically
+    # CVC4 was a special-case for bundling libcvc4.a into libsmt-switch-cvc4.a
+    # see cvc4/CMakeLists.txt from the top-level directory
+    add_dependencies(${test}.out repack-cvc4-static-lib)
+  endif()
+  target_link_libraries(${test}.out smt-switch smt-switch-cvc4)
+  target_link_libraries(${test}.out test-deps)
+  target_link_libraries(${test}.out smt-switch-msat)
+  target_link_libraries(${test}.out smt-switch-msat test-deps)
+  target_link_libraries(${test}.out smt-switch-yices2)
+  target_link_libraries(${test}.out gtest_main)
+  add_test(${test} ${test}.out)
+  # add_test(NAME test_portfolio_solver_test COMMAND test_portfolio_solver)
+endforeach()

tests/portfolio/test-portfolio-solver.cpp

@@ -0,0 +1,117 @@
+/*********************                                                        */
+/*! \file test-generic-solver.cpp
+** \verbatim
+** Top contributors (to current version):
+**   Amalee Wilson
+** This file is part of the smt-switch project.
+** Copyright (c) 2020 by the authors listed in the file AUTHORS
+** in the top-level source directory) and their institutional affiliations.
+** All rights reserved.  See the file LICENSE in the top-level source
+** directory for licensing information.\endverbatim
+**
+** \brief
+**
+**
+**/
+
+#include "assert.h"
+#include "boolector_factory.h"
+#include "cvc4_factory.h"
+#include "msat_factory.h"
+#include "portfolio_solver.h"
+#include "yices2_factory.h"
+
+using namespace smt;
+using namespace std;
+
+int main()
+{
+  cout << "testing portfolio solver" << endl;
+  SmtSolver s = MsatSolverFactory::create(false);
+  s->set_opt("produce-models", "true");
+  Sort bvsort = s->make_sort(BV, 10);
+
+  int pg = 300;
+
+  vector<Term> nts;
+  for (int i = 0; i < pg; ++i)
+  {
+    Term x = s->make_symbol("x" + to_string(i), bvsort);
+    nts.push_back(x);
+  }
+
+  Term ten24 = s->make_term(256, bvsort);
+  vector<Term> neqs;
+  for (int i = 0; i < pg; ++i)
+  {
+    for (int j = 0; j < pg; ++j)
+    {
+      if (i != j)
+      {
+        Term x = s->make_term(Not, s->make_term(Equal, nts[i], nts[j]));
+        neqs.push_back(x);
+      }
+    }
+    Term y = s->make_term(BVSle, nts[i], ten24);
+    neqs.push_back(y);
+  }
+
+  Term test_term = s->make_term(Equal, neqs[0], neqs[0]);
+  for (Term t : neqs)
+  {
+    test_term = s->make_term(And, t, test_term);
+  }
+
+  SmtSolver s1 = MsatSolverFactory::create(false);
+  SmtSolver s2 = MsatSolverFactory::create(false);
+  SmtSolver s3 = MsatSolverFactory::create(false);
+  SmtSolver s4 = BoolectorSolverFactory::create(false);
+  SmtSolver s5 = BoolectorSolverFactory::create(false);
+  SmtSolver s6 = Yices2SolverFactory::create(true);
+  SmtSolver s7 = CVC4SolverFactory::create(false);
+  SmtSolver s8 = CVC4SolverFactory::create(false);
+  SmtSolver s9 = Yices2SolverFactory::create(true);
+  vector<SmtSolver> solvers;
+  solvers.push_back(s1);
+  solvers.push_back(s2);
+  solvers.push_back(s3);
+  solvers.push_back(s4);
+  solvers.push_back(s5);
+  solvers.push_back(s6);
+  solvers.push_back(s7);
+  solvers.push_back(s8);
+  solvers.push_back(s9);
+
+  PortfolioSolver p(solvers, test_term);
+  smt::Result res = p.portfolio_solve();
+  cout << "portfolio_solve " << res.is_sat() << endl;
+
+  assert(res.is_sat());
+
+  SmtSolver s1_2 = MsatSolverFactory::create(false);
+  SmtSolver s2_2 = MsatSolverFactory::create(false);
+  SmtSolver s3_2 = MsatSolverFactory::create(false);
+  SmtSolver s4_2 = BoolectorSolverFactory::create(false);
+  SmtSolver s5_2 = BoolectorSolverFactory::create(false);
+  SmtSolver s6_2 = Yices2SolverFactory::create(true);
+  SmtSolver s7_2 = CVC4SolverFactory::create(false);
+  SmtSolver s8_2 = CVC4SolverFactory::create(false);
+  SmtSolver s9_2 = Yices2SolverFactory::create(true);
+  vector<SmtSolver> solvers2;
+  solvers2.push_back(s1_2);
+  solvers2.push_back(s2_2);
+  solvers2.push_back(s3_2);
+  solvers2.push_back(s4_2);
+  solvers2.push_back(s5_2);
+  solvers2.push_back(s6_2);
+  solvers2.push_back(s7_2);
+  solvers2.push_back(s8_2);
+  solvers2.push_back(s9_2);
+  PortfolioSolver p2(solvers2, test_term);
+  smt::Result res2 = p2.portfolio_solve();
+  cout << "portfolio_solve2 " << res2.is_sat() << endl;
+
+  assert(res2.is_sat());
+
+  return 0;
+}

travis-scripts/setup-yices2.sh

@@ -24,7 +24,7 @@ if [ ! -d "$DEPS/yices2" ]; then
     cd yices2
     git checkout -f $YICES2_VERSION
     autoconf
-    ./configure
+    ./configure --enable-thread-safety
     make build_dir=build BUILD=build -j$NUM_CORES
     cd $DIR
 else

yices2/src/yices2_factory.cpp

@@ -27,9 +27,13 @@ bool initialized = false;
 /* Yices2SolverFactory implementation with logging */
 SmtSolver Yices2SolverFactory::create(bool logging)
 {
-  // Must initialize only once.
+  // Must initialize only once, even if planning to 
+  // create multiple contexts. 
   // Different instances of the solver will have
-  // different contexts.
+  // different contexts. Yices2 must be configured 
+  // with --enable-thread-safety in order for 
+  // multiple threads to manipulate different contexts.
+  // https://github.com/SRI-CSL/yices2#support-for-thread-safety
   if (!initialized)
   {
     yices_init();