projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add REGEXP_ALL kind to API (#8264)
[cvc5.git] / src / api / cpp / cvc5.cpp
2022-03-09 Andrew ReynoldsAdd REGEXP_ALL kind to API (#8264) blob | commitdiff | raw
2022-03-09 Andrew ReynoldsEliminate the APPLY_SELECTOR_TOTAL kind (#8266) blob | commitdiff | raw | diff to current
2022-03-05 Andrew ReynoldsMake seq.unit robust wrt subtyping (#8209) blob | commitdiff | raw | diff to current
2022-03-04 Andrew ReynoldsAdd support for get learned literals in the API (#8099) blob | commitdiff | raw | diff to current
2022-02-24 Andrew ReynoldsCheck for free variables in several SolverEngine calls... blob | commitdiff | raw | diff to current
2022-02-08 Andrew ReynoldsAlways produce assertions (#8041) blob | commitdiff | raw | diff to current
2022-02-04 Aina NiemetzFP: Rename tester kinds. (#8037) blob | commitdiff | raw | diff to current
2022-02-03 mudathirmahgoubAdd table.product operator (#8020) blob | commitdiff | raw | diff to current
2022-02-03 Aina NiemetzRename kind PLUS -> ADD. (#8036) blob | commitdiff | raw | diff to current
2022-02-03 Aina Niemetzapi: Rename kinds MINUS -> SUB and UMINUS -> NEG. ... blob | commitdiff | raw | diff to current
2022-02-03 Aina Niemetzapi: Add explicit guard for option produce-assertions... blob | commitdiff | raw | diff to current
2022-02-02 Aina NiemetzRename kinds MINUS -> SUB and UMINUS -> NEG. (#8035) blob | commitdiff | raw | diff to current
2022-02-02 Aina Niemetzapi: Rename mk<Value> functions for FP for consistency... blob | commitdiff | raw | diff to current
2022-02-01 mudathirmahgoubAdd bag.filter operator (#8006) blob | commitdiff | raw | diff to current
2022-01-18 Andres Noetzli[API] Add missing arity check (#7905) blob | commitdiff | raw | diff to current
2022-01-13 Andres NoetzliUnify abstract values and uninterpreted constants ... blob | commitdiff | raw | diff to current
2022-01-10 Andrew ReynoldsCheck arity in Sort::instantiate (#7897) blob | commitdiff | raw | diff to current
2022-01-10 Aina Niemetzapi: Remove Sort::isComparableTo(). (#7903) blob | commitdiff | raw | diff to current
2022-01-10 Matthew SotoudehAvoid gcc/10.1.0 bug by moving some configuration into... blob | commitdiff | raw | diff to current
2022-01-06 Andrew ReynoldsMake alpha equivalence user context dependent (#7889) blob | commitdiff | raw | diff to current
2022-01-05 Aina Niemetzcppapi: Remove Datatype::hasNestedRecursion(). (#7878) blob | commitdiff | raw | diff to current
2022-01-05 Aina Niemetzapi: Add missing guard for Datatype::isFinite(). (... blob | commitdiff | raw | diff to current
2022-01-04 mudathirmahgoubAdd bag.member operator to theory of bags (#7857) blob | commitdiff | raw | diff to current
2022-01-04 Aina Niemetzapi: Remove redundant check in Term::toString(). (... blob | commitdiff | raw | diff to current
2022-01-03 Aina Niemetzapi: Remove redundant check in Sort::toString(). (... blob | commitdiff | raw | diff to current
2021-12-22 Andrew ReynoldsAdd support for incremental + interpolants (#7853) blob | commitdiff | raw | diff to current
2021-12-21 Andrew ReynoldsSupport get-abduct-next (#7850) blob | commitdiff | raw | diff to current
2021-12-20 Andrew ReynoldsAllow SyGuS subsolver to be reused in incremental mode... blob | commitdiff | raw | diff to current
2021-12-17 Andrew ReynoldsMinor refactoring of API for eliminating arithmetic... blob | commitdiff | raw | diff to current
2021-12-17 Andrew ReynoldsGet getRealOrIntegerValueSign to the API (#7832) blob | commitdiff | raw | diff to current
2021-12-17 Aina Niemetzapi: Rename DatatypeSelector::getRangeSort() to getCodo... blob | commitdiff | raw | diff to current
2021-12-17 Aina Niemetzapi: Add Solver::mkUnresolvedSort(). (#7817) blob | commitdiff | raw | diff to current
2021-12-16 Aina Niemetzapi: Add Sort::hasSymbol() and Sort::getSymbol(). ... blob | commitdiff | raw | diff to current
2021-12-14 Andrew ReynoldsThrow exception for getting value of non-well-founded... blob | commitdiff | raw | diff to current
2021-12-13 Andrew ReynoldsFixes and additions for API for parametric datatypes... blob | commitdiff | raw | diff to current
2021-12-10 Andrew ReynoldsRefactor and fixes related to getSpecializedConstructor... blob | commitdiff | raw | diff to current
2021-12-08 Aina Niemetzapi: Fix Sort::getDatatypeArity() for non-parametric... blob | commitdiff | raw | diff to current
2021-12-03 Andrew ReynoldsProper error for using constructor in multiple datatype... blob | commitdiff | raw | diff to current
2021-12-02 Gereon KremerAdd explicit 64bit getters for Integer class (#7728) blob | commitdiff | raw | diff to current
2021-12-02 mudathirmahgoubadd bag.fold operator (#7718) blob | commitdiff | raw | diff to current
2021-12-01 Mathias Preinerapi: Add missing bit-width 0 check to mkBVFromStrHelper... blob | commitdiff | raw | diff to current
2021-11-25 Aina Niemetzapi: Refactor mkTerm for kinds with arity = 0. (#7699) blob | commitdiff | raw | diff to current
2021-11-24 Aina Niemetzapi: Fix creation of nary term kinds via Op. (#7688) blob | commitdiff | raw | diff to current
2021-11-19 Andres Noetzli[API] Avoid copying values (#7666) blob | commitdiff | raw | diff to current
2021-11-18 Aina Niemetzapi: Fix categorization of DT kinds in kind maps. ... blob | commitdiff | raw | diff to current
2021-11-15 Aina Niemetzapi: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632) blob | commitdiff | raw | diff to current
2021-11-13 mudathirmahgoubAdd operator set.map to theory of sets (#7641) blob | commitdiff | raw | diff to current
2021-11-12 mudathirmahgoubbags: Rename kinds with a more consistent naming scheme... blob | commitdiff | raw | diff to current
2021-11-12 Andres NoetzliRemove `ConstantMap<Rational>` (#7635) blob | commitdiff | raw | diff to current
2021-11-11 Abdalrhman MohamedAdd an API method to get the raw name of a term. (... blob | commitdiff | raw | diff to current
2021-11-11 Andrew ReynoldsGeneralize front-end checks to check for shadowed varia... blob | commitdiff | raw | diff to current
2021-11-10 Aina Niemetzapi: Add Solver::mkRegexpAll(). (#7614) blob | commitdiff | raw | diff to current
2021-11-10 Aina Niemetzsets: Rename set.intersection to set.inter. (#7622) blob | commitdiff | raw | diff to current
2021-11-09 Aina Niemetzregex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match... blob | commitdiff | raw | diff to current
2021-11-08 Aina Niemetzsets: Rename kinds with a more consistent naming scheme... blob | commitdiff | raw | diff to current
2021-11-06 Abdalrhman MohamedPrint `unsupported` for unrecognized flags. (#7384) blob | commitdiff | raw | diff to current
2021-11-04 Gereon KremerStart refactoring of `-o` and `-v` (#7449) blob | commitdiff | raw | diff to current
2021-11-03 Aina Niemetzapi: Rename some separation logic functions for consist... blob | commitdiff | raw | diff to current
2021-10-31 Mathias Preinerapi: Add guard against querying value from term with... blob | commitdiff | raw | diff to current
2021-10-28 Abdalrhman MohamedAdd a `define-fun` command for each `:named` term.... blob | commitdiff | raw | diff to current
2021-10-27 Andrew ReynoldsAdd missing API checks to getValue (#7475) blob | commitdiff | raw | diff to current
2021-10-25 Andrew ReynoldsJava and python unit tests for mkCardinalityConstraint... blob | commitdiff | raw | diff to current
2021-10-21 Andrew ReynoldsMake cardinality constraint a nullary operator (#7333) blob | commitdiff | raw | diff to current
2021-10-20 Aina Niemetzapi: Add Solver::mkSepEmp(). (#7432) blob | commitdiff | raw | diff to current
2021-10-20 Andrew ReynoldsCheck whether abduct option is enabled (#7418) blob | commitdiff | raw | diff to current
2021-10-20 Aina Niemetzapi: Rename get(BV|FP)*Size functions for consistency... blob | commitdiff | raw | diff to current
2021-10-07 Gereon KremerChange behaviour of Term::getRealValue() (#7316) blob | commitdiff | raw | diff to current
2021-10-01 Aina NiemetzRename SmtEngine to SolverEngine. (#7282) blob | commitdiff | raw | diff to current
2021-09-30 Aina NiemetzRename files smt_engine.(cpp|h) to solver_engine.(cpp... blob | commitdiff | raw | diff to current
2021-09-30 Andrew ReynoldsSimplify the syntax and representation of the separatio... blob | commitdiff | raw | diff to current
2021-09-23 Gereon KremerEliminate Output macro in favor of simple Env functions... blob | commitdiff | raw | diff to current
2021-09-17 Andres NoetzliUse a single `NodeManager` per thread (#7204) blob | commitdiff | raw | diff to current
2021-09-14 Andrew ReynoldsAdd get-difficulty to the API (#7194) blob | commitdiff | raw | diff to current
2021-09-14 Andrew ReynoldsSupport sygus version 2.1 command assume (#7081) blob | commitdiff | raw | diff to current
2021-09-13 Gereon KremerAdd Solver::isOutputOn() (#7187) blob | commitdiff | raw | diff to current
2021-09-09 Gereon KremerAdd Solver::getOutput() (#7162) blob | commitdiff | raw | diff to current
2021-09-02 Gereon KremerAdd API check whether option in getOptionInfo() exists... blob | commitdiff | raw | diff to current
2021-09-01 Andrew ReynoldsPrint response to get-model using the API (#7084) blob | commitdiff | raw | diff to current
2021-09-01 Gereon KremerNo longer use direct access to options in driver (... blob | commitdiff | raw | diff to current
2021-08-30 Gereon KremerAdd API function to obtain information about a single... blob | commitdiff | raw | diff to current
2021-08-30 mudathirmahgoubAdd kind BAG_MAP and its type rule to bags (#6503) blob | commitdiff | raw | diff to current
2021-08-27 Gereon KremerAdd Driver options (#7078) blob | commitdiff | raw | diff to current
2021-08-27 Andrew ReynoldsAdd missing methods to Solver API for models (#7052) blob | commitdiff | raw | diff to current
2021-08-27 yoni206Add `isNull` to cpp api tests, python api, and python... blob | commitdiff | raw | diff to current
2021-08-23 Aina Niemetzapi: Require size argument for mkBitVector. (#6998) blob | commitdiff | raw | diff to current
2021-08-20 Gereon KremerMake driver use options from the solver (#6930) blob | commitdiff | raw | diff to current
2021-08-20 Gereon KremerAdd CVC5ApiOptionException (#6992) blob | commitdiff | raw | diff to current
2021-08-05 Alex OzdemirNormalize val in BitVector(val_str, base) (#6955) blob | commitdiff | raw | diff to current
2021-08-04 Gereon KremerAdd API function to get list of option names (#6971) blob | commitdiff | raw | diff to current
2021-08-04 Haniel Barbosa[proof] Add getProof to API and use it in GetProofComma... blob | commitdiff | raw | diff to current
2021-08-04 Alex OzdemirAdd IEEE-BV-to-FP to external-to-internal mapping in... blob | commitdiff | raw | diff to current
2021-07-31 Gereon KremerPerform statistics printing via the API (#6952) blob | commitdiff | raw | diff to current
2021-07-30 Gereon KremerAllow changing certain options while solving (#6945) blob | commitdiff | raw | diff to current
2021-07-22 mudathirmahgoubAdd std::vector<Term> Op:: getIndices() and operator... blob | commitdiff | raw | diff to current
2021-07-14 Gereon KremerClean up option usage in command executor (#6844) blob | commitdiff | raw | diff to current
2021-06-28 Andrew ReynoldsRename internal string kinds to match API (#6797) blob | commitdiff | raw | diff to current
2021-06-26 yoni206pow2 -- final changes (#6800) blob | commitdiff | raw | diff to current
2021-06-24 Aina Niemetzapi: getRealValue: Fix printing of integer values.... blob | commitdiff | raw | diff to current
2021-06-16 Aina NiemetzMake symfpu a required dependency. (#6749) blob | commitdiff | raw | diff to current
2021-06-15 Gereon KremerRemove public option wrappers (#6716) blob | commitdiff | raw | diff to current
next