projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
More precise includes of `Node` constants (#6617)
[cvc5.git] / src / theory / uf /
2021-05-26 Andres Noetzli More precise includes of `Node` constants (#6617) tree | commitdiff
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611) tree | commitdiff
2021-05-20 Haniel BarbosaRemove old unsat cores (#6581) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-04-23 Andrew ReynoldsMove implementation of UF rewriter to cpp (#6393) tree | commitdiff
2021-04-21 Aina NiemetzUF: Move implementation of type rules to cpp. (#6403) tree | commitdiff
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) tree | commitdiff
2021-04-14 Gereon KremerRefactor / reimplement statistics (#6162) tree | commitdiff
2021-04-14 Aina NiemetzRename public and private headers in src/include. ... tree | commitdiff
2021-04-12 Andrew ReynoldsFix computation of whether a type is finite (#6312) tree | commitdiff
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) tree | commitdiff
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327) tree | commitdiff
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326) tree | commitdiff
2021-04-08 Andrew ReynoldsAdd identifiers for sources of incompleteness (#6311) tree | commitdiff
2021-04-07 Andrew ReynoldsSet incomplete if not applying ho extensionality (... tree | commitdiff
2021-04-07 Andrew Reynolds(proof-new) Proper implementation of proof node cloning... tree | commitdiff
2021-04-07 Andrew ReynoldsReplace calls to NodeManager::mkSkolem with SkolemManag... tree | commitdiff
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290) tree | commitdiff
2021-04-05 Haniel Barbosa[proof-new] Registering proof checkers uniformly from... tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-29 Andrew ReynoldsMove decision manager into theory inference manager... tree | commitdiff
2021-03-22 Andrew Reynolds Function types are always first-class (#6167) tree | commitdiff
2021-03-21 Andrew ReynoldsClean up remaining raw uses of output channel (#6161) tree | commitdiff
2021-03-20 Andrew ReynoldsImproved tracing for equivalence classes of EE (#6169) tree | commitdiff
2021-03-18 Andrew ReynoldsEliminate dependency on quantifiers engine in quantifie... tree | commitdiff
2021-03-12 Haniel Barbosa[proof-new] Fix arity check when building equality... tree | commitdiff
2021-03-11 Gereon KremerFirst refactoring of statistics classes (#6105) tree | commitdiff
2021-03-11 Aina NiemetzDelete Expr layer. (#6117) tree | commitdiff
2021-03-10 Aina NiemetzMove ExprManager::isNAryKind to NodeManager. (#6107) tree | commitdiff
2021-03-10 Andrew Reynolds(proof-new) Update ppRewrite to use skolem lemmas ... tree | commitdiff
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-24 Andrew ReynoldsAdd interface to TheoryState for sort inference and... tree | commitdiff
2021-02-19 Andrew ReynoldsRefactoring theory inference process (#5920) tree | commitdiff
2021-02-18 Gereon KremerAdd statistic for InferenceId to TheoryInferenceManager... tree | commitdiff
2021-02-17 Gereon KremerTheoryIds for UF theory. (#5901) tree | commitdiff
2021-02-11 Gereon KremerMake most methods of TheoryInferenceManager expect... tree | commitdiff
2021-02-02 Andrew ReynoldsCleanup some includes (#5847) tree | commitdiff
2020-12-10 Gereon KremerRefactor KindMap (#5646) tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-03 Gereon KremerUse mkAnd where the number of children may be less... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) tree | commitdiff
2020-11-23 Andrew ReynoldsChange UF ho to ppRewrite instead of expand definition... tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Separate explanation stages in proof equali... tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Fix true explanations of propagations in... tree | commitdiff
2020-10-24 Haniel Barbosa[proof-new] Fix n-ary kind handling in EqEngine explana... tree | commitdiff
2020-10-23 Andrew ReynoldsFix related to preregistering boolean term variables... tree | commitdiff
2020-10-22 Andrew ReynoldsRemove unused equality engine types (#5319) tree | commitdiff
2020-10-20 Aina NiemetzFix compiler warnings. (#5305) tree | commitdiff
2020-10-20 Andrew Reynolds(proof-new) Update add lazy step interface in LazyCDPro... tree | commitdiff
2020-10-20 Andrew ReynoldsFix miscellaneous warnings (#5256) tree | commitdiff
2020-10-12 Andrew ReynoldsRemove uf-ss-totality option (#5251) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-16 Haniel Barbosa[proof-new] Extending eqproof conversion to HO congruen... tree | commitdiff
2020-09-16 Haniel Barbosa[proof-new] A simple proof generator for buffered proof... tree | commitdiff
2020-09-16 Andrew Reynolds(proof-new) Make proofs mandatory in proof equality... tree | commitdiff
2020-09-15 Andrew ReynoldsStandard equality engine notify class for Theory (... tree | commitdiff
2020-09-14 Andrew ReynoldsStandardize uses of inference manager in datatypes... tree | commitdiff
2020-09-11 Andrew ReynoldsMove finite model minimization to UF last call effort... tree | commitdiff
2020-09-11 Andrew Reynolds(proof-new) Handle mismatched assumptions in proof... tree | commitdiff
2020-09-11 Andrew Reynolds(proof-new) Use deep copy for final lemma step in proof... tree | commitdiff
2020-09-10 Andrew ReynoldsUse state and inference manager in UF CardinalityExtens... tree | commitdiff
2020-09-04 Andrew ReynoldsAdd interfaces for making trust nodes in TheoryInferenc... tree | commitdiff
2020-09-02 Andrew Reynolds(proof-new) Add proof support in TheoryUF (#5002) tree | commitdiff
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) tree | commitdiff
2020-08-31 Andrew ReynoldsBasic proof support in inference manager (#4975) tree | commitdiff
2020-08-28 Andrew ReynoldsReplace Theory::Set with TheoryIdSet (#4959) tree | commitdiff
2020-08-27 Andrew Reynolds(proof-new) Add the proof equality engine (#4881) tree | commitdiff
2020-08-27 Andrew Reynolds(new theory) Update TheoryUF to new interface (#4944) tree | commitdiff
2020-08-24 Andrew ReynoldsAdd a few basic extensions for equality engine (#4937) tree | commitdiff
2020-08-24 Andrew ReynoldsExtend the standard Theory template based on equality... tree | commitdiff
2020-08-21 Andrew ReynoldsRemove spurious theory methods calls (#4931) tree | commitdiff
2020-08-21 Andrew ReynoldsSimplify and fix care graph for ufHo (#4924) tree | commitdiff
2020-08-20 Andrew ReynoldsAdd TheoryState objects to each Theory (#4920) tree | commitdiff
2020-08-20 Andrew ReynoldsSimplify trigger notifications in equality engine ... tree | commitdiff
2020-08-17 Andrew ReynoldsDynamic allocation of equality engine in Theory (#4890) tree | commitdiff
2020-08-14 Andrew ReynoldsSimplify equality engine notifications (#4896) tree | commitdiff
2020-08-13 Haniel Barbosa[proof-new] Adding support for corner case of transitiv... tree | commitdiff
2020-08-12 Haniel Barbosageneralize handling MERGED_THROUGH_CONSTANST in EqProof... tree | commitdiff
2020-08-12 Andrew Reynolds(proof-new) Improve robustness of CONG rule (#4882) tree | commitdiff
2020-08-12 Haniel Barbosa(proof-new) Improving proof-production in Equality... tree | commitdiff
2020-08-09 Andrew ReynoldsMake valuation class more robust to null underlying... tree | commitdiff
2020-08-09 Andrew ReynoldsSplitting a few utility classes from EqualityEngine... tree | commitdiff
2020-07-18 Haniel BarbosaImproving equality engine tracing (#4770) tree | commitdiff
2020-07-17 Haniel BarbosaFix EqProof to ProofNode conversion (#4760) tree | commitdiff
2020-07-16 Haniel Barbosa(proof-new) Implements the conversion between EqProof... tree | commitdiff
2020-07-16 Haniel Barbosa(proof-new) Adding API for converting EqProof into... tree | commitdiff
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-06-03 Haniel Barbosa(proof-new) Adding rules and proof checker for EUF... tree | commitdiff
2020-04-18 Haniel BarbosaImproving EqProof printing (#4329) tree | commitdiff
2020-04-14 Andrew ReynoldsRemove mergePredicates from EqualityEngine interface... tree | commitdiff
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) tree | commitdiff
2020-04-03 Andres NoetzliUpdate theory rewriter ownership, add stats to strings... tree | commitdiff
2020-04-02 Andres NoetzliInitialize theory rewriters in theories (#4197) tree | commitdiff
2020-03-20 Andrew ReynoldsGuard cases of sort inference in quantifier free logics... tree | commitdiff
next