summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
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
2020-09-28[proof-new] Adds a proof manager for the SAT solver (#5140)Haniel Barbosa
2020-09-23Modify lemma vs fact policy for datatype equalities (#5115)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-21(proof-new) Add the arrays proof checker (#5047)Andrew Reynolds
2020-09-17(proof-new) Updates to proof node updater algorithm (#5088)Andrew Reynolds
2020-09-17(proof-new) Rewrites involving operators in term conversion proof generator (...Andrew Reynolds
2020-09-17[proof-new] Have mkScope agnostic to True assumptions (#5086)Haniel Barbosa
2020-09-16[proof-new] Adds Lazy CDProof chain data-structure (#5060)Haniel Barbosa
2020-09-16[proof-new] Resolution rules and checkers (#5070)Haniel Barbosa
2020-09-15[proof-new] A simple proof generator for buffered proof steps (#5069)Haniel Barbosa
2020-09-11(proof-new) Handle mismatched assumptions in proof equality engine during mkS...Andrew Reynolds
2020-09-11(proof-new) Use deep copy for final lemma step in proof equality engine (#5013)Andrew Reynolds
2020-09-09(proof-new) Minor changes to proof node updater (#5011)Andrew Reynolds
2020-09-02(proof-new) Improve debugging infrastructure for open proofs (#4984)Andrew Reynolds
2020-09-02Remove #line directives from generated files. (#5005)Gereon Kremer
2020-09-02(proof-new) Updates to builtin proof checker (#4962)Andrew Reynolds
2020-09-02(proof-new) Add proof support in TheoryUF (#5002)Andrew Reynolds
2020-09-02(proof-new) Make term conversion proof generator optionally term-context sens...Andrew Reynolds
2020-08-31Basic proof support in inference manager (#4975)Andrew Reynolds
2020-08-28(proof-new) More term context utilities. (#4912)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback