src/api/python/cvc5.pxi

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