from abc import ABCMeta, abstractmethod

class Solver:
  __metaclass__ = ABCMeta

  @abstractmethod
  def __init__(self):
    pass

  @abstractmethod
  def __del__(self):
    pass

  @abstractmethod
  def are_equal_expr(self, a, b):
    pass
  
  @abstractmethod
  def true(self):
    pass
  
  @abstractmethod
  def false(self):
    pass
  
  # integer constants
  @abstractmethod
  def num(self, n):
    pass
  
  # real constants
  @abstractmethod
  def real(self, n):
    pass
  
  # boolean variable with name
  @abstractmethod
  def boolvar(self, n):
    pass
  
  # integer variable with name
  @abstractmethod
  def intvar(self, n):
    pass
  
  # real variable with name
  @abstractmethod
  def realvar(self, n):
    pass
  
  # logical conjunction
  @abstractmethod
  def land(self, l):
    pass

  # logical disjunction
  @abstractmethod
  def lor(self, l):
    pass

  # logical negation
  @abstractmethod
  def neg(self, a):
    pass

  # logical implication
  @abstractmethod
  def implies(self, a, b):
    pass

  # logical biimplication
  @abstractmethod
  def iff(self, a, b):
    pass

  # equality of arithmetic terms
  @abstractmethod
  def eq(self, a, b):
    pass

  # less-than on arithmetic terms
  @abstractmethod
  def lt(self, a, b):
    pass

  # greater-or-equal on arithmetic terms
  @abstractmethod
  def ge(self, a, b):
    pass

  # increment of arithmetic term by 1
  @abstractmethod
  def inc(self, a):
    pass
  
  # subtraction
  @abstractmethod
  def minus(self, a, b):
    pass

  # addition
  @abstractmethod
  def plus(self, a, b):
    pass

  # multiplication
  @abstractmethod
  def mult(self, a, b):
    pass

  # if-then-else
  @abstractmethod
  def ite(self, cond, a, b):
    pass

  # minimum of two arithmetic expressions
  def min(self, a, b):
    if self.are_equal_expr(a, b):
      return a
    return self.ite(self.lt(a, b), a, b)

  # maximum of two arithmetic expressions
  def max(self, a, b):
    return self.ite(self.gt(a, b), a, b)

  @abstractmethod
  def exists(self, x, e):
    pass

  @abstractmethod
  def subst(self, vars, terms, e):
    pass

  # term inspection
  @abstractmethod
  def num_args(self, e):
    pass

  @abstractmethod
  def arg(self, e, i):
    pass

  @abstractmethod
  def is_true(self, e):
    pass

  @abstractmethod
  def is_false(self, e):
    pass

  @abstractmethod
  def is_int(self, e):
    pass

  @abstractmethod
  def is_real(self, e):
    pass

  def is_numeric(self, e):
    return self.is_int(e) or self.is_real(e)

  @abstractmethod
  def numeric_value(self, e):
    pass

  @abstractmethod
  def is_var(self, e):
    pass

  @abstractmethod
  def is_not(self, e):
    pass

  @abstractmethod
  def is_and(self, e):
    pass

  @abstractmethod
  def is_or(self, e):
    pass

  @abstractmethod
  def is_eq(self, e):
    pass

  @abstractmethod
  def is_le(self, e):
    pass

  @abstractmethod
  def is_lt(self, e):
    pass

  @abstractmethod
  def is_ge(self, e):
    pass

  @abstractmethod
  def is_gt(self, e):
    pass

  @abstractmethod
  def is_plus(self, e):
    pass

  @abstractmethod
  def is_minus(self, e):
    pass

  @abstractmethod
  def is_mult(self, e):
    pass


  # whether two arithmetic expressions are equivalent
  @abstractmethod
  def equivalent(self, a, b):
    pass

  @abstractmethod
  def push(self):
    pass

  @abstractmethod
  def pop(self):
    pass

  @abstractmethod
  def simplify(self, e):
    pass

  @abstractmethod
  def qe_simp(self, e):
    pass

  # add list of assertions
  @abstractmethod
  def require(self):
    pass

  # check satisfiability
  @abstractmethod
  def check_sat(self, e, eval=None):
    pass

  # minimize given expression
  @abstractmethod
  def minimize(self, e):
    pass

  # reset context
  @abstractmethod
  def reset(self):
    pass


class Model:
  __metaclass__ = ABCMeta

  @abstractmethod
  def __init__(self):
      pass
  
  @abstractmethod
  def eval_bool(self, v):
    pass
  
  @abstractmethod
  def eval_int(self, v):
    pass
  
  @abstractmethod
  def eval_real(self, v):
    pass

  @abstractmethod
  def destroy(self):
    pass
  