test/unit/api/python/test_solver.py

   1 ###############################################################################
   2 # Top contributors (to current version):
   3 #   Yoni Zohar, Ying Sheng
   4 #
   5 # This file is part of the cvc5 project.
   6 #
   7 # Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8 # in the top-level source directory and their institutional affiliations.
   9 # All rights reserved.  See the file COPYING in the top-level source
  10 # directory for licensing information.
  11 # #############################################################################
  12 ##
  13
  14 import pytest
  15 import pycvc5
  16 import sys
  17
  18 from pycvc5 import Kind
  19
  20
  21 @pytest.fixture
  22 def solver():
  23     return pycvc5.Solver()
  24
  25
  26 def test_recoverable_exception(solver):
  27     solver.setOption("produce-models", "true")
  28     x = solver.mkConst(solver.getBooleanSort(), "x")
  29     solver.assertFormula(x.eqTerm(x).notTerm())
  30     with pytest.raises(RuntimeError):
  31         c = solver.getValue(x)
  32
  33
  34 def test_supports_floating_point(solver):
  35     solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
  36
  37
  38 def test_get_boolean_sort(solver):
  39     solver.getBooleanSort()
  40
  41
  42 def test_get_integer_sort(solver):
  43     solver.getIntegerSort()
  44
  45
  46 def test_get_null_sort(solver):
  47     solver.getNullSort()
  48
  49
  50 def test_get_real_sort(solver):
  51     solver.getRealSort()
  52
  53
  54 def test_get_reg_exp_sort(solver):
  55     solver.getRegExpSort()
  56
  57
  58 def test_get_string_sort(solver):
  59     solver.getStringSort()
  60
  61
  62 def test_get_rounding_mode_sort(solver):
  63     solver.getRoundingModeSort()
  64
  65
  66 def test_mk_array_sort(solver):
  67     boolSort = solver.getBooleanSort()
  68     intSort = solver.getIntegerSort()
  69     realSort = solver.getRealSort()
  70     bvSort = solver.mkBitVectorSort(32)
  71     solver.mkArraySort(boolSort, boolSort)
  72     solver.mkArraySort(intSort, intSort)
  73     solver.mkArraySort(realSort, realSort)
  74     solver.mkArraySort(bvSort, bvSort)
  75     solver.mkArraySort(boolSort, intSort)
  76     solver.mkArraySort(realSort, bvSort)
  77
  78     fpSort = solver.mkFloatingPointSort(3, 5)
  79     solver.mkArraySort(fpSort, fpSort)
  80     solver.mkArraySort(bvSort, fpSort)
  81
  82     slv = pycvc5.Solver()
  83     with pytest.raises(RuntimeError):
  84         slv.mkArraySort(boolSort, boolSort)
  85
  86
  87 def test_mk_bit_vector_sort(solver):
  88     solver.mkBitVectorSort(32)
  89     with pytest.raises(RuntimeError):
  90         solver.mkBitVectorSort(0)
  91
  92
  93 def test_mk_floating_point_sort(solver):
  94     solver.mkFloatingPointSort(4, 8)
  95     with pytest.raises(RuntimeError):
  96         solver.mkFloatingPointSort(0, 8)
  97     with pytest.raises(RuntimeError):
  98         solver.mkFloatingPointSort(4, 0)
  99
 100
 101 def test_mk_datatype_sort(solver):
 102     dtypeSpec = solver.mkDatatypeDecl("list")
 103     cons = solver.mkDatatypeConstructorDecl("cons")
 104     cons.addSelector("head", solver.getIntegerSort())
 105     dtypeSpec.addConstructor(cons)
 106     nil = solver.mkDatatypeConstructorDecl("nil")
 107     dtypeSpec.addConstructor(nil)
 108     solver.mkDatatypeSort(dtypeSpec)
 109
 110     slv = pycvc5.Solver()
 111     with pytest.raises(RuntimeError):
 112         slv.mkDatatypeSort(dtypeSpec)
 113
 114     throwsDtypeSpec = solver.mkDatatypeDecl("list")
 115     with pytest.raises(RuntimeError):
 116         solver.mkDatatypeSort(throwsDtypeSpec)
 117
 118
 119 def test_mk_datatype_sorts(solver):
 120     slv = pycvc5.Solver()
 121
 122     dtypeSpec1 = solver.mkDatatypeDecl("list1")
 123     cons1 = solver.mkDatatypeConstructorDecl("cons1")
 124     cons1.addSelector("head1", solver.getIntegerSort())
 125     dtypeSpec1.addConstructor(cons1)
 126     nil1 = solver.mkDatatypeConstructorDecl("nil1")
 127     dtypeSpec1.addConstructor(nil1)
 128
 129     dtypeSpec2 = solver.mkDatatypeDecl("list2")
 130     cons2 = solver.mkDatatypeConstructorDecl("cons2")
 131     cons2.addSelector("head2", solver.getIntegerSort())
 132     dtypeSpec2.addConstructor(cons2)
 133     nil2 = solver.mkDatatypeConstructorDecl("nil2")
 134     dtypeSpec2.addConstructor(nil2)
 135
 136     decls = [dtypeSpec1, dtypeSpec2]
 137     solver.mkDatatypeSorts(decls, set([]))
 138
 139     with pytest.raises(RuntimeError):
 140         slv.mkDatatypeSorts(decls, set([]))
 141
 142     throwsDtypeSpec = solver.mkDatatypeDecl("list")
 143     throwsDecls = [throwsDtypeSpec]
 144     with pytest.raises(RuntimeError):
 145         solver.mkDatatypeSorts(throwsDecls, set([]))
 146
 147     # with unresolved sorts
 148     unresList = solver.mkUnresolvedSort("ulist")
 149     unresSorts = set([unresList])
 150     ulist = solver.mkDatatypeDecl("ulist")
 151     ucons = solver.mkDatatypeConstructorDecl("ucons")
 152     ucons.addSelector("car", unresList)
 153     ucons.addSelector("cdr", unresList)
 154     ulist.addConstructor(ucons)
 155     unil = solver.mkDatatypeConstructorDecl("unil")
 156     ulist.addConstructor(unil)
 157     udecls = [ulist]
 158
 159     solver.mkDatatypeSorts(udecls, unresSorts)
 160     with pytest.raises(RuntimeError):
 161         slv.mkDatatypeSorts(udecls, unresSorts)
 162
 163     # mutually recursive with unresolved parameterized sorts
 164     p0 = solver.mkParamSort("p0")
 165     p1 = solver.mkParamSort("p1")
 166     u0 = solver.mkUnresolvedSort("dt0", 1)
 167     u1 = solver.mkUnresolvedSort("dt1", 1)
 168     dtdecl0 = solver.mkDatatypeDecl("dt0", p0)
 169     dtdecl1 = solver.mkDatatypeDecl("dt1", p1)
 170     ctordecl0 = solver.mkDatatypeConstructorDecl("c0")
 171     ctordecl0.addSelector("s0", u1.instantiate({p0}))
 172     ctordecl1 = solver.mkDatatypeConstructorDecl("c1")
 173     ctordecl1.addSelector("s1", u0.instantiate({p1}))
 174     dtdecl0.addConstructor(ctordecl0)
 175     dtdecl1.addConstructor(ctordecl1)
 176     dt_sorts = solver.mkDatatypeSorts([dtdecl0, dtdecl1], {u0, u1})
 177     isort1 = dt_sorts[1].instantiate({solver.getBooleanSort()})
 178     t1 = solver.mkConst(isort1, "t")
 179     t0 = solver.mkTerm(
 180         Kind.ApplySelector,
 181         t1.getSort().getDatatype().getSelector("s1").getSelectorTerm(),
 182         t1)
 183     assert dt_sorts[0].instantiate({solver.getBooleanSort()}) == t0.getSort()
 184
 185 def test_mk_function_sort(solver):
 186     funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
 187             solver.getIntegerSort())
 188
 189     # function arguments are allowed
 190     solver.mkFunctionSort(funSort, solver.getIntegerSort())
 191
 192     # non-first-class arguments are not allowed
 193     reSort = solver.getRegExpSort()
 194     with pytest.raises(RuntimeError):
 195         solver.mkFunctionSort(reSort, solver.getIntegerSort())
 196     with pytest.raises(RuntimeError):
 197         solver.mkFunctionSort(solver.getIntegerSort(), funSort)
 198
 199     solver.mkFunctionSort([solver.mkUninterpretedSort("u"),\
 200             solver.getIntegerSort()],\
 201             solver.getIntegerSort())
 202     funSort2 = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
 203             solver.getIntegerSort())
 204
 205     # function arguments are allowed
 206     solver.mkFunctionSort([funSort2, solver.mkUninterpretedSort("u")],\
 207             solver.getIntegerSort())
 208
 209     with pytest.raises(RuntimeError):
 210         solver.mkFunctionSort([solver.getIntegerSort(),\
 211                 solver.mkUninterpretedSort("u")],\
 212                 funSort2)
 213
 214     slv = pycvc5.Solver()
 215     with pytest.raises(RuntimeError):
 216         slv.mkFunctionSort(solver.mkUninterpretedSort("u"),\
 217                 solver.getIntegerSort())
 218     with pytest.raises(RuntimeError):
 219         slv.mkFunctionSort(slv.mkUninterpretedSort("u"),\
 220                 solver.getIntegerSort())
 221     sorts1 = [solver.getBooleanSort(),\
 222             slv.getIntegerSort(),\
 223             solver.getIntegerSort()]
 224     sorts2 = [slv.getBooleanSort(), slv.getIntegerSort()]
 225     slv.mkFunctionSort(sorts2, slv.getIntegerSort())
 226     with pytest.raises(RuntimeError):
 227         slv.mkFunctionSort(sorts1, slv.getIntegerSort())
 228     with pytest.raises(RuntimeError):
 229         slv.mkFunctionSort(sorts2, solver.getIntegerSort())
 230
 231
 232 def test_mk_param_sort(solver):
 233     solver.mkParamSort("T")
 234     solver.mkParamSort("")
 235
 236
 237 def test_mk_predicate_sort(solver):
 238     solver.mkPredicateSort([solver.getIntegerSort()])
 239     with pytest.raises(RuntimeError):
 240         solver.mkPredicateSort([])
 241
 242     funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
 243             solver.getIntegerSort())
 244     # functions as arguments are allowed
 245     solver.mkPredicateSort([solver.getIntegerSort(), funSort])
 246
 247     slv = pycvc5.Solver()
 248     with pytest.raises(RuntimeError):
 249         slv.mkPredicateSort([solver.getIntegerSort()])
 250
 251
 252 def test_mk_record_sort(solver):
 253     fields = [("b", solver.getBooleanSort()),\
 254               ("bv", solver.mkBitVectorSort(8)),\
 255               ("i", solver.getIntegerSort())]
 256     empty = []
 257     solver.mkRecordSort(fields)
 258     solver.mkRecordSort(empty)
 259     recSort = solver.mkRecordSort(fields)
 260     recSort.getDatatype()
 261
 262
 263 def test_mk_set_sort(solver):
 264     solver.mkSetSort(solver.getBooleanSort())
 265     solver.mkSetSort(solver.getIntegerSort())
 266     solver.mkSetSort(solver.mkBitVectorSort(4))
 267     slv = pycvc5.Solver()
 268     with pytest.raises(RuntimeError):
 269         slv.mkSetSort(solver.mkBitVectorSort(4))
 270
 271
 272 def test_mk_bag_sort(solver):
 273     solver.mkBagSort(solver.getBooleanSort())
 274     solver.mkBagSort(solver.getIntegerSort())
 275     solver.mkBagSort(solver.mkBitVectorSort(4))
 276     slv = pycvc5.Solver()
 277     with pytest.raises(RuntimeError):
 278         slv.mkBagSort(solver.mkBitVectorSort(4))
 279
 280
 281 def test_mk_sequence_sort(solver):
 282     solver.mkSequenceSort(solver.getBooleanSort())
 283     solver.mkSequenceSort(\
 284             solver.mkSequenceSort(solver.getIntegerSort()))
 285     slv = pycvc5.Solver()
 286     with pytest.raises(RuntimeError):
 287         slv.mkSequenceSort(solver.getIntegerSort())
 288
 289
 290 def test_mk_uninterpreted_sort(solver):
 291     solver.mkUninterpretedSort("u")
 292     solver.mkUninterpretedSort("")
 293
 294
 295 def test_mk_unresolved_sort(solver):
 296     solver.mkUnresolvedSort("u")
 297     solver.mkUnresolvedSort("u", 1)
 298     solver.mkUnresolvedSort("")
 299     solver.mkUnresolvedSort("", 1)
 300
 301
 302 def test_mk_sort_constructor_sort(solver):
 303     solver.mkSortConstructorSort("s", 2)
 304     solver.mkSortConstructorSort("", 2)
 305     with pytest.raises(RuntimeError):
 306         solver.mkSortConstructorSort("", 0)
 307
 308
 309 def test_mk_tuple_sort(solver):
 310     solver.mkTupleSort([solver.getIntegerSort()])
 311     funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
 312                                     solver.getIntegerSort())
 313     with pytest.raises(RuntimeError):
 314         solver.mkTupleSort([solver.getIntegerSort(), funSort])
 315
 316     slv = pycvc5.Solver()
 317     with pytest.raises(RuntimeError):
 318         slv.mkTupleSort([solver.getIntegerSort()])
 319
 320
 321 def test_mk_bit_vector(solver):
 322     solver.mkBitVector(8, 2)
 323     solver.mkBitVector(32, 2)
 324
 325     solver.mkBitVector(4, "1010", 2)
 326     solver.mkBitVector(8, "0101", 2)
 327     solver.mkBitVector(8, "-1111111", 2)
 328     solver.mkBitVector(8, "00000101", 2)
 329     solver.mkBitVector(8, "-127", 10)
 330     solver.mkBitVector(8, "255", 10)
 331     solver.mkBitVector(10, "1010", 10)
 332     solver.mkBitVector(11, "1234", 10)
 333     solver.mkBitVector(8, "-7f", 16)
 334     solver.mkBitVector(8, "a0", 16)
 335     solver.mkBitVector(16, "1010", 16)
 336     solver.mkBitVector(16, "a09f", 16)
 337
 338     with pytest.raises(RuntimeError):
 339         solver.mkBitVector(0, 2)
 340     with pytest.raises(RuntimeError):
 341         solver.mkBitVector(0, "-127", 10)
 342     with pytest.raises(RuntimeError):
 343         solver.mkBitVector(0, "a0", 16)
 344
 345     with pytest.raises(RuntimeError):
 346         solver.mkBitVector(2, "", 2)
 347
 348     with pytest.raises(RuntimeError):
 349         solver.mkBitVector(8, "101", 5)
 350     with pytest.raises(RuntimeError):
 351         solver.mkBitVector(8, "127", 11)
 352     with pytest.raises(RuntimeError):
 353         solver.mkBitVector(8, "a0", 21)
 354
 355     with pytest.raises(RuntimeError):
 356         solver.mkBitVector(8, "101010101", 2)
 357     with pytest.raises(RuntimeError):
 358         solver.mkBitVector(8, "-11111111", 2)
 359     with pytest.raises(RuntimeError):
 360         solver.mkBitVector(8, "-256", 10)
 361     with pytest.raises(RuntimeError):
 362         solver.mkBitVector(8, "257", 10)
 363     with pytest.raises(RuntimeError):
 364         solver.mkBitVector(8, "-a0", 16)
 365     with pytest.raises(RuntimeError):
 366         solver.mkBitVector(8, "fffff", 16)
 367
 368     with pytest.raises(RuntimeError):
 369         solver.mkBitVector(8, "10201010", 2)
 370     with pytest.raises(RuntimeError):
 371         solver.mkBitVector(8, "-25x", 10)
 372     with pytest.raises(RuntimeError):
 373         solver.mkBitVector(8, "2x7", 10)
 374     with pytest.raises(RuntimeError):
 375         solver.mkBitVector(8, "fzff", 16)
 376
 377     assert solver.mkBitVector(8, "0101",
 378                               2) == solver.mkBitVector(8, "00000101", 2)
 379     assert solver.mkBitVector(4, "1010", 2) == solver.mkBitVector(4, "10", 10)
 380     assert solver.mkBitVector(4, "1010", 2) == solver.mkBitVector(4, "a", 16)
 381     assert str(solver.mkBitVector(8, "01010101", 2)) == "#b01010101"
 382     assert str(solver.mkBitVector(8, "F", 16)) == "#b00001111"
 383     assert solver.mkBitVector(8, "-1", 10) ==\
 384             solver.mkBitVector(8, "FF", 16)
 385
 386
 387 def test_mk_var(solver):
 388     boolSort = solver.getBooleanSort()
 389     intSort = solver.getIntegerSort()
 390     funSort = solver.mkFunctionSort(intSort, boolSort)
 391     solver.mkVar(boolSort)
 392     solver.mkVar(funSort)
 393     solver.mkVar(boolSort, "b")
 394     solver.mkVar(funSort, "")
 395     with pytest.raises(RuntimeError):
 396         solver.mkVar(pycvc5.Sort(solver))
 397     with pytest.raises(RuntimeError):
 398         solver.mkVar(pycvc5.Sort(solver), "a")
 399     slv = pycvc5.Solver()
 400     with pytest.raises(RuntimeError):
 401         slv.mkVar(boolSort, "x")
 402
 403
 404 def test_mk_boolean(solver):
 405     solver.mkBoolean(True)
 406     solver.mkBoolean(False)
 407
 408
 409 def test_mk_rounding_mode(solver):
 410     solver.mkRoundingMode(pycvc5.RoundTowardZero)
 411
 412
 413 def test_mk_floating_point(solver):
 414     t1 = solver.mkBitVector(8)
 415     t2 = solver.mkBitVector(4)
 416     t3 = solver.mkInteger(2)
 417     solver.mkFloatingPoint(3, 5, t1)
 418
 419     with pytest.raises(RuntimeError):
 420         solver.mkFloatingPoint(0, 5, pycvc5.Term(solver))
 421     with pytest.raises(RuntimeError):
 422         solver.mkFloatingPoint(0, 5, t1)
 423     with pytest.raises(RuntimeError):
 424         solver.mkFloatingPoint(3, 0, t1)
 425     with pytest.raises(RuntimeError):
 426         solver.mkFloatingPoint(3, 5, t2)
 427     with pytest.raises(RuntimeError):
 428         solver.mkFloatingPoint(3, 5, t2)
 429
 430     slv = pycvc5.Solver()
 431     with pytest.raises(RuntimeError):
 432         slv.mkFloatingPoint(3, 5, t1)
 433
 434
 435 def test_mk_cardinality_constraint(solver):
 436     su = solver.mkUninterpretedSort("u")
 437     si = solver.getIntegerSort()
 438     solver.mkCardinalityConstraint(su, 3)
 439     with pytest.raises(RuntimeError):
 440         solver.mkEmptySet(solver.mkCardinalityConstraint(si, 3))
 441     with pytest.raises(RuntimeError):
 442         solver.mkEmptySet(solver.mkCardinalityConstraint(su, 0))
 443     slv = pycvc5.Solver()
 444     with pytest.raises(RuntimeError):
 445         slv.mkCardinalityConstraint(su, 3)
 446
 447
 448 def test_mk_empty_set(solver):
 449     slv = pycvc5.Solver()
 450     s = solver.mkSetSort(solver.getBooleanSort())
 451     solver.mkEmptySet(pycvc5.Sort(solver))
 452     solver.mkEmptySet(s)
 453     with pytest.raises(RuntimeError):
 454         solver.mkEmptySet(solver.getBooleanSort())
 455     with pytest.raises(RuntimeError):
 456         slv.mkEmptySet(s)
 457
 458
 459 def test_mk_empty_bag(solver):
 460     slv = pycvc5.Solver()
 461     s = solver.mkBagSort(solver.getBooleanSort())
 462     solver.mkEmptyBag(pycvc5.Sort(solver))
 463     solver.mkEmptyBag(s)
 464     with pytest.raises(RuntimeError):
 465         solver.mkEmptyBag(solver.getBooleanSort())
 466     with pytest.raises(RuntimeError):
 467         slv.mkEmptyBag(s)
 468
 469
 470 def test_mk_empty_sequence(solver):
 471     slv = pycvc5.Solver()
 472     s = solver.mkSequenceSort(solver.getBooleanSort())
 473     solver.mkEmptySequence(s)
 474     solver.mkEmptySequence(solver.getBooleanSort())
 475     with pytest.raises(RuntimeError):
 476         slv.mkEmptySequence(s)
 477
 478
 479 def test_mk_false(solver):
 480     solver.mkFalse()
 481     solver.mkFalse()
 482
 483
 484 def test_mk_floating_point_nan(solver):
 485     solver.mkFloatingPointNaN(3, 5)
 486
 487
 488 def test_mk_floating_point_neg_zero(solver):
 489     solver.mkFloatingPointNegZero(3, 5)
 490
 491
 492 def test_mk_floating_point_neg_inf(solver):
 493     solver.mkFloatingPointNegInf(3, 5)
 494
 495
 496 def test_mk_floating_point_pos_inf(solver):
 497     solver.mkFloatingPointPosInf(3, 5)
 498
 499
 500 def test_mk_floating_point_pos_zero(solver):
 501     solver.mkFloatingPointPosZero(3, 5)
 502
 503
 504 def test_mk_op(solver):
 505     with pytest.raises(ValueError):
 506         solver.mkOp(Kind.BVExtract, Kind.Equal)
 507
 508     solver.mkOp(Kind.Divisible, "2147483648")
 509     with pytest.raises(RuntimeError):
 510         solver.mkOp(Kind.BVExtract, "asdf")
 511
 512     solver.mkOp(Kind.Divisible, 1)
 513     solver.mkOp(Kind.BVRotateLeft, 1)
 514     solver.mkOp(Kind.BVRotateRight, 1)
 515     with pytest.raises(RuntimeError):
 516         solver.mkOp(Kind.BVExtract, 1)
 517
 518     solver.mkOp(Kind.BVExtract, 1, 1)
 519     with pytest.raises(RuntimeError):
 520         solver.mkOp(Kind.Divisible, 1, 2)
 521
 522     args = [1, 2, 2]
 523     solver.mkOp(Kind.TupleProject, args)
 524
 525
 526 def test_mk_pi(solver):
 527     solver.mkPi()
 528
 529
 530 def test_mk_integer(solver):
 531     solver.mkInteger("123")
 532     with pytest.raises(RuntimeError):
 533         solver.mkInteger("1.23")
 534     with pytest.raises(RuntimeError):
 535         solver.mkInteger("1/23")
 536     with pytest.raises(RuntimeError):
 537         solver.mkInteger("12/3")
 538     with pytest.raises(RuntimeError):
 539         solver.mkInteger(".2")
 540     with pytest.raises(RuntimeError):
 541         solver.mkInteger("2.")
 542     with pytest.raises(RuntimeError):
 543         solver.mkInteger("")
 544     with pytest.raises(RuntimeError):
 545         solver.mkInteger("asdf")
 546     with pytest.raises(RuntimeError):
 547         solver.mkInteger("1.2/3")
 548     with pytest.raises(RuntimeError):
 549         solver.mkInteger(".")
 550     with pytest.raises(RuntimeError):
 551         solver.mkInteger("/")
 552     with pytest.raises(RuntimeError):
 553         solver.mkInteger("2/")
 554     with pytest.raises(RuntimeError):
 555         solver.mkInteger("/2")
 556
 557     solver.mkReal("123")
 558     with pytest.raises(RuntimeError):
 559         solver.mkInteger("1.23")
 560     with pytest.raises(RuntimeError):
 561         solver.mkInteger("1/23")
 562     with pytest.raises(RuntimeError):
 563         solver.mkInteger("12/3")
 564     with pytest.raises(RuntimeError):
 565         solver.mkInteger(".2")
 566     with pytest.raises(RuntimeError):
 567         solver.mkInteger("2.")
 568     with pytest.raises(RuntimeError):
 569         solver.mkInteger("")
 570     with pytest.raises(RuntimeError):
 571         solver.mkInteger("asdf")
 572     with pytest.raises(RuntimeError):
 573         solver.mkInteger("1.2/3")
 574     with pytest.raises(RuntimeError):
 575         solver.mkInteger(".")
 576     with pytest.raises(RuntimeError):
 577         solver.mkInteger("/")
 578     with pytest.raises(RuntimeError):
 579         solver.mkInteger("2/")
 580     with pytest.raises(RuntimeError):
 581         solver.mkInteger("/2")
 582
 583     val1 = 1
 584     val2 = -1
 585     val3 = 1
 586     val4 = -1
 587     solver.mkInteger(val1)
 588     solver.mkInteger(val2)
 589     solver.mkInteger(val3)
 590     solver.mkInteger(val4)
 591     solver.mkInteger(val4)
 592
 593
 594 def test_mk_real(solver):
 595     solver.mkReal("123")
 596     solver.mkReal("1.23")
 597     solver.mkReal("1/23")
 598     solver.mkReal("12/3")
 599     solver.mkReal(".2")
 600     solver.mkReal("2.")
 601     with pytest.raises(RuntimeError):
 602         solver.mkReal("")
 603     with pytest.raises(RuntimeError):
 604         solver.mkReal("asdf")
 605     with pytest.raises(RuntimeError):
 606         solver.mkReal("1.2/3")
 607     with pytest.raises(RuntimeError):
 608         solver.mkReal(".")
 609     with pytest.raises(RuntimeError):
 610         solver.mkReal("/")
 611     with pytest.raises(RuntimeError):
 612         solver.mkReal("2/")
 613     with pytest.raises(RuntimeError):
 614         solver.mkReal("/2")
 615
 616     solver.mkReal("123")
 617     solver.mkReal("1.23")
 618     solver.mkReal("1/23")
 619     solver.mkReal("12/3")
 620     solver.mkReal(".2")
 621     solver.mkReal("2.")
 622     with pytest.raises(RuntimeError):
 623         solver.mkReal("")
 624     with pytest.raises(RuntimeError):
 625         solver.mkReal("asdf")
 626     with pytest.raises(RuntimeError):
 627         solver.mkReal("1.2/3")
 628     with pytest.raises(RuntimeError):
 629         solver.mkReal(".")
 630     with pytest.raises(RuntimeError):
 631         solver.mkReal("/")
 632     with pytest.raises(RuntimeError):
 633         solver.mkReal("2/")
 634     with pytest.raises(RuntimeError):
 635         solver.mkReal("/2")
 636
 637     val1 = 1
 638     val2 = -1
 639     val3 = 1
 640     val4 = -1
 641     solver.mkReal(val1)
 642     solver.mkReal(val2)
 643     solver.mkReal(val3)
 644     solver.mkReal(val4)
 645     solver.mkReal(val4)
 646     solver.mkReal(val1, val1)
 647     solver.mkReal(val2, val2)
 648     solver.mkReal(val3, val3)
 649     solver.mkReal(val4, val4)
 650
 651
 652 def test_mk_regexp_none(solver):
 653     strSort = solver.getStringSort()
 654     s = solver.mkConst(strSort, "s")
 655     solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpNone())
 656
 657
 658 def test_mk_regexp_all(solver):
 659     strSort = solver.getStringSort()
 660     s = solver.mkConst(strSort, "s")
 661     solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpAll())
 662
 663
 664 def test_mk_regexp_allchar(solver):
 665     strSort = solver.getStringSort()
 666     s = solver.mkConst(strSort, "s")
 667     solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpAllchar())
 668
 669
 670 def test_mk_sep_emp(solver):
 671     solver.mkSepEmp()
 672
 673
 674 def test_mk_sep_nil(solver):
 675     solver.mkSepNil(solver.getBooleanSort())
 676     with pytest.raises(RuntimeError):
 677         solver.mkSepNil(pycvc5.Sort(solver))
 678     slv = pycvc5.Solver()
 679     with pytest.raises(RuntimeError):
 680         slv.mkSepNil(solver.getIntegerSort())
 681
 682
 683 def test_mk_string(solver):
 684     solver.mkString("")
 685     solver.mkString("asdfasdf")
 686     str(solver.mkString("asdf\\nasdf")) == "\"asdf\\u{5c}nasdf\""
 687     str(solver.mkString("asdf\\u{005c}nasdf", True)) ==\
 688             "\"asdf\\u{5c}nasdf\""
 689
 690
 691 def test_mk_term(solver):
 692     bv32 = solver.mkBitVectorSort(32)
 693     a = solver.mkConst(bv32, "a")
 694     b = solver.mkConst(bv32, "b")
 695     v1 = [a, b]
 696     v2 = [a, pycvc5.Term(solver)]
 697     v3 = [a, solver.mkTrue()]
 698     v4 = [solver.mkInteger(1), solver.mkInteger(2)]
 699     v5 = [solver.mkInteger(1), pycvc5.Term(solver)]
 700     v6 = []
 701     slv = pycvc5.Solver()
 702
 703     # mkTerm(Kind kind) const
 704     solver.mkPi()
 705     solver.mkTerm(Kind.Pi)
 706     solver.mkTerm(Kind.Pi, v6)
 707     solver.mkTerm(solver.mkOp(Kind.Pi))
 708     solver.mkTerm(solver.mkOp(Kind.Pi), v6)
 709     solver.mkTerm(Kind.RegexpNone)
 710     solver.mkTerm(Kind.RegexpNone, v6)
 711     solver.mkTerm(solver.mkOp(Kind.RegexpNone))
 712     solver.mkTerm(solver.mkOp(Kind.RegexpNone), v6)
 713     solver.mkTerm(Kind.RegexpAllchar)
 714     solver.mkTerm(Kind.RegexpAllchar, v6)
 715     solver.mkTerm(solver.mkOp(Kind.RegexpAllchar))
 716     solver.mkTerm(solver.mkOp(Kind.RegexpAllchar), v6)
 717     solver.mkTerm(Kind.SepEmp)
 718     solver.mkTerm(Kind.SepEmp, v6)
 719     solver.mkTerm(solver.mkOp(Kind.SepEmp))
 720     solver.mkTerm(solver.mkOp(Kind.SepEmp), v6)
 721     with pytest.raises(RuntimeError):
 722         solver.mkTerm(Kind.ConstBV)
 723
 724     # mkTerm(Kind kind, Term child) const
 725     solver.mkTerm(Kind.Not, solver.mkTrue())
 726     with pytest.raises(RuntimeError):
 727         solver.mkTerm(Kind.Not, pycvc5.Term(solver))
 728     with pytest.raises(RuntimeError):
 729         solver.mkTerm(Kind.Not, a)
 730     with pytest.raises(RuntimeError):
 731         slv.mkTerm(Kind.Not, solver.mkTrue())
 732
 733     # mkTerm(Kind kind, Term child1, Term child2) const
 734     solver.mkTerm(Kind.Equal, a, b)
 735     with pytest.raises(RuntimeError):
 736         solver.mkTerm(Kind.Equal, pycvc5.Term(solver), b)
 737     with pytest.raises(RuntimeError):
 738         solver.mkTerm(Kind.Equal, a, pycvc5.Term(solver))
 739     with pytest.raises(RuntimeError):
 740         solver.mkTerm(Kind.Equal, a, solver.mkTrue())
 741     with pytest.raises(RuntimeError):
 742         slv.mkTerm(Kind.Equal, a, b)
 743
 744     # mkTerm(Kind kind, Term child1, Term child2, Term child3) const
 745     solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue())
 746     with pytest.raises(RuntimeError):
 747         solver.mkTerm(Kind.Ite, pycvc5.Term(solver), solver.mkTrue(),
 748                       solver.mkTrue())
 749     with pytest.raises(RuntimeError):
 750         solver.mkTerm(Kind.Ite, solver.mkTrue(), pycvc5.Term(solver),
 751                       solver.mkTrue())
 752     with pytest.raises(RuntimeError):
 753         solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(),
 754                       pycvc5.Term(solver))
 755     with pytest.raises(RuntimeError):
 756         solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), b)
 757     with pytest.raises(RuntimeError):
 758         slv.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(),
 759                    solver.mkTrue())
 760
 761     solver.mkTerm(Kind.Equal, v1)
 762     with pytest.raises(RuntimeError):
 763         solver.mkTerm(Kind.Equal, v2)
 764     with pytest.raises(RuntimeError):
 765         solver.mkTerm(Kind.Equal, v3)
 766     with pytest.raises(RuntimeError):
 767         solver.mkTerm(Kind.Distinct, v6)
 768
 769     # Test cases that are nary via the API but have arity = 2 internally
 770     s_bool = solver.getBooleanSort()
 771     t_bool = solver.mkConst(s_bool, "t_bool")
 772     solver.mkTerm(Kind.Implies, [t_bool, t_bool, t_bool])
 773     solver.mkTerm(Kind.Xor, [t_bool, t_bool, t_bool])
 774     solver.mkTerm(solver.mkOp(Kind.Xor), [t_bool, t_bool, t_bool])
 775     t_int = solver.mkConst(solver.getIntegerSort(), "t_int")
 776     solver.mkTerm(Kind.Division, [t_int, t_int, t_int])
 777     solver.mkTerm(solver.mkOp(Kind.Division), [t_int, t_int, t_int])
 778     solver.mkTerm(Kind.IntsDivision, [t_int, t_int, t_int])
 779     solver.mkTerm(solver.mkOp(Kind.IntsDivision), [t_int, t_int, t_int])
 780     solver.mkTerm(Kind.Minus, [t_int, t_int, t_int])
 781     solver.mkTerm(solver.mkOp(Kind.Minus), [t_int, t_int, t_int])
 782     solver.mkTerm(Kind.Equal, [t_int, t_int, t_int])
 783     solver.mkTerm(solver.mkOp(Kind.Equal), [t_int, t_int, t_int])
 784     solver.mkTerm(Kind.Lt, [t_int, t_int, t_int])
 785     solver.mkTerm(solver.mkOp(Kind.Lt), [t_int, t_int, t_int])
 786     solver.mkTerm(Kind.Gt, [t_int, t_int, t_int])
 787     solver.mkTerm(solver.mkOp(Kind.Gt), [t_int, t_int, t_int])
 788     solver.mkTerm(Kind.Leq, [t_int, t_int, t_int])
 789     solver.mkTerm(solver.mkOp(Kind.Leq), [t_int, t_int, t_int])
 790     solver.mkTerm(Kind.Geq, [t_int, t_int, t_int])
 791     solver.mkTerm(solver.mkOp(Kind.Geq), [t_int, t_int, t_int])
 792     t_reg = solver.mkConst(solver.getRegExpSort(), "t_reg")
 793     solver.mkTerm(Kind.RegexpDiff, [t_reg, t_reg, t_reg])
 794     solver.mkTerm(solver.mkOp(Kind.RegexpDiff), [t_reg, t_reg, t_reg])
 795     t_fun = solver.mkConst(solver.mkFunctionSort(
 796         [s_bool, s_bool, s_bool], s_bool))
 797     solver.mkTerm(Kind.HoApply, [t_fun, t_bool, t_bool, t_bool])
 798     solver.mkTerm(solver.mkOp(Kind.HoApply), [t_fun, t_bool, t_bool, t_bool])
 799
 800 def test_mk_term_from_op(solver):
 801     bv32 = solver.mkBitVectorSort(32)
 802     a = solver.mkConst(bv32, "a")
 803     b = solver.mkConst(bv32, "b")
 804     v1 = [solver.mkInteger(1), solver.mkInteger(2)]
 805     v2 = [solver.mkInteger(1), pycvc5.Term(solver)]
 806     v3 = []
 807     v4 = [solver.mkInteger(5)]
 808     slv = pycvc5.Solver()
 809
 810     # simple operator terms
 811     opterm1 = solver.mkOp(Kind.BVExtract, 2, 1)
 812     opterm2 = solver.mkOp(Kind.Divisible, 1)
 813
 814     # list datatype
 815     sort = solver.mkParamSort("T")
 816     listDecl = solver.mkDatatypeDecl("paramlist", sort)
 817     cons = solver.mkDatatypeConstructorDecl("cons")
 818     nil = solver.mkDatatypeConstructorDecl("nil")
 819     cons.addSelector("head", sort)
 820     cons.addSelectorSelf("tail")
 821     listDecl.addConstructor(cons)
 822     listDecl.addConstructor(nil)
 823     listSort = solver.mkDatatypeSort(listDecl)
 824     intListSort =\
 825         listSort.instantiate([solver.getIntegerSort()])
 826     c = solver.mkConst(intListSort, "c")
 827     lis = listSort.getDatatype()
 828
 829     # list datatype constructor and selector operator terms
 830     consTerm1 = lis.getConstructorTerm("cons")
 831     consTerm2 = lis.getConstructor("cons").getConstructorTerm()
 832     nilTerm1 = lis.getConstructorTerm("nil")
 833     nilTerm2 = lis.getConstructor("nil").getConstructorTerm()
 834     headTerm1 = lis["cons"].getSelectorTerm("head")
 835     headTerm2 = lis["cons"].getSelector("head").getSelectorTerm()
 836     tailTerm1 = lis["cons"].getSelectorTerm("tail")
 837     tailTerm2 = lis["cons"]["tail"].getSelectorTerm()
 838
 839     # mkTerm(Op op, Term term) const
 840     solver.mkTerm(Kind.ApplyConstructor, nilTerm1)
 841     solver.mkTerm(Kind.ApplyConstructor, nilTerm2)
 842     with pytest.raises(RuntimeError):
 843         solver.mkTerm(Kind.ApplySelector, nilTerm1)
 844     with pytest.raises(RuntimeError):
 845         solver.mkTerm(Kind.ApplySelector, consTerm1)
 846     with pytest.raises(RuntimeError):
 847         solver.mkTerm(Kind.ApplyConstructor, consTerm2)
 848     with pytest.raises(RuntimeError):
 849         solver.mkTerm(opterm1)
 850     with pytest.raises(RuntimeError):
 851         solver.mkTerm(Kind.ApplySelector, headTerm1)
 852     with pytest.raises(RuntimeError):
 853         solver.mkTerm(opterm1)
 854     with pytest.raises(RuntimeError):
 855         slv.mkTerm(Kind.ApplyConstructor, nilTerm1)
 856
 857     # mkTerm(Op op, Term child) const
 858     solver.mkTerm(opterm1, a)
 859     solver.mkTerm(opterm2, solver.mkInteger(1))
 860     solver.mkTerm(Kind.ApplySelector, headTerm1, c)
 861     solver.mkTerm(Kind.ApplySelector, tailTerm2, c)
 862     with pytest.raises(RuntimeError):
 863         solver.mkTerm(opterm2, a)
 864     with pytest.raises(RuntimeError):
 865         solver.mkTerm(opterm1, pycvc5.Term(solver))
 866     with pytest.raises(RuntimeError):
 867         solver.mkTerm(Kind.ApplyConstructor, consTerm1, solver.mkInteger(0))
 868     with pytest.raises(RuntimeError):
 869         slv.mkTerm(opterm1, a)
 870
 871     # mkTerm(Op op, Term child1, Term child2) const
 872     solver.mkTerm(Kind.ApplyConstructor, consTerm1, solver.mkInteger(0),
 873                   solver.mkTerm(Kind.ApplyConstructor, nilTerm1))
 874     with pytest.raises(RuntimeError):
 875         solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2))
 876     with pytest.raises(RuntimeError):
 877         solver.mkTerm(opterm1, a, b)
 878     with pytest.raises(RuntimeError):
 879         solver.mkTerm(opterm2, solver.mkInteger(1), pycvc5.Term(solver))
 880     with pytest.raises(RuntimeError):
 881         solver.mkTerm(opterm2, pycvc5.Term(solver), solver.mkInteger(1))
 882     with pytest.raises(RuntimeError):
 883         slv.mkTerm(Kind.ApplyConstructor,\
 884                         consTerm1,\
 885                         solver.mkInteger(0),\
 886                         solver.mkTerm(Kind.ApplyConstructor, nilTerm1))
 887
 888     # mkTerm(Op op, Term child1, Term child2, Term child3) const
 889     with pytest.raises(RuntimeError):
 890         solver.mkTerm(opterm1, a, b, a)
 891     with pytest.raises(RuntimeError):
 892         solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(1),
 893                       pycvc5.Term(solver))
 894
 895     solver.mkTerm(opterm2, v4)
 896     with pytest.raises(RuntimeError):
 897         solver.mkTerm(opterm2, v1)
 898     with pytest.raises(RuntimeError):
 899         solver.mkTerm(opterm2, v2)
 900     with pytest.raises(RuntimeError):
 901         solver.mkTerm(opterm2, v3)
 902     with pytest.raises(RuntimeError):
 903         slv.mkTerm(opterm2, v4)
 904
 905
 906 def test_mk_true(solver):
 907     solver.mkTrue()
 908     solver.mkTrue()
 909
 910
 911 def test_mk_tuple(solver):
 912     solver.mkTuple([solver.mkBitVectorSort(3)],
 913                    [solver.mkBitVector(3, "101", 2)])
 914     solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")])
 915
 916     with pytest.raises(RuntimeError):
 917         solver.mkTuple([], [solver.mkBitVector(3, "101", 2)])
 918     with pytest.raises(RuntimeError):
 919         solver.mkTuple([solver.mkBitVectorSort(4)],
 920                        [solver.mkBitVector(3, "101", 2)])
 921     with pytest.raises(RuntimeError):
 922         solver.mkTuple([solver.getIntegerSort()], [solver.mkReal("5.3")])
 923     slv = pycvc5.Solver()
 924     with pytest.raises(RuntimeError):
 925         slv.mkTuple([solver.mkBitVectorSort(3)],
 926                     [slv.mkBitVector(3, "101", 2)])
 927     with pytest.raises(RuntimeError):
 928         slv.mkTuple([slv.mkBitVectorSort(3)],
 929                     [solver.mkBitVector(3, "101", 2)])
 930
 931
 932 def test_mk_universe_set(solver):
 933     solver.mkUniverseSet(solver.getBooleanSort())
 934     with pytest.raises(RuntimeError):
 935         solver.mkUniverseSet(pycvc5.Sort(solver))
 936     slv = pycvc5.Solver()
 937     with pytest.raises(RuntimeError):
 938         slv.mkUniverseSet(solver.getBooleanSort())
 939
 940
 941 def test_mk_const(solver):
 942     boolSort = solver.getBooleanSort()
 943     intSort = solver.getIntegerSort()
 944     funSort = solver.mkFunctionSort(intSort, boolSort)
 945     solver.mkConst(boolSort)
 946     solver.mkConst(funSort)
 947     solver.mkConst(boolSort, "b")
 948     solver.mkConst(intSort, "i")
 949     solver.mkConst(funSort, "f")
 950     solver.mkConst(funSort, "")
 951     with pytest.raises(RuntimeError):
 952         solver.mkConst(pycvc5.Sort(solver))
 953     with pytest.raises(RuntimeError):
 954         solver.mkConst(pycvc5.Sort(solver), "a")
 955
 956     slv = pycvc5.Solver()
 957     with pytest.raises(RuntimeError):
 958         slv.mkConst(boolSort)
 959
 960
 961 def test_mk_const_array(solver):
 962     intSort = solver.getIntegerSort()
 963     arrSort = solver.mkArraySort(intSort, intSort)
 964     zero = solver.mkInteger(0)
 965     constArr = solver.mkConstArray(arrSort, zero)
 966
 967     solver.mkConstArray(arrSort, zero)
 968     with pytest.raises(RuntimeError):
 969         solver.mkConstArray(pycvc5.Sort(solver), zero)
 970     with pytest.raises(RuntimeError):
 971         solver.mkConstArray(arrSort, pycvc5.Term(solver))
 972     with pytest.raises(RuntimeError):
 973         solver.mkConstArray(arrSort, solver.mkBitVector(1, 1))
 974     with pytest.raises(RuntimeError):
 975         solver.mkConstArray(intSort, zero)
 976     slv = pycvc5.Solver()
 977     zero2 = slv.mkInteger(0)
 978     arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort())
 979     with pytest.raises(RuntimeError):
 980         slv.mkConstArray(arrSort2, zero)
 981     with pytest.raises(RuntimeError):
 982         slv.mkConstArray(arrSort, zero2)
 983
 984
 985 def test_declare_fun(solver):
 986     bvSort = solver.mkBitVectorSort(32)
 987     funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
 988                                     solver.getIntegerSort())
 989     solver.declareFun("f1", [], bvSort)
 990     solver.declareFun("f3", [bvSort, solver.getIntegerSort()], bvSort)
 991     with pytest.raises(RuntimeError):
 992         solver.declareFun("f2", [], funSort)
 993     # functions as arguments is allowed
 994     solver.declareFun("f4", [bvSort, funSort], bvSort)
 995     with pytest.raises(RuntimeError):
 996         solver.declareFun("f5", [bvSort, bvSort], funSort)
 997     slv = pycvc5.Solver()
 998     with pytest.raises(RuntimeError):
 999         slv.declareFun("f1", [], bvSort)
