cvc5.git
2022-04-20 Andres NoetzliImprove handling of `(push)` and `(pop)` (#8641)
2022-04-20 Andrew ReynoldsAdd declare-oracle-fun command (#8621)
2022-04-20 Andrew ReynoldsMinor simplifications for datatype selector triggers...
2022-04-20 yoni206int-blaster: direct support for bvcomp (#8640)
2022-04-20 yoni206Remove redundant assertion in int-blaster (#8639)
2022-04-20 Andrew ReynoldsUpdates to zero level learner (#8597)
2022-04-19 Andrew ReynoldsAvoid trivial equalities in explanation of SETS_CARD_CY...
2022-04-19 Andrew ReynoldsSimplify implementation of subtype methods in TypeNode...
2022-04-19 mudathirmahgoubAdd table.project evaluator (#8632)
2022-04-19 Andrew ReynoldsMove linear arithmetic solver to theory::arith::linear...
2022-04-19 Andrew ReynoldsGeneralize concat conflict for sequences in LFSC (...
2022-04-18 Abdalrhman... Remove instances of `check-proofs` in regressions....
2022-04-18 Andrew ReynoldsAdd some missing FP symbols to LFSC (#8629)
2022-04-18 Andrew ReynoldsDistinguish name variants for types in LFSC node conver...
2022-04-18 Andrew ReynoldsMake more utilities distinguish Int and Real (#8626)
2022-04-18 Andrew ReynoldsSimplify management of separation logic heap (#8580)
2022-04-18 Andres NoetzliRemove support for unused `declare-*` commands (#8623)
2022-04-14 Andrew ReynoldsFix internal type issue for congruence over quantifiers...
2022-04-14 Andrew ReynoldsImplement internal support for (definitional) satisfiab...
2022-04-14 Andrew ReynoldsMake LFSC printer robust to internal types (#8616)
2022-04-14 Andrew ReynoldsImplement internal support for synthesis modulo oracles...
2022-04-14 Andrew ReynoldsRemove static calls to rewrite involving array constant...
2022-04-14 Andrew ReynoldsImprovements to phase shifting + purification lemmas...
2022-04-14 Amalee WilsonRevised partitioning (#8143)
2022-04-14 vinciusb[proofs] [dot] New way to traverse the proof when print...
2022-04-14 Andrew ReynoldsIntegrate oracle checker into quantifiers term registry...
2022-04-14 Andrew ReynoldsFix spurious assertion involving subtypes (#8611)
2022-04-14 Andrew ReynoldsUpdate LFSC version (#8614)
2022-04-13 mudathirmahgoubAdd Relation and Table types to SMTLib parser (#8605)
2022-04-13 Andrew ReynoldsFix type issue for FP constants in LFSC node converter...
2022-04-12 Andrew ReynoldsFix spurious assertion failure caused by subtyping...
2022-04-12 Andrew ReynoldsFix type issue for LFSC null terminator (#8607)
2022-04-12 Andrew ReynoldsAdd oracle checker utility (#8603)
2022-04-12 Andrew ReynoldsAdd oracle caller utility (#8599)
2022-04-12 Andrew ReynoldsMaking some benchmarks SMT-LIB compliant for subtypes...
2022-04-12 Andrew ReynoldsFix more misuses of arithmetic subtypes (#8601)
2022-04-12 vinciusb[proofs] [dot] Print nodes clusters at dot format ...
2022-04-11 Andrew ReynoldsMore cleaning uses of arithmetic subtyping (#8595)
2022-04-11 Andrew ReynoldsAdd oracle engine to quantifiers engine (#8589)
2022-04-11 Andrew ReynoldsRemove spurious case of ppRewrite (#8596)
2022-04-11 Andrew ReynoldsAdd learned literal type and prop learned database...
2022-04-08 Andres NoetzliSimplify parser (#8592)
2022-04-08 Andrew ReynoldsMinor refactoring of smt2 printer (#8588)
2022-04-08 Andrew ReynoldsDo not allow unresolved sorts in smt2 (#8587)
2022-04-08 Andrew ReynoldsEliminate more uses of CONST_RATIONAL (#8590)
2022-04-08 Andrew ReynoldsProperly parse numerals as real when integers are disab...
2022-04-07 Andrew ReynoldsGeneralization for sygus verify utility (#8586)
2022-04-07 Andrew ReynoldsInternal representation of oracle interface quantifiers...
2022-04-07 Andrew ReynoldsAdd method to get leaves of a NodeTrie (#8583)
2022-04-07 Andrew ReynoldsMake sets and bags operators left-associative (#8584)
2022-04-07 Andrew ReynoldsEliminate SmtSolver dependency on SolverEngineState...
2022-04-07 Andrew ReynoldsMinor fix for printing nullary operators in smt2 (...
2022-04-07 Andrew ReynoldsFix proof checker for SUBS (#8578)
2022-04-06 Andrew ReynoldsFixes for LFSC printing and signatures (#8579)
2022-04-05 Mathias PreinerStart post-release for 1.0.0
2022-04-05 Mathias PreinerBump version to 1.0.0 cvc5-1.0.0
2022-04-05 Aina Niemetzapi: Fix doc generation for kinds in java API. (#8576)
2022-04-05 Mathias PreinerUpdate copyright headers for release 1.0 (#8539)
2022-04-05 Mathias PreinerUpdate NEWS for cvc5 1.0. (#8460)
2022-04-05 Andrew ReynoldsMake inst constant attribute robust to purification...
2022-04-05 Gereon KremerMake rewriter more robust against RAN becoming rational...
2022-04-05 Aina Niemetzapi: More fixes in the java API. (#8571)
2022-04-05 Andrew ReynoldsBe permissive for subtyping in function definitions...
2022-04-05 Aina Niemetzapi: More fixes in C++ API docs. (#8570)
2022-04-05 Alex OzdemirWrite-up for Pythonic API quickstart (#8566)
2022-04-05 Mathias Preinerdocs: Fix mkTerm calls in theory documentation. (#8567)
2022-04-05 Aina Niemetzapi: Fix OptionInfo docs for java API. (#8569)
2022-04-05 Aina Niemetzapi: Fixes in docs for Op. (#8565)
2022-04-05 Aina Niemetzapi: Fixes for Grammar docs in java API. (#8563)
2022-04-05 Aina Niemetzapi: Fixes in java api docs. (#8562)
2022-04-05 Aina Niemetzapi: Fixes in docs for DatatypeConstructor. (#8561)
2022-04-05 mudathirmahgoubDocs: remove api from package name in java.rst (#8560)
2022-04-04 Aina Niemetzapi: More fixes in docs. (#8559)
2022-04-04 Aina Niemetzapi: First batch of fixes in the api docs. (#8558)
2022-04-04 Gereon KremerFix links when converting kinds documentation to python...
2022-04-04 Aina Niemetzpython api: More fixes. (#8556)
2022-04-04 Mathias PreinerStart post-release for 0.0.12
2022-04-04 Mathias PreinerBump version to 0.0.12
2022-04-04 Gereon KremerMaintain symlink to docs for latest release (#8555)
2022-04-04 Gereon KremerRemove duplicate lines (#8552)
2022-04-04 Alex OzdemirBump Pythonic (transcendentals) & exception example...
2022-04-04 Aina Niemetzapi: Various fixes in Python documentation. (#8554)
2022-04-04 Gereon KremerVarious improvements and fixes in the documentation...
2022-04-04 Andrew ReynoldsRename getInstantiatedConstructorTerm to getInstantiate...
2022-04-04 Andrew ReynoldsUse raw symbols in proofs (#8550)
2022-04-04 Haniel Barbosa[proofs] [sat] Make SAT assumption bookeeping robust...
2022-04-04 Andrew ReynoldsFix for get-value with empty uninterpreted sort domain...
2022-04-03 Mathias PreinerStart post-release for 0.0.11
2022-04-03 Mathias PreinerBump version to 0.0.11
2022-04-02 Gereon Kremeruse one process more than we have cores (#8545)
2022-04-02 Andrew ReynoldsRename mkSygusGrammar to mkGrammar (#8544)
2022-04-02 Andrew ReynoldsRemove variant of mkDatatypeDecl with one sort paramete...
2022-04-02 Aina Niemetzapi: Rename get(Selector|Constructor)Term() to getTerm...
2022-04-02 Gereon KremerFollow renaming within pythonic API (#8532)
2022-04-02 Gereon KremerAlways cancel already running CI runs on forks (#8542)
2022-04-02 Cesare TinelliMinor edits in docs. (#8540)
2022-04-02 Andrew ReynoldsIgnore irrelevant exponential terms (#8534)
2022-04-02 Mathias Preinerdocs: Add Python installation instructions for pip...
2022-04-02 Aina Niemetzapi: Remove DatatypeConstructor::getSelectorTerm()...
2022-04-02 Andrew ReynoldsRequire that used model values are constant in CEGQI...
next