1 // Copyright (c) 2017 John Abbott and Anna M. Bigatti
2 // Authors: Anna M. Bigatti, Alberto Griggio
3 // This file is part of the CoCoALib suite of examples.
4 // You are free to use any part of this example in your own programs.
5
6 #include "CoCoA/library.H"
7
8 ///// first prototype
9 #include "CoCoA/ExternalLibs-MathSAT.H"
10
11 using namespace std;
12
13 //----------------------------------------------------------------------
14 const string ShortDescription =
15 "This program shows a prototype for MathSAT communication.\n";
16
17 const string LongDescription =
18 "This program shows the first prototype for MathSAT communication.\n"
19 "The CoCoA class to use is MathSAT::env. \n"
20 "Only linear constraints, defined by matrices or polynomials. \n"
21 "The matrices have n+1 columns: last col is for constants. \n"
22 "The linear polynomials are compared with 0 (eq0, neq0, leq0, lt0).\n";
23
24
25 //----------------------------------------------------------------------
26
27 namespace CoCoA
28 {
29
program()30 void program()
31 {
32 GlobalManager CoCoAFoundations;
33
34 cout << ShortDescription << endl;
35 cout << LongDescription << endl;
36 cout << boolalpha; // so that bools print out as true/false
37
38 #ifndef CoCoA_WITH_MATHSAT
39 cout << "MathSAT library is not available to CoCoALib." << endl;
40 #else // MathSAT is available
41
42 ring QQ = RingQQ();
43
44 ring P = NewPolyRing(QQ, symbols("x,y"));
45 RingElem x(P,"x"), y(P,"y");
46
47 cout << " --------------------------------------" << endl
48 << " -- add the constraints via polynomials"
49 << endl;
50
51 // create a MathSAT environment: E
52 MathSAT::env E;
53
54 // polynomial syntax:
55 MathSAT::AddLeq0(E, x-9); // x -9 <= 0
56 MathSAT::AddEq0(E, x -y); // x -y = 0
57 MathSAT::AddLt0(E, 2*x -1); // 2*x -1 < 0
58
59 cout << "A solution is " << MathSAT::LinSolve(E) << endl; //-> 0, 0
60
61 cout << " ------------------------------------" << endl
62 << " -- add more constraints via matrices"
63 << endl;
64
65 matrix M = NewDenseMat(QQ, 2, 3); // (2x3 matrix)
66 SetEntry(M,0,0, 3); SetEntry(M,0,1, 1); SetEntry(M,0,2, -2);
67 SetEntry(M,1,0, 1); SetEntry(M,1,1, -1); SetEntry(M,1,2, 0);
68 MathSAT::AddLeq0(E, M); // 3*x -y -2 <= 0
69 // x -y <= 0
70 M = NewDenseMat(QQ, 1, 3); SetEntry(M,0,0, 1); // (1x3 matrix)
71 MathSAT::AddNeq0(E, M); // x != 0
72
73 cout << "A solution is " << MathSAT::LinSolve(E) << endl; //-> 1/4, 1/4
74
75 #endif // CoCoA_WITH_MATHSAT
76 }
77
78
79
80
81 } // end of namespace CoCoA
82
83 //----------------------------------------------------------------------
84 // Use main() to handle any uncaught exceptions and warn the user about them.
main()85 int main()
86 {
87 try
88 {
89 CoCoA::program();
90 return 0;
91 }
92 catch (const CoCoA::ErrorInfo& err)
93 {
94 cerr << "***ERROR*** UNCAUGHT CoCoA error";
95 ANNOUNCE(cerr, err);
96 }
97 catch (const std::exception& exc)
98 {
99 cerr << "***ERROR*** UNCAUGHT std::exception: " << exc.what() << endl;
100 }
101 catch(...)
102 {
103 cerr << "***ERROR*** UNCAUGHT UNKNOWN EXCEPTION" << endl;
104 }
105
106 CoCoA::BuildInfo::PrintAll(cerr);
107 return 1;
108 }
109
110 //----------------------------------------------------------------------
111 // RCS header/log in the next few lines
112 // $Header: /Volumes/Home_1/cocoa/cvs-repository/CoCoALib-0.99/examples/ex-MathSat1.C,v 1.7 2019/09/16 14:38:52 abbott Exp $
113 // $Log: ex-MathSat1.C,v $
114 // Revision 1.7 2019/09/16 14:38:52 abbott
115 // Summary: Removed useless include of gmpxx.h
116 //
117 // Revision 1.6 2017/12/15 16:03:22 bigatti
118 // -- polished examples
119 //
120 // Revision 1.5 2017/08/08 14:22:20 bigatti
121 // -- updated example (after SC2 worshop 2017)
122 //
123 // Revision 1.4 2017/07/14 09:31:15 bigatti
124 // -- new class MathSAT::env. Consequent changes
125 //
126 // Revision 1.3 2017/07/13 16:21:39 bigatti
127 // -- three MathSAT examples, following the development of the interface
128 //
129 // Revision 1.2 2017/07/12 16:44:53 bigatti
130 // -- developed experimental code for MathSat and moved it from example
131 // to ExternalLib-MathSAT.[CH]
132 //
133 // Revision 1.1 2017/02/24 08:19:39 bigatti
134 // -- first import
135