summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
2020-11-25Fully decouple SmtEngine and the Expr layer (#5532)Andrew Reynolds
2020-11-23(proof-new) Miscellaneous changes from proof-new (#5445)Andrew Reynolds
2020-11-23Add declare model symbol methods to SymbolManager and Model (#5480)Andrew Reynolds
2020-11-20(proof-new) Replace LazyCDProofSet by generic CDProofSet (#5487)Gereon Kremer
2020-11-19Include stddef.h (needed for size_t) in cvc4_public.h (#5476)Aina Niemetz
2020-11-19Add nested quantifier elimination module (#5422)Andrew Reynolds
2020-11-19Use symbol manager for unsat cores (#5468)Andrew Reynolds
2020-11-17FloatingPoint: Clean up and document header, format. (#5453)Aina Niemetz
2020-11-16Cleaning up scopes in preparation for symbol manager (#5442)Andrew Reynolds
2020-11-13Add more features to symbol manager (#5434)Andrew Reynolds
2020-11-12(proof-new) Fix true explanations of propagations in pf equality engine (#5338)Andrew Reynolds
2020-11-12(proof-new) Improve printing and debugging for pedantic checking (#5337)Andrew Reynolds
2020-11-12Make symbol manager context dependent (#5424)Andrew Reynolds
2020-11-11Move symbol manager to src/expr/ (#5420)Andrew Reynolds
2020-11-11Add simple substitution utility (#5397)Andrew Reynolds
2020-11-10Add getSubtermKinds to node algorithm (#5398)Andrew Reynolds
2020-11-09Migrate some documentation about attributes (#5390)Andrew Reynolds
2020-11-05Simplify printing with respect to expression types (#5394)Andrew Reynolds
2020-11-03Add scope methods constructing types in API (#5393)Andrew Reynolds
2020-11-02Avoid dynamic allocation in symbol table implementation (#5368)Andrew Reynolds
2020-10-29Update api::Sort to use TypeNode instead of Type (#5363)Andrew Reynolds
2020-10-29Add mkInteger to the API (#5274)mudathirmahgoub
2020-10-29Add NodeManager::mkOr() (#5360)Gereon Kremer
2020-10-28Convert symbol table from Expr-level to Term-level (#5355)Andrew Reynolds
2020-10-27Add missing methods involving datatype sorts to the API (#5290)Andrew Reynolds
2020-10-26(proof-new) Add datatypes proof checker (#5340)Andrew Reynolds
2020-10-21(proof-new) Updates to lazy proof chain (#5317)Andrew Reynolds
2020-10-21Add operator MakeBagOp for constructing bags (#5209)mudathirmahgoub
2020-10-20(proof-new) Fixes for proofs in rewriter (#5307)Andrew Reynolds
2020-10-20(proof-new) Fix for CDProof::isSame (#5297)Andrew Reynolds
2020-10-20(proof-new) Update add lazy step interface in LazyCDProof (#5299)Andrew Reynolds
2020-10-19[proof-new] Fixing resolution proof checker (#5262)Haniel Barbosa
2020-10-19[proof-new] Improving cycle checking in lazycdproofchain (#5302)Haniel Barbosa
2020-10-18(proof-new) Refactoring cyclic checks (#5291)Andrew Reynolds
2020-10-18 (proof-new) Witness axiom reconstruction for purification skolems (#5289)Andrew Reynolds
2020-10-18(proof-new) Implementation of trust substitution (#5276)Andrew Reynolds
2020-10-13(proof-new) Simplifications for proof rule checker interface (#5244)Andrew Reynolds
2020-10-13(proof-new) New rules for Booleans (#5243)Andrew Reynolds
2020-10-13(proof-new) Change merge policy for proof node updater (#5242)Andrew Reynolds
2020-10-11SyGuS instantiation modes (#5228)Mathias Preiner
2020-10-08(proof-new) Add lazy proof set utility (#5221)Andrew Reynolds
2020-10-08(proof-new) Fixes and improvements for smt proof postprocessor (#5197)Andrew Reynolds
2020-10-06(proof-new) Allow null proofs from generators in LazyCDProof (#5196)Andrew Reynolds
2020-10-05Remove subtyping for sets (#5205)mudathirmahgoub
2020-10-04Remove subtyping for sets theory (#5179)mudathirmahgoub
2020-10-02(proof-new) Fixes for theory preprocessing proofs (#5171)Andrew Reynolds
2020-09-30(proof-new) Add the term conversion sequence generator (#5097)Andrew Reynolds
2020-09-29[proof-new] Updates to proof node updater (#5156)Haniel Barbosa
2020-09-28[proof-new] Adds a proof node hash function (#5154)Haniel Barbosa
2020-09-28Minor fixes to quantifiers proofs (#5151)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback