projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Ensure uses of ground terms in triggers are preprocessed and registered (#5808)
[cvc5.git] / src / CMakeLists.txt
2021-01-25 Andrew ReynoldsSplit inst match generator into multiple files (#5805) blob | commitdiff | raw
2021-01-25 Andrew ReynoldsSplit E-matching strategies to own files (#5807) blob | commitdiff | raw | diff to current
2021-01-24 Andrew Reynolds(proof-new) Instantiation list utility (#5768) blob | commitdiff | raw | diff to current
2021-01-15 Andrew ReynoldsImplement --no-strings-lazy-pp as a preprocessing pass... blob | commitdiff | raw | diff to current
2021-01-13 Andrew ReynoldsSplit eager solver from strings solver state (#5775) blob | commitdiff | raw | diff to current
2021-01-11 Andrew ReynoldsMerge theory registrar and theory proxy (#5758) blob | commitdiff | raw | diff to current
2021-01-08 mudathirmahgoubAdd bags inference generator (#5731) blob | commitdiff | raw | diff to current
2021-01-06 yoni206strings arith checks preprocessing pass: step 1 (#5747) blob | commitdiff | raw | diff to current
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716) blob | commitdiff | raw | diff to current
2020-12-23 Haniel Barbosa[proof-new] Adding a manager for the new unsat cores... blob | commitdiff | raw | diff to current
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi... blob | commitdiff | raw | diff to current
2020-12-18 Gereon Kremer(proof-new) Setup proof infrastructure for transcendent... blob | commitdiff | raw | diff to current
2020-12-17 Gereon Kremer(proof-new) Prepare nonlinear extension and nl-ext... blob | commitdiff | raw | diff to current
2020-12-15 Andrew ReynoldsMove trigger trie to own file (#5680) blob | commitdiff | raw | diff to current
2020-12-15 Andrew ReynoldsConsolidate basic sygus utilities regarding sygus conje... blob | commitdiff | raw | diff to current
2020-12-08 Mathias PreinerAdd support for BV proofs with the simple bitblasting... blob | commitdiff | raw | diff to current
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328) blob | commitdiff | raw | diff to current
2020-12-02 Andrew ReynoldsRemove dagification visitor (#5574) blob | commitdiff | raw | diff to current
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) blob | commitdiff | raw | diff to current
2020-11-26 Andrew ReynoldsMove expand definitions to its own file (#5528) blob | commitdiff | raw | diff to current
2020-11-25 Gereon KremerRefactor transcendental solver (#5514) blob | commitdiff | raw | diff to current
2020-11-21 Aina NiemetzRename symfpu_literal.(h.in|cpp) -> floatingpoint_liter... blob | commitdiff | raw | diff to current
2020-11-21 Aina NiemetzRename floatingpoint.h.in -> floatingpoin.h. (#5500) blob | commitdiff | raw | diff to current
2020-11-19 Andrew ReynoldsAdd nested quantifier elimination module (#5422) blob | commitdiff | raw | diff to current
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) blob | commitdiff | raw | diff to current
2020-11-18 Andrew ReynoldsAdd let binding utility (#5444) blob | commitdiff | raw | diff to current
2020-11-13 Andrew Reynolds(proof-new) Enable proofs for datatypes (#5436) blob | commitdiff | raw | diff to current
2020-11-11 Andrew ReynoldsMove symbol manager to src/expr/ (#5420) blob | commitdiff | raw | diff to current
2020-11-10 Andrew ReynoldsMake mkGroundTerm deterministic (#5347) blob | commitdiff | raw | diff to current
2020-11-09 Andrew ReynoldsAdd symbol manager (#5380) blob | commitdiff | raw | diff to current
2020-11-06 Andrew ReynoldsSplit sygus template inference to its own file (#5388) blob | commitdiff | raw | diff to current
2020-11-03 Andrew ReynoldsMove sygus qe preproc to its own file (#5375) blob | commitdiff | raw | diff to current
2020-10-28 Gereon KremerSplit NlSolver in multiple subsolvers (#5315) blob | commitdiff | raw | diff to current
2020-10-28 Andrew ReynoldsAdd rewrites for div/mod in the arithmetic rewriter... blob | commitdiff | raw | diff to current
2020-10-21 Alex Ozdemir(proof-new) Add arith proof macros file to CMake (... blob | commitdiff | raw | diff to current
2020-10-21 mudathirmahgoubAdd operator MakeBagOp for constructing bags (#5209) blob | commitdiff | raw | diff to current
2020-10-20 Gereon Kremer(proof-new) Add proofs for circuit propagator (#5301) blob | commitdiff | raw | diff to current
2020-10-20 Andrew ReynoldsSplit CheckModels utility to its own file (#5303) blob | commitdiff | raw | diff to current
2020-10-16 Andrew ReynoldsAdd inference enumeration to datatypes (#5275) blob | commitdiff | raw | diff to current
2020-10-10 yoni206bv2int: bvand translation code move (#5227) blob | commitdiff | raw | diff to current
2020-10-07 Andrew Reynolds(proof-new) Add the strings proof constructor (#4903) blob | commitdiff | raw | diff to current
2020-10-06 Andrew Reynolds(proof-new) Add interface for trusted substitution... blob | commitdiff | raw | diff to current
2020-10-06 Andrew ReynoldsAdd arithmetic preprocess module (#5188) blob | commitdiff | raw | diff to current
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179) blob | commitdiff | raw | diff to current
2020-10-02 Andrew ReynoldsDecouple modules from TheoryArithPrivate (#5184) blob | commitdiff | raw | diff to current
2020-10-01 Andrew Reynolds(proof-new) Make arrays proof producing (#5112) blob | commitdiff | raw | diff to current
2020-09-30 Gereon KremerAdd strategy for nonlinear extension (#5160) blob | commitdiff | raw | diff to current
2020-09-29 Haniel Barbosa[proof-new] Adds a proof manager for prop engine (... blob | commitdiff | raw | diff to current
2020-09-29 Haniel Barbosa[proof-new] Adds a proof post processor for the Prop... blob | commitdiff | raw | diff to current
2020-09-29 Haniel Barbosa[proof-new] Adds a proof-producing CNF converter (... blob | commitdiff | raw | diff to current
2020-09-29 Alex OzdemirAdd utilities for arith/proof_checker and build it... blob | commitdiff | raw | diff to current
2020-09-28 Haniel Barbosa[proof-new] Adds a proof manager for the SAT solver... blob | commitdiff | raw | diff to current
2020-09-28 mudathirmahgoubImplement bags rewriter (#5132) blob | commitdiff | raw | diff to current
2020-09-28 Gereon KremerAdd new arithmetic BoundInference class (#5148) blob | commitdiff | raw | diff to current
2020-09-24 Andrew Reynolds Function definition fmf preprocessing pass (#5064) blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerAdd simple BV solver (#5065) blob | commitdiff | raw | diff to current
2020-09-22 mudathirmahgoubAdd skeleton for theory of bags (multisets) (#5100) blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... blob | commitdiff | raw | diff to current
2020-09-22 Gereon KremerICP-based solver for nonlinear arithmetic (#5017) blob | commitdiff | raw | diff to current
2020-09-21 Andrew Reynolds(proof-new) Add the arrays proof checker (#5047) blob | commitdiff | raw | diff to current
2020-09-18 Andrew ReynoldsAdd the shared solver (#4982) blob | commitdiff | raw | diff to current
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... blob | commitdiff | raw | diff to current
2020-09-15 Andrew ReynoldsMove quantifiers engine private to own file (#5053) blob | commitdiff | raw | diff to current
2020-09-15 Andrew ReynoldsStandard equality engine notify class for Theory (... blob | commitdiff | raw | diff to current
2020-09-15 Ying ShengInterpolation: Add implementation for SyGuS interpolati... blob | commitdiff | raw | diff to current
2020-09-12 Andrew Reynolds(proof-new) Add SMT proof manager (#5054) blob | commitdiff | raw | diff to current
2020-09-09 Andrew Reynolds(proof-new) Minor changes to proof node updater (#5011) blob | commitdiff | raw | diff to current
2020-09-09 Andrew ReynoldsSplit term registry from theory state in sets (#5037) blob | commitdiff | raw | diff to current
2020-09-04 Mathias PreinerSplit lazy bit-vector solver from TheoryBV (#5009) blob | commitdiff | raw | diff to current
2020-09-03 Gereon KremerBasic integration of arith::InferenceManager (#4999) blob | commitdiff | raw | diff to current
2020-09-03 FabianWolffDrop {INCLUDE,LIBRARY,RUNTIME}_INSTALL_DIR variables... blob | commitdiff | raw | diff to current
2020-09-03 Andrew ReynoldsMake ExtTheory independent of Theory (#5010) blob | commitdiff | raw | diff to current
2020-09-02 Abdalrhman MohamedIntroduce an internal version of Commands. (#4988) blob | commitdiff | raw | diff to current
2020-09-02 Andrew Reynolds(new theory) Update TheoryArrays to the new standard... blob | commitdiff | raw | diff to current
2020-09-02 Gereon KremerAdd ArithLemma and arith::InferenceManager (#4960) blob | commitdiff | raw | diff to current
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) blob | commitdiff | raw | diff to current
2020-09-01 Andrew ReynoldsAdd TheoryInference base class (#4990) blob | commitdiff | raw | diff to current
2020-09-01 Andrew ReynoldsAdd the inference manager for datatypes (#4968) blob | commitdiff | raw | diff to current
2020-08-28 Andrew ReynoldsAdd the buffered inference manager (#4954) blob | commitdiff | raw | diff to current
2020-08-27 Andrew Reynolds(proof-new) Add the proof equality engine (#4881) blob | commitdiff | raw | diff to current
2020-08-27 Andrew ReynoldsAdd the theory inference manager (#4948) blob | commitdiff | raw | diff to current
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... blob | commitdiff | raw | diff to current
2020-08-25 Andrew ReynoldsAdd the combination engine (#4939) blob | commitdiff | raw | diff to current
2020-08-24 Andrew ReynoldsAdd the distributed model manager (#4934) blob | commitdiff | raw | diff to current
2020-08-21 Andrew ReynoldsDynamic allocation of model equality engine (#4911) blob | commitdiff | raw | diff to current
2020-08-20 Andrew ReynoldsAdd TheoryState objects to each Theory (#4920) blob | commitdiff | raw | diff to current
2020-08-20 Andrew ReynoldsSplit QuantElimSolver from SmtEngine (#4919) blob | commitdiff | raw | diff to current
2020-08-18 Andrew ReynoldsIntroduce the theory state object (#4910) blob | commitdiff | raw | diff to current
2020-08-18 Andrew ReynoldsSplit SygusSolver from SmtEngine (#4891) blob | commitdiff | raw | diff to current
2020-08-18 Andrew ReynoldsAdd the relevance manager module (#4894) blob | commitdiff | raw | diff to current
2020-08-15 Andrew Reynolds(proof-new) Add the strings proof checker (#4858) blob | commitdiff | raw | diff to current
2020-08-13 Andrew ReynoldsSplit SmtSolver from SmtEngine (#4880) blob | commitdiff | raw | diff to current
2020-08-13 Andrew ReynoldsAdd the distributed equality engine manager (#4867) blob | commitdiff | raw | diff to current
2020-08-12 makaimannAdd option to only build library (#4801) blob | commitdiff | raw | diff to current
2020-08-12 Andrew Reynolds(proof-new) Witness form proof generator (#4782) blob | commitdiff | raw | diff to current
2020-08-12 Andrew ReynoldsSplit SmtEngineState from SmtEngine (#4855) blob | commitdiff | raw | diff to current
2020-08-09 Andrew ReynoldsSplitting a few utility classes from EqualityEngine... blob | commitdiff | raw | diff to current
2020-08-06 Andrew ReynoldsSplit preprocessor from SmtEngine (#4854) blob | commitdiff | raw | diff to current
2020-08-05 Andrew ReynoldsSplit Assertions from SmtEngine (#4788) blob | commitdiff | raw | diff to current
2020-08-04 Gereon KremerAdd CAD-based solver (#4834) blob | commitdiff | raw | diff to current
next