← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to lpsolve/lp_SOS.h

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
lpsolve/lp_SOS.h
1
 
#ifndef HEADER_lp_SOS
2
 
#define HEADER_lp_SOS
3
 
 
4
 
/* Specially Ordered Sets (SOS) prototypes and settings                      */
5
 
/* ------------------------------------------------------------------------- */
6
 
 
7
 
#include "lp_types.h"
8
 
#include "lp_utils.h"
9
 
#include "lp_matrix.h"
10
 
 
11
 
 
12
 
/* SOS constraint defines                                                    */
13
 
/* ------------------------------------------------------------------------- */
14
 
#define SOS1                     1
15
 
#define SOS2                     2
16
 
#define SOS3                    -1
17
 
#define SOSn                      MAXINT32
18
 
#define SOS_START_SIZE          10  /* Start size of SOS_list array; realloced if needed */
19
 
 
20
 
/* Define SOS_is_feasible() return values                                    */
21
 
/* ------------------------------------------------------------------------- */
22
 
#define SOS3_INCOMPLETE         -2
23
 
#define SOS_INCOMPLETE          -1
24
 
#define SOS_COMPLETE             0
25
 
#define SOS_INFEASIBLE           1
26
 
#define SOS_INTERNALERROR        2
27
 
 
28
 
 
29
 
typedef struct _SOSgroup SOSgroup;
30
 
 
31
 
typedef struct _SOSrec
32
 
{
33
 
  SOSgroup  *parent;
34
 
  int       tagorder;
35
 
  char      *name;
36
 
  int       type;
37
 
  MYBOOL    isGUB;
38
 
  int       size;
39
 
  int       priority;
40
 
  int       *members;
41
 
  REAL      *weights;
42
 
  int       *membersSorted;
43
 
  int       *membersMapped;
44
 
} SOSrec;
45
 
 
46
 
/* typedef */ struct _SOSgroup
47
 
{
48
 
  lprec     *lp;                /* Pointer to owner */
49
 
  SOSrec    **sos_list;         /* Array of pointers to SOS lists */
50
 
  int       sos_alloc;          /* Size allocated to specially ordered sets (SOS1, SOS2...) */
51
 
  int       sos_count;          /* Number of specially ordered sets (SOS1, SOS2...) */
52
 
  int       maxorder;           /* The highest-order SOS in the group */
53
 
  int       sos1_count;         /* Number of the lowest order SOS in the group */
54
 
  int       *membership;        /* Array of variable-sorted indeces to SOSes that the variable is member of */
55
 
  int       *memberpos;         /* Starting positions of the each column's membership list */
56
 
} /* SOSgroup */;
57
 
 
58
 
 
59
 
#ifdef __cplusplus
60
 
extern "C" {
61
 
#endif
62
 
 
63
 
/* SOS storage structure */
64
 
STATIC SOSgroup *create_SOSgroup(lprec *lp);
65
 
STATIC void resize_SOSgroup(SOSgroup *group);
66
 
STATIC int append_SOSgroup(SOSgroup *group, SOSrec *SOS);
67
 
STATIC int clean_SOSgroup(SOSgroup *group, MYBOOL forceupdatemap);
68
 
STATIC void free_SOSgroup(SOSgroup **group);
69
 
 
70
 
STATIC SOSrec *create_SOSrec(SOSgroup *group, char *name, int type, int priority, int size, int *variables, REAL *weights);
71
 
STATIC MYBOOL delete_SOSrec(SOSgroup *group, int sosindex);
72
 
STATIC int append_SOSrec(SOSrec *SOS, int size, int *variables, REAL *weights);
73
 
STATIC void free_SOSrec(SOSrec *SOS);
74
 
 
75
 
/* SOS utilities */
76
 
STATIC int make_SOSchain(lprec *lp, MYBOOL forceresort);
77
 
STATIC int SOS_member_updatemap(SOSgroup *group);
78
 
STATIC MYBOOL SOS_member_sortlist(SOSgroup *group, int sosindex);
79
 
STATIC MYBOOL SOS_shift_col(SOSgroup *group, int sosindex, int column, int delta, LLrec *usedmap, MYBOOL forceresort);
80
 
int SOS_member_delete(SOSgroup *group, int sosindex, int member);
81
 
int SOS_get_type(SOSgroup *group, int sosindex);
82
 
int SOS_infeasible(SOSgroup *group, int sosindex);
83
 
int SOS_member_index(SOSgroup *group, int sosindex, int member);
84
 
int SOS_member_count(SOSgroup *group, int sosindex);
85
 
int SOS_memberships(SOSgroup *group, int column);
86
 
int *SOS_get_candidates(SOSgroup *group, int sosindex, int column, MYBOOL excludetarget, REAL *upbound, REAL *lobound);
87
 
int SOS_is_member(SOSgroup *group, int sosindex, int column);
88
 
MYBOOL SOS_is_member_of_type(SOSgroup *group, int column, int sostype);
89
 
MYBOOL SOS_set_GUB(SOSgroup *group, int sosindex, MYBOOL state);
90
 
MYBOOL SOS_is_GUB(SOSgroup *group, int sosindex);
91
 
MYBOOL SOS_is_marked(SOSgroup *group, int sosindex, int column);
92
 
MYBOOL SOS_is_active(SOSgroup *group, int sosindex, int column);
93
 
MYBOOL SOS_is_full(SOSgroup *group, int sosindex, int column, MYBOOL activeonly);
94
 
MYBOOL SOS_can_activate(SOSgroup *group, int sosindex, int column);
95
 
MYBOOL SOS_set_marked(SOSgroup *group, int sosindex, int column, MYBOOL asactive);
96
 
MYBOOL SOS_unmark(SOSgroup *group, int sosindex, int column);
97
 
int SOS_fix_unmarked(SOSgroup *group, int sosindex, int variable, REAL *bound, REAL value,
98
 
                     MYBOOL isupper, int *diffcount, DeltaVrec *changelog);
99
 
int SOS_fix_list(SOSgroup *group, int sosindex, int variable, REAL *bound, 
100
 
                  int *varlist, MYBOOL isleft, DeltaVrec *changelog);
101
 
int SOS_is_satisfied(SOSgroup *group, int sosindex, REAL *solution);
102
 
MYBOOL SOS_is_feasible(SOSgroup *group, int sosindex, REAL *solution);
103
 
 
104
 
#ifdef __cplusplus
105
 
 }
106
 
#endif
107
 
 
108
 
#endif /* HEADER_lp_SOS */