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