1000
1001
1002 def test_declare_sort(solver):
1003     solver.declareSort("s", 0)
1004     solver.declareSort("s", 2)
1005     solver.declareSort("", 2)
1006
1007
1008 def test_define_fun(solver):
1009     bvSort = solver.mkBitVectorSort(32)
1010     funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
1011                                     solver.getIntegerSort())
1012     b1 = solver.mkVar(bvSort, "b1")
1013     b2 = solver.mkVar(solver.getIntegerSort(), "b2")
1014     b3 = solver.mkVar(funSort, "b3")
1015     v1 = solver.mkConst(bvSort, "v1")
1016     v2 = solver.mkConst(funSort, "v2")
1017     solver.defineFun("f", [], bvSort, v1)
1018     solver.defineFun("ff", [b1, b2], bvSort, v1)
1019     with pytest.raises(RuntimeError):
1020         solver.defineFun("ff", [v1, b2], bvSort, v1)
1021     with pytest.raises(RuntimeError):
1022         solver.defineFun("fff", [b1], bvSort, v2)
1023     with pytest.raises(RuntimeError):
1024         solver.defineFun("ffff", [b1], funSort, v2)
1025     # b3 has function sort, which is allowed as an argument
1026     solver.defineFun("fffff", [b1, b3], bvSort, v1)
1027
1028     slv = pycvc5.Solver()
1029     bvSort2 = slv.mkBitVectorSort(32)
1030     v12 = slv.mkConst(bvSort2, "v1")
1031     b12 = slv.mkVar(bvSort2, "b1")
1032     b22 = slv.mkVar(slv.getIntegerSort(), "b2")
1033     with pytest.raises(RuntimeError):
1034         slv.defineFun("f", [], bvSort, v12)
1035     with pytest.raises(RuntimeError):
1036         slv.defineFun("f", [], bvSort2, v1)
1037     with pytest.raises(RuntimeError):
1038         slv.defineFun("ff", [b1, b22], bvSort2, v12)
1039     with pytest.raises(RuntimeError):
1040         slv.defineFun("ff", [b12, b2], bvSort2, v12)
1041     with pytest.raises(RuntimeError):
1042         slv.defineFun("ff", [b12, b22], bvSort, v12)
1043     with pytest.raises(RuntimeError):
1044         slv.defineFun("ff", [b12, b22], bvSort2, v1)
1045
1046
1047 def test_define_fun_rec(solver):
1048     bvSort = solver.mkBitVectorSort(32)
1049     funSort1 = solver.mkFunctionSort([bvSort, bvSort], bvSort)
1050     funSort2 = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
1051                                      solver.getIntegerSort())
1052     b1 = solver.mkVar(bvSort, "b1")
1053     b11 = solver.mkVar(bvSort, "b1")
1054     b2 = solver.mkVar(solver.getIntegerSort(), "b2")
1055     b3 = solver.mkVar(funSort2, "b3")
1056     v1 = solver.mkConst(bvSort, "v1")
1057     v2 = solver.mkConst(solver.getIntegerSort(), "v2")
1058     v3 = solver.mkConst(funSort2, "v3")
1059     f1 = solver.mkConst(funSort1, "f1")
1060     f2 = solver.mkConst(funSort2, "f2")
1061     f3 = solver.mkConst(bvSort, "f3")
1062     solver.defineFunRec("f", [], bvSort, v1)
1063     solver.defineFunRec("ff", [b1, b2], bvSort, v1)
1064     solver.defineFunRec(f1, [b1, b11], v1)
1065     with pytest.raises(RuntimeError):
1066         solver.defineFunRec("fff", [b1], bvSort, v3)
1067     with pytest.raises(RuntimeError):
1068         solver.defineFunRec("ff", [b1, v2], bvSort, v1)
1069     with pytest.raises(RuntimeError):
1070         solver.defineFunRec("ffff", [b1], funSort2, v3)
1071     # b3 has function sort, which is allowed as an argument
1072     solver.defineFunRec("fffff", [b1, b3], bvSort, v1)
1073     with pytest.raises(RuntimeError):
1074         solver.defineFunRec(f1, [b1], v1)
1075     with pytest.raises(RuntimeError):
1076         solver.defineFunRec(f1, [b1, b11], v2)
1077     with pytest.raises(RuntimeError):
1078         solver.defineFunRec(f1, [b1, b11], v3)
1079     with pytest.raises(RuntimeError):
1080         solver.defineFunRec(f2, [b1], v2)
1081     with pytest.raises(RuntimeError):
1082         solver.defineFunRec(f3, [b1], v1)
1083
1084     slv = pycvc5.Solver()
1085     bvSort2 = slv.mkBitVectorSort(32)
1086     v12 = slv.mkConst(bvSort2, "v1")
1087     b12 = slv.mkVar(bvSort2, "b1")
1088     b22 = slv.mkVar(slv.getIntegerSort(), "b2")
1089     slv.defineFunRec("f", [], bvSort2, v12)
1090     slv.defineFunRec("ff", [b12, b22], bvSort2, v12)
1091     with pytest.raises(RuntimeError):
1092         slv.defineFunRec("f", [], bvSort, v12)
1093     with pytest.raises(RuntimeError):
1094         slv.defineFunRec("f", [], bvSort2, v1)
1095     with pytest.raises(RuntimeError):
1096         slv.defineFunRec("ff", [b1, b22], bvSort2, v12)
1097     with pytest.raises(RuntimeError):
1098         slv.defineFunRec("ff", [b12, b2], bvSort2, v12)
1099     with pytest.raises(RuntimeError):
1100         slv.defineFunRec("ff", [b12, b22], bvSort, v12)
1101     with pytest.raises(RuntimeError):
1102         slv.defineFunRec("ff", [b12, b22], bvSort2, v1)
1103
1104
1105 def test_define_fun_rec_wrong_logic(solver):
1106     solver.setLogic("QF_BV")
1107     bvSort = solver.mkBitVectorSort(32)
1108     funSort = solver.mkFunctionSort([bvSort, bvSort], bvSort)
1109     b = solver.mkVar(bvSort, "b")
1110     v = solver.mkConst(bvSort, "v")
1111     f = solver.mkConst(funSort, "f")
1112     with pytest.raises(RuntimeError):
1113         solver.defineFunRec("f", [], bvSort, v)
1114     with pytest.raises(RuntimeError):
1115         solver.defineFunRec(f, [b, b], v)
1116
1117
1118 def test_uf_iteration(solver):
1119     intSort = solver.getIntegerSort()
1120     funSort = solver.mkFunctionSort([intSort, intSort], intSort)
1121     x = solver.mkConst(intSort, "x")
1122     y = solver.mkConst(intSort, "y")
1123     f = solver.mkConst(funSort, "f")
1124     fxy = solver.mkTerm(Kind.ApplyUf, f, x, y)
1125
1126     # Expecting the uninterpreted function to be one of the children
1127     expected_children = [f, x, y]
1128     idx = 0
1129     for c in fxy:
1130         assert idx < 3
1131         assert c == expected_children[idx]
1132         idx = idx + 1
1133
1134
1135 def test_get_info(solver):
1136     solver.getInfo("name")
1137     with pytest.raises(RuntimeError):
1138         solver.getInfo("asdf")
1139
1140
1141 def test_get_op(solver):
1142     bv32 = solver.mkBitVectorSort(32)
1143     a = solver.mkConst(bv32, "a")
1144     ext = solver.mkOp(Kind.BVExtract, 2, 1)
1145     exta = solver.mkTerm(ext, a)
1146
1147     assert not a.hasOp()
1148     with pytest.raises(RuntimeError):
1149         a.getOp()
1150     assert exta.hasOp()
1151     assert exta.getOp() == ext
1152
1153     # Test Datatypes -- more complicated
1154     consListSpec = solver.mkDatatypeDecl("list")
1155     cons = solver.mkDatatypeConstructorDecl("cons")
1156     cons.addSelector("head", solver.getIntegerSort())
1157     cons.addSelectorSelf("tail")
1158     consListSpec.addConstructor(cons)
1159     nil = solver.mkDatatypeConstructorDecl("nil")
1160     consListSpec.addConstructor(nil)
1161     consListSort = solver.mkDatatypeSort(consListSpec)
1162     consList = consListSort.getDatatype()
1163
1164     consTerm = consList.getConstructorTerm("cons")
1165     nilTerm = consList.getConstructorTerm("nil")
1166     headTerm = consList["cons"].getSelectorTerm("head")
1167
1168     listnil = solver.mkTerm(Kind.ApplyConstructor, nilTerm)
1169     listcons1 = solver.mkTerm(Kind.ApplyConstructor, consTerm,
1170                               solver.mkInteger(1), listnil)
1171     listhead = solver.mkTerm(Kind.ApplySelector, headTerm, listcons1)
1172
1173     assert listnil.hasOp()
1174     assert listcons1.hasOp()
1175     assert listhead.hasOp()
1176
1177
1178 def test_get_option(solver):
1179     solver.getOption("incremental")
1180     with pytest.raises(RuntimeError):
1181         solver.getOption("asdf")
1182
1183
1184 def test_get_unsat_assumptions1(solver):
1185     solver.setOption("incremental", "false")
1186     solver.checkSatAssuming(solver.mkFalse())
1187     with pytest.raises(RuntimeError):
1188         solver.getUnsatAssumptions()
1189
1190
1191 def test_get_unsat_assumptions2(solver):
1192     solver.setOption("incremental", "true")
1193     solver.setOption("produce-unsat-assumptions", "false")
1194     solver.checkSatAssuming(solver.mkFalse())
1195     with pytest.raises(RuntimeError):
1196         solver.getUnsatAssumptions()
1197
1198
1199 def test_get_unsat_assumptions3(solver):
1200     solver.setOption("incremental", "true")
1201     solver.setOption("produce-unsat-assumptions", "true")
1202     solver.checkSatAssuming(solver.mkFalse())
1203     solver.getUnsatAssumptions()
1204     solver.checkSatAssuming(solver.mkTrue())
1205     with pytest.raises(RuntimeError):
1206         solver.getUnsatAssumptions()
1207
1208
1209 def test_get_unsat_core1(solver):
1210     solver.setOption("incremental", "false")
1211     solver.assertFormula(solver.mkFalse())
1212     solver.checkSat()
1213     with pytest.raises(RuntimeError):
1214         solver.getUnsatCore()
1215
1216
1217 def test_get_unsat_core2(solver):
1218     solver.setOption("incremental", "false")
1219     solver.setOption("produce-unsat-cores", "false")
1220     solver.assertFormula(solver.mkFalse())
1221     solver.checkSat()
1222     with pytest.raises(RuntimeError):
1223         solver.getUnsatCore()
1224
1225
1226 def test_get_unsat_core3(solver):
1227     solver.setOption("incremental", "true")
1228     solver.setOption("produce-unsat-cores", "true")
1229
1230     uSort = solver.mkUninterpretedSort("u")
1231     intSort = solver.getIntegerSort()
1232     boolSort = solver.getBooleanSort()
1233     uToIntSort = solver.mkFunctionSort(uSort, intSort)
1234     intPredSort = solver.mkFunctionSort(intSort, boolSort)
1235
1236     x = solver.mkConst(uSort, "x")
1237     y = solver.mkConst(uSort, "y")
1238     f = solver.mkConst(uToIntSort, "f")
1239     p = solver.mkConst(intPredSort, "p")
1240     zero = solver.mkInteger(0)
1241     one = solver.mkInteger(1)
1242     f_x = solver.mkTerm(Kind.ApplyUf, f, x)
1243     f_y = solver.mkTerm(Kind.ApplyUf, f, y)
1244     summ = solver.mkTerm(Kind.Plus, f_x, f_y)
1245     p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
1246     p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
1247     solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_x))
1248     solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_y))
1249     solver.assertFormula(solver.mkTerm(Kind.Gt, summ, one))
1250     solver.assertFormula(p_0)
1251     solver.assertFormula(p_f_y.notTerm())
1252     assert solver.checkSat().isUnsat()
1253
1254     unsat_core = solver.getUnsatCore()
1255
1256     solver.resetAssertions()
1257     for t in unsat_core:
1258         solver.assertFormula(t)
1259     res = solver.checkSat()
1260     assert res.isUnsat()
1261
1262
1263 def test_get_value1(solver):
1264     solver.setOption("produce-models", "false")
1265     t = solver.mkTrue()
1266     solver.assertFormula(t)
1267     solver.checkSat()
1268     with pytest.raises(RuntimeError):
1269         solver.getValue(t)
1270
1271
1272 def test_get_value2(solver):
1273     solver.setOption("produce-models", "true")
1274     t = solver.mkFalse()
1275     solver.assertFormula(t)
1276     solver.checkSat()
1277     with pytest.raises(RuntimeError):
1278         solver.getValue(t)
1279
1280
1281 def test_get_value3(solver):
1282     solver.setOption("produce-models", "true")
1283     uSort = solver.mkUninterpretedSort("u")
1284     intSort = solver.getIntegerSort()
1285     boolSort = solver.getBooleanSort()
1286     uToIntSort = solver.mkFunctionSort(uSort, intSort)
1287     intPredSort = solver.mkFunctionSort(intSort, boolSort)
1288
1289     x = solver.mkConst(uSort, "x")
1290     y = solver.mkConst(uSort, "y")
1291     z = solver.mkConst(uSort, "z")
1292     f = solver.mkConst(uToIntSort, "f")
1293     p = solver.mkConst(intPredSort, "p")
1294     zero = solver.mkInteger(0)
1295     one = solver.mkInteger(1)
1296     f_x = solver.mkTerm(Kind.ApplyUf, f, x)
1297     f_y = solver.mkTerm(Kind.ApplyUf, f, y)
1298     summ = solver.mkTerm(Kind.Plus, f_x, f_y)
1299     p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
1300     p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
1301
1302     solver.assertFormula(solver.mkTerm(Kind.Leq, zero, f_x))
1303     solver.assertFormula(solver.mkTerm(Kind.Leq, zero, f_y))
1304     solver.assertFormula(solver.mkTerm(Kind.Leq, summ, one))
1305     solver.assertFormula(p_0.notTerm())
1306     solver.assertFormula(p_f_y)
1307     assert solver.checkSat().isSat()
1308     solver.getValue(x)
1309     solver.getValue(y)
1310     solver.getValue(z)
1311     solver.getValue(summ)
1312     solver.getValue(p_f_y)
1313
1314     slv = pycvc5.Solver()
1315     with pytest.raises(RuntimeError):
1316         slv.getValue(x)
1317
1318
1319 def test_declare_sep_heap(solver):
1320     solver.setLogic("ALL")
1321     solver.setOption("incremental", "false")
1322     integer = solver.getIntegerSort()
1323     solver.declareSepHeap(integer, integer)
1324     # cannot declare separation logic heap more than once
1325     with pytest.raises(RuntimeError):
1326         solver.declareSepHeap(integer, integer)
1327
1328
1329 # Helper function for test_get_separation_{heap,nil}_termX. Asserts and checks
1330 # some simple separation logic constraints.
1331 def checkSimpleSeparationConstraints(slv):
1332     integer = slv.getIntegerSort()
1333     # declare the separation heap
1334     slv.declareSepHeap(integer, integer)
1335     x = slv.mkConst(integer, "x")
1336     p = slv.mkConst(integer, "p")
1337     heap = slv.mkTerm(Kind.SepPto, p, x)
1338     slv.assertFormula(heap)
1339     nil = slv.mkSepNil(integer)
1340     slv.assertFormula(nil.eqTerm(slv.mkReal(5)))
1341     slv.checkSat()
1342
1343
1344 def test_get_value_sep_heap_1(solver):
1345     solver.setLogic("QF_BV")
1346     solver.setOption("incremental", "false")
1347     solver.setOption("produce-models", "true")
1348     t = solver.mkTrue()
1349     solver.assertFormula(t)
1350     with pytest.raises(RuntimeError):
1351         solver.getValueSepHeap()
1352
1353
1354 def test_get_value_sep_heap_2(solver):
1355     solver.setLogic("ALL")
1356     solver.setOption("incremental", "false")
1357     solver.setOption("produce-models", "false")
1358     checkSimpleSeparationConstraints(solver)
1359     with pytest.raises(RuntimeError):
1360         solver.getValueSepHeap()
1361
1362
1363 def test_get_value_sep_heap_3(solver):
1364     solver.setLogic("ALL")
1365     solver.setOption("incremental", "false")
1366     solver.setOption("produce-models", "true")
1367     t = solver.mkFalse()
1368     solver.assertFormula(t)
1369     solver.checkSat()
1370     with pytest.raises(RuntimeError):
1371         solver.getValueSepHeap()
1372
1373
1374 def test_get_value_sep_heap_4(solver):
1375     solver.setLogic("ALL")
1376     solver.setOption("incremental", "false")
1377     solver.setOption("produce-models", "true")
1378     t = solver.mkTrue()
1379     solver.assertFormula(t)
1380     solver.checkSat()
1381     with pytest.raises(RuntimeError):
1382         solver.getValueSepHeap()
1383
1384
1385 def test_get_value_sep_heap_5(solver):
1386     solver.setLogic("ALL")
1387     solver.setOption("incremental", "false")
1388     solver.setOption("produce-models", "true")
1389     checkSimpleSeparationConstraints(solver)
1390     solver.getValueSepHeap()
1391
1392
1393 def test_get_value_sep_nil_1(solver):
1394     solver.setLogic("QF_BV")
1395     solver.setOption("incremental", "false")
1396     solver.setOption("produce-models", "true")
1397     t = solver.mkTrue()
1398     solver.assertFormula(t)
1399     with pytest.raises(RuntimeError):
1400         solver.getValueSepNil()
1401
1402
1403 def test_get_value_sep_nil_2(solver):
1404     solver.setLogic("ALL")
1405     solver.setOption("incremental", "false")
1406     solver.setOption("produce-models", "false")
1407     checkSimpleSeparationConstraints(solver)
1408     with pytest.raises(RuntimeError):
1409         solver.getValueSepNil()
1410
1411
1412 def test_get_value_sep_nil_3(solver):
1413     solver.setLogic("ALL")
1414     solver.setOption("incremental", "false")
1415     solver.setOption("produce-models", "true")
1416     t = solver.mkFalse()
1417     solver.assertFormula(t)
1418     solver.checkSat()
1419     with pytest.raises(RuntimeError):
1420         solver.getValueSepNil()
1421
1422
1423 def test_get_value_sep_nil_4(solver):
1424     solver.setLogic("ALL")
1425     solver.setOption("incremental", "false")
1426     solver.setOption("produce-models", "true")
1427     t = solver.mkTrue()
1428     solver.assertFormula(t)
1429     solver.checkSat()
1430     with pytest.raises(RuntimeError):
1431         solver.getValueSepNil()
1432
1433
1434 def test_get_value_sep_nil_5(solver):
1435     solver.setLogic("ALL")
1436     solver.setOption("incremental", "false")
1437     solver.setOption("produce-models", "true")
1438     checkSimpleSeparationConstraints(solver)
1439     solver.getValueSepNil()
1440
1441
1442 def test_push1(solver):
1443     solver.setOption("incremental", "true")
1444     solver.push(1)
1445     with pytest.raises(RuntimeError):
1446         solver.setOption("incremental", "false")
1447     with pytest.raises(RuntimeError):
1448         solver.setOption("incremental", "true")
1449
1450
1451 def test_push2(solver):
1452     solver.setOption("incremental", "false")
1453     with pytest.raises(RuntimeError):
1454         solver.push(1)
1455
1456
1457 def test_pop1(solver):
1458     solver.setOption("incremental", "false")
1459     with pytest.raises(RuntimeError):
1460         solver.pop(1)
1461
1462
1463 def test_pop2(solver):
1464     solver.setOption("incremental", "true")
1465     with pytest.raises(RuntimeError):
1466         solver.pop(1)
1467
1468
1469 def test_pop3(solver):
1470     solver.setOption("incremental", "true")
1471     solver.push(1)
1472     solver.pop(1)
1473     with pytest.raises(RuntimeError):
1474         solver.pop(1)
1475
1476
1477 def test_set_info(solver):
1478     with pytest.raises(RuntimeError):
1479         solver.setInfo("cvc5-lagic", "QF_BV")
1480     with pytest.raises(RuntimeError):
1481         solver.setInfo("cvc2-logic", "QF_BV")
1482     with pytest.raises(RuntimeError):
1483         solver.setInfo("cvc5-logic", "asdf")
1484
1485     solver.setInfo("source", "asdf")
1486     solver.setInfo("category", "asdf")
1487     solver.setInfo("difficulty", "asdf")
1488     solver.setInfo("filename", "asdf")
1489     solver.setInfo("license", "asdf")
1490     solver.setInfo("name", "asdf")
1491     solver.setInfo("notes", "asdf")
1492
1493     solver.setInfo("smt-lib-version", "2")
1494     solver.setInfo("smt-lib-version", "2.0")
1495     solver.setInfo("smt-lib-version", "2.5")
1496     solver.setInfo("smt-lib-version", "2.6")
1497     with pytest.raises(RuntimeError):
1498         solver.setInfo("smt-lib-version", ".0")
1499
1500     solver.setInfo("status", "sat")
1501     solver.setInfo("status", "unsat")
1502     solver.setInfo("status", "unknown")
1503     with pytest.raises(RuntimeError):
1504         solver.setInfo("status", "asdf")
1505
1506
1507 def test_simplify(solver):
1508     with pytest.raises(RuntimeError):
1509         solver.simplify(pycvc5.Term(solver))
1510
1511     bvSort = solver.mkBitVectorSort(32)
1512     uSort = solver.mkUninterpretedSort("u")
1513     funSort1 = solver.mkFunctionSort([bvSort, bvSort], bvSort)
1514     funSort2 = solver.mkFunctionSort(uSort, solver.getIntegerSort())
1515     consListSpec = solver.mkDatatypeDecl("list")
1516     cons = solver.mkDatatypeConstructorDecl("cons")
1517     cons.addSelector("head", solver.getIntegerSort())
1518     cons.addSelectorSelf("tail")
1519     consListSpec.addConstructor(cons)
1520     nil = solver.mkDatatypeConstructorDecl("nil")
1521     consListSpec.addConstructor(nil)
1522     consListSort = solver.mkDatatypeSort(consListSpec)
1523
1524     x = solver.mkConst(bvSort, "x")
1525     solver.simplify(x)
1526     a = solver.mkConst(bvSort, "a")
1527     solver.simplify(a)
1528     b = solver.mkConst(bvSort, "b")
1529     solver.simplify(b)
1530     x_eq_x = solver.mkTerm(Kind.Equal, x, x)
1531     solver.simplify(x_eq_x)
1532     assert solver.mkTrue() != x_eq_x
1533     assert solver.mkTrue() == solver.simplify(x_eq_x)
1534     x_eq_b = solver.mkTerm(Kind.Equal, x, b)
1535     solver.simplify(x_eq_b)
1536     assert solver.mkTrue() != x_eq_b
1537     assert solver.mkTrue() != solver.simplify(x_eq_b)
1538     slv = pycvc5.Solver()
1539     with pytest.raises(RuntimeError):
1540         slv.simplify(x)
1541
1542     i1 = solver.mkConst(solver.getIntegerSort(), "i1")
1543     solver.simplify(i1)
1544     i2 = solver.mkTerm(Kind.Mult, i1, solver.mkInteger("23"))
1545     solver.simplify(i2)
1546     assert i1 != i2
1547     assert i1 != solver.simplify(i2)
1548     i3 = solver.mkTerm(Kind.Plus, i1, solver.mkInteger(0))
1549     solver.simplify(i3)
1550     assert i1 != i3
1551     assert i1 == solver.simplify(i3)
1552
1553     consList = consListSort.getDatatype()
1554     dt1 = solver.mkTerm(\
1555         Kind.ApplyConstructor,\
1556         consList.getConstructorTerm("cons"),\
1557         solver.mkInteger(0),\
1558         solver.mkTerm(Kind.ApplyConstructor, consList.getConstructorTerm("nil")))
1559     solver.simplify(dt1)
1560     dt2 = solver.mkTerm(\
1561       Kind.ApplySelector, consList["cons"].getSelectorTerm("head"), dt1)
1562     solver.simplify(dt2)
1563
1564     b1 = solver.mkVar(bvSort, "b1")
1565     solver.simplify(b1)
1566     b2 = solver.mkVar(bvSort, "b1")
1567     solver.simplify(b2)
1568     b3 = solver.mkVar(uSort, "b3")
1569     solver.simplify(b3)
1570     v1 = solver.mkConst(bvSort, "v1")
1571     solver.simplify(v1)
1572     v2 = solver.mkConst(solver.getIntegerSort(), "v2")
1573     solver.simplify(v2)
1574     f1 = solver.mkConst(funSort1, "f1")
1575     solver.simplify(f1)
1576     f2 = solver.mkConst(funSort2, "f2")
1577     solver.simplify(f2)
1578     solver.defineFunsRec([f1, f2], [[b1, b2], [b3]], [v1, v2])
1579     solver.simplify(f1)
1580     solver.simplify(f2)
1581
1582
1583 def test_assert_formula(solver):
1584     solver.assertFormula(solver.mkTrue())
1585     with pytest.raises(RuntimeError):
1586         solver.assertFormula(pycvc5.Term(solver))
1587     slv = pycvc5.Solver()
1588     with pytest.raises(RuntimeError):
1589         slv.assertFormula(solver.mkTrue())
1590
1591
1592 def test_check_entailed(solver):
1593     solver.setOption("incremental", "false")
1594     solver.checkEntailed(solver.mkTrue())
1595     with pytest.raises(RuntimeError):
1596         solver.checkEntailed(solver.mkTrue())
1597     slv = pycvc5.Solver()
1598     with pytest.raises(RuntimeError):
1599         slv.checkEntailed(solver.mkTrue())
1600
1601
1602 def test_check_entailed1(solver):
1603     boolSort = solver.getBooleanSort()
1604     x = solver.mkConst(boolSort, "x")
1605     y = solver.mkConst(boolSort, "y")
1606     z = solver.mkTerm(Kind.And, x, y)
1607     solver.setOption("incremental", "true")
1608     solver.checkEntailed(solver.mkTrue())
1609     with pytest.raises(RuntimeError):
1610         solver.checkEntailed(pycvc5.Term(solver))
1611     solver.checkEntailed(solver.mkTrue())
1612     solver.checkEntailed(z)
1613     slv = pycvc5.Solver()
1614     with pytest.raises(RuntimeError):
1615         slv.checkEntailed(solver.mkTrue())
1616
1617
1618 def test_check_entailed2(solver):
1619     solver.setOption("incremental", "true")
1620
1621     uSort = solver.mkUninterpretedSort("u")
1622     intSort = solver.getIntegerSort()
1623     boolSort = solver.getBooleanSort()
1624     uToIntSort = solver.mkFunctionSort(uSort, intSort)
1625     intPredSort = solver.mkFunctionSort(intSort, boolSort)
1626
1627     n = pycvc5.Term(solver)
1628     # Constants
1629     x = solver.mkConst(uSort, "x")
1630     y = solver.mkConst(uSort, "y")
1631     # Functions
1632     f = solver.mkConst(uToIntSort, "f")
1633     p = solver.mkConst(intPredSort, "p")
1634     # Values
1635     zero = solver.mkInteger(0)
1636     one = solver.mkInteger(1)
1637     # Terms
1638     f_x = solver.mkTerm(Kind.ApplyUf, f, x)
1639     f_y = solver.mkTerm(Kind.ApplyUf, f, y)
1640     summ = solver.mkTerm(Kind.Plus, f_x, f_y)
1641     p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
1642     p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
1643     # Assertions
1644     assertions =\
1645         solver.mkTerm(Kind.And,\
1646                       [solver.mkTerm(Kind.Leq, zero, f_x),  # 0 <= f(x)
1647                        solver.mkTerm(Kind.Leq, zero, f_y),  # 0 <= f(y)
1648                        solver.mkTerm(Kind.Leq, summ, one),  # f(x) + f(y) <= 1
1649                        p_0.notTerm(),                        # not p(0)
1650                        p_f_y                                 # p(f(y))
1651                       ])
1652
1653     solver.checkEntailed(solver.mkTrue())
1654     solver.assertFormula(assertions)
1655     solver.checkEntailed(solver.mkTerm(Kind.Distinct, x, y))
1656     solver.checkEntailed(\
1657         [solver.mkFalse(), solver.mkTerm(Kind.Distinct, x, y)])
1658     with pytest.raises(RuntimeError):
1659         solver.checkEntailed(n)
1660     with pytest.raises(RuntimeError):
1661         solver.checkEntailed([n, solver.mkTerm(Kind.Distinct, x, y)])
1662     slv = pycvc5.Solver()
1663     with pytest.raises(RuntimeError):
1664         slv.checkEntailed(solver.mkTrue())
1665
1666
1667 def test_check_sat(solver):
1668     solver.setOption("incremental", "false")
1669     solver.checkSat()
1670     with pytest.raises(RuntimeError):
1671         solver.checkSat()
1672
1673
1674 def test_check_sat_assuming(solver):
1675     solver.setOption("incremental", "false")
1676     solver.checkSatAssuming(solver.mkTrue())
1677     with pytest.raises(RuntimeError):
1678         solver.checkSatAssuming(solver.mkTrue())
1679     slv = pycvc5.Solver()
1680     with pytest.raises(RuntimeError):
1681         slv.checkSatAssuming(solver.mkTrue())
1682
1683
1684 def test_check_sat_assuming1(solver):
1685     boolSort = solver.getBooleanSort()
1686     x = solver.mkConst(boolSort, "x")
1687     y = solver.mkConst(boolSort, "y")
1688     z = solver.mkTerm(Kind.And, x, y)
1689     solver.setOption("incremental", "true")
1690     solver.checkSatAssuming(solver.mkTrue())
1691     with pytest.raises(RuntimeError):
1692         solver.checkSatAssuming(pycvc5.Term(solver))
1693     solver.checkSatAssuming(solver.mkTrue())
1694     solver.checkSatAssuming(z)
1695     slv = pycvc5.Solver()
1696     with pytest.raises(RuntimeError):
1697         slv.checkSatAssuming(solver.mkTrue())
1698
1699
1700 def test_check_sat_assuming2(solver):
1701     solver.setOption("incremental", "true")
1702
1703     uSort = solver.mkUninterpretedSort("u")
1704     intSort = solver.getIntegerSort()
1705     boolSort = solver.getBooleanSort()
1706     uToIntSort = solver.mkFunctionSort(uSort, intSort)
1707     intPredSort = solver.mkFunctionSort(intSort, boolSort)
1708
1709     n = pycvc5.Term(solver)
1710     # Constants
1711     x = solver.mkConst(uSort, "x")
1712     y = solver.mkConst(uSort, "y")
1713     # Functions
1714     f = solver.mkConst(uToIntSort, "f")
1715     p = solver.mkConst(intPredSort, "p")
1716     # Values
1717     zero = solver.mkInteger(0)
1718     one = solver.mkInteger(1)
1719     # Terms
1720     f_x = solver.mkTerm(Kind.ApplyUf, f, x)
1721     f_y = solver.mkTerm(Kind.ApplyUf, f, y)
1722     summ = solver.mkTerm(Kind.Plus, f_x, f_y)
1723     p_0 = solver.mkTerm(Kind.ApplyUf, p, zero)
1724     p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y)
1725     # Assertions
1726     assertions =\
1727         solver.mkTerm(Kind.And,\
1728                       [solver.mkTerm(Kind.Leq, zero, f_x),  # 0 <= f(x)
1729                        solver.mkTerm(Kind.Leq, zero, f_y),  # 0 <= f(y)
1730                        solver.mkTerm(Kind.Leq, summ, one),  # f(x) + f(y) <= 1
1731                        p_0.notTerm(),                        # not p(0)
1732                        p_f_y                                 # p(f(y))
1733                       ])
1734
1735     solver.checkSatAssuming(solver.mkTrue())
1736     solver.assertFormula(assertions)
1737     solver.checkSatAssuming(solver.mkTerm(Kind.Distinct, x, y))
1738     solver.checkSatAssuming(
1739         [solver.mkFalse(),
1740          solver.mkTerm(Kind.Distinct, x, y)])
1741     with pytest.raises(RuntimeError):
1742         solver.checkSatAssuming(n)
1743     with pytest.raises(RuntimeError):
1744         solver.checkSatAssuming([n, solver.mkTerm(Kind.Distinct, x, y)])
1745     slv = pycvc5.Solver()
1746     with pytest.raises(RuntimeError):
1747         slv.checkSatAssuming(solver.mkTrue())
1748
1749
1750 def test_set_logic(solver):
1751     solver.setLogic("AUFLIRA")
1752     with pytest.raises(RuntimeError):
1753         solver.setLogic("AF_BV")
1754     solver.assertFormula(solver.mkTrue())
1755     with pytest.raises(RuntimeError):
1756         solver.setLogic("AUFLIRA")
1757
1758
1759 def test_set_option(solver):
1760     solver.setOption("bv-sat-solver", "minisat")
1761     with pytest.raises(RuntimeError):
1762         solver.setOption("bv-sat-solver", "1")
1763     solver.assertFormula(solver.mkTrue())
1764     with pytest.raises(RuntimeError):
1765         solver.setOption("bv-sat-solver", "minisat")
1766
1767
1768 def test_reset_assertions(solver):
1769     solver.setOption("incremental", "true")
1770
1771     bvSort = solver.mkBitVectorSort(4)
1772     one = solver.mkBitVector(4, 1)
1773     x = solver.mkConst(bvSort, "x")
1774     ule = solver.mkTerm(Kind.BVUle, x, one)
1775     srem = solver.mkTerm(Kind.BVSrem, one, x)
1776     solver.push(4)
1777     slt = solver.mkTerm(Kind.BVSlt, srem, one)
1778     solver.resetAssertions()
1779     solver.checkSatAssuming([slt, ule])
1780
1781
1782 def test_mk_sygus_grammar(solver):
1783     nullTerm = pycvc5.Term(solver)
1784     boolTerm = solver.mkBoolean(True)
1785     boolVar = solver.mkVar(solver.getBooleanSort())
1786     intVar = solver.mkVar(solver.getIntegerSort())
1787
1788     solver.mkSygusGrammar([], [intVar])
1789     solver.mkSygusGrammar([boolVar], [intVar])
1790     with pytest.raises(RuntimeError):
1791         solver.mkSygusGrammar([], [])
1792     with pytest.raises(RuntimeError):
1793         solver.mkSygusGrammar([], [nullTerm])
1794     with pytest.raises(RuntimeError):
1795         solver.mkSygusGrammar([], [boolTerm])
1796     with pytest.raises(RuntimeError):
1797         solver.mkSygusGrammar([boolTerm], [intVar])
1798     slv = pycvc5.Solver()
1799     boolVar2 = slv.mkVar(slv.getBooleanSort())
1800     intVar2 = slv.mkVar(slv.getIntegerSort())
1801     slv.mkSygusGrammar([boolVar2], [intVar2])
1802     with pytest.raises(RuntimeError):
1803         slv.mkSygusGrammar([boolVar], [intVar2])
1804     with pytest.raises(RuntimeError):
1805         slv.mkSygusGrammar([boolVar2], [intVar])
1806
1807
1808 def test_synth_inv(solver):
1809     boolean = solver.getBooleanSort()
1810     integer = solver.getIntegerSort()
1811
1812     nullTerm = pycvc5.Term(solver)
1813     x = solver.mkVar(boolean)
1814
1815     start1 = solver.mkVar(boolean)
1816     start2 = solver.mkVar(integer)
1817
1818     g1 = solver.mkSygusGrammar([x], [start1])
1819     g1.addRule(start1, solver.mkBoolean(False))
1820
1821     g2 = solver.mkSygusGrammar([x], [start2])
1822     g2.addRule(start2, solver.mkInteger(0))
1823
1824     solver.synthInv("", [])
1825     solver.synthInv("i1", [x])
1826     solver.synthInv("i2", [x], g1)
1827
1828     with pytest.raises(RuntimeError):
1829         solver.synthInv("i3", [nullTerm])
1830     with pytest.raises(RuntimeError):
1831         solver.synthInv("i4", [x], g2)
1832
1833
1834 def test_add_sygus_constraint(solver):
1835     nullTerm = pycvc5.Term(solver)
1836     boolTerm = solver.mkBoolean(True)
1837     intTerm = solver.mkInteger(1)
1838
1839     solver.addSygusConstraint(boolTerm)
1840     with pytest.raises(RuntimeError):
1841         solver.addSygusConstraint(nullTerm)
1842     with pytest.raises(RuntimeError):
1843         solver.addSygusConstraint(intTerm)
1844
1845     slv = pycvc5.Solver()
1846     with pytest.raises(RuntimeError):
1847         slv.addSygusConstraint(boolTerm)
1848
1849
1850 def test_add_sygus_inv_constraint(solver):
1851     boolean = solver.getBooleanSort()
1852     real = solver.getRealSort()
1853
1854     nullTerm = pycvc5.Term(solver)
1855     intTerm = solver.mkInteger(1)
1856
1857     inv = solver.declareFun("inv", [real], boolean)
1858     pre = solver.declareFun("pre", [real], boolean)
1859     trans = solver.declareFun("trans", [real, real], boolean)
1860     post = solver.declareFun("post", [real], boolean)
1861
1862     inv1 = solver.declareFun("inv1", [real], real)
1863
1864     trans1 = solver.declareFun("trans1", [boolean, real], boolean)
1865     trans2 = solver.declareFun("trans2", [real, boolean], boolean)
1866     trans3 = solver.declareFun("trans3", [real, real], real)
1867
1868     solver.addSygusInvConstraint(inv, pre, trans, post)
1869
1870     with pytest.raises(RuntimeError):
1871         solver.addSygusInvConstraint(nullTerm, pre, trans, post)
1872     with pytest.raises(RuntimeError):
1873         solver.addSygusInvConstraint(inv, nullTerm, trans, post)
1874     with pytest.raises(RuntimeError):
1875         solver.addSygusInvConstraint(inv, pre, nullTerm, post)
1876     with pytest.raises(RuntimeError):
1877         solver.addSygusInvConstraint(inv, pre, trans, nullTerm)
1878
1879     with pytest.raises(RuntimeError):
1880         solver.addSygusInvConstraint(intTerm, pre, trans, post)
1881
1882     with pytest.raises(RuntimeError):
1883         solver.addSygusInvConstraint(inv1, pre, trans, post)
1884
1885     with pytest.raises(RuntimeError):
1886         solver.addSygusInvConstraint(inv, trans, trans, post)
1887
1888     with pytest.raises(RuntimeError):
1889         solver.addSygusInvConstraint(inv, pre, intTerm, post)
1890     with pytest.raises(RuntimeError):
1891         solver.addSygusInvConstraint(inv, pre, pre, post)
1892     with pytest.raises(RuntimeError):
1893         solver.addSygusInvConstraint(inv, pre, trans1, post)
1894     with pytest.raises(RuntimeError):
1895         solver.addSygusInvConstraint(inv, pre, trans2, post)
1896     with pytest.raises(RuntimeError):
1897         solver.addSygusInvConstraint(inv, pre, trans3, post)
1898
1899     with pytest.raises(RuntimeError):
1900         solver.addSygusInvConstraint(inv, pre, trans, trans)
1901     slv = pycvc5.Solver()
1902     boolean2 = slv.getBooleanSort()
1903     real2 = slv.getRealSort()
1904     inv22 = slv.declareFun("inv", [real2], boolean2)
1905     pre22 = slv.declareFun("pre", [real2], boolean2)
1906     trans22 = slv.declareFun("trans", [real2, real2], boolean2)
1907     post22 = slv.declareFun("post", [real2], boolean2)
1908     slv.addSygusInvConstraint(inv22, pre22, trans22, post22)
1909     with pytest.raises(RuntimeError):
1910         slv.addSygusInvConstraint(inv, pre22, trans22, post22)
1911     with pytest.raises(RuntimeError):
1912         slv.addSygusInvConstraint(inv22, pre, trans22, post22)
1913     with pytest.raises(RuntimeError):
1914         slv.addSygusInvConstraint(inv22, pre22, trans, post22)
1915     with pytest.raises(RuntimeError):
1916         slv.addSygusInvConstraint(inv22, pre22, trans22, post)
1917
1918
1919 def test_get_synth_solution(solver):
1920     solver.setOption("lang", "sygus2")
1921     solver.setOption("incremental", "false")
1922
1923     nullTerm = pycvc5.Term(solver)
1924     x = solver.mkBoolean(False)
1925     f = solver.synthFun("f", [], solver.getBooleanSort())
1926
1927     with pytest.raises(RuntimeError):
1928         solver.getSynthSolution(f)
1929
1930     solver.checkSynth()
1931
1932     solver.getSynthSolution(f)
1933     solver.getSynthSolution(f)
1934
1935     with pytest.raises(RuntimeError):
1936         solver.getSynthSolution(nullTerm)
1937     with pytest.raises(RuntimeError):
1938         solver.getSynthSolution(x)
1939
1940     slv = pycvc5.Solver()
1941     with pytest.raises(RuntimeError):
1942         slv.getSynthSolution(f)
1943
1944 def test_check_synth_next(solver):
1945     solver.setOption("lang", "sygus2")
1946     solver.setOption("incremental", "true")
1947     f = solver.synthFun("f", [], solver.getBooleanSort())
1948
1949     solver.checkSynth()
1950     solver.getSynthSolutions([f])
1951
1952     solver.checkSynthNext()
1953     solver.getSynthSolutions([f])
1954
1955 def test_check_synth_next2(solver):
1956     solver.setOption("lang", "sygus2")
1957     solver.setOption("incremental", "false")
1958     f = solver.synthFun("f", [], solver.getBooleanSort())
1959
1960     solver.checkSynth()
1961     with pytest.raises(RuntimeError):
1962         solver.checkSynthNext()
1963
1964 def test_check_synth_next3(solver):
1965     solver.setOption("lang", "sygus2")
1966     solver.setOption("incremental", "true")
1967     f = solver.synthFun("f", [], solver.getBooleanSort())
1968     with pytest.raises(RuntimeError):
1969         solver.checkSynthNext()
1970
1971 def test_get_abduct(solver):
1972     solver.setLogic("QF_LIA")
1973     solver.setOption("produce-abducts", "true")
1974     solver.setOption("incremental", "false")
1975
1976     intSort = solver.getIntegerSort()
1977     zero = solver.mkInteger(0)
1978     x = solver.mkConst(intSort, "x")
1979     y = solver.mkConst(intSort, "y")
1980
1981     solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero))
1982     conj = solver.mkTerm(Kind.Gt, y, zero)
1983     output = pycvc5.Term(solver)
1984     assert solver.getAbduct(conj, output)
1985     assert not output.isNull() and output.getSort().isBoolean()
1986
1987     boolean = solver.getBooleanSort()
1988     truen = solver.mkBoolean(True)
1989     start = solver.mkVar(boolean)
1990     output2 = pycvc5.Term(solver)
1991     g = solver.mkSygusGrammar([], [start])
1992     conj2 = solver.mkTerm(Kind.Gt, x, zero)
1993     g.addRule(start, truen)
1994     assert solver.getAbduct(conj2, g, output2)
1995     assert output2 == truen
1996
1997 def test_get_abduct2(solver):
1998     solver.setLogic("QF_LIA")
1999     solver.setOption("incremental", "false")
2000     intSort = solver.getIntegerSort()
2001     zero = solver.mkInteger(0)
2002     x = solver.mkConst(intSort, "x")
2003     y = solver.mkConst(intSort, "y")
2004     solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero))
2005     conj = solver.mkTerm(Kind.Gt, y, zero)
2006     output = pycvc5.Term(solver)
2007     with pytest.raises(RuntimeError):
2008         solver.getAbduct(conj, output)
2009
2010 def test_get_abduct_next(solver):
2011     solver.setLogic("QF_LIA")
2012     solver.setOption("produce-abducts", "true")
2013     solver.setOption("incremental", "true")
2014
2015     intSort = solver.getIntegerSort()
2016     zero = solver.mkInteger(0)
2017     x = solver.mkConst(intSort, "x")
2018     y = solver.mkConst(intSort, "y")
2019
2020     solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero))
2021     conj = solver.mkTerm(Kind.Gt, y, zero)
2022     output = pycvc5.Term(solver)
2023     assert solver.getAbduct(conj, output)
2024     output2 = pycvc5.Term(solver)
2025     assert solver.getAbductNext(output2)
2026     assert output != output2
2027
2028
2029 def test_get_interpolant(solver):
2030     solver.setLogic("QF_LIA")
2031     solver.setOption("produce-interpols", "default")
2032     solver.setOption("incremental", "false")
2033
2034     intSort = solver.getIntegerSort()
2035     zero = solver.mkInteger(0)
2036     x = solver.mkConst(intSort, "x")
2037     y = solver.mkConst(intSort, "y")
2038     z = solver.mkConst(intSort, "z")
2039
2040     solver.assertFormula(solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, x, y), zero))
2041     solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero))
2042     conj = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, y, z), zero), solver.mkTerm(Kind.Lt, z, zero))
2043     output = pycvc5.Term(solver)
2044     solver.getInterpolant(conj, output)
2045     assert output.getSort().isBoolean()
2046
2047 def test_get_interpolant_next(solver):
2048     solver.setLogic("QF_LIA")
2049     solver.setOption("produce-interpols", "default")
2050     solver.setOption("incremental", "true")
2051
2052     intSort = solver.getIntegerSort()
2053     zero = solver.mkInteger(0)
2054     x = solver.mkConst(intSort, "x")
2055     y = solver.mkConst(intSort, "y")
2056     z = solver.mkConst(intSort, "z")
2057
2058     solver.assertFormula(solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, x, y), zero))
2059     solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero))
2060     conj = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, y, z), zero), solver.mkTerm(Kind.Lt, z, zero))
2061     output = pycvc5.Term(solver)
2062     solver.getInterpolant(conj, output)
2063     output2 = pycvc5.Term(solver)
2064     solver.getInterpolantNext(output2)
2065
2066     assert output != output2
2067
2068
2069 def test_declare_pool(solver):
2070     intSort = solver.getIntegerSort()
2071     setSort = solver.mkSetSort(intSort)
2072     zero = solver.mkInteger(0)
2073     x = solver.mkConst(intSort, "x")
2074     y = solver.mkConst(intSort, "y")
2075     # declare a pool with initial value  0, x, y
2076     p = solver.declarePool("p", intSort, [zero, x, y])
2077     # pool should have the same sort
2078     assert p.getSort() == setSort
2079     # cannot pass null sort
2080     nullSort = pycvc5.Sort(solver)
2081     with pytest.raises(RuntimeError):
2082         solver.declarePool("i", nullSort, [])
2083
2084 def test_define_fun_global(solver):
2085     bSort = solver.getBooleanSort()
2086
2087     bTrue = solver.mkBoolean(True)
2088     # (define-fun f () Bool true)
2089     f = solver.defineFun("f", [], bSort, bTrue, True)
2090     b = solver.mkVar(bSort, "b")
2091     # (define-fun g (b Bool) Bool b)
2092     g = solver.defineFun("g", [b], bSort, b, True)
2093
2094     # (assert (or (not f) (not (g true))))
2095     solver.assertFormula(
2096         solver.mkTerm(Kind.Or, f.notTerm(),
2097                       solver.mkTerm(Kind.ApplyUf, g, bTrue).notTerm()))
2098     assert solver.checkSat().isUnsat()
2099     solver.resetAssertions()
2100     # (assert (or (not f) (not (g true))))
2101     solver.assertFormula(
2102         solver.mkTerm(Kind.Or, f.notTerm(),
2103                       solver.mkTerm(Kind.ApplyUf, g, bTrue).notTerm()))
2104     assert solver.checkSat().isUnsat()
2105
2106
2107 def test_define_sort(solver):
2108     sortVar0 = solver.mkParamSort("T0")
2109     sortVar1 = solver.mkParamSort("T1")
2110     intSort = solver.getIntegerSort()
2111     realSort = solver.getRealSort()
2112     arraySort0 = solver.mkArraySort(sortVar0, sortVar0)
2113     arraySort1 = solver.mkArraySort(sortVar0, sortVar1)
2114     # Now create instantiations of the defined sorts
2115     arraySort0.substitute(sortVar0, intSort)
2116
2117     arraySort1.substitute([sortVar0, sortVar1], [intSort, realSort])
2118
2119
2120 def test_get_model_domain_elements(solver):
2121     solver.setOption("produce-models", "true")
2122     uSort = solver.mkUninterpretedSort("u")
2123     intSort = solver.getIntegerSort()
2124     x = solver.mkConst(uSort, "x")
2125     y = solver.mkConst(uSort, "y")
2126     z = solver.mkConst(uSort, "z")
2127     f = solver.mkTerm(Kind.Distinct, x, y, z)
2128     solver.assertFormula(f)
2129     solver.checkSat()
2130     solver.getModelDomainElements(uSort)
2131     assert len(solver.getModelDomainElements(uSort)) >= 3
2132     with pytest.raises(RuntimeError):
2133         solver.getModelDomainElements(intSort)
2134
2135
2136 def test_get_synth_solutions(solver):
2137     solver.setOption("lang", "sygus2")
2138     solver.setOption("incremental", "false")
2139
2140     nullTerm = pycvc5.Term(solver)
2141     x = solver.mkBoolean(False)
2142     f = solver.synthFun("f", [], solver.getBooleanSort())
2143
2144     with pytest.raises(RuntimeError):
2145         solver.getSynthSolutions([])
2146     with pytest.raises(RuntimeError):
2147         solver.getSynthSolutions([f])
2148
2149     solver.checkSynth()
2150
2151     solver.getSynthSolutions([f])
2152     solver.getSynthSolutions([f, f])
2153
2154     with pytest.raises(RuntimeError):
2155         solver.getSynthSolutions([])
2156     with pytest.raises(RuntimeError):
2157         solver.getSynthSolutions([nullTerm])
2158     with pytest.raises(RuntimeError):
2159         solver.getSynthSolutions([x])
2160
2161     slv = pycvc5.Solver()
2162     with pytest.raises(RuntimeError):
2163         slv.getSynthSolutions([x])
2164
2165
2166 def test_get_value_sep_heap1(solver):
2167     solver.setLogic("QF_BV")
2168     solver.setOption("incremental", "false")
2169     solver.setOption("produce-models", "true")
2170     t = solver.mkTrue()
2171     solver.assertFormula(t)
2172     with pytest.raises(RuntimeError):
2173         solver.getValueSepHeap()
2174
2175
2176 def test_get_value_sep_heap2(solver):
2177     solver.setLogic("ALL")
2178     solver.setOption("incremental", "false")
2179     solver.setOption("produce-models", "false")
2180     checkSimpleSeparationConstraints(solver)
2181     with pytest.raises(RuntimeError):
2182         solver.getValueSepHeap()
2183
2184
2185 def test_get_value_sep_heap3(solver):
2186     solver.setLogic("ALL")
2187     solver.setOption("incremental", "false")
2188     solver.setOption("produce-models", "true")
2189     t = solver.mkFalse()
2190     solver.assertFormula(t)
2191     solver.checkSat()
2192     with pytest.raises(RuntimeError):
2193         solver.getValueSepHeap()
2194
2195
2196 def test_get_value_sep_heap4(solver):
2197     solver.setLogic("ALL")
2198     solver.setOption("incremental", "false")
2199     solver.setOption("produce-models", "true")
2200     t = solver.mkTrue()
2201     solver.assertFormula(t)
2202     solver.checkSat()
2203     with pytest.raises(RuntimeError):
2204         solver.getValueSepHeap()
2205
2206
2207 def test_get_value_sep_heap5(solver):
2208     solver.setLogic("ALL")
2209     solver.setOption("incremental", "false")
2210     solver.setOption("produce-models", "true")
2211     checkSimpleSeparationConstraints(solver)
2212     solver.getValueSepHeap()
2213
2214
2215 def test_get_value_sep_nil1(solver):
2216     solver.setLogic("QF_BV")
2217     solver.setOption("incremental", "false")
2218     solver.setOption("produce-models", "true")
2219     t = solver.mkTrue()
2220     solver.assertFormula(t)
2221     with pytest.raises(RuntimeError):
2222         solver.getValueSepNil()
2223
2224
2225 def test_get_value_sep_nil2(solver):
2226     solver.setLogic("ALL")
2227     solver.setOption("incremental", "false")
2228     solver.setOption("produce-models", "false")
2229     checkSimpleSeparationConstraints(solver)
2230     with pytest.raises(RuntimeError):
2231         solver.getValueSepNil()
2232
2233
2234 def test_get_value_sep_nil3(solver):
2235     solver.setLogic("ALL")
2236     solver.setOption("incremental", "false")
2237     solver.setOption("produce-models", "true")
2238     t = solver.mkFalse()
2239     solver.assertFormula(t)
2240     solver.checkSat()
2241     with pytest.raises(RuntimeError):
2242         solver.getValueSepNil()
2243
2244
2245 def test_get_value_sep_nil4(solver):
2246     solver.setLogic("ALL")
2247     solver.setOption("incremental", "false")
2248     solver.setOption("produce-models", "true")
2249     t = solver.mkTrue()
2250     solver.assertFormula(t)
2251     solver.checkSat()
2252     with pytest.raises(RuntimeError):
2253         solver.getValueSepNil()
2254
2255
2256 def test_get_value_sep_nil5(solver):
2257     solver.setLogic("ALL")
2258     solver.setOption("incremental", "false")
2259     solver.setOption("produce-models", "true")
2260     checkSimpleSeparationConstraints(solver)
2261     solver.getValueSepNil()
2262
2263
2264 def test_is_model_core_symbol(solver):
2265     solver.setOption("produce-models", "true")
2266     solver.setOption("model-cores", "simple")
2267     uSort = solver.mkUninterpretedSort("u")
2268     x = solver.mkConst(uSort, "x")
2269     y = solver.mkConst(uSort, "y")
2270     z = solver.mkConst(uSort, "z")
2271     zero = solver.mkInteger(0)
2272     f = solver.mkTerm(Kind.Not, solver.mkTerm(Kind.Equal, x, y))
2273     solver.assertFormula(f)
2274     solver.checkSat()
2275     assert solver.isModelCoreSymbol(x)
2276     assert solver.isModelCoreSymbol(y)
2277     assert not solver.isModelCoreSymbol(z)
2278     with pytest.raises(RuntimeError):
2279         solver.isModelCoreSymbol(zero)
2280
2281
2282 def test_issue5893(solver):
2283     slv = pycvc5.Solver()
2284     bvsort4 = solver.mkBitVectorSort(4)
2285     bvsort8 = solver.mkBitVectorSort(8)
2286     arrsort = solver.mkArraySort(bvsort4, bvsort8)
2287     arr = solver.mkConst(arrsort, "arr")
2288     idx = solver.mkConst(bvsort4, "idx")
2289     ten = solver.mkBitVector(8, "10", 10)
2290     sel = solver.mkTerm(Kind.Select, arr, idx)
2291     distinct = solver.mkTerm(Kind.Distinct, sel, ten)
2292     distinct.getOp()
2293
2294
2295 def test_issue7000(solver):
2296     s1 = solver.getIntegerSort()
2297     s2 = solver.mkFunctionSort(s1, s1)
2298     s3 = solver.getRealSort()
2299     t4 = solver.mkPi()
2300     t7 = solver.mkConst(s3, "_x5")
2301     t37 = solver.mkConst(s2, "_x32")
2302     t59 = solver.mkConst(s2, "_x51")
2303     t72 = solver.mkTerm(Kind.Equal, t37, t59)
2304     t74 = solver.mkTerm(Kind.Gt, t4, t7)
2305     # throws logic exception since logic is not higher order by default
2306     with pytest.raises(RuntimeError):
2307         solver.checkEntailed(t72, t74, t72, t72)
2308
2309
2310 def test_mk_sygus_var(solver):
2311     boolSort = solver.getBooleanSort()
2312     intSort = solver.getIntegerSort()
2313     funSort = solver.mkFunctionSort(intSort, boolSort)
2314
2315     solver.mkSygusVar(boolSort)
2316     solver.mkSygusVar(funSort)
2317     solver.mkSygusVar(boolSort, "b")
2318     solver.mkSygusVar(funSort, "")
2319     with pytest.raises(RuntimeError):
2320         solver.mkSygusVar(pycvc5.Sort(solver))
2321     with pytest.raises(RuntimeError):
2322         solver.mkSygusVar(solver.getNullSort(), "a")
2323     slv = pycvc5.Solver()
2324     with pytest.raises(RuntimeError):
2325         slv.mkSygusVar(boolSort)
2326
2327
2328 def test_synth_fun(solver):
2329     null = solver.getNullSort()
2330     boolean = solver.getBooleanSort()
2331     integer = solver.getIntegerSort()
2332
2333     nullTerm = pycvc5.Term(solver)
2334     x = solver.mkVar(boolean)
2335
2336     start1 = solver.mkVar(boolean)
2337     start2 = solver.mkVar(integer)
2338
2339     g1 = solver.mkSygusGrammar(x, [start1])
2340     g1.addRule(start1, solver.mkBoolean(False))
2341
2342     g2 = solver.mkSygusGrammar(x, [start2])
2343     g2.addRule(start2, solver.mkInteger(0))
2344
2345     solver.synthFun("", [], boolean)
2346     solver.synthFun("f1", [x], boolean)
2347     solver.synthFun("f2", [x], boolean, g1)
2348
2349     with pytest.raises(RuntimeError):
2350         solver.synthFun("f3", [nullTerm], boolean)
2351     with pytest.raises(RuntimeError):
2352         solver.synthFun("f4", [], null)
2353     with pytest.raises(RuntimeError):
2354         solver.synthFun("f6", [x], boolean, g2)
2355     slv = pycvc5.Solver()
2356     x2 = slv.mkVar(slv.getBooleanSort())
2357     slv.synthFun("f1", [x2], slv.getBooleanSort())
2358     with pytest.raises(RuntimeError):
2359         slv.synthFun("", [], solver.getBooleanSort())
2360     with pytest.raises(RuntimeError):
2361         slv.synthFun("f1", [x], solver.getBooleanSort())
2362
2363
2364 def test_tuple_project(solver):
2365     sorts = [solver.getBooleanSort(),\
2366                                solver.getIntegerSort(),\
2367                                solver.getStringSort(),\
2368                                solver.mkSetSort(solver.getStringSort())]
2369     elements = [\
2370         solver.mkBoolean(True), \
2371         solver.mkInteger(3),\
2372         solver.mkString("C"),\
2373         solver.mkTerm(Kind.SetSingleton, solver.mkString("Z"))]
2374
2375     tuple = solver.mkTuple(sorts, elements)
2376
2377     indices1 = []
2378     indices2 = [0]
2379     indices3 = [0, 1]
2380     indices4 = [0, 0, 2, 2, 3, 3, 0]
2381     indices5 = [4]
2382     indices6 = [0, 4]
2383
2384     solver.mkTerm(solver.mkOp(Kind.TupleProject, indices1), tuple)
2385
2386     solver.mkTerm(solver.mkOp(Kind.TupleProject, indices2), tuple)
2387
2388     solver.mkTerm(solver.mkOp(Kind.TupleProject, indices3), tuple)
2389
2390     solver.mkTerm(solver.mkOp(Kind.TupleProject, indices4), tuple)
2391
2392     with pytest.raises(RuntimeError):
2393         solver.mkTerm(solver.mkOp(Kind.TupleProject, indices5), tuple)
2394     with pytest.raises(RuntimeError):
2395         solver.mkTerm(solver.mkOp(Kind.TupleProject, indices6), tuple)
2396
2397     indices = [0, 3, 2, 0, 1, 2]
2398
2399     op = solver.mkOp(Kind.TupleProject, indices)
2400     projection = solver.mkTerm(op, tuple)
2401
2402     datatype = tuple.getSort().getDatatype()
2403     constructor = datatype[0]
2404
2405     for i in indices:
2406
2407         selectorTerm = constructor[i].getSelectorTerm()
2408         selectedTerm = solver.mkTerm(Kind.ApplySelector, selectorTerm, tuple)
2409         simplifiedTerm = solver.simplify(selectedTerm)
2410         assert elements[i] == simplifiedTerm
2411
2412         assert "((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton \"Z\")))" == str(
2413             projection)