projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Split expression names from SmtEngine (#4832)
[cvc5.git] / src / CMakeLists.txt
2020-08-03 Andrew ReynoldsSplit expression names from SmtEngine (#4832) blob | commitdiff | raw
2020-08-03 Andrew ReynoldsSplit dump manager from SmtEngine (#4824) blob | commitdiff | raw | diff to current
2020-07-31 Andrew ReynoldsSplit listener classes from SmtEngine (#4816) blob | commitdiff | raw | diff to current
2020-07-30 Gereon KremerAdds the interface for the CAD-based arithmetic solver... blob | commitdiff | raw | diff to current
2020-07-28 Andrew ReynoldsUse lemma property enum for OutputChannel::lemma (... blob | commitdiff | raw | diff to current
2020-07-21 Gereon KremerPreparations for a CAD-based arithmetic solver (#4762) blob | commitdiff | raw | diff to current
2020-07-17 Andrew ReynoldsAdd option manager and simpler option listener (#4745) blob | commitdiff | raw | diff to current
2020-07-17 Gereon KremerIntegration of libpoly (#4679) blob | commitdiff | raw | diff to current
2020-07-16 Andrew ReynoldsSplit abstract values utility from SmtEngine (#4754) blob | commitdiff | raw | diff to current
2020-07-16 Haniel Barbosa(proof-new) Adding API for converting EqProof into... blob | commitdiff | raw | diff to current
2020-07-15 Andrew ReynoldsSplit abduction solver from SmtEngine (#4733) blob | commitdiff | raw | diff to current
2020-07-15 Gereon KremerAdd missing header (Fixes #4743) (#4749) blob | commitdiff | raw | diff to current
2020-07-14 Andrew ReynoldsRemove sygus print callback (#4727) blob | commitdiff | raw | diff to current
2020-07-14 Andrew Reynolds(proof-new) Skeleton proof support in the Rewriter... blob | commitdiff | raw | diff to current
2020-07-13 Andrew Reynolds (proof-new) SMT Preprocess proof generator (#4708) blob | commitdiff | raw | diff to current
2020-07-13 Andres NoetzliRemove ExprSequence (#4724) blob | commitdiff | raw | diff to current
2020-07-10 Ying Sheng[Interpolation] Add interface for SyGuS interpolation... blob | commitdiff | raw | diff to current
2020-07-09 Andrew ReynoldsAssociate all lemmas in non-linear arithmetic with... blob | commitdiff | raw | diff to current
2020-07-09 Andrew Reynolds(proof-new) Theory engine proof generator (#4657) blob | commitdiff | raw | diff to current
2020-07-02 Andrew Reynolds(proof-new) Proof rule checkers run on skolem forms... blob | commitdiff | raw | diff to current
2020-07-01 Andrew ReynoldsAdd solver for integer AND (#4681) blob | commitdiff | raw | diff to current
2020-06-30 Andrew ReynoldsAdd internal support for integer and operator (#4668) blob | commitdiff | raw | diff to current
2020-06-19 Andrew Reynolds(proof-new) Split operator elimination from arithmetic... blob | commitdiff | raw | diff to current
2020-06-19 Andrew ReynoldsClean the header file of TheoryStrings (#4272) blob | commitdiff | raw | diff to current
2020-06-16 Andrew Reynolds(proof-new) Add quantifiers proof checker (#4593) blob | commitdiff | raw | diff to current
2020-06-13 Andrew ReynoldsMove sygus datatype utility functions to their own... blob | commitdiff | raw | diff to current
2020-06-12 Andrew Reynolds(proof-new) Split TheoryEngine (#4558) blob | commitdiff | raw | diff to current
2020-06-11 Andrew Reynolds(proof-new) Add eager proof generator utility. (#4592) blob | commitdiff | raw | diff to current
2020-06-10 Andrew Reynolds(proof-new) Theory proof step buffer utility (#4580) blob | commitdiff | raw | diff to current
2020-06-09 Andrew Reynolds(proof-new) Add trust node utility (#4588) blob | commitdiff | raw | diff to current
2020-06-03 Haniel Barbosa(proof-new) Adding rules and proof checker for EUF... blob | commitdiff | raw | diff to current
2020-06-03 Haniel Barbosa(proof-new) Adding rules and proof checker for Boolean... blob | commitdiff | raw | diff to current
2020-06-03 Andrew Reynolds(proof-new) Add builtin proof checker (#4537) blob | commitdiff | raw | diff to current
2020-06-01 Andrew ReynoldsMove non-linear files to src/theory/arith/nl (#4548) blob | commitdiff | raw | diff to current
2020-05-27 Andrew ReynoldsAdd the Expr-level sequence datatype (#4526) blob | commitdiff | raw | diff to current
2020-05-22 Aina NiemetzAdd support for SAT solver Kissat. (#4514) blob | commitdiff | raw | diff to current
2020-04-17 Mathias PreinerSyGuS instantiation quantifiers module (#3910) blob | commitdiff | raw | diff to current
2020-04-15 Andrew ReynoldsSplit TermRegistry object from TheoryStrings (#4312) blob | commitdiff | raw | diff to current
2020-04-14 Andrew ReynoldsRemove argument extender (#4223) blob | commitdiff | raw | diff to current
2020-04-11 Andrew ReynoldsSplit the non-linear solver (#4219) blob | commitdiff | raw | diff to current
2020-04-09 Andrew ReynoldsSplit ProcessAssertions module from SmtEngine (#4210) blob | commitdiff | raw | diff to current
2020-04-03 Andrew ReynoldsSplit sequences rewriter (#4194) blob | commitdiff | raw | diff to current
2020-03-31 Andrew ReynoldsRemove replay and use-theory options and idl (#4186) blob | commitdiff | raw | diff to current
2020-03-30 Andrew ReynoldsSupport indexed operators re.loop and re.^ (#4167) blob | commitdiff | raw | diff to current
2020-03-29 Andrew ReynoldsEnumeration for String rewrites (#4173) blob | commitdiff | raw | diff to current
2020-03-28 Andrew ReynoldsSplit transcendental solver to its own file (#4156) blob | commitdiff | raw | diff to current
2020-03-27 Andrew ReynoldsMove string utility file (#4164) blob | commitdiff | raw | diff to current
2020-03-27 Andrew ReynoldsMove set defaults function to its own file (#4154) blob | commitdiff | raw | diff to current
2020-03-23 Andres NoetzliCollect statistics about normal form inferences (#4127) blob | commitdiff | raw | diff to current
2020-03-20 Andrew ReynoldsSplit string-specific operators from TheoryStringsRewri... blob | commitdiff | raw | diff to current
2020-03-20 Andrew ReynoldsRefactor enumerator for strings (#4014) blob | commitdiff | raw | diff to current
2020-03-18 Alex OzdemirMove node visitor class from smt_util/ to expr/ (#4110) blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsRemove experimental symmetry breaker (#4005) blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsRemove partial instantiation for local theory extension... blob | commitdiff | raw | diff to current
2020-03-10 Andrew ReynoldsRemove instantiation propagator infrastructure (#3975) blob | commitdiff | raw | diff to current
2020-03-06 Andres NoetzliRemove --apply-to-const preprocessing pass (#3919) blob | commitdiff | raw | diff to current
2020-03-03 mudathirmahgoubRefactoring and cleaning the type enumerator for sets... blob | commitdiff | raw | diff to current
2020-03-03 Andrew ReynoldsStandardize the interface for SMT engine subsolvers... blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsUse side effect utility for non-linear lemmas (#3780) blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsMove equivalence class info to its own file in strings... blob | commitdiff | raw | diff to current
2020-02-26 Andres NoetzliRemove portfolio leftovers (#3821) blob | commitdiff | raw | diff to current
2020-02-25 yoni206bv_to_int preprocessing pass blob | commitdiff | raw | diff to current
2020-02-24 Andrew ReynoldsUtilities for words (#3797) blob | commitdiff | raw | diff to current
2020-02-21 Andrew ReynoldsSplit extended functions solver in strings (#3768) blob | commitdiff | raw | diff to current
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767) blob | commitdiff | raw | diff to current
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) blob | commitdiff | raw | diff to current
2020-02-14 Andrew ReynoldsUpdate sygus v1 parser to use ParseOp utility (#3756) blob | commitdiff | raw | diff to current
2020-02-08 Andrew ReynoldsSplit strings finite model finding strategy (#3727) blob | commitdiff | raw | diff to current
2020-02-08 Andrew ReynoldsSplit core solver from the theory of strings (#3713) blob | commitdiff | raw | diff to current
2020-02-08 Andrew ReynoldsInterface for example evaluation cache utilities (... blob | commitdiff | raw | diff to current
2020-02-04 Andrew ReynoldsSplit base solver from the theory of strings (#3680) blob | commitdiff | raw | diff to current
2020-02-03 Andrew ReynoldsExample inference utility (#3670) blob | commitdiff | raw | diff to current
2020-01-31 Andrew ReynoldsRefactor sygus stats (#3684) blob | commitdiff | raw | diff to current
2020-01-30 Andrew ReynoldsExample minimize evaluation utility. (#3671) blob | commitdiff | raw | diff to current
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) blob | commitdiff | raw | diff to current
2019-12-09 Andres NoetzliMake theory rewriters non-static (#3547) blob | commitdiff | raw | diff to current
2019-12-06 Andrew ReynoldsNew algorithm for interpolation and abduction based... blob | commitdiff | raw | diff to current
2019-11-06 Andrew ReynoldsSupport for SyGuS PBE + recursive functions (#3433) blob | commitdiff | raw | diff to current
2019-11-05 Andrew ReynoldsSeparate model object in non-linear extension (#3426) blob | commitdiff | raw | diff to current
2019-11-01 Andrew ReynoldsRename datatypes sygus solver (#3417) blob | commitdiff | raw | diff to current
2019-10-30 Andrew ReynoldsSplit some generic utilities from the non-linear extens... blob | commitdiff | raw | diff to current
2019-10-17 Andrew Reynolds Move datatype utility functions to own file (#3397) blob | commitdiff | raw | diff to current
2019-10-16 Andrew ReynoldsSolver state for theory of strings (#3181) blob | commitdiff | raw | diff to current
2019-10-11 Aina NiemetzMake order of theories explicit in the source code... blob | commitdiff | raw | diff to current
2019-10-08 Ying ShengMake ackermannization generally applicable rather than... blob | commitdiff | raw | diff to current
2019-09-25 Mathias PreinerUse separate CMake project for CVC4 examples. (#3196) blob | commitdiff | raw | diff to current
2019-09-16 Andrew ReynoldsSygus type info class (#3187) blob | commitdiff | raw | diff to current
2019-09-16 Andrew ReynoldsMove virtual term substitution utilities to own file... blob | commitdiff | raw | diff to current
2019-09-13 Andrew ReynoldsSplit, refactor and document the theory of sets (#3085) blob | commitdiff | raw | diff to current
2019-09-12 Andrew Reynolds Rename UF with cardinality extension (#3241) blob | commitdiff | raw | diff to current
2019-09-12 Andrew ReynoldsRefactoring finite bounds in Quantifiers Engine (#3261) blob | commitdiff | raw | diff to current
2019-09-07 Andrew ReynoldsRemove portfolio (#3236) blob | commitdiff | raw | diff to current
2019-08-23 Andrew ReynoldsDocument transition inference utility (#3207) blob | commitdiff | raw | diff to current
2019-08-14 Mathias Preinercmake: Export CVC4 library interface. (#3179) blob | commitdiff | raw | diff to current
2019-08-02 Andrew Reynolds Move basic sygus enumerator to its own file (#3149) blob | commitdiff | raw | diff to current
2019-08-01 Andrew ReynoldsMove some generic utilities out of quantifiers (#3139) blob | commitdiff | raw | diff to current
2019-07-29 Andrew ReynoldsModel blocker feature (#3112) blob | commitdiff | raw | diff to current
2019-07-29 Andrew ReynoldsSupport get-abduct smt2 command (#3122) blob | commitdiff | raw | diff to current
2019-07-25 Andrew ReynoldsSplit infer info data structure in strings (#3107) blob | commitdiff | raw | diff to current
2019-07-08 Andrew ReynoldsTowards refactoring relations (#3078) blob | commitdiff | raw | diff to current
next