summaryrefslogtreecommitdiff
path: root/src/expr/CMakeLists.txt
AgeCommit message (Expand)Author
2020-11-19Add nested quantifier elimination module (#5422)Andrew Reynolds
2020-11-11Move symbol manager to src/expr/ (#5420)Andrew Reynolds
2020-10-29Update api::Sort to use TypeNode instead of Type (#5363)Andrew Reynolds
2020-10-08(proof-new) Add lazy proof set utility (#5221)Andrew Reynolds
2020-09-30(proof-new) Add the term conversion sequence generator (#5097)Andrew Reynolds
2020-09-22Add skeleton for theory of bags (multisets) (#5100)mudathirmahgoub
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-16[proof-new] Adds Lazy CDProof chain data-structure (#5060)Haniel Barbosa
2020-09-15[proof-new] A simple proof generator for buffered proof steps (#5069)Haniel Barbosa
2020-09-02(proof-new) Make term conversion proof generator optionally term-context sens...Andrew Reynolds
2020-08-25Replace Expr-level datatype with Node-level DType (#4875)Andrew Reynolds
2020-08-18(proof-new) Callbacks for term-context-sensitive terms (#4842)Andrew Reynolds
2020-08-07Move datatype index constant to its own file (#4859)Andrew Reynolds
2020-07-12Remove ExprSequence (#4724)Andres Noetzli
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
2020-07-02(proof-new) Proof node updater (#4647)Andrew Reynolds
2020-06-15(proof-new) Update proof node, add proof node algorithm utility file. (#4600)Andrew Reynolds
2020-06-12(proof-new) Term conversion proof generator utility (#4603)Andrew Reynolds
2020-06-11 (proof-new) Add lazy proof utility (#4589)Andrew Reynolds
2020-06-08(proof-new) Add abstract proof generator class (#4574)Andrew Reynolds
2020-06-05(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)Andrew Reynolds
2020-06-01(proof-new) Proof step buffer utilities (#4533)Andrew Reynolds
2020-05-27Add the Expr-level sequence datatype (#4526)Andrew Reynolds
2020-05-23Add the sequence datatype (#4153)Andrew Reynolds
2020-05-22(proof-new) Proof node to SExpr utility. (#4512)Andrew Reynolds
2020-05-20Add proof skolem cache (#4485)Andrew Reynolds
2020-04-17Add (context-dependent) Proof (#4323)Andrew Reynolds
2020-04-16Add ProofNodeManager and ProofChecker (#4317)Andrew Reynolds
2020-04-15Add ProofNode data structure (#4311)Andrew Reynolds
2020-03-31Remove replay and use-theory options and idl (#4186)Andrew Reynolds
2020-03-27Node traversal iterator (#3845)Alex Ozdemir
2020-03-18Move node visitor class from smt_util/ to expr/ (#4110)Alex Ozdemir
2020-02-20Remove front-end support for Chain (#3767)Andrew Reynolds
2019-12-05Introduce the Node-level Datatypes API (#3462)Andrew Reynolds
2019-11-15Introduce SyGuS datatype API (#3465)Andrew Reynolds
2019-11-05Refactor type matcher utility (#3439)Andrew Reynolds
2019-09-06Remove portfolio (#3236)Andrew Reynolds
2019-08-01Move some generic utilities out of quantifiers (#3139)Andrew Reynolds
2018-11-27Make (T)NodeTrie a general utility (#2489)Andrew Reynolds
2018-09-24cmake: Fix dependencies for code generation. (#2524)Mathias Preiner
2018-09-24cmake: Fix theory order #2. (#2522)Mathias Preiner
2018-09-22cmake: Only build libcvc4 and libcvc4parser as libraries.Mathias Preiner
2018-09-22cmake: Rebase with current master, add new tests/source files.Mathias Preiner
2018-09-22cmake: Add missing dependency.Mathias Preiner
2018-09-22cmake: Cleanup CMakeLists.txt files, remove SHARED.Mathias Preiner
2018-09-22cmake: Working build infrastructure.Mathias Preiner
2018-09-22cmake: .cpp generation done, .h generation not yet completeAina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback