src/api/python/cvc5.pxi

   1 from collections import defaultdict
   2 from fractions import Fraction
   3 import sys
   4
   5 from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
   6
   7 from libcpp.pair cimport pair
   8 from libcpp.set cimport set
   9 from libcpp.string cimport string
  10 from libcpp.vector cimport vector
  11
  12 from cvc5 cimport cout
  13 from cvc5 cimport Datatype as c_Datatype
  14 from cvc5 cimport DatatypeConstructor as c_DatatypeConstructor
  15 from cvc5 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl
  16 from cvc5 cimport DatatypeDecl as c_DatatypeDecl
  17 from cvc5 cimport DatatypeSelector as c_DatatypeSelector
  18 from cvc5 cimport Result as c_Result
  19 from cvc5 cimport RoundingMode as c_RoundingMode
  20 from cvc5 cimport Op as c_Op
  21 from cvc5 cimport Solver as c_Solver
  22 from cvc5 cimport Grammar as c_Grammar
  23 from cvc5 cimport Sort as c_Sort
  24 from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
  25 from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
  26 from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
  27 from cvc5 cimport Term as c_Term
  28 from cvc5 cimport hash as c_hash
  29
  30 from cvc5kinds cimport Kind as c_Kind
  31
  32 ################################## DECORATORS #################################
  33 def expand_list_arg(num_req_args=0):
  34     '''
  35     Creates a decorator that looks at index num_req_args of the args,
  36     if it's a list, it expands it before calling the function.
  37     '''
  38     def decorator(func):
  39         def wrapper(owner, *args):
  40             if len(args) == num_req_args + 1 and \
  41                isinstance(args[num_req_args], list):
  42                 args = list(args[:num_req_args]) + args[num_req_args]
  43             return func(owner, *args)
  44         return wrapper
  45     return decorator
  46 ###############################################################################
  47
  48 # Style Guidelines
  49 ### Using PEP-8 spacing recommendations
  50 ### Limit linewidth to 79 characters
  51 ### Break before binary operators
  52 ### surround top level functions and classes with two spaces
  53 ### separate methods by one space
  54 ### use spaces in functions sparingly to separate logical blocks
  55 ### can omit spaces between unrelated oneliners
  56 ### always use c++ default arguments
  57 #### only use default args of None at python level
  58
  59 # References and pointers
  60 # The Solver object holds a pointer to a c_Solver.
  61 # This is because the assignment operator is deleted in the C++ API for solvers.
  62 # Cython has a limitation where you can't stack allocate objects
  63 # that have constructors with arguments:
  64 # https://groups.google.com/forum/#!topic/cython-users/fuKd-nQLpBs.
  65 # To get around that you can either have a nullary constructor and assignment
  66 # or, use a pointer (which is what we chose).
  67 # An additional complication of this is that to free up resources, you must
  68 # know when to delete the object.
  69 # Python will not follow the same scoping rules as in C++, so it must be
  70 # able to reference count. To do this correctly, the solver must be a
  71 # reference in the Python class for any class that keeps a pointer to
  72 # the solver in C++ (to ensure the solver is not deleted before something
  73 # that depends on it).
  74
  75
  76 ## Objects for hashing
  77 cdef c_hash[c_Op] cophash = c_hash[c_Op]()
  78 cdef c_hash[c_Sort] csorthash = c_hash[c_Sort]()
  79 cdef c_hash[c_Term] ctermhash = c_hash[c_Term]()
  80
  81
  82 cdef class Datatype:
  83     """Wrapper class for :cpp:class:`cvc5::api::Datatype`."""
  84     cdef c_Datatype cd
  85     cdef Solver solver
  86     def __cinit__(self, Solver solver):
  87         self.solver = solver
  88
  89     def __getitem__(self, index):
  90         """Return a constructor by index or by name."""
  91         cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
  92         if isinstance(index, int) and index >= 0:
  93             dc.cdc = self.cd[(<int?> index)]
  94         elif isinstance(index, str):
  95             dc.cdc = self.cd[(<const string &> index.encode())]
  96         else:
  97             raise ValueError("Expecting a non-negative integer or string")
  98         return dc
  99
 100     def getConstructor(self, str name):
 101         """Return a constructor by name."""
 102         cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
 103         dc.cdc = self.cd.getConstructor(name.encode())
 104         return dc
 105
 106     def getConstructorTerm(self, str name):
 107         """:return: the term representing the datatype constructor with the given name (see :cpp:func:`Datatype::getConstructorTerm() <cvc5::api::Datatype::getConstructorTerm>`)."""
 108         cdef Term term = Term(self.solver)
 109         term.cterm = self.cd.getConstructorTerm(name.encode())
 110         return term
 111
 112     def getNumConstructors(self):
 113         """:return: number of constructors."""
 114         return self.cd.getNumConstructors()
 115
 116     def isParametric(self):
 117         """:return: whether this datatype is parametric."""
 118         return self.cd.isParametric()
 119
 120     def isCodatatype(self):
 121         """:return: whether this datatype corresponds to a co-datatype."""
 122         return self.cd.isCodatatype()
 123
 124     def isTuple(self):
 125         """:return: whether this datatype corresponds to a tuple."""
 126         return self.cd.isTuple()
 127
 128     def isRecord(self):
 129         """:return: whether this datatype corresponds to a record."""
 130         return self.cd.isRecord()
 131
 132     def isFinite(self):
 133         """:return: whether this datatype is finite."""
 134         return self.cd.isFinite()
 135
 136     def isWellFounded(self):
 137         """:return: whether this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
 138         return self.cd.isWellFounded()
 139
 140     def hasNestedRecursion(self):
 141         """:return: whether this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`)."""
 142         return self.cd.hasNestedRecursion()
 143
 144     def __str__(self):
 145         return self.cd.toString().decode()
 146
 147     def __repr__(self):
 148         return self.cd.toString().decode()
 149
 150     def __iter__(self):
 151         for ci in self.cd:
 152             dc = DatatypeConstructor(self.solver)
 153             dc.cdc = ci
 154             yield dc
 155
 156
 157 cdef class DatatypeConstructor:
 158     cdef c_DatatypeConstructor cdc
 159     cdef Solver solver
 160     def __cinit__(self, Solver solver):
 161         self.cdc = c_DatatypeConstructor()
 162         self.solver = solver
 163
 164     def __getitem__(self, index):
 165         cdef DatatypeSelector ds = DatatypeSelector(self.solver)
 166         if isinstance(index, int) and index >= 0:
 167             ds.cds = self.cdc[(<int?> index)]
 168         elif isinstance(index, str):
 169             ds.cds = self.cdc[(<const string &> name.encode())]
 170         else:
 171             raise ValueError("Expecting a non-negative integer or string")
 172         return ds
 173
 174     def getName(self):
 175         return self.cdc.getName().decode()
 176
 177     def getConstructorTerm(self):
 178         cdef Term term = Term(self.solver)
 179         term.cterm = self.cdc.getConstructorTerm()
 180         return term
 181
 182     def getTesterTerm(self):
 183         cdef Term term = Term(self.solver)
 184         term.cterm = self.cdc.getTesterTerm()
 185         return term
 186
 187     def getNumSelectors(self):
 188         return self.cdc.getNumSelectors()
 189
 190     def getSelector(self, str name):
 191         cdef DatatypeSelector ds = DatatypeSelector(self.solver)
 192         ds.cds = self.cdc.getSelector(name.encode())
 193         return ds
 194
 195     def getSelectorTerm(self, str name):
 196         cdef Term term = Term(self.solver)
 197         term.cterm = self.cdc.getSelectorTerm(name.encode())
 198         return term
 199
 200     def __str__(self):
 201         return self.cdc.toString().decode()
 202
 203     def __repr__(self):
 204         return self.cdc.toString().decode()
 205
 206     def __iter__(self):
 207         for ci in self.cdc:
 208             ds = DatatypeSelector(self.solver)
 209             ds.cds = ci
 210             yield ds
 211
 212
 213 cdef class DatatypeConstructorDecl:
 214     cdef c_DatatypeConstructorDecl cddc
 215     cdef Solver solver
 216
 217     def __cinit__(self, Solver solver):
 218         self.solver = solver
 219
 220     def addSelector(self, str name, Sort sort):
 221         self.cddc.addSelector(name.encode(), sort.csort)
 222
 223     def addSelectorSelf(self, str name):
 224         self.cddc.addSelectorSelf(name.encode())
 225
 226     def __str__(self):
 227         return self.cddc.toString().decode()
 228
 229     def __repr__(self):
 230         return self.cddc.toString().decode()
 231
 232
 233 cdef class DatatypeDecl:
 234     cdef c_DatatypeDecl cdd
 235     cdef Solver solver
 236     def __cinit__(self, Solver solver):
 237         self.solver = solver
 238
 239     def addConstructor(self, DatatypeConstructorDecl ctor):
 240         self.cdd.addConstructor(ctor.cddc)
 241
 242     def getNumConstructors(self):
 243         return self.cdd.getNumConstructors()
 244
 245     def isParametric(self):
 246         return self.cdd.isParametric()
 247
 248     def __str__(self):
 249         return self.cdd.toString().decode()
 250
 251     def __repr__(self):
 252         return self.cdd.toString().decode()
 253
 254
 255 cdef class DatatypeSelector:
 256     cdef c_DatatypeSelector cds
 257     cdef Solver solver
 258     def __cinit__(self, Solver solver):
 259         self.cds = c_DatatypeSelector()
 260         self.solver = solver
 261
 262     def getName(self):
 263         return self.cds.getName().decode()
 264
 265     def getSelectorTerm(self):
 266         cdef Term term = Term(self.solver)
 267         term.cterm = self.cds.getSelectorTerm()
 268         return term
 269
 270     def getRangeSort(self):
 271         cdef Sort sort = Sort(self.solver)
 272         sort.csort = self.cds.getRangeSort()
 273         return sort
 274
 275     def __str__(self):
 276         return self.cds.toString().decode()
 277
 278     def __repr__(self):
 279         return self.cds.toString().decode()
 280
 281
 282 cdef class Op:
 283     cdef c_Op cop
 284     cdef Solver solver
 285     def __cinit__(self, Solver solver):
 286         self.cop = c_Op()
 287         self.solver = solver
 288
 289     def __eq__(self, Op other):
 290         return self.cop == other.cop
 291
 292     def __ne__(self, Op other):
 293         return self.cop != other.cop
 294
 295     def __str__(self):
 296         return self.cop.toString().decode()
 297
 298     def __repr__(self):
 299         return self.cop.toString().decode()
 300
 301     def __hash__(self):
 302         return cophash(self.cop)
 303
 304     def getKind(self):
 305         return kind(<int> self.cop.getKind())
 306
 307     def isNull(self):
 308         return self.cop.isNull()
 309
 310     def getIndices(self):
 311         indices = None
 312         try:
 313             indices = self.cop.getIndices[string]()
 314         except:
 315             pass
 316
 317         try:
 318             indices = self.cop.getIndices[uint32_t]()
 319         except:
 320             pass
 321
 322         try:
 323             indices = self.cop.getIndices[pair[uint32_t, uint32_t]]()
 324         except:
 325             pass
 326
 327         if indices is None:
 328             raise RuntimeError("Unable to retrieve indices from {}".format(self))
 329
 330         return indices
 331
 332 cdef class Grammar:
 333     cdef c_Grammar  cgrammar
 334     cdef Solver solver
 335     def __cinit__(self, Solver solver):
 336         self.solver = solver
 337         self.cgrammar = c_Grammar()
 338
 339     def addRule(self, Term ntSymbol, Term rule):
 340         self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
 341
 342     def addAnyConstant(self, Term ntSymbol):
 343         self.cgrammar.addAnyConstant(ntSymbol.cterm)
 344
 345     def addAnyVariable(self, Term ntSymbol):
 346         self.cgrammar.addAnyVariable(ntSymbol.cterm)
 347
 348     def addRules(self, Term ntSymbol, rules):
 349         cdef vector[c_Term] crules
 350         for r in rules:
 351             crules.push_back((<Term?> r).cterm)
 352         self.cgrammar.addRules(ntSymbol.cterm, crules)
 353
 354 cdef class Result:
 355     cdef c_Result cr
 356     def __cinit__(self):
 357         # gets populated by solver
 358         self.cr = c_Result()
 359
 360     def isNull(self):
 361         return self.cr.isNull()
 362
 363     def isSat(self):
 364         return self.cr.isSat()
 365
 366     def isUnsat(self):
 367         return self.cr.isUnsat()
 368
 369     def isSatUnknown(self):
 370         return self.cr.isSatUnknown()
 371
 372     def isEntailed(self):
 373         return self.cr.isEntailed()
 374
 375     def isNotEntailed(self):
 376         return self.cr.isNotEntailed()
 377
 378     def isEntailmentUnknown(self):
 379         return self.cr.isEntailmentUnknown()
 380
 381     def __eq__(self, Result other):
 382         return self.cr == other.cr
 383
 384     def __ne__(self, Result other):
 385         return self.cr != other.cr
 386
 387     def getUnknownExplanation(self):
 388         return self.cr.getUnknownExplanation().decode()
 389
 390     def __str__(self):
 391         return self.cr.toString().decode()
 392
 393     def __repr__(self):
 394         return self.cr.toString().decode()
 395
 396
 397 cdef class RoundingMode:
 398     cdef c_RoundingMode crm
 399     cdef str name
 400     def __cinit__(self, int rm):
 401         # crm always assigned externally
 402         self.crm = <c_RoundingMode> rm
 403         self.name = __rounding_modes[rm]
 404
 405     def __eq__(self, RoundingMode other):
 406         return (<int> self.crm) == (<int> other.crm)
 407
 408     def __ne__(self, RoundingMode other):
 409         return not self.__eq__(other)
 410
 411     def __hash__(self):
 412         return hash((<int> self.crm, self.name))
 413
 414     def __str__(self):
 415         return self.name
 416
 417     def __repr__(self):
 418         return self.name
 419
 420
 421 cdef class Solver:
 422     cdef c_Solver* csolver
 423
 424     def __cinit__(self):
 425         self.csolver = new c_Solver(NULL)
 426
 427     def __dealloc__(self):
 428         del self.csolver
 429
 430     def supportsFloatingPoint(self):
 431         return self.csolver.supportsFloatingPoint()
 432
 433     def getBooleanSort(self):
 434         cdef Sort sort = Sort(self)
 435         sort.csort = self.csolver.getBooleanSort()
 436         return sort
 437
 438     def getIntegerSort(self):
 439         cdef Sort sort = Sort(self)
 440         sort.csort = self.csolver.getIntegerSort()
 441         return sort
 442
 443     def getRealSort(self):
 444         cdef Sort sort = Sort(self)
 445         sort.csort = self.csolver.getRealSort()
 446         return sort
 447
 448     def getRegExpSort(self):
 449         cdef Sort sort = Sort(self)
 450         sort.csort = self.csolver.getRegExpSort()
 451         return sort
 452
 453     def getRoundingModeSort(self):
 454         cdef Sort sort = Sort(self)
 455         sort.csort = self.csolver.getRoundingModeSort()
 456         return sort
 457
 458     def getStringSort(self):
 459         cdef Sort sort = Sort(self)
 460         sort.csort = self.csolver.getStringSort()
 461         return sort
 462
 463     def mkArraySort(self, Sort indexSort, Sort elemSort):
 464         cdef Sort sort = Sort(self)
 465         sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort)
 466         return sort
 467
 468     def mkBitVectorSort(self, uint32_t size):
 469         cdef Sort sort = Sort(self)
 470         sort.csort = self.csolver.mkBitVectorSort(size)
 471         return sort
 472
 473     def mkFloatingPointSort(self, uint32_t exp, uint32_t sig):
 474         cdef Sort sort = Sort(self)
 475         sort.csort = self.csolver.mkFloatingPointSort(exp, sig)
 476         return sort
 477
 478     def mkDatatypeSort(self, DatatypeDecl dtypedecl):
 479         cdef Sort sort = Sort(self)
 480         sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd)
 481         return sort
 482
 483     def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts):
 484         sorts = []
 485
 486         cdef vector[c_DatatypeDecl] decls
 487         for decl in dtypedecls:
 488             decls.push_back((<DatatypeDecl?> decl).cdd)
 489
 490         cdef set[c_Sort] usorts
 491         for usort in unresolvedSorts:
 492             usorts.insert((<Sort?> usort).csort)
 493
 494         csorts = self.csolver.mkDatatypeSorts(
 495             <const vector[c_DatatypeDecl]&> decls, <const set[c_Sort]&> usorts)
 496         for csort in csorts:
 497           sort = Sort(self)
 498           sort.csort = csort
 499           sorts.append(sort)
 500
 501         return sorts
 502
 503     def mkFunctionSort(self, sorts, Sort codomain):
 504
 505         cdef Sort sort = Sort(self)
 506         # populate a vector with dereferenced c_Sorts
 507         cdef vector[c_Sort] v
 508
 509         if isinstance(sorts, Sort):
 510             sort.csort = self.csolver.mkFunctionSort((<Sort?> sorts).csort,
 511                                                      codomain.csort)
 512         elif isinstance(sorts, list):
 513             for s in sorts:
 514                 v.push_back((<Sort?>s).csort)
 515
 516             sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
 517                                                       codomain.csort)
 518         return sort
 519
 520     def mkParamSort(self, symbolname):
 521         cdef Sort sort = Sort(self)
 522         sort.csort = self.csolver.mkParamSort(symbolname.encode())
 523         return sort
 524
 525     @expand_list_arg(num_req_args=0)
 526     def mkPredicateSort(self, *sorts):
 527         '''
 528         Supports the following arguments:
 529                  Sort mkPredicateSort(List[Sort] sorts)
 530
 531                  where sorts can also be comma-separated arguments of
 532                   type Sort
 533         '''
 534         cdef Sort sort = Sort(self)
 535         cdef vector[c_Sort] v
 536         for s in sorts:
 537             v.push_back((<Sort?> s).csort)
 538         sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v)
 539         return sort
 540
 541     @expand_list_arg(num_req_args=0)
 542     def mkRecordSort(self, *fields):
 543         '''
 544         Supports the following arguments:
 545                 Sort mkRecordSort(List[Tuple[str, Sort]] fields)
 546
 547                   where fields can also be comma-separated arguments of
 548           type Tuple[str, Sort]
 549         '''
 550         cdef Sort sort = Sort(self)
 551         cdef vector[pair[string, c_Sort]] v
 552         cdef pair[string, c_Sort] p
 553         for f in fields:
 554             name, sortarg = f
 555             name = name.encode()
 556             p = pair[string, c_Sort](<string?> name, (<Sort?> sortarg).csort)
 557             v.push_back(p)
 558         sort.csort = self.csolver.mkRecordSort(
 559             <const vector[pair[string, c_Sort]] &> v)
 560         return sort
 561
 562     def mkSetSort(self, Sort elemSort):
 563         cdef Sort sort = Sort(self)
 564         sort.csort = self.csolver.mkSetSort(elemSort.csort)
 565         return sort
 566
 567     def mkBagSort(self, Sort elemSort):
 568         cdef Sort sort = Sort(self)
 569         sort.csort = self.csolver.mkBagSort(elemSort.csort)
 570         return sort
 571
 572     def mkSequenceSort(self, Sort elemSort):
 573         cdef Sort sort = Sort(self)
 574         sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
 575         return sort
 576
 577     def mkUninterpretedSort(self, str name):
 578         cdef Sort sort = Sort(self)
 579         sort.csort = self.csolver.mkUninterpretedSort(name.encode())
 580         return sort
 581
 582     def mkSortConstructorSort(self, str symbol, size_t arity):
 583         cdef Sort sort = Sort(self)
 584         sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity)
 585         return sort
 586
 587     @expand_list_arg(num_req_args=0)
 588     def mkTupleSort(self, *sorts):
 589         '''
 590            Supports the following arguments:
 591                 Sort mkTupleSort(List[Sort] sorts)
 592
 593                  where sorts can also be comma-separated arguments of
 594                  type Sort
 595         '''
 596         cdef Sort sort = Sort(self)
 597         cdef vector[c_Sort] v
 598         for s in sorts:
 599             v.push_back((<Sort?> s).csort)
 600         sort.csort = self.csolver.mkTupleSort(v)
 601         return sort
 602
 603     @expand_list_arg(num_req_args=1)
 604     def mkTerm(self, kind_or_op, *args):
 605         '''
 606             Supports the following arguments:
 607                     Term mkTerm(Kind kind)
 608                     Term mkTerm(Kind kind, Op child1, List[Term] children)
 609                     Term mkTerm(Kind kind, List[Term] children)
 610
 611                 where List[Term] can also be comma-separated arguments
 612         '''
 613         cdef Term term = Term(self)
 614         cdef vector[c_Term] v
 615
 616         op = kind_or_op
 617         if isinstance(kind_or_op, kind):
 618             op = self.mkOp(kind_or_op)
 619
 620         if len(args) == 0:
 621             term.cterm = self.csolver.mkTerm((<Op?> op).cop)
 622         else:
 623             for a in args:
 624                 v.push_back((<Term?> a).cterm)
 625             term.cterm = self.csolver.mkTerm((<Op?> op).cop, v)
 626         return term
 627
 628     def mkOp(self, kind k, arg0=None, arg1 = None):
 629         '''
 630         Supports the following uses:
 631                 Op mkOp(Kind kind)
 632                 Op mkOp(Kind kind, Kind k)
 633                 Op mkOp(Kind kind, const string& arg)
 634                 Op mkOp(Kind kind, uint32_t arg)
 635                 Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)
 636         '''
 637         cdef Op op = Op(self)
 638
 639         if arg0 is None:
 640             op.cop = self.csolver.mkOp(k.k)
 641         elif arg1 is None:
 642             if isinstance(arg0, kind):
 643                 op.cop = self.csolver.mkOp(k.k, (<kind?> arg0).k)
 644             elif isinstance(arg0, str):
 645                 op.cop = self.csolver.mkOp(k.k,
 646                                            <const string &>
 647                                            arg0.encode())
 648             elif isinstance(arg0, int):
 649                 op.cop = self.csolver.mkOp(k.k, <int?> arg0)
 650             else:
 651                 raise ValueError("Unsupported signature"
 652                                  " mkOp: {}".format(" X ".join([k, arg0])))
 653         else:
 654             if isinstance(arg0, int) and isinstance(arg1, int):
 655                 op.cop = self.csolver.mkOp(k.k, <int> arg0,
 656                                                        <int> arg1)
 657             else:
 658                 raise ValueError("Unsupported signature"
 659                                  " mkOp: {}".format(" X ".join([k, arg0, arg1])))
 660         return op
 661
 662     def mkTrue(self):
 663         cdef Term term = Term(self)
 664         term.cterm = self.csolver.mkTrue()
 665         return term
 666
 667     def mkFalse(self):
 668         cdef Term term = Term(self)
 669         term.cterm = self.csolver.mkFalse()
 670         return term
 671
 672     def mkBoolean(self, bint val):
 673         cdef Term term = Term(self)
 674         term.cterm = self.csolver.mkBoolean(val)
 675         return term
 676
 677     def mkPi(self):
 678         cdef Term term = Term(self)
 679         term.cterm = self.csolver.mkPi()
 680         return term
 681
 682     def mkInteger(self, val):
 683         cdef Term term = Term(self)
 684         integer = int(val)
 685         term.cterm = self.csolver.mkInteger("{}".format(integer).encode())
 686         return term
 687
 688     def mkReal(self, val, den=None):
 689         cdef Term term = Term(self)
 690         if den is None:
 691             term.cterm = self.csolver.mkReal(str(val).encode())
 692         else:
 693             if not isinstance(val, int) or not isinstance(den, int):
 694                 raise ValueError("Expecting integers when"
 695                                  " constructing a rational"
 696                                  " but got: {}".format((val, den)))
 697             term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode())
 698         return term
 699
 700     def mkRegexpEmpty(self):
 701         cdef Term term = Term(self)
 702         term.cterm = self.csolver.mkRegexpEmpty()
 703         return term
 704
 705     def mkRegexpSigma(self):
 706         cdef Term term = Term(self)
 707         term.cterm = self.csolver.mkRegexpSigma()
 708         return term
 709
 710     def mkEmptySet(self, Sort s):
 711         cdef Term term = Term(self)
 712         term.cterm = self.csolver.mkEmptySet(s.csort)
 713         return term
 714
 715
 716     def mkSepNil(self, Sort sort):
 717         cdef Term term = Term(self)
 718         term.cterm = self.csolver.mkSepNil(sort.csort)
 719         return term
 720
 721     def mkString(self, str_or_vec):
 722         cdef Term term = Term(self)
 723         cdef vector[unsigned] v
 724         if isinstance(str_or_vec, str):
 725             for u in str_or_vec:
 726                 v.push_back(<unsigned> ord(u))
 727             term.cterm = self.csolver.mkString(<const vector[unsigned]&> v)
 728         elif isinstance(str_or_vec, list):
 729             for u in str_or_vec:
 730                 if not isinstance(u, int):
 731                     raise ValueError("List should contain ints but got: {}"
 732                                      .format(str_or_vec))
 733                 v.push_back(<unsigned> u)
 734             term.cterm = self.csolver.mkString(<const vector[unsigned]&> v)
 735         else:
 736             raise ValueError("Expected string or vector of ASCII codes"
 737                              " but got: {}".format(str_or_vec))
 738         return term
 739
 740     def mkEmptySequence(self, Sort sort):
 741         cdef Term term = Term(self)
 742         term.cterm = self.csolver.mkEmptySequence(sort.csort)
 743         return term
 744
 745     def mkUniverseSet(self, Sort sort):
 746         cdef Term term = Term(self)
 747         term.cterm = self.csolver.mkUniverseSet(sort.csort)
 748         return term
 749
 750     def mkBitVector(self, size_or_str, val = None):
 751         cdef Term term = Term(self)
 752         if isinstance(size_or_str, int):
 753             if val is None:
 754                 term.cterm = self.csolver.mkBitVector(<uint32_t> size_or_str)
 755             else:
 756                 term.cterm = self.csolver.mkBitVector(<uint32_t> size_or_str,
 757                                                       <const string &> str(val).encode(),
 758                                                       10)
 759         elif isinstance(size_or_str, str):
 760             # handle default value
 761             if val is None:
 762                 term.cterm = self.csolver.mkBitVector(
 763                     <const string &> size_or_str.encode())
 764             else:
 765                 term.cterm = self.csolver.mkBitVector(
 766                     <const string &> size_or_str.encode(), <uint32_t> val)
 767         else:
 768             raise ValueError("Unexpected inputs {} to"
 769                              " mkBitVector".format((size_or_str, val)))
 770         return term
 771
 772     def mkConstArray(self, Sort sort, Term val):
 773         cdef Term term = Term(self)
 774         term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
 775         return term
 776
 777     def mkPosInf(self, int exp, int sig):
 778         cdef Term term = Term(self)
 779         term.cterm = self.csolver.mkPosInf(exp, sig)
 780         return term
 781
 782     def mkNegInf(self, int exp, int sig):
 783         cdef Term term = Term(self)
 784         term.cterm = self.csolver.mkNegInf(exp, sig)
 785         return term
 786
 787     def mkNaN(self, int exp, int sig):
 788         cdef Term term = Term(self)
 789         term.cterm = self.csolver.mkNaN(exp, sig)
 790         return term
 791
 792     def mkPosZero(self, int exp, int sig):
 793         cdef Term term = Term(self)
 794         term.cterm = self.csolver.mkPosZero(exp, sig)
 795         return term
 796
 797     def mkNegZero(self, int exp, int sig):
 798         cdef Term term = Term(self)
 799         term.cterm = self.csolver.mkNegZero(exp, sig)
 800         return term
 801
 802     def mkRoundingMode(self, RoundingMode rm):
 803         cdef Term term = Term(self)
 804         term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm)
 805         return term
 806
 807     def mkUninterpretedConst(self, Sort sort, int index):
 808         cdef Term term = Term(self)
 809         term.cterm = self.csolver.mkUninterpretedConst(sort.csort, index)
 810         return term
 811
 812     def mkAbstractValue(self, index):
 813         cdef Term term = Term(self)
 814         try:
 815             term.cterm = self.csolver.mkAbstractValue(str(index).encode())
 816         except:
 817             raise ValueError("mkAbstractValue expects a str representing a number"
 818                              " or an int, but got{}".format(index))
 819         return term
 820
 821     def mkFloatingPoint(self, int exp, int sig, Term val):
 822         cdef Term term = Term(self)
 823         term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
 824         return term
 825
 826     def mkConst(self, Sort sort, symbol=None):
 827         cdef Term term = Term(self)
 828         if symbol is None:
 829             term.cterm = self.csolver.mkConst(sort.csort)
 830         else:
 831             term.cterm = self.csolver.mkConst(sort.csort,
 832                                             (<str?> symbol).encode())
 833         return term
 834
 835     def mkVar(self, Sort sort, symbol=None):
 836         cdef Term term = Term(self)
 837         if symbol is None:
 838             term.cterm = self.csolver.mkVar(sort.csort)
 839         else:
 840             term.cterm = self.csolver.mkVar(sort.csort,
 841                                             (<str?> symbol).encode())
 842         return term
 843
 844     def mkDatatypeConstructorDecl(self, str name):
 845         cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
 846         ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
 847         return ddc
 848
 849     def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
 850         cdef DatatypeDecl dd = DatatypeDecl(self)
 851         cdef vector[c_Sort] v
 852
 853         # argument cases
 854         if sorts_or_bool is None and isCoDatatype is None:
 855             dd.cdd = self.csolver.mkDatatypeDecl(name.encode())
 856         elif sorts_or_bool is not None and isCoDatatype is None:
 857             if isinstance(sorts_or_bool, bool):
 858                 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
 859                                                      <bint> sorts_or_bool)
 860             elif isinstance(sorts_or_bool, Sort):
 861                 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
 862                                                      (<Sort> sorts_or_bool).csort)
 863             elif isinstance(sorts_or_bool, list):
 864                 for s in sorts_or_bool:
 865                     v.push_back((<Sort?> s).csort)
 866                 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
 867                                                      <const vector[c_Sort]&> v)
 868             else:
 869                 raise ValueError("Unhandled second argument type {}"
 870                                  .format(type(sorts_or_bool)))
 871         elif sorts_or_bool is not None and isCoDatatype is not None:
 872             if isinstance(sorts_or_bool, Sort):
 873                 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
 874                                                      (<Sort> sorts_or_bool).csort,
 875                                                      <bint> isCoDatatype)
 876             elif isinstance(sorts_or_bool, list):
 877                 for s in sorts_or_bool:
 878                     v.push_back((<Sort?> s).csort)
 879                 dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(),
 880                                                      <const vector[c_Sort]&> v,
 881                                                      <bint> isCoDatatype)
 882             else:
 883                 raise ValueError("Unhandled second argument type {}"
 884                                  .format(type(sorts_or_bool)))
 885         else:
 886             raise ValueError("Can't create DatatypeDecl with {}".format([type(a)
 887                                                                          for a in [name,
 888                                                                                    sorts_or_bool,
 889                                                                                    isCoDatatype]]))
 890
 891         return dd
 892
 893     def simplify(self, Term t):
 894         cdef Term term = Term(self)
 895         term.cterm = self.csolver.simplify(t.cterm)
 896         return term
 897
 898     def assertFormula(self, Term term):
 899         self.csolver.assertFormula(term.cterm)
 900
 901     def checkSat(self):
 902         cdef Result r = Result()
 903         r.cr = self.csolver.checkSat()
 904         return r
 905
 906     def mkSygusGrammar(self, boundVars, ntSymbols):
 907         cdef Grammar grammar = Grammar(self)
 908         cdef vector[c_Term] bvc
 909         cdef vector[c_Term] ntc
 910         for bv in boundVars:
 911             bvc.push_back((<Term?> bv).cterm)
 912         for nt in ntSymbols:
 913             ntc.push_back((<Term?> nt).cterm)
 914         grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> ntc)
 915         return grammar
 916
 917     def mkSygusVar(self, Sort sort, str symbol=""):
 918         cdef Term term = Term(self)
 919         term.cterm = self.csolver.mkSygusVar(sort.csort, symbol.encode())
 920         return term
 921
 922     def addSygusConstraint(self, Term t):
 923         self.csolver.addSygusConstraint(t.cterm)
 924
 925     def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f):
 926         self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm)
 927
 928     def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None):
 929         cdef Term term = Term(self)
 930         cdef vector[c_Term] v
 931         for bv in bound_vars:
 932             v.push_back((<Term?> bv).cterm)
 933         if grammar is None:
 934           term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort)
 935         else:
 936           term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort, grammar.cgrammar)
 937         return term
 938
 939     def checkSynth(self):
 940         cdef Result r = Result()
 941         r.cr = self.csolver.checkSynth()
 942         return r
 943
 944     def getSynthSolution(self, Term term):
 945         cdef Term t = Term(self)
 946         t.cterm = self.csolver.getSynthSolution(term.cterm)
 947         return t
 948
 949     def synthInv(self, symbol, bound_vars, Grammar grammar=None):
 950         cdef Term term = Term(self)
 951         cdef vector[c_Term] v
 952         for bv in bound_vars:
 953             v.push_back((<Term?> bv).cterm)
 954         if grammar is None:
 955             term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v)
 956         else:
 957             term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v, grammar.cgrammar)
 958         return term
 959
 960     def printSynthSolution(self):
 961         self.csolver.printSynthSolution(cout)
 962
 963     @expand_list_arg(num_req_args=0)
 964     def checkSatAssuming(self, *assumptions):
 965         '''
 966             Supports the following arguments:
 967                  Result checkSatAssuming(List[Term] assumptions)
 968
 969                  where assumptions can also be comma-separated arguments of
 970                  type (boolean) Term
 971         '''
 972         cdef Result r = Result()
 973         # used if assumptions is a list of terms
 974         cdef vector[c_Term] v
 975         for a in assumptions:
 976             v.push_back((<Term?> a).cterm)
 977         r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
 978         return r
 979
 980     @expand_list_arg(num_req_args=0)
 981     def checkEntailed(self, *assumptions):
 982         '''
 983             Supports the following arguments:
 984                  Result checkEntailed(List[Term] assumptions)
 985
 986                  where assumptions can also be comma-separated arguments of
 987                  type (boolean) Term
 988         '''
 989         cdef Result r = Result()
 990         # used if assumptions is a list of terms
 991         cdef vector[c_Term] v
 992         for a in assumptions:
 993             v.push_back((<Term?> a).cterm)
 994         r.cr = self.csolver.checkEntailed(<const vector[c_Term]&> v)
 995         return r
 996
 997     @expand_list_arg(num_req_args=1)
 998     def declareDatatype(self, str symbol, *ctors):
 999         '''
1000             Supports the following arguments:
1001                  Sort declareDatatype(str symbol, List[Term] ctors)
1002
1003                  where ctors can also be comma-separated arguments of
1004                   type DatatypeConstructorDecl
1005         '''
1006         cdef Sort sort = Sort(self)
1007         cdef vector[c_DatatypeConstructorDecl] v
1008
1009         for c in ctors:
1010             v.push_back((<DatatypeConstructorDecl?> c).cddc)
1011         sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
1012         return sort
1013
1014     def declareFun(self, str symbol, list sorts, Sort sort):
1015         cdef Term term = Term(self)
1016         cdef vector[c_Sort] v
1017         for s in sorts:
1018             v.push_back((<Sort?> s).csort)
1019         term.cterm = self.csolver.declareFun(symbol.encode(),
1020                                              <const vector[c_Sort]&> v,
1021                                              sort.csort)
1022         return term
1023
1024     def declareSort(self, str symbol, int arity):
1025         cdef Sort sort = Sort(self)
1026         sort.csort = self.csolver.declareSort(symbol.encode(), arity)
1027         return sort
1028
1029     def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
1030         '''
1031         Supports two uses:
1032                 Term defineFun(str symbol, List[Term] bound_vars,
1033                                Sort sort, Term term, bool glbl)
1034                 Term defineFun(Term fun, List[Term] bound_vars,
1035                                Term term, bool glbl)
1036         '''
1037         cdef Term term = Term(self)
1038         cdef vector[c_Term] v
1039         for bv in bound_vars:
1040             v.push_back((<Term?> bv).cterm)
1041
1042         if t is not None:
1043             term.cterm = self.csolver.defineFun((<str?> sym_or_fun).encode(),
1044                                                 <const vector[c_Term] &> v,
1045                                                 (<Sort?> sort_or_term).csort,
1046                                                 (<Term?> t).cterm,
1047                                                 <bint> glbl)
1048         else:
1049             term.cterm = self.csolver.defineFun((<Term?> sym_or_fun).cterm,
1050                                                 <const vector[c_Term]&> v,
1051                                                 (<Term?> sort_or_term).cterm,
1052                                                 <bint> glbl)
1053
1054         return term
1055
1056     def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
1057         '''
1058         Supports two uses:
1059                 Term defineFunRec(str symbol, List[Term] bound_vars,
1060                                Sort sort, Term term, bool glbl)
1061                 Term defineFunRec(Term fun, List[Term] bound_vars,
1062                                Term term, bool glbl)
1063         '''
1064         cdef Term term = Term(self)
1065         cdef vector[c_Term] v
1066         for bv in bound_vars:
1067             v.push_back((<Term?> bv).cterm)
1068
1069         if t is not None:
1070             term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
1071                                                 <const vector[c_Term] &> v,
1072                                                 (<Sort?> sort_or_term).csort,
1073                                                 (<Term?> t).cterm,
1074                                                 <bint> glbl)
1075         else:
1076             term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm,
1077                                                    <const vector[c_Term]&> v,
1078                                                    (<Term?> sort_or_term).cterm,
1079                                                    <bint> glbl)
1080
1081         return term
1082
1083     def defineFunsRec(self, funs, bound_vars, terms):
1084         cdef vector[c_Term] vf
1085         cdef vector[vector[c_Term]] vbv
1086         cdef vector[c_Term] vt
1087
1088         for f in funs:
1089             vf.push_back((<Term?> f).cterm)
1090
1091         cdef vector[c_Term] temp
1092         for v in bound_vars:
1093             for t in v:
1094                 temp.push_back((<Term?> t).cterm)
1095             vbv.push_back(temp)
1096             temp.clear()
1097
1098         for t in terms:
1099             vf.push_back((<Term?> t).cterm)
1100
1101     def getAssertions(self):
1102         assertions = []
1103         for a in self.csolver.getAssertions():
1104             term = Term(self)
1105             term.cterm = a
1106             assertions.append(term)
1107         return assertions
1108
1109     def getInfo(self, str flag):
1110         return self.csolver.getInfo(flag.encode())
1111
1112     def getOption(self, str option):
1113         return self.csolver.getOption(option.encode())
1114
1115     def getUnsatAssumptions(self):
1116         assumptions = []
1117         for a in self.csolver.getUnsatAssumptions():
1118             term = Term(self)
1119             term.cterm = a
1120             assumptions.append(term)
1121         return assumptions
1122
1123     def getUnsatCore(self):
1124         core = []
1125         for a in self.csolver.getUnsatCore():
1126             term = Term(self)
1127             term.cterm = a
1128             core.append(term)
1129         return core
1130
1131     def getValue(self, Term t):
1132         cdef Term term = Term(self)
1133         term.cterm = self.csolver.getValue(t.cterm)
1134         return term
1135
1136     def getSeparationHeap(self):
1137         cdef Term term = Term(self)
1138         term.cterm = self.csolver.getSeparationHeap()
1139         return term
1140
1141     def declareSeparationHeap(self, Sort locType, Sort dataType):
1142         self.csolver.declareSeparationHeap(locType.csort, dataType.csort)
1143
1144     def getSeparationNilTerm(self):
1145         cdef Term term = Term(self)
1146         term.cterm = self.csolver.getSeparationNilTerm()
1147         return term
1148
1149     def declarePool(self, str symbol, Sort sort, initValue):
1150         cdef Term term = Term(self)
1151         cdef vector[c_Term] niv
1152         for v in initValue:
1153             niv.push_back((<Term?> v).cterm)
1154         term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
1155         return term
1156
1157     def pop(self, nscopes=1):
1158         self.csolver.pop(nscopes)
1159
1160     def push(self, nscopes=1):
1161         self.csolver.push(nscopes)
1162
1163     def resetAssertions(self):
1164         self.csolver.resetAssertions()
1165
1166     def setInfo(self, str keyword, str value):
1167         self.csolver.setInfo(keyword.encode(), value.encode())
1168
1169     def setLogic(self, str logic):
1170         self.csolver.setLogic(logic.encode())
1171
1172     def setOption(self, str option, str value):
1173         self.csolver.setOption(option.encode(), value.encode())
1174
1175
1176 cdef class Sort:
1177     cdef c_Sort csort
1178     cdef Solver solver
1179     def __cinit__(self, Solver solver):
1180         # csort always set by Solver
1181         self.solver = solver
1182
1183     def __eq__(self, Sort other):
1184         return self.csort == other.csort
1185
1186     def __ne__(self, Sort other):
1187         return self.csort != other.csort
1188
1189     def __lt__(self, Sort other):
1190         return self.csort < other.csort
1191
1192     def __gt__(self, Sort other):
1193         return self.csort > other.csort
1194
1195     def __le__(self, Sort other):
1196         return self.csort <= other.csort
1197
1198     def __ge__(self, Sort other):
1199         return self.csort >= other.csort
1200
1201     def __str__(self):
1202         return self.csort.toString().decode()
1203
1204     def __repr__(self):
1205         return self.csort.toString().decode()
1206
1207     def __hash__(self):
1208         return csorthash(self.csort)
1209
1210     def isBoolean(self):
1211         return self.csort.isBoolean()
1212
1213     def isInteger(self):
1214         return self.csort.isInteger()
1215
1216     def isReal(self):
1217         return self.csort.isReal()
1218
1219     def isString(self):
1220         return self.csort.isString()
1221
1222     def isRegExp(self):
1223         return self.csort.isRegExp()
1224
1225     def isRoundingMode(self):
1226         return self.csort.isRoundingMode()
1227
1228     def isBitVector(self):
1229         return self.csort.isBitVector()
1230
1231     def isFloatingPoint(self):
1232         return self.csort.isFloatingPoint()
1233
1234     def isDatatype(self):
1235         return self.csort.isDatatype()
1236
1237     def isParametricDatatype(self):
1238         return self.csort.isParametricDatatype()
1239
1240     def isConstructor(self):
1241         return self.csort.isConstructor()
1242
1243     def isSelector(self):
1244         return self.csort.isSelector()
1245
1246     def isTester(self):
1247         return self.csort.isTester()
1248
1249     def isFunction(self):
1250         return self.csort.isFunction()
1251
1252     def isPredicate(self):
1253         return self.csort.isPredicate()
1254
1255     def isTuple(self):
1256         return self.csort.isTuple()
1257
1258     def isRecord(self):
1259         return self.csort.isRecord()
1260
1261     def isArray(self):
1262         return self.csort.isArray()
1263
1264     def isSet(self):
1265         return self.csort.isSet()
1266
1267     def isBag(self):
1268         return self.csort.isBag()
1269
1270     def isSequence(self):
1271         return self.csort.isSequence()
1272
1273     def isUninterpretedSort(self):
1274         return self.csort.isUninterpretedSort()
1275
1276     def isSortConstructor(self):
1277         return self.csort.isSortConstructor()
1278
1279     def isFirstClass(self):
1280         return self.csort.isFirstClass()
1281
1282     def isFunctionLike(self):
1283         return self.csort.isFunctionLike()
1284
1285     def isSubsortOf(self, Sort sort):
1286         return self.csort.isSubsortOf(sort.csort)
1287
1288     def isComparableTo(self, Sort sort):
1289         return self.csort.isComparableTo(sort.csort)
1290
1291     def getDatatype(self):
1292         cdef Datatype d = Datatype(self.solver)
1293         d.cd = self.csort.getDatatype()
1294         return d
1295
1296     def instantiate(self, params):
1297         cdef Sort sort = Sort(self.solver)
1298         cdef vector[c_Sort] v
1299         for s in params:
1300             v.push_back((<Sort?> s).csort)
1301         sort.csort = self.csort.instantiate(v)
1302         return sort
1303
1304     def getConstructorArity(self):
1305         return self.csort.getConstructorArity()
1306
1307     def getConstructorDomainSorts(self):
1308         domain_sorts = []
1309         for s in self.csort.getConstructorDomainSorts():
1310             sort = Sort(self.solver)
1311             sort.csort = s
1312             domain_sorts.append(sort)
1313         return domain_sorts
1314
1315     def getConstructorCodomainSort(self):
1316         cdef Sort sort = Sort(self.solver)
1317         sort.csort = self.csort.getConstructorCodomainSort()
1318         return sort
1319
1320     def getSelectorDomainSort(self):
1321         cdef Sort sort = Sort(self.solver)
1322         sort.csort = self.csort.getSelectorDomainSort()
1323         return sort
1324
1325     def getSelectorCodomainSort(self):
1326         cdef Sort sort = Sort(self.solver)
1327         sort.csort = self.csort.getSelectorCodomainSort()
1328         return sort
1329
1330     def getTesterDomainSort(self):
1331         cdef Sort sort = Sort(self.solver)
1332         sort.csort = self.csort.getTesterDomainSort()
1333         return sort
1334
1335     def getTesterCodomainSort(self):
1336         cdef Sort sort = Sort(self.solver)
1337         sort.csort = self.csort.getTesterCodomainSort()
1338         return sort
1339
1340     def getFunctionArity(self):
1341         return self.csort.getFunctionArity()
1342
1343     def getFunctionDomainSorts(self):
1344         domain_sorts = []
1345         for s in self.csort.getFunctionDomainSorts():
1346             sort = Sort(self.solver)
1347             sort.csort = s
1348             domain_sorts.append(sort)
1349         return domain_sorts
1350
1351     def getFunctionCodomainSort(self):
1352         cdef Sort sort = Sort(self.solver)
1353         sort.csort = self.csort.getFunctionCodomainSort()
1354         return sort
1355
1356     def getArrayIndexSort(self):
1357         cdef Sort sort = Sort(self.solver)
1358         sort.csort = self.csort.getArrayIndexSort()
1359         return sort
1360
1361     def getArrayElementSort(self):
1362         cdef Sort sort = Sort(self.solver)
1363         sort.csort = self.csort.getArrayElementSort()
1364         return sort
1365
1366     def getSetElementSort(self):
1367         cdef Sort sort = Sort(self.solver)
1368         sort.csort = self.csort.getSetElementSort()
1369         return sort
1370
1371     def getBagElementSort(self):
1372         cdef Sort sort = Sort(self.solver)
1373         sort.csort = self.csort.getBagElementSort()
1374         return sort
1375
1376     def getSequenceElementSort(self):
1377         cdef Sort sort = Sort(self.solver)
1378         sort.csort = self.csort.getSequenceElementSort()
1379         return sort
1380
1381     def getUninterpretedSortName(self):
1382         return self.csort.getUninterpretedSortName().decode()
1383
1384     def isUninterpretedSortParameterized(self):
1385         return self.csort.isUninterpretedSortParameterized()
1386
1387     def getUninterpretedSortParamSorts(self):
1388         param_sorts = []
1389         for s in self.csort.getUninterpretedSortParamSorts():
1390             sort = Sort(self.solver)
1391             sort.csort = s
1392             param_sorts.append(sort)
1393         return param_sorts
1394
1395     def getSortConstructorName(self):
1396         return self.csort.getSortConstructorName().decode()
1397
1398     def getSortConstructorArity(self):
1399         return self.csort.getSortConstructorArity()
1400
1401     def getBVSize(self):
1402         return self.csort.getBVSize()
1403
1404     def getFPExponentSize(self):
1405         return self.csort.getFPExponentSize()
1406
1407     def getFPSignificandSize(self):
1408         return self.csort.getFPSignificandSize()
1409
1410     def getDatatypeParamSorts(self):
1411         param_sorts = []
1412         for s in self.csort.getDatatypeParamSorts():
1413             sort = Sort(self.solver)
1414             sort.csort = s
1415             param_sorts.append(sort)
1416         return param_sorts
1417
1418     def getDatatypeArity(self):
1419         return self.csort.getDatatypeArity()
1420
1421     def getTupleLength(self):
1422         return self.csort.getTupleLength()
1423
1424     def getTupleSorts(self):
1425         tuple_sorts = []
1426         for s in self.csort.getTupleSorts():
1427             sort = Sort(self.solver)
1428             sort.csort = s
1429             tuple_sorts.append(sort)
1430         return tuple_sorts
1431
1432
1433 cdef class Term:
1434     cdef c_Term cterm
1435     cdef Solver solver
1436     def __cinit__(self, Solver solver):
1437         # cterm always set in the Solver object
1438         self.solver = solver
1439
1440     def __eq__(self, Term other):
1441         return self.cterm == other.cterm
1442
1443     def __ne__(self, Term other):
1444         return self.cterm != other.cterm
1445
1446     def __getitem__(self, int index):
1447         cdef Term term = Term(self.solver)
1448         if index >= 0:
1449             term.cterm = self.cterm[index]
1450         else:
1451             raise ValueError("Expecting a non-negative integer or string")
1452         return term
1453
1454     def __str__(self):
1455         return self.cterm.toString().decode()
1456
1457     def __repr__(self):
1458         return self.cterm.toString().decode()
1459
1460     def __iter__(self):
1461         for ci in self.cterm:
1462             term = Term(self.solver)
1463             term.cterm = ci
1464             yield term
1465
1466     def __hash__(self):
1467         return ctermhash(self.cterm)
1468
1469     def getKind(self):
1470         return kind(<int> self.cterm.getKind())
1471
1472     def getSort(self):
1473         cdef Sort sort = Sort(self.solver)
1474         sort.csort = self.cterm.getSort()
1475         return sort
1476
1477     def substitute(self, list es, list replacements):
1478         cdef vector[c_Term] ces
1479         cdef vector[c_Term] creplacements
1480         cdef Term term = Term(self.solver)
1481
1482         if len(es) != len(replacements):
1483             raise RuntimeError("Expecting list inputs to substitute to "
1484                                "have the same length but got: "
1485                                "{} and {}".format(len(es), len(replacements)))
1486
1487         for e, r in zip(es, replacements):
1488             ces.push_back((<Term?> e).cterm)
1489             creplacements.push_back((<Term?> r).cterm)
1490
1491         term.cterm = self.cterm.substitute(ces, creplacements)
1492         return term
1493
1494     def hasOp(self):
1495         return self.cterm.hasOp()
1496
1497     def getOp(self):
1498         cdef Op op = Op(self.solver)
1499         op.cop = self.cterm.getOp()
1500         return op
1501
1502     def isNull(self):
1503         return self.cterm.isNull()
1504
1505     def getConstArrayBase(self):
1506         cdef Term term = Term(self.solver)
1507         term.cterm = self.cterm.getConstArrayBase()
1508         return term
1509
1510     def getConstSequenceElements(self):
1511         elems = []
1512         for e in self.cterm.getConstSequenceElements():
1513             term = Term(self.solver)
1514             term.cterm = e
1515             elems.append(term)
1516         return elems
1517
1518     def notTerm(self):
1519         cdef Term term = Term(self.solver)
1520         term.cterm = self.cterm.notTerm()
1521         return term
1522
1523     def andTerm(self, Term t):
1524         cdef Term term = Term(self.solver)
1525         term.cterm = self.cterm.andTerm((<Term> t).cterm)
1526         return term
1527
1528     def orTerm(self, Term t):
1529         cdef Term term = Term(self.solver)
1530         term.cterm = self.cterm.orTerm(t.cterm)
1531         return term
1532
1533     def xorTerm(self, Term t):
1534         cdef Term term = Term(self.solver)
1535         term.cterm = self.cterm.xorTerm(t.cterm)
1536         return term
1537
1538     def eqTerm(self, Term t):
1539         cdef Term term = Term(self.solver)
1540         term.cterm = self.cterm.eqTerm(t.cterm)
1541         return term
1542
1543     def impTerm(self, Term t):
1544         cdef Term term = Term(self.solver)
1545         term.cterm = self.cterm.impTerm(t.cterm)
1546         return term
1547
1548     def iteTerm(self, Term then_t, Term else_t):
1549         cdef Term term = Term(self.solver)
1550         term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm)
1551         return term
1552
1553     def toPythonObj(self):
1554         '''
1555         Converts a constant value Term to a Python object.
1556
1557         Currently supports:
1558           Boolean -- returns a Python bool
1559           Int     -- returns a Python int
1560           Real    -- returns a Python Fraction
1561           BV      -- returns a Python int (treats BV as unsigned)
1562           Array   -- returns a Python dict mapping indices to values
1563                   -- the constant base is returned as the default value
1564           String  -- returns a Python Unicode string
1565         '''
1566
1567         string_repr = self.cterm.toString().decode()
1568         assert string_repr
1569         sort = self.getSort()
1570         res = None
1571         if sort.isBoolean():
1572             if string_repr == "true":
1573                 res = True
1574             else:
1575                 assert string_repr == "false"
1576                 res = False
1577         elif sort.isInteger():
1578             updated_string_repr = string_repr.strip('()').replace(' ', '')
1579             try:
1580                 res = int(updated_string_repr)
1581             except:
1582                 raise ValueError("Failed to convert"
1583                                  " {} to an int".format(string_repr))
1584         elif sort.isReal():
1585             updated_string_repr = string_repr
1586             try:
1587                 # expecting format (/ a b)
1588                 # note: a or b could be negated: (- a)
1589                 splits = [s.strip('()/')
1590                           for s in updated_string_repr.strip('()/') \
1591                           .replace('(- ', '(-').split()]
1592                 assert len(splits) == 2
1593                 num = int(splits[0])
1594                 den = int(splits[1])
1595                 res = Fraction(num, den)
1596             except:
1597                 raise ValueError("Failed to convert "
1598                                  "{} to a Fraction".format(string_repr))
1599
1600         elif sort.isBitVector():
1601             # expecting format #b<bits>
1602             assert string_repr[:2] == "#b"
1603             python_bin_repr = "0" + string_repr[1:]
1604             try:
1605                 res = int(python_bin_repr, 2)
1606             except:
1607                 raise ValueError("Failed to convert bitvector "
1608                                  "{} to an int".format(string_repr))
1609         elif sort.isArray():
1610             keys = []
1611             values = []
1612             base_value = None
1613             to_visit = [self]
1614             # Array models are represented as a series of store operations
1615             # on a constant array
1616             while to_visit:
1617                 t = to_visit.pop()
1618                 if t.getKind() == kinds.Store:
1619                     # save the mappings
1620                     keys.append(t[1].toPythonObj())
1621                     values.append(t[2].toPythonObj())
1622                     to_visit.append(t[0])
1623                 else:
1624                     assert t.getKind() == kinds.ConstArray
1625                     base_value = t.getConstArrayBase().toPythonObj()
1626
1627             assert len(keys) == len(values)
1628             assert base_value is not None
1629
1630             # put everything in a dictionary with the constant
1631             # base as the result for any index not included in the stores
1632             res = defaultdict(lambda : base_value)
1633             for k, v in zip(keys, values):
1634                 res[k] = v
1635         elif sort.isString():
1636             # Strip leading and trailing double quotes and replace double
1637             # double quotes by single quotes
1638             string_repr = string_repr[1:-1].replace('""', '"')
1639
1640             # Convert escape sequences
1641             res = ''
1642             escape_prefix = '\\u{'
1643             i = 0
1644             while True:
1645               prev_i = i
1646               i = string_repr.find(escape_prefix, i)
1647               if i == -1:
1648                 res += string_repr[prev_i:]
1649                 break
1650
1651               res += string_repr[prev_i:i]
1652               val = string_repr[i + len(escape_prefix):string_repr.find('}', i)]
1653               res += chr(int(val, 16))
1654               i += len(escape_prefix) + len(val) + 1
1655         else:
1656             raise ValueError("Cannot convert term {}"
1657                              " of sort {} to Python object".format(string_repr,
1658                                                                    sort))
1659
1660         assert res is not None
1661         return res
1662
1663
1664 # Generate rounding modes
1665 cdef __rounding_modes = {
1666     <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven",
1667     <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive",
1668     <int> ROUND_TOWARD_NEGATIVE: "RoundTowardNegative",
1669     <int> ROUND_TOWARD_ZERO: "RoundTowardZero",
1670     <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway"
1671 }
1672
1673 mod_ref = sys.modules[__name__]
1674 for rm_int, name in __rounding_modes.items():
1675     r = RoundingMode(rm_int)
1676
1677     if name in dir(mod_ref):
1678         raise RuntimeError("Redefinition of Python RoundingMode %s."%name)
1679
1680     setattr(mod_ref, name, r)
1681
1682 del r
1683 del rm_int
1684 del name