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