projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Minor fix for term database + central equality engine (#6928)
[cvc5.git] / src /
2021-07-27 Andrew ReynoldsMinor fix for term database + central equality engine... tree | commitdiff
2021-07-27 Andrew ReynoldsMake all dependencies in the fast enumerator optional... tree | commitdiff
2021-07-27 Andrew ReynoldsAdd print expression utility (#6880) tree | commitdiff
2021-07-27 Andrew ReynoldsMinor changes from proof-new (#6937) tree | commitdiff
2021-07-27 Andrew ReynoldsMiscellaneous fixes from proof-new (#6914) tree | commitdiff
2021-07-27 Andrew ReynoldsAdd proof letify utility (#6881) tree | commitdiff
2021-07-27 Andrew ReynoldsFix eq proof conversion for constant merged parameteriz... tree | commitdiff
2021-07-27 Andrew ReynoldsDefault equality proofs for bags and separation logic... tree | commitdiff
2021-07-27 Andrew ReynoldsAdd sygus enumerator callback (#6923) tree | commitdiff
2021-07-26 Gereon KremerMove public options functions to separate file (#6671) tree | commitdiff
2021-07-26 Andrew ReynoldsEnable default equality proofs for sets (#6931) tree | commitdiff
2021-07-26 Andrew ReynoldsMore updates to arithmetic in preparation for central... tree | commitdiff
2021-07-25 Andrew ReynoldsChanges to datatypes in preparation for central equalit... tree | commitdiff
2021-07-25 Andrew ReynoldsRefactor equality engine setup for arithmetic congruenc... tree | commitdiff
2021-07-23 Aina NiemetzFP: Add option to word-blast more lazily. (#6904) tree | commitdiff
2021-07-22 Andrew ReynoldsSimplify computation of relevant terms in datatypes... tree | commitdiff
2021-07-22 Andrew ReynoldsAdd the central equality engine manager (#6893) tree | commitdiff
2021-07-22 Andrew ReynoldsMiscellaneous changes in preparation for central equali... tree | commitdiff
2021-07-22 Andres NoetzliAdd support for minimal unsat cores (#4605) tree | commitdiff
2021-07-22 Andrew ReynoldsPreparation for carry the rewrite rule database in... tree | commitdiff
2021-07-22 mudathirmahgoubAdd std::vector<Term> Op:: getIndices() and operator... tree | commitdiff
2021-07-18 Andrew ReynoldsAdd n-ary term utilities (#6896) tree | commitdiff
2021-07-16 Andrew ReynoldsDo not exhaustive instantiation when FMF is disabled... tree | commitdiff
2021-07-15 Andrew ReynoldsFix context for proofs of instantiations (#6890) tree | commitdiff
2021-07-15 Andrew ReynoldsDistinguish quantifiers preprocess as its own proof... tree | commitdiff
2021-07-15 Andrew ReynoldsConnect the equality solver to theory arith (#6894) tree | commitdiff
2021-07-15 Andrew ReynoldsArithmetic equality solver (#6876) tree | commitdiff
2021-07-15 Andrew ReynoldsMove master equality engine notification to own file... tree | commitdiff
2021-07-15 Andrew ReynoldsAdd node converter utility (#6878) tree | commitdiff
2021-07-15 Mathias Preinerbv: Disable bv-assert-input if proofs are enabled.... tree | commitdiff
2021-07-15 Mathias Preinerbv: Rename BBSimple to NodeBitblaster. (#6891) tree | commitdiff
2021-07-15 Mathias Preinerbv: Rename lazy solver to layered solver. (#6889) tree | commitdiff
2021-07-15 Mathias Preinerbv: Rename simple solver to bitblast-internal. (#6888) tree | commitdiff
2021-07-14 Haniel Barbosa[proof] Fix open proof issues in SAT proof (#6887) tree | commitdiff
2021-07-14 Haniel BarbosaGeneralize congruence handling for HO in eq proofs... tree | commitdiff
2021-07-14 Andrew ReynoldsFix for context on input proof generator (#6873) tree | commitdiff
2021-07-14 Andrew ReynoldsMove synthesis verification check to own file (#6882) tree | commitdiff
2021-07-14 Andrew ReynoldsRefactor setup of proof equality engine for central... tree | commitdiff
2021-07-14 Andrew ReynoldsFix models for sequences of infinite element type ... tree | commitdiff
2021-07-14 Gereon KremerClean up option usage in command executor (#6844) tree | commitdiff
2021-07-14 Mathias PreinerAdd missing space for check macro error messages. ... tree | commitdiff
2021-07-14 Mathias Preinerbv: Add missing BV_EAGER_ATOM proof rule. (#6874) tree | commitdiff
2021-07-13 Mathias Preinerbv: Simplify BV_BITBLAST_* proof rules. (#6871) tree | commitdiff
2021-07-13 Haniel Barbosa[rewriter] Add rewrite to order IFF (equality for Boole... tree | commitdiff
2021-07-13 Mathias Preinerbv: Do not rewrite below BV leafs in BBProof's TConvPro... tree | commitdiff
2021-07-13 Andrew ReynoldsAdd branch and bound lemma if linear arithmetic generat... tree | commitdiff
2021-07-13 Mathias Preinerbv: Expand bitblast proof steps in the proof post proce... tree | commitdiff
2021-07-12 Andrew ReynoldsAdd branch and bound (#6865) tree | commitdiff
2021-07-12 Andrew ReynoldsFix for learned rewrite pass, add regression (#6850) tree | commitdiff
2021-07-12 Andrew ReynoldsAdd arithmetic preprocess rewrite equality module ... tree | commitdiff
2021-07-12 Andrew ReynoldsAdd trace for combination splits (#6862) tree | commitdiff
2021-07-12 Andres NoetzliUse default visibility for `cvc5::Exception` (#6856) tree | commitdiff
2021-07-12 Andrew ReynoldsImprovements to debug check model (#6861) tree | commitdiff
2021-07-09 Andrew ReynoldsFix sets cardinality inference involving equivalent... tree | commitdiff
2021-07-09 Andrew ReynoldsImplement stop-only for new justification heuristic... tree | commitdiff
2021-07-08 Andrew ReynoldsDisable ordering heuristic for justification by default... tree | commitdiff
2021-07-08 makaimannAdd script to build wheel for pycvc5 (#6839) tree | commitdiff
2021-07-08 Haniel Barbosa[proof] [dot] Print let map (of terms in proof) as... tree | commitdiff
2021-07-07 Aina NiemetzRename operator pow2 to int.pow2. (#6849) tree | commitdiff
2021-07-07 Andrew ReynoldsStandard output for trigger selection (#6841) tree | commitdiff
2021-07-06 Gereon KremerIntegrate Lazard into CAD module (#6812) tree | commitdiff
2021-07-06 Andrew ReynoldsIntegrate learned rewrite preprocessing pass (#6840) tree | commitdiff
2021-07-06 Andrew ReynoldsAdd implementation of learned rewrite pass (#6843) tree | commitdiff
2021-07-06 Andrew ReynoldsAdd learned rewrite preprocessing pass (#6842) tree | commitdiff
2021-07-06 OuyanchengAdd some printing functions for OptimizationObjective... tree | commitdiff
2021-07-05 Andres Noetzli[Strings] Fix incorrect rewrite (#6837) tree | commitdiff
2021-07-05 Andrew ReynoldsMake buffered inference manager more robust to backtrac... tree | commitdiff
2021-07-03 Andres NoetzliFix performance of string regression (#6832) tree | commitdiff
2021-07-03 Mathias PreinerAdd output tags -o, --output. (#6826) tree | commitdiff
2021-07-02 Mathias PreinerFix bv assert input reset assertions (#6820) tree | commitdiff
2021-07-02 Andrew ReynoldsFix rewriter for negative constant seq.nth (#6827) tree | commitdiff
2021-07-02 Andres NoetzliAdd reverse iterators to `Node`/`TNode` (#6825) tree | commitdiff
2021-07-01 Andrew ReynoldsAdd recursive function definitions to subsolver in... tree | commitdiff
2021-07-01 Andrew ReynoldsAdd option to limit the number of instantiation rounds... tree | commitdiff
2021-06-30 Mathias PreinerUse SAT context level for --bv-assert-input instead... tree | commitdiff
2021-06-30 Andrew ReynoldsDo not notify during equality engine initialization... tree | commitdiff
2021-06-30 Andrew ReynoldsDo not apply fmfBound to standard quantifiers when... tree | commitdiff
2021-06-30 Andrew ReynoldsFix pre vs. post-rewrite in proofs for theory preproces... tree | commitdiff
2021-06-30 yoni206int-to-bv: correct model values (#6811) tree | commitdiff
2021-06-29 Gereon KremerAdd new variants for the CAD projection (#6794) tree | commitdiff
2021-06-29 Mathias PreinerFix statistics in AigBitblaster. (#6810) tree | commitdiff
2021-06-29 Aina NiemetzFP: Refactor, rewrite and clean up word blasting. ... tree | commitdiff
2021-06-28 yoni206Rewrite POW to POW2 when the base is 2 (#6806) tree | commitdiff
2021-06-28 Andrew ReynoldsRename internal string kinds to match API (#6797) tree | commitdiff
2021-06-28 OuyanchengFurther fix #6453 (#6804) tree | commitdiff
2021-06-28 Haniel Barbosa[proof] [dot] Make dot printer stateful (#6799) tree | commitdiff
2021-06-26 yoni206pow2 -- final changes (#6800) tree | commitdiff
2021-06-25 yoni206pow2: Adding monotonicity lemma (#6793) tree | commitdiff
2021-06-24 Aina Niemetzapi: getRealValue: Fix printing of integer values.... tree | commitdiff
2021-06-24 Andrew ReynoldsFix linear arithmetic for duplicate lemmas in increment... tree | commitdiff
2021-06-24 Gereon KremerAdd CoCoA implementation (#6733) tree | commitdiff
2021-06-23 Haniel Barbosa[hol] Disable bound fmf when HOL (#6792) tree | commitdiff
2021-06-23 yoni206pow2: more implementations (#6756) tree | commitdiff
2021-06-23 Haniel Barbosa[proofs] [dot] Adding a counter for subproofs (#6735) tree | commitdiff
2021-06-23 Haniel Barbosa[parser] [hol] Fix parser check for allowing functions... tree | commitdiff
2021-06-23 Aina NiemetzFP: Remove sections guarded with undefined macro SYMFPU... tree | commitdiff
2021-06-23 Andres NoetzliRemove `--tear-down-incremental` (#6745) tree | commitdiff
2021-06-22 Andrew ReynoldsAvoid full normalization of lambdas in getValue (#6787) tree | commitdiff
2021-06-22 yoni206python api unit tests for Op (#6785) tree | commitdiff
2021-06-22 yoni206modular bv2int: Stubs and some implementations (#6760) tree | commitdiff
next