projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Refactor transcendental solver (#5514)
[cvc5.git] / src / theory / uf /
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
2020-03-16 Andres NoetzliCreate master equality engine at context level 0 (... tree | commitdiff
2020-03-12 Andrew ReynoldsFix double notify in equality engine (#4036) tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-27 Andrew ReynoldsInitial work towards -Wshadow (#3817) tree | commitdiff
2020-02-25 yoni206remove redundant includes (#3815) tree | commitdiff
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource... tree | commitdiff
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) tree | commitdiff
2019-12-09 Andres NoetzliMake theory rewriters non-static (#3547) tree | commitdiff
2019-11-18 Andres NoetzliUse -Wimplicit-fallthrough (#3464) tree | commitdiff
2019-11-04 Andrew ReynoldsFix ho extensionality in collect model info (#3435) tree | commitdiff
2019-10-31 Mathias PreinerFix Unimplemented() macros missed in #3366. (#3424) tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-10-27 Andrew ReynoldsFix collect model info for higher-order (#3409) tree | commitdiff
2019-09-19 Andrew ReynoldsSupport context-(in)dependent decision strategies.... tree | commitdiff
2019-09-13 Andrew ReynoldsMove higher-order matching predicate (#3280) tree | commitdiff
2019-09-12 Andrew Reynolds Rename UF with cardinality extension (#3241) tree | commitdiff
2019-07-08 Andrew ReynoldsTowards refactoring relations (#3078) tree | commitdiff
2019-07-02 Andrew ReynoldsUse unique_ptr for UF modules (#3080) tree | commitdiff
2019-07-01 Andrew Reynolds Split higher-order UF solver (#2890) tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-04-18 Andrew Reynolds Less aggressive caching in equality engine when proofs... tree | commitdiff
2019-04-17 Andrew ReynoldsCache explanations in the equality engine (#2937) tree | commitdiff
2019-04-17 Andrew ReynoldsMore use of isClosure (#2959) tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-15 Haniel BarbosaNew beta-reduction for HOL solving (#2869) tree | commitdiff
2019-03-15 Andrew ReynoldsFix non-variable function head elimination in UF. ... tree | commitdiff
2018-12-11 Andrew ReynoldsRemove alternate versions of mbqi (#2742) tree | commitdiff
2018-11-27 Andrew ReynoldsMake (T)NodeTrie a general utility (#2489) tree | commitdiff
2018-09-22 Mathias Preinercmake: Remove unused CMakeLists.txt tree | commitdiff
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure. tree | commitdiff
2018-09-17 Andrew ReynoldsDecision strategy: incorporate UF with cardinality... tree | commitdiff
2018-08-22 Andrew Reynolds More unused code elimination (#2358) tree | commitdiff
2018-08-21 Andrew ReynoldsMore unused code elimination (#2339) tree | commitdiff
2018-08-08 Andrew ReynoldsMove uf model code from uf to quantifiers (#2095) tree | commitdiff
2018-08-02 Andrew Reynolds Remove references to deprecated propagate as decision... tree | commitdiff
2018-07-06 Andrew ReynoldssygusComp2018: simplify beta reduction in uf rewriter... tree | commitdiff
2018-06-25 Aina NiemetzUpdated copyright headers. tree | commitdiff
2018-05-23 Andrew ReynoldsAdd notions of evaluated kinds in TheoryModel (#1947) tree | commitdiff
2018-04-30 Andrew ReynoldsRemove subsort symmetry breaking (#1807) tree | commitdiff
2018-04-11 Andrew ReynoldsProperly implement function extensionality based on... tree | commitdiff
2018-04-10 Andrew ReynoldsFix higher-order term indexing. (#1754) tree | commitdiff
2018-03-25 Andrew ReynoldsCleanup various exit calls (#1692) tree | commitdiff
2018-03-23 Andrew ReynoldsRemove unused code (#1700) tree | commitdiff
2018-03-07 Mathias PreinerMake statistics output consistent. (#1647) tree | commitdiff
2018-03-05 Mathias PreinerEnable -Wsuggest-override by default. (#1643) tree | commitdiff
2018-02-06 Tim KingResolving warnings from -Winconsistent-missing-override... tree | commitdiff
next