Project

General

Profile

Design #1091

ExternaLib-MathSAT: (first) prototype CoCoA-5 interface for MathSAT

Added by Anna Maria Bigatti about 7 years ago. Updated over 6 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Anna Maria Bigatti
Category:
CoCoA-5 function: new
Target version:
CoCoA-5.2.2
Start date:
13 Jul 2017
Due date:
% Done:

100%

Estimated time:
8.01 h
Spent time:
7.00 h

Related issues

Related to CoCoALib - Feature #1090: ExternaLib-MathSAT: first prototypeClosed2017-07-122017-07-29

History

#1 Updated by Anna Maria Bigatti about 7 years ago

  • % Done changed from 0 to 40
  • Estimated time set to 16.00 h

First prototype working, very naive implementation

/**/ M := mat([[1,9],[2,5]]);   L := [123,456];
/**/ LinSolve(M, ColMat(L));
matrix(QQ,
 [[3489/13],
  [-210/13]])
/**/ MSatLinSolve(record[eq := ConcatHor(M, ColMat(L))]);
matrix(QQ,
 [[3489/13],
  [-210/13]])

Now I have to make it working for 3x3 matrices ;-)
Need some data type designing....

#2 Updated by Anna Maria Bigatti about 7 years ago

  • % Done changed from 40 to 60
MSatLinSolve(record[leq := matrix([[1,2,3, 4],  --   x1 +2*x2 +3*x3 <= 4
                                   [9,8,7, 0]]),-- 9*x1 +8*x2 +7*x3 <= 0
            eq :=  RowMat([1,0,0, 0]),  -- x1 = 0
            lt :=  RowMat([0,1,0, 0])   -- x2 < 0
            ]);

gives
matrix(QQ,
 [[0],
  [-14/5],
  [16/5]])

#3 Updated by Anna Maria Bigatti about 7 years ago

  • Related to Feature #1090: ExternaLib-MathSAT: first prototype added

#4 Updated by Anna Maria Bigatti about 7 years ago

  • Status changed from New to In Progress

#5 Updated by Anna Maria Bigatti over 6 years ago

  • Subject changed from ExternaLib-MathSAT: prototype CoCoA-5 interface for MathSAT to ExternaLib-MathSAT: (first) prototype CoCoA-5 interface for MathSAT
  • Status changed from In Progress to Closed
  • % Done changed from 60 to 100
  • Estimated time changed from 16.00 h to 8.01 h

Also available in: Atom PDF