sypet-non-incremental/src/edu/utexas/sypet/synthesis/sat4j/Constraint.java

   1 /*
   2  * Copyright (C) 2017 The SyPet Authors
   3  *
   4  * Licensed under the Apache License, Version 2.0 (the "License");
   5  * you may not use this file except in compliance with the License.
   6  * You may obtain a copy of the License at
   7  *
   8  * http://www.apache.org/licenses/LICENSE-2.0
   9  *
  10  * Unless required by applicable law or agreed to in writing, software
  11  * distributed under the License is distributed on an "AS IS" BASIS,
  12  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  13  * See the License for the specific language governing permissions and
  14  * limitations under the License.
  15  */
  16 package edu.utexas.sypet.synthesis.sat4j;
  17
  18 import java.util.ArrayList;
  19 import java.util.List;
  20
  21 public class Constraint {
  22
  23         public static enum ConstraintType {
  24                 LEQ, GEQ, EQ
  25         }
  26
  27         public static enum EncodingType {
  28                 INIT, GOAL, ONE_TRANSACTION, FIRE_TRANSACTION, FRAME_AXIOMS
  29         }
  30
  31         /**
  32          * Members of Encoding class
  33          */
  34         protected List<Variable> literals;
  35         protected List<Integer> coefficients;
  36         protected ConstraintType type;
  37         protected Integer rhs;
  38         protected EncodingType enctype;
  39
  40         /**
  41          * Constructors
  42          */
  43         public Constraint(List<Variable> literals, List<Integer> coefficients, ConstraintType type, Integer rhs){
  44                 for(Variable v : literals) {
  45                         assert v != null;
  46                 }
  47                 this.literals = literals;
  48                 this.coefficients = coefficients;
  49                 this.type = type;
  50                 this.rhs = rhs;
  51         }
  52
  53         public Constraint(List<Variable> literals, List<Integer> coefficients, ConstraintType type, Integer rhs, EncodingType enctype){
  54                 for(Variable v : literals) {
  55                         assert v != null;
  56                 }
  57                 this.literals = literals;
  58                 this.coefficients = coefficients;
  59                 this.type = type;
  60                 this.rhs = rhs;
  61                 this.enctype = enctype;
  62         }
  63
  64
  65         public Constraint(List<Variable> literals, ConstraintType type, Integer rhs){
  66                 for(Variable v : literals) {
  67                         assert v != null;
  68                 }
  69                 this.literals = literals;
  70                 this.type = type;
  71
  72                 coefficients = new ArrayList<Integer>();
  73                 for (int i = 0; i < literals.size(); i++)
  74                         coefficients.add(1);
  75
  76                 this.rhs = rhs;
  77         }
  78
  79         public Constraint(List<Variable> literals, ConstraintType type, Integer rhs, EncodingType enctype){
  80                 for(Variable v : literals) {
  81                         assert v != null;
  82                 }
  83                 this.literals = literals;
  84                 this.type = type;
  85                 this.enctype = enctype;
  86
  87                 coefficients = new ArrayList<Integer>();
  88                 for (int i = 0; i < literals.size(); i++)
  89                         coefficients.add(1);
  90
  91                 this.rhs = rhs;
  92         }
  93
  94         public Constraint(){
  95                 this.literals = new ArrayList<Variable>();
  96                 this.coefficients = new ArrayList<Integer>();
  97                 this.type = ConstraintType.GEQ;
  98                 this.rhs = 0;
  99         }
 100
 101         /**
 102          * Public methods
 103          */
 104         public void addLiteral(Variable v, int coeff){
 105                 literals.add(v);
 106                 coefficients.add(coeff);
 107         }
 108
 109         public List<Variable> getLiterals(){
 110                 return literals;
 111         }
 112
 113         public List<Integer> getCoefficients(){
 114                 return coefficients;
 115         }
 116
 117         public ConstraintType getType(){
 118                 return type;
 119         }
 120
 121         public int getRhs(){
 122                 return rhs;
 123         }
 124
 125         public void setRhs(int rhs){
 126                 this.rhs = rhs;
 127         }
 128
 129         public void setType(ConstraintType type){
 130                 this.type = type;
 131         }
 132
 133         public int getSize(){
 134                 return literals.size();
 135         }
 136
 137         public EncodingType getEncodingType(){
 138                 return enctype;
 139         }
 140
 141         public void print(){
 142                 assert (literals.size() == coefficients.size());
 143                 int pos = 0;
 144                 for (Variable v : literals){
 145                         System.out.print(coefficients.get(pos) + " x" + (v.getSolverId()+1) + " [" + v.toString() + "] ");
 146                         pos++;
 147                 }
 148                 if(type == ConstraintType.EQ)
 149                         System.out.print("=");
 150                 else if (type == ConstraintType.GEQ)
 151                         System.out.print(">=");
 152                 else if (type == ConstraintType.LEQ)
 153                         System.out.print("<=");
 154
 155                 System.out.println(" " + rhs);
 156         }
 157 }