Adding some missing python API methods and tests (#8441)
[cvc5.git] / test /
2022-03-30 yoni206Adding some missing python API methods and tests (...
2022-03-30 Andrew ReynoldsChange tuple tokens and update datatypes theory ref...
2022-03-30 mudathirmahgoubFix some documentation warnings (#8453)
2022-03-30 Mathias PreinerRename master branch to main. (#8452)
2022-03-30 Aina NiemetzTypeNode: Rename isSort() and getSortConstructorArity...
2022-03-29 Mathias PreinerIntroduce internal namespace and remove api namespace...
2022-03-29 Aina Niemetzapi: Add Sort::getInstantiatedParameters(). (#8445)
2022-03-29 yoni206bv-to-int: fix translation of bvneg (#8437)
2022-03-29 Andrew ReynoldsAdd information for cardinality constraint to the API...
2022-03-29 Andrew ReynoldsMake ProofNodeManager mkScope more robust (#8435)
2022-03-29 Andrew ReynoldsFix issue related to use of Boolean term variable for...
2022-03-29 Andres Noetzli[API] Add `{is,get}RoundingModeValue()` (#8429)
2022-03-29 Clark BarrettFix for issue 5925: constant arrays should be nonlinear...
2022-03-29 Aina Niemetzapi: Add Sort::isInstantiated(). (#8425)
2022-03-29 Andres NoetzliMove `RoundingMode` to `cvc5_types.h` (#8427)
2022-03-28 Mathias PreinerRename get-interpol to get-interpolant. (#8424)
2022-03-28 Aina Niemetzapi: Remove left-over Sort::getUninterpretedSortName...
2022-03-28 Andrew ReynoldsFix synth result python unit test (#8418)
2022-03-26 yoni206Separating produce-interpols from the mode of interpola...
2022-03-26 Aina Niemetzapi: Rename *SortConstructor* to *UninterpretedSortCons...
2022-03-26 Andrew ReynoldsFix spurious assertion failure (#8404)
2022-03-26 Andrew ReynoldsMore minor cleaning of options (#8401)
2022-03-26 Andrew ReynoldsFixes for API kind documentation (#8397)
2022-03-26 Gereon KremerAdd API unit tests for options (#8339)
2022-03-25 Mathias Preinerapi: Unify mkOp variants. (#8369)
2022-03-25 Andres Noetzli[Parser] Fix resolution of indexed symbols (#8383)
2022-03-25 Aina Niemetzapi: Remove Sort::isParametricDatatype(). (#8405)
2022-03-25 Haniel Barbosa[proofs] [sat] Have SAT solver communicate whether...
2022-03-25 Andrew ReynoldsUpdate checkSynth and checkSynthNext to return SynthRes...
2022-03-25 Andrew ReynoldsChange output of abduction/interpolation for failed...
2022-03-25 Andres NoetzliFix Python API tests (#8392)
2022-03-25 Andrew ReynoldsProperly guard commands in the SyGuS API (#8390)
2022-03-25 Andrew ReynoldsRecategorize options (#8386)
2022-03-24 Haniel Barbosa[unsat-cores] [sat-proof] Fix open proofs due to theory...
2022-03-23 Andrew ReynoldsClean options (#8309)
2022-03-23 Gereon KremerAdd API unit tests for statistics (#8341)
2022-03-23 Andrew ReynoldsAdd SynthResult to the API (#8370)
2022-03-23 Gereon KremerAdd `getOptionInfo()` and `getOptionNames()` to python...
2022-03-23 Andrew ReynoldsMake IDOF_MAX rewrite only apply when all children...
2022-03-23 mudathirmahgoubFix cvc5-projects issue 497 (#8331)
2022-03-23 Andrew ReynoldsFix non-termination issue in sygus enumerator (#8340)
2022-03-22 Andres Noetzli[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334)
2022-03-22 Andrew ReynoldsFixes for witness terms appearing in CEGQI instantiatio...
2022-03-22 Andrew ReynoldsRefactor result class (#8313)
2022-03-22 Mathias Preinerapi: Unify mkTerm variants. (#8357)
2022-03-22 Andres Noetzli[API] Support `Op::operator[]` in Java and Python ...
2022-03-21 Andres NoetzliRemove `Op::getIndices()` (#8355)
2022-03-21 Gereon KremerFix names of unit tests (#8338)
2022-03-20 Gereon KremerAdd `getStatistics()` to python API (#8343)
2022-03-17 Aina Niemetzctest: Fix labels for python unit tests. (#8328)
2022-03-17 Gereon KremerReplace `Debug` by `Trace` (#7793)
2022-03-16 Aina NiemetzAdd unit test and assertion to test and catch cvc5...
2022-03-16 Andres NoetzliRemove unused files in `regress0` (#8325)
2022-03-16 Mathias Preinerunit: Add test for api::Kind. (#8322)
2022-03-16 Aina NiemetzFirst step towards refactoring regression tests. (...
2022-03-16 mudathirmahgoubAdd regression for cvc5-projects issue 490 (#8317)
2022-03-16 Mathias Preinerrun_regression: Make sure to strip trailing whitespaces...
2022-03-16 Andrew ReynoldsFix getModelValue for arithmetic (#8316)
2022-03-16 Andrew ReynoldsEnsure trusted steps are given for skolem lemmas when...
2022-03-15 Andrew ReynoldsMake learned literal computation more robust (#8308)
2022-03-15 Aina Niemetzapi: Remove Sort::isFirstClass(). (#8312)
2022-03-15 Andres Noetzli[BV] Fix strategy for rewriting `bvnot` (#8297)
2022-03-15 Andrew ReynoldsAdd unit test involving seq concat term (#8257)
2022-03-15 Andrew ReynoldsFix issues involving multiple sources of model substitu...
2022-03-15 mudathirmahgoubAdd skolem lemmas for bags card terms (#7995)
2022-03-15 Andrew ReynoldsProperly guard sort instantiate (#8247)
2022-03-15 Andrew ReynoldsFix to consider leafs of theory sets to be variables...
2022-03-15 Andrew ReynoldsSimplify reductions for set and bag choose (#8304)
2022-03-15 Aina NiemetzRename TO_FP operator kinds. (#8285)
2022-03-14 Andrew ReynoldsFixes for skolem definition management (#8301)
2022-03-14 Andrew ReynoldsRemove unecessary methods from the API (#8260)
2022-03-14 Andrew ReynoldsAdd rewrite for allchar beneath union + star (#8299)
2022-03-14 Andrew ReynoldsRun preprocess rewrite on equalities until fixed point...
2022-03-12 Andrew ReynoldsIntroduce new splitting inference in sets + cardinality...
2022-03-12 Mathias Preinercmake: Do not require googletest if unit tests are...
2022-03-12 Andrew ReynoldsAlways ensure literal when requiring phase via inferenc...
2022-03-11 Andres Noetzli[API/Python] Add support for `Solver::getModel()` ...
2022-03-11 Andrew ReynoldsRemove old decision justification heurstic (#8275)
2022-03-11 Andrew ReynoldsUpdate abduction and interpolation API to not use pass...
2022-03-11 Andrew ReynoldsConsider APPLY_CONSTRUCTOR applied to values to be...
2022-03-11 Andrew ReynoldsFix reduction for arc trig functions (#8289)
2022-03-10 Andrew ReynoldsFix theoryOf call in get equality status (#8279)
2022-03-10 Andrew ReynoldsEliminate unecessary datatype options (#8280)
2022-03-10 mudathirmahgoubFix cvc5-projects issue 475 (#8278)
2022-03-10 Andrew ReynoldsAdd output -o pre-asserts (#8270)
2022-03-10 Andrew ReynoldsDisable timing out regressions (#8273)
2022-03-10 Mathias PreinerFix regression errors for arm64 nightlies. (#8268)
2022-03-09 Gereon KremerRename expert statistics to internal, add documentation...
2022-03-09 Gereon KremerClear obsolete pending lemmas in arithmetic (#8236)
2022-03-09 Andrew ReynoldsAdd regression for fixed issue 6700 (#8265)
2022-03-08 Andrew ReynoldsDo not expand APPLY_SELECTOR (#8174)
2022-03-08 Andres Noetzli[API/Python] Add support for `Solver::getProof()` ...
2022-03-08 Andrew ReynoldsGuard another case of non-termination in quantifiers...
2022-03-08 Gereon KremerMake one CI job not use libpoly (#8261)
2022-03-08 Andrew ReynoldsEliminate shadowing in the quantifiers rewriter (#8244)
2022-03-08 Andrew ReynoldsAdd unit for fixed project issue (#8253)
2022-03-07 Andres NoetzliUpdate documentation of `Solver::getUnsatCore()` (...
2022-03-07 Gereon KremerTry harder to show that a RAN is rational (#8230)
2022-03-06 Andres NoetzliDisallow models with `--arrays-weak-equiv` (#8217)
2022-03-05 Andrew ReynoldsUnit tests for fixed projects issues (#8229)
next