Recent

Author Topic: Lazarus + Cryptominisat + Linux + Windows  (Read 1522 times)

benbar

  • Newbie
  • Posts: 1
Lazarus + Cryptominisat + Linux + Windows
« on: June 20, 2018, 10:13:56 pm »
Hi all,
I am new in this Forum, but I have used Lazarus for approx 8 years (under linux and windows). I would like to program a simple GUI (something like a time-table) which encodes a problem in CNF, calls another program called Cryptominisat to solve the problem, and then constructs and shows the time-table.

I've already implemented the program in:
JAVA --> Worked, but I could not integrate Cryptominisat, so I had to work with files to communicate with Cryptominisat. And not all users are allowed to install JAVA on their PCs.
QT --> Worked, but I was not able to cross compile for windows and I was not able to create a single executable in Linux.

What I want:
- integration of Cryptominisat (https://github.com/msoos/cryptominisat)
- single executable in windows
- single executable in linux

Is this possible and how would I call/convert these lines?
Code: Pascal  [Select][+][-]
  1. #include <cryptominisat5/cryptominisat.h>
  2. #include <assert.h>
  3. #include <vector>
  4. using std::vector;
  5. using namespace CMSat;
  6.  
  7. int main()
  8. {
  9.     SATSolver solver;
  10.     vector<Lit> clause;
  11.  
  12.     //Let's use 4 threads
  13.     solver.set_num_threads(4);
  14.  
  15.     //We need 3 variables
  16.     solver.new_vars(3);
  17.  
  18.     //adds "1 0"
  19.     clause.push_back(Lit(0, false));
  20.     solver.add_clause(clause);
  21.  
  22.     //adds "-2 0"
  23.     clause.clear();
  24.     clause.push_back(Lit(1, true));
  25.     solver.add_clause(clause);
  26.  
  27.     //adds "-1 2 3 0"
  28.     clause.clear();
  29.     clause.push_back(Lit(0, true));
  30.     clause.push_back(Lit(1, false));
  31.     clause.push_back(Lit(2, false));
  32.     solver.add_clause(clause);
  33.  
  34.     lbool ret = solver.solve();
  35.     assert(ret == l_True);
  36.     assert(solver.get_model()[0] == l_True);
  37.     assert(solver.get_model()[1] == l_False);
  38.     assert(solver.get_model()[2] == l_True);
  39.     std::cout
  40.     << "Solution is: "
  41.     << solver.get_model()[0]
  42.     << ", " << solver.get_model()[1]
  43.     << ", " << solver.get_model()[2]
  44.     << std::endl;
  45.  
  46.     return 0;
  47. }
  48.  

Thank you for your time

 

TinyPortal © 2005-2018