projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Rename getInstantiatedConstructorTerm to getInstantiatedTerm (#8549)
[cvc5.git] / test /
2022-04-04 Andrew ReynoldsRename getInstantiatedConstructorTerm to getInstantiate... tree | commitdiff
2022-04-04 Haniel Barbosa[proofs] [sat] Make SAT assumption bookeeping robust... tree | commitdiff
2022-04-04 Andrew ReynoldsFix for get-value with empty uninterpreted sort domain... tree | commitdiff
2022-04-02 Andrew ReynoldsRename mkSygusGrammar to mkGrammar (#8544) tree | commitdiff
2022-04-02 Andrew ReynoldsRemove variant of mkDatatypeDecl with one sort paramete... tree | commitdiff
2022-04-02 Aina Niemetzapi: Rename get(Selector|Constructor)Term() to getTerm... tree | commitdiff
2022-04-02 Andrew ReynoldsIgnore irrelevant exponential terms (#8534) tree | commitdiff
2022-04-02 Aina Niemetzapi: Remove DatatypeConstructor::getSelectorTerm()... tree | commitdiff
2022-04-02 Andrew ReynoldsRequire that used model values are constant in CEGQI... tree | commitdiff
2022-04-02 mudathirmahgoubRemove java API methods that accepts lists as arguments... tree | commitdiff
2022-04-01 Gereon KremerSimplify the python base API in a few places (#8514) tree | commitdiff
2022-04-01 Andrew ReynoldsSimplifications to the datatypes API (#8511) tree | commitdiff
2022-04-01 Gereon KremerPrevent using the coverings solver with extended operat... tree | commitdiff
2022-04-01 Aina Niemetzapi: Remove Datatype::getConstructorTerm(). (#8529) tree | commitdiff
2022-04-01 Haniel BarbosaReplace regression by minimized one via ddSMT (#8531) tree | commitdiff
2022-04-01 Aina NiemetzPython API: Do not rename enumerators. (#8507) tree | commitdiff
2022-04-01 Haniel Barbosa[proofs] [alethe] Fix Alethe post-processor (#8525) tree | commitdiff
2022-04-01 Andrew ReynoldsInternal simplifications to constructing datatypes... tree | commitdiff
2022-04-01 Gereon KremerRemove decorator from python API (#8505) tree | commitdiff
2022-04-01 Andres Noetzli[API] Add mode argument for `Solver::blockModel()`... tree | commitdiff
2022-04-01 Andres Noetzli[API] Remove redundant version of `mkFunctionSort`... tree | commitdiff
2022-04-01 Andrew ReynoldsFix sygus-inst when combined with bounded string quanti... tree | commitdiff
2022-04-01 Mathias Preinerapi: Swap arguments of declareSygusVar. (#8499) tree | commitdiff
2022-04-01 Mathias Preinerapi: Use std::optional for symbols in mk* functions... tree | commitdiff
2022-03-31 Andrew ReynoldsHandled quoted symbols in indexed operators (#8491) tree | commitdiff
2022-03-31 Aina NiemetzSort, TypeNode: Rename functions related to datatypes... tree | commitdiff
2022-03-31 Andrew ReynoldsDisable minisat variable elimination when a parametric... tree | commitdiff
2022-03-31 Andrew ReynoldsDo not export dt.size (#8483) tree | commitdiff
2022-03-31 Andrew ReynoldsFix check for whether PI is reduced (#8485) tree | commitdiff
2022-03-31 Andrew ReynoldsFix lower vs upper bound issue for eager RE conflicts... tree | commitdiff
2022-03-31 Andres NoetzliMove Java package to `io.github.cvc5` (#8469) tree | commitdiff
2022-03-31 Andrew ReynoldsFix non-termination in the strings rewriter (#8438) tree | commitdiff
2022-03-31 Andrew ReynoldsFix case of Boolean skolem for ground term E-matching... tree | commitdiff
2022-03-30 Gereon KremerAllow for multiple (equal) base model values (#8467) tree | commitdiff
2022-03-30 Mathias PreinerExclude competition build for issue8377-resolve-indexed... tree | commitdiff
2022-03-30 Mathias PreinerMove cvc5::internal::context to cvc5::context. (#8451) tree | commitdiff
2022-03-30 mudathirmahgoubPatch cross reference in Kind.java documentation (... tree | commitdiff
2022-03-30 Aina Niemetzapi: Add Sort::getUninterpretedSortConstructor(). ... tree | commitdiff
2022-03-30 Andrew ReynoldsFix policy for purifying arguments of exp (#8416) tree | commitdiff
2022-03-30 Andrew ReynoldsFixes for sygus-inst (#8448) tree | commitdiff
2022-03-30 Andrew ReynoldsFix subtype issue in cegqi arithmetic (#8440) tree | commitdiff
2022-03-30 yoni206Add information for cardinality constraint to the Pytho... tree | commitdiff
2022-03-30 yoni206Adding some missing python API methods and tests (... tree | commitdiff
2022-03-30 Andrew ReynoldsChange tuple tokens and update datatypes theory ref... tree | commitdiff
2022-03-30 mudathirmahgoubFix some documentation warnings (#8453) tree | commitdiff
2022-03-30 Mathias PreinerRename master branch to main. (#8452) tree | commitdiff
2022-03-30 Aina NiemetzTypeNode: Rename isSort() and getSortConstructorArity... tree | commitdiff
2022-03-29 Mathias PreinerIntroduce internal namespace and remove api namespace... tree | commitdiff
2022-03-29 Aina Niemetzapi: Add Sort::getInstantiatedParameters(). (#8445) tree | commitdiff
2022-03-29 yoni206bv-to-int: fix translation of bvneg (#8437) tree | commitdiff
2022-03-29 Andrew ReynoldsAdd information for cardinality constraint to the API... tree | commitdiff
2022-03-29 Andrew ReynoldsMake ProofNodeManager mkScope more robust (#8435) tree | commitdiff
2022-03-29 Andrew ReynoldsFix issue related to use of Boolean term variable for... tree | commitdiff
2022-03-29 Andres Noetzli[API] Add `{is,get}RoundingModeValue()` (#8429) tree | commitdiff
2022-03-29 Clark BarrettFix for issue 5925: constant arrays should be nonlinear... tree | commitdiff
2022-03-29 Aina Niemetzapi: Add Sort::isInstantiated(). (#8425) tree | commitdiff
2022-03-29 Andres NoetzliMove `RoundingMode` to `cvc5_types.h` (#8427) tree | commitdiff
2022-03-28 Mathias PreinerRename get-interpol to get-interpolant. (#8424) tree | commitdiff
2022-03-28 Aina Niemetzapi: Remove left-over Sort::getUninterpretedSortName... tree | commitdiff
2022-03-28 Andrew ReynoldsFix synth result python unit test (#8418) tree | commitdiff
2022-03-26 yoni206Separating produce-interpols from the mode of interpola... tree | commitdiff
2022-03-26 Aina Niemetzapi: Rename *SortConstructor* to *UninterpretedSortCons... tree | commitdiff
2022-03-26 Andrew ReynoldsFix spurious assertion failure (#8404) tree | commitdiff
2022-03-26 Andrew ReynoldsMore minor cleaning of options (#8401) tree | commitdiff
2022-03-26 Andrew ReynoldsFixes for API kind documentation (#8397) tree | commitdiff
2022-03-26 Gereon KremerAdd API unit tests for options (#8339) tree | commitdiff
2022-03-25 Mathias Preinerapi: Unify mkOp variants. (#8369) tree | commitdiff
2022-03-25 Andres Noetzli[Parser] Fix resolution of indexed symbols (#8383) tree | commitdiff
2022-03-25 Aina Niemetzapi: Remove Sort::isParametricDatatype(). (#8405) tree | commitdiff
2022-03-25 Haniel Barbosa[proofs] [sat] Have SAT solver communicate whether... tree | commitdiff
2022-03-25 Andrew ReynoldsUpdate checkSynth and checkSynthNext to return SynthRes... tree | commitdiff
2022-03-25 Andrew ReynoldsChange output of abduction/interpolation for failed... tree | commitdiff
2022-03-25 Andres NoetzliFix Python API tests (#8392) tree | commitdiff
2022-03-25 Andrew ReynoldsProperly guard commands in the SyGuS API (#8390) tree | commitdiff
2022-03-25 Andrew ReynoldsRecategorize options (#8386) tree | commitdiff
2022-03-24 Haniel Barbosa[unsat-cores] [sat-proof] Fix open proofs due to theory... tree | commitdiff
2022-03-23 Andrew ReynoldsClean options (#8309) tree | commitdiff
2022-03-23 Gereon KremerAdd API unit tests for statistics (#8341) tree | commitdiff
2022-03-23 Andrew ReynoldsAdd SynthResult to the API (#8370) tree | commitdiff
2022-03-23 Gereon KremerAdd `getOptionInfo()` and `getOptionNames()` to python... tree | commitdiff
2022-03-23 Andrew ReynoldsMake IDOF_MAX rewrite only apply when all children... tree | commitdiff
2022-03-23 mudathirmahgoubFix cvc5-projects issue 497 (#8331) tree | commitdiff
2022-03-23 Andrew ReynoldsFix non-termination issue in sygus enumerator (#8340) tree | commitdiff
2022-03-22 Andres Noetzli[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334) tree | commitdiff
2022-03-22 Andrew ReynoldsFixes for witness terms appearing in CEGQI instantiatio... tree | commitdiff
2022-03-22 Andrew ReynoldsRefactor result class (#8313) tree | commitdiff
2022-03-22 Mathias Preinerapi: Unify mkTerm variants. (#8357) tree | commitdiff
2022-03-22 Andres Noetzli[API] Support `Op::operator[]` in Java and Python ... tree | commitdiff
2022-03-21 Andres NoetzliRemove `Op::getIndices()` (#8355) tree | commitdiff
2022-03-21 Gereon KremerFix names of unit tests (#8338) tree | commitdiff
2022-03-20 Gereon KremerAdd `getStatistics()` to python API (#8343) tree | commitdiff
2022-03-17 Aina Niemetzctest: Fix labels for python unit tests. (#8328) tree | commitdiff
2022-03-17 Gereon KremerReplace `Debug` by `Trace` (#7793) tree | commitdiff
2022-03-16 Aina NiemetzAdd unit test and assertion to test and catch cvc5... tree | commitdiff
2022-03-16 Andres NoetzliRemove unused files in `regress0` (#8325) tree | commitdiff
2022-03-16 Mathias Preinerunit: Add test for api::Kind. (#8322) tree | commitdiff
2022-03-16 Aina NiemetzFirst step towards refactoring regression tests. (... tree | commitdiff
2022-03-16 mudathirmahgoubAdd regression for cvc5-projects issue 490 (#8317) tree | commitdiff
2022-03-16 Mathias Preinerrun_regression: Make sure to strip trailing whitespaces... tree | commitdiff
2022-03-16 Andrew ReynoldsFix getModelValue for arithmetic (#8316) tree | commitdiff
next