projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Update theory preprocessor to use Env (#7288)
[cvc5.git] / src /
2021-10-01 Andrew ReynoldsUpdate theory preprocessor to use Env (#7288) tree | commitdiff
2021-10-01 Andrew ReynoldsFix ascription check for return types on ordinary funct... tree | commitdiff
2021-10-01 Andrew ReynoldsMake preregistration safe for uninterpreted constants... tree | commitdiff
2021-10-01 Gereon KremerClean options handlers (#7201) tree | commitdiff
2021-10-01 Gereon KremerFix some python docstrings which lead to sphinx warning... tree | commitdiff
2021-10-01 Andrew ReynoldsAdd the LFSC printer (#7158) tree | commitdiff
2021-10-01 Andrew ReynoldsAdd the print benchmark utility (#7196) tree | commitdiff
2021-10-01 Andrew ReynoldsUse the proper evaluator for optimized SyGuS datatype... tree | commitdiff
2021-10-01 Aina NiemetzRename SmtEngine to SolverEngine. (#7282) tree | commitdiff
2021-09-30 Aina NiemetzRename files smt_engine.(cpp|h) to solver_engine.(cpp... tree | commitdiff
2021-09-30 Gereon KremerIntegrate javadoc documentation (#7278) tree | commitdiff
2021-09-30 Mathias Preinerbv: Refactor ppRewrite and move to TheoryBV. (#7271) tree | commitdiff
2021-09-30 Gereon KremerRefactor our static builds (#7251) tree | commitdiff
2021-09-30 Mathias PreinerProperly cache assertions in static learning preprocess... tree | commitdiff
2021-09-30 mudathirmahgoubFinish the Java Api (#6396) tree | commitdiff
2021-09-30 Andrew ReynoldsMake theory engine modules use Env (#7277) tree | commitdiff
2021-09-30 Andrew ReynoldsSimplify the syntax and representation of the separatio... tree | commitdiff
2021-09-30 Gereon KremerRemove usage of static options in arithmetic theory... tree | commitdiff
2021-09-30 Abdalrhman MohamedPrint `str.is_digit` and `int.pow2` correctly. (#7276) tree | commitdiff
2021-09-30 Andres Noetzli[Printer] Only quote `set-info` value if necessary... tree | commitdiff
2021-09-29 Andres Noetzli[API] Update comments w.r.t. SymFPU, fix typos (#7263) tree | commitdiff
2021-09-29 Abdalrhman MohamedRemove support for extended `(check-sat <term>)` comman... tree | commitdiff
2021-09-29 Andrew ReynoldsProperly restrict PBE symmetry breaking for abduction... tree | commitdiff
2021-09-29 Andrew ReynoldsUpdate the syntax for tuples in smt2 (#7265) tree | commitdiff
2021-09-29 Andrew ReynoldsAdd the strings array solver (#7232) tree | commitdiff
2021-09-29 Andres NoetzliUpdate `--lang=help` (#7260) tree | commitdiff
2021-09-29 mudathirmahgoubAdd Statistics and Stat to the Java API (#7243) tree | commitdiff
2021-09-29 Gereon Kremerremove stuff (#7258) tree | commitdiff
2021-09-29 mudathirmahgoubAdd Sort.java to the java API (#6382) tree | commitdiff
2021-09-28 Gereon KremerRemove linking against RT (#7257) tree | commitdiff
2021-09-24 Andrew ReynoldsEliminate calls to Rewriter::rewrite from strings entai... tree | commitdiff
2021-09-23 Andrew ReynoldsGeneralize string enumerator for fixed length sequences... tree | commitdiff
2021-09-23 Gereon KremerEliminate Output macro in favor of simple Env functions... tree | commitdiff
2021-09-23 Lachnitt[proofs[ Alethe: Fix Order of Arguments of addAletheSte... tree | commitdiff
2021-09-23 Lachnitt[proofs] Alethe: Translate THEORY_REWRITE (#7236) tree | commitdiff
2021-09-23 Lachnitt[proofs] Alethe: Add Alethe Files to be Compiled ... tree | commitdiff
2021-09-23 Gereon KremerRefactor check interface of nonlinear extension (#7235) tree | commitdiff
2021-09-23 Andrew ReynoldsMore uses of EnvObj (#7230) tree | commitdiff
2021-09-23 Lachnitt[proofs] Alethe: Translate SCOPE rule (#7224) tree | commitdiff
2021-09-23 Abdalrhman MohamedUse `|` to print quoted strings in `set-info` command... tree | commitdiff
2021-09-23 Andrew ReynoldsImplement alpha equivalence proofs (#7066) tree | commitdiff
2021-09-22 Andrew ReynoldsMake cegqi subsolvers EnvObj (#7205) tree | commitdiff
2021-09-22 Mathias PreinerRemove CVC language support (#7219) tree | commitdiff
2021-09-22 Andrew ReynoldsTowards standard usage of evaluator (#7189) tree | commitdiff
2021-09-22 Andrew ReynoldsAdd extensionality option for strings disequalities... tree | commitdiff
2021-09-22 Aina Niemetzarrays: Use EnvObj::rewrite and EnvObj::options. (... tree | commitdiff
2021-09-22 Aina Niemetzarrays: Move type enumerator implementation to .cpp... tree | commitdiff
2021-09-22 Gereon KremerEliminate arithmetic proof macros (#7226) tree | commitdiff
2021-09-22 Andrew ReynoldsMinimal fixing version for tuple update parsing (#7228) tree | commitdiff
2021-09-21 Lachnitt[Proofs] Alethe: Translate ASSUME rule (#7213) tree | commitdiff
2021-09-21 Lachnitt[proofs] Alethe: Implementation of AletheProofPostproce... tree | commitdiff
2021-09-21 Andres NoetzliFix handling of conversions between FP and reals (... tree | commitdiff
2021-09-20 Alex OzdemirStart python API Solver documentation (#7064) tree | commitdiff
2021-09-20 Haniel Barbosa[proofs] Alethe: adds a node converter tree | commitdiff
2021-09-20 Andrew ReynoldsAdd the LFSC proof post-processor (#7134) tree | commitdiff
2021-09-20 Aina NiemetzTheoryModel: Use EnvObj::rewrite instead of Rewriter... tree | commitdiff
2021-09-20 Gereon KremerAdd anchors to cmdline options (#7210) tree | commitdiff
2021-09-18 Andrew ReynoldsFix printer for datatype udpater (#7208) tree | commitdiff
2021-09-18 Gereon KremerRefactor tag suggestion mechanism (#7199) tree | commitdiff
2021-09-17 Andres NoetzliUse a single `NodeManager` per thread (#7204) tree | commitdiff
2021-09-17 Lachnitt[proofs] Alethe: Added Proof Postprocessor to alethe_pr... tree | commitdiff
2021-09-17 Lachnitt[proofs] Alethe: Added Final Callback Function to aleth... tree | commitdiff
2021-09-17 Gereon KremerReplace write access to options by a local variable... tree | commitdiff
2021-09-17 Gereon KremerMinor cleanup related to EnvObj (#7206) tree | commitdiff
2021-09-16 Andrew ReynoldsFix relevant domain for parametric operators (#7198) tree | commitdiff
2021-09-15 Lachnitt[proofs] Alethe: Added Callback Function to alethe_proo... tree | commitdiff
2021-09-15 Andrew ReynoldsMinor changes to E-matching utilities (#7062) tree | commitdiff
2021-09-15 Gereon Kremerremove options that are no longer used (#7197) tree | commitdiff
2021-09-15 Lachnitt[proof] Added printer for proof rule names (#7185) tree | commitdiff
2021-09-15 Lachnitt[proof] Alethe proof rules (#7180) tree | commitdiff
2021-09-15 Andrew ReynoldsEliminate global access to options:: from quantifiers... tree | commitdiff
2021-09-14 Andrew ReynoldsAdd get-difficulty to the API (#7194) tree | commitdiff
2021-09-14 Gereon KremerFinal cleanup (#7193) tree | commitdiff
2021-09-14 Andres NoetzliMake `-o raw-benchmark` work with `--parse-only` (... tree | commitdiff
2021-09-14 Andrew ReynoldsSupport sygus version 2.1 command assume (#7081) tree | commitdiff
2021-09-14 Andrew ReynoldsUtilities in preparation for print benchmark utility... tree | commitdiff
2021-09-14 Andrew ReynoldsAdd proof manager method to translate difficulty map... tree | commitdiff
2021-09-14 Gereon KremerRefactor code generation for option modules (#7182) tree | commitdiff
2021-09-14 Gereon KremerTurn sphinx generation into a function (#7181) tree | commitdiff
2021-09-14 Mathias Preinerbv: Unify bit-blasting code for udiv and urem. (#7188) tree | commitdiff
2021-09-14 Mathias Preinerproofs: Properly track pre- and post-rewrites in bbAtom... tree | commitdiff
2021-09-14 Andrew ReynoldsReimplement `--dump=raw-benchmark` as `-o raw-benchmark... tree | commitdiff
2021-09-13 Andres NoetzliRemove context getters from `TheoryState` (#7174) tree | commitdiff
2021-09-13 Andrew ReynoldsConnect difficulty manager to TheoryEngine (#7161) tree | commitdiff
2021-09-13 Gereon KremerAdd Solver::isOutputOn() (#7187) tree | commitdiff
2021-09-13 Aina NiemetzFP: Rename FpConverter to FpWordBlaster. (#7170) tree | commitdiff
2021-09-13 Gereon KremerRefactor generation code for getInfo() (#7176) tree | commitdiff
2021-09-13 Gereon KremerAdd main options to cmake (#7178) tree | commitdiff
2021-09-13 Gereon KremerReorder code (#7175) tree | commitdiff
2021-09-13 Gereon KremerRefactor options parsing (#7143) tree | commitdiff
2021-09-11 Gereon KremerUse StatisticsRegistry from Env (#7166) tree | commitdiff
2021-09-11 Aina NiemetzcheckModel: Extend documentation. (#7177) tree | commitdiff
2021-09-11 Mathias Preinerbv: Move IsPowerOfTwo rule to preprocessing pass and... tree | commitdiff
2021-09-10 Aina NiemetzFP: Enable caching in the theory inference manager... tree | commitdiff
2021-09-10 Mathias Preinerbv: Use EnvObj::rewrite() and EnvObj::options() in... tree | commitdiff
2021-09-10 Aina NiemetzFP: Use EnvObj::rewrite() and options() in theory_fp... tree | commitdiff
2021-09-10 Aina NiemetzFP: Do not send trivial lemmas. (#7167) tree | commitdiff
2021-09-10 mudathirmahgoubAdd Op.java to the java API (#6387) tree | commitdiff
2021-09-10 Andres NoetzliUse C++17 attributes (#7154) tree | commitdiff
2021-09-10 Andrew ReynoldsMore refactoring of set defaults (#7160) tree | commitdiff
next