summaryrefslogtreecommitdiff
path: root/src/api/cpp/cvc5.cpp
AgeCommit message (Expand)Author
2021-12-14Throw exception for getting value of non-well-founded datatype (#7806)Andrew Reynolds
2021-12-13Fixes and additions for API for parametric datatypes (#7760)Andrew Reynolds
2021-12-10Refactor and fixes related to getSpecializedConstructorTerm (#7774)Andrew Reynolds
2021-12-08api: Fix Sort::getDatatypeArity() for non-parametric datatypes. (#7766)Aina Niemetz
2021-12-03Proper error for using constructor in multiple datatypes (#7738)Andrew Reynolds
2021-12-02Add explicit 64bit getters for Integer class (#7728)Gereon Kremer
2021-12-02add bag.fold operator (#7718)mudathirmahgoub
2021-12-01api: Add missing bit-width 0 check to mkBVFromStrHelper. (#7727)Mathias Preiner
2021-11-25api: Refactor mkTerm for kinds with arity = 0. (#7699)Aina Niemetz
2021-11-24api: Fix creation of nary term kinds via Op. (#7688)Aina Niemetz
2021-11-19[API] Avoid copying values (#7666)Andres Noetzli
2021-11-18api: Fix categorization of DT kinds in kind maps. (#7668)Aina Niemetz
2021-11-15api: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632)Aina Niemetz
2021-11-13Add operator set.map to theory of sets (#7641)mudathirmahgoub
2021-11-12bags: Rename kinds with a more consistent naming scheme (#7611)mudathirmahgoub
2021-11-12Remove `ConstantMap<Rational>` (#7635)Andres Noetzli
2021-11-11Add an API method to get the raw name of a term. (#7618)Abdalrhman Mohamed
2021-11-11Generalize front-end checks to check for shadowed variables (#7634)Andrew Reynolds
2021-11-10api: Add Solver::mkRegexpAll(). (#7614)Aina Niemetz
2021-11-10sets: Rename set.intersection to set.inter. (#7622)Aina Niemetz
2021-11-09regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match SMT-LIB. (#7609)Aina Niemetz
2021-11-08sets: Rename kinds with a more consistent naming scheme. (#7595)Aina Niemetz
2021-11-06Print `unsupported` for unrecognized flags. (#7384)Abdalrhman Mohamed
2021-11-04Start refactoring of `-o` and `-v` (#7449)Gereon Kremer
2021-11-03api: Rename some separation logic functions for consistency. (#7564)Aina Niemetz
2021-10-31api: Add guard against querying value from term with free vars. (#7529)Mathias Preiner
2021-10-28Add a `define-fun` command for each `:named` term. (#7308)Abdalrhman Mohamed
2021-10-27Add missing API checks to getValue (#7475)Andrew Reynolds
2021-10-25Java and python unit tests for mkCardinalityConstraint (#7486)Andrew Reynolds
2021-10-21Make cardinality constraint a nullary operator (#7333)Andrew Reynolds
2021-10-20api: Add Solver::mkSepEmp(). (#7432)Aina Niemetz
2021-10-20Check whether abduct option is enabled (#7418)Andrew Reynolds
2021-10-20api: Rename get(BV|FP)*Size functions for consistency. (#7428)Aina Niemetz
2021-10-06Change behaviour of Term::getRealValue() (#7316)Gereon Kremer
2021-09-30Rename SmtEngine to SolverEngine. (#7282)Aina Niemetz
2021-09-30Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)Aina Niemetz
2021-09-30Simplify the syntax and representation of the separation logic empty heap con...Andrew Reynolds
2021-09-23Eliminate Output macro in favor of simple Env functions (#7223)Gereon Kremer
2021-09-17Use a single `NodeManager` per thread (#7204)Andres Noetzli
2021-09-14Add get-difficulty to the API (#7194)Andrew Reynolds
2021-09-14Support sygus version 2.1 command assume (#7081)Andrew Reynolds
2021-09-13Add Solver::isOutputOn() (#7187)Gereon Kremer
2021-09-09Add Solver::getOutput() (#7162)Gereon Kremer
2021-09-02Add API check whether option in getOptionInfo() exists (#7093)Gereon Kremer
2021-09-01Print response to get-model using the API (#7084)Andrew Reynolds
2021-09-01No longer use direct access to options in driver (#7094)Gereon Kremer
2021-08-30Add API function to obtain information about a single option (#6980)Gereon Kremer
2021-08-30Add kind BAG_MAP and its type rule to bags (#6503)mudathirmahgoub
2021-08-27Add Driver options (#7078)Gereon Kremer
2021-08-27Add missing methods to Solver API for models (#7052)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback