summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2021-09-30Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)Aina Niemetz
2021-09-30Integrate javadoc documentation (#7278)Gereon Kremer
2021-09-30bv: Refactor ppRewrite and move to TheoryBV. (#7271)Mathias Preiner
2021-09-30Refactor our static builds (#7251)Gereon Kremer
2021-09-30Properly cache assertions in static learning preprocessing pass. (#7242)Mathias Preiner
2021-09-30Finish the Java Api (#6396)mudathirmahgoub
2021-09-30Make theory engine modules use Env (#7277)Andrew Reynolds
2021-09-30Simplify the syntax and representation of the separation logic empty heap con...Andrew Reynolds
2021-09-30Remove usage of static options in arithmetic theory (#7221)Gereon Kremer
2021-09-30Print `str.is_digit` and `int.pow2` correctly. (#7276)Abdalrhman Mohamed
2021-09-30[Printer] Only quote `set-info` value if necessary (#7262)Andres Noetzli
2021-09-29[API] Update comments w.r.t. SymFPU, fix typos (#7263)Andres Noetzli
2021-09-29Remove support for extended `(check-sat <term>)` command. (#7270)Abdalrhman Mohamed
2021-09-29Properly restrict PBE symmetry breaking for abduction queries (#7269)Andrew Reynolds
2021-09-29Update the syntax for tuples in smt2 (#7265)Andrew Reynolds
2021-09-29Add the strings array solver (#7232)Andrew Reynolds
2021-09-28Update `--lang=help` (#7260)Andres Noetzli
2021-09-29Add Statistics and Stat to the Java API (#7243)mudathirmahgoub
2021-09-29remove stuff (#7258)Gereon Kremer
2021-09-29Add Sort.java to the java API (#6382)mudathirmahgoub
2021-09-28Remove linking against RT (#7257)Gereon Kremer
2021-09-24Eliminate calls to Rewriter::rewrite from strings entailment checks (#7203)Andrew Reynolds
2021-09-23Generalize string enumerator for fixed length sequences (#7234)Andrew Reynolds
2021-09-23Eliminate Output macro in favor of simple Env functions (#7223)Gereon Kremer
2021-09-23[proofs[ Alethe: Fix Order of Arguments of addAletheStepFromOr (#7237)Lachnitt
2021-09-23[proofs] Alethe: Translate THEORY_REWRITE (#7236)Lachnitt
2021-09-23[proofs] Alethe: Add Alethe Files to be Compiled (#7241)Lachnitt
2021-09-23Refactor check interface of nonlinear extension (#7235)Gereon Kremer
2021-09-23More uses of EnvObj (#7230)Andrew Reynolds
2021-09-23[proofs] Alethe: Translate SCOPE rule (#7224)Lachnitt
2021-09-23Use `|` to print quoted strings in `set-info` command. (#7240)Abdalrhman Mohamed
2021-09-23Implement alpha equivalence proofs (#7066)Andrew Reynolds
2021-09-22Make cegqi subsolvers EnvObj (#7205)Andrew Reynolds
2021-09-22Remove CVC language support (#7219)Mathias Preiner
2021-09-22Towards standard usage of evaluator (#7189)Andrew Reynolds
2021-09-22Add extensionality option for strings disequalities (#7229)Andrew Reynolds
2021-09-22arrays: Use EnvObj::rewrite and EnvObj::options. (#7217)Aina Niemetz
2021-09-22arrays: Move type enumerator implementation to .cpp. (#7216)Aina Niemetz
2021-09-22Eliminate arithmetic proof macros (#7226)Gereon Kremer
2021-09-22Minimal fixing version for tuple update parsing (#7228)Andrew Reynolds
2021-09-21[Proofs] Alethe: Translate ASSUME rule (#7213)Lachnitt
2021-09-21[proofs] Alethe: Implementation of AletheProofPostprocessCallback (#7212)Lachnitt
2021-09-20Fix handling of conversions between FP and reals (#7149)Andres Noetzli
2021-09-20Start python API Solver documentation (#7064)Alex Ozdemir
2021-09-20[proofs] Alethe: adds a node converterHaniel Barbosa
2021-09-20Add the LFSC proof post-processor (#7134)Andrew Reynolds
2021-09-20TheoryModel: Use EnvObj::rewrite instead of Rewriter::rewrite. (#7215)Aina Niemetz
2021-09-20Add anchors to cmdline options (#7210)Gereon Kremer
2021-09-18Fix printer for datatype udpater (#7208)Andrew Reynolds
2021-09-18Refactor tag suggestion mechanism (#7199)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback