projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Top-level structure for set defaults (#7047)
2021-08-24
Andrew Reynolds
Top-level structure for set defaults (#7047)
commit
|
commitdiff
|
tree
2021-08-24
Andrew Reynolds
Uniform treatment of trusted theory inferences in proofs...
commit
|
commitdiff
|
tree
2021-08-24
Andrew Reynolds
Miscellaneous changes from proof-new (#7042)
commit
|
commitdiff
|
tree
2021-08-23
Andrew Reynolds
Fix non-deterministism in quantified datatypes expansion...
commit
|
commitdiff
|
tree
2021-08-23
Andrew Reynolds
Purify substitutions in strings proof reconstruction...
commit
|
commitdiff
|
tree
2021-08-23
Andrew Reynolds
Generalize inequality elimination in quantifiers rewriter...
commit
|
commitdiff
|
tree
2021-08-23
Andrew Reynolds
Fix single invocation partition for higher-order (...
commit
|
commitdiff
|
tree
2021-08-22
Andrew Reynolds
Simplify model printing modes (#7049)
commit
|
commitdiff
|
tree
2021-08-22
Andrew Reynolds
Prenex quantified formulas with user annotations by...
commit
|
commitdiff
|
tree
2021-08-20
Andrew Reynolds
Simplify how user-provided quantifier attributes are...
commit
|
commitdiff
|
tree
2021-08-20
Andrew Reynolds
More refactoring of set defaults (#7043)
commit
|
commitdiff
|
tree
2021-08-20
Andrew Reynolds
Support sygus standard command syntax set-feature ...
commit
|
commitdiff
|
tree
2021-08-20
Andrew Reynolds
Eliminate eager model building (#7038)
commit
|
commitdiff
|
tree
2021-08-19
Andrew Reynolds
Catch cases where recursive functions reference functions...
commit
|
commitdiff
|
tree
2021-08-19
Andrew Reynolds
Split proof final callback to its own file (#6984)
commit
|
commitdiff
|
tree
2021-08-19
Andrew Reynolds
Refactor proof output for TPTP (#7029)
commit
|
commitdiff
|
tree
2021-08-18
Andrew Reynolds
Make TheoryProxy use Env, simplify initialization of...
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Make SmtEngineState use Env (#7028)
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Refactoring theory-specific variable elimination in...
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Fix policy for eliminating quantified formulas (#7017)
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Make theory BV use central eq engine when option is...
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Cosmetic improvements to theory datatypes (#7020)
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Improve conversion to skolems in expression miner ...
commit
|
commitdiff
|
tree
2021-08-17
Andrew Reynolds
Initial refactoring of set defaults (#7021)
commit
|
commitdiff
|
tree
2021-08-05
Andrew Reynolds
Generalize term canonizer for type classes (#6895)
commit
|
commitdiff
|
tree
2021-08-05
Andrew Reynolds
Fix policy for rewriting string equalities (#6916)
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Proper printing of proofs in the internal calculus...
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Fix policy for merging subproofs (#6981)
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Add inference ids for remainder of sygus solver (#6977)
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Add optional debug information for dumping instantiations...
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Add containsAssumption proof utility (#6953)
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Add missing inference identifiers (#6962)
commit
|
commitdiff
|
tree
2021-08-04
Andrew Reynolds
Remove dependencies on smt engine in smt solver (#6965)
commit
|
commitdiff
|
tree
2021-08-03
Andrew Reynolds
Refactor shared solver to use theory builtin inference...
commit
|
commitdiff
|
tree
2021-08-03
Andrew Reynolds
Remove "inUnsatCore" flag throughout (#6964)
commit
|
commitdiff
|
tree
2021-07-30
Andrew Reynolds
Simplify smt2 printer (#6954)
commit
|
commitdiff
|
tree
2021-07-29
Andrew Reynolds
Integrate central equality engine approach into theory...
commit
|
commitdiff
|
tree
2021-07-29
Andrew Reynolds
Minor updates to shared terms database for central...
commit
|
commitdiff
|
tree
2021-07-28
Andrew Reynolds
Minor changes to arrays in preparation for central...
commit
|
commitdiff
|
tree
2021-07-28
Andrew Reynolds
Make extended rewriter methods const (#6948)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Track instantiation reasons in proofs (#6935)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Add basic LFSC utilities (#6879)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Move enum value generator to own file (#6941)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Minor fix for term database + central equality engine...
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Revert change to regression (#6940)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Make all dependencies in the fast enumerator optional...
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Add print expression utility (#6880)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Minor changes from proof-new (#6937)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Miscellaneous fixes from proof-new (#6914)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Add proof letify utility (#6881)
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Fix eq proof conversion for constant merged parameterized...
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Default equality proofs for bags and separation logic...
commit
|
commitdiff
|
tree
2021-07-27
Andrew Reynolds
Add sygus enumerator callback (#6923)
commit
|
commitdiff
|
tree
2021-07-26
Andrew Reynolds
Enable default equality proofs for sets (#6931)
commit
|
commitdiff
|
tree
2021-07-26
Andrew Reynolds
More updates to arithmetic in preparation for central...
commit
|
commitdiff
|
tree
2021-07-25
Andrew Reynolds
Changes to datatypes in preparation for central equality...
commit
|
commitdiff
|
tree
2021-07-25
Andrew Reynolds
Refactor equality engine setup for arithmetic congruence...
commit
|
commitdiff
|
tree
2021-07-22
Andrew Reynolds
Simplify computation of relevant terms in datatypes...
commit
|
commitdiff
|
tree
2021-07-22
Andrew Reynolds
Add the central equality engine manager (#6893)
commit
|
commitdiff
|
tree
2021-07-22
Andrew Reynolds
Miscellaneous changes in preparation for central equality...
commit
|
commitdiff
|
tree
2021-07-22
Andrew Reynolds
Preparation for carry the rewrite rule database in...
commit
|
commitdiff
|
tree
2021-07-18
Andrew Reynolds
Add n-ary term utilities (#6896)
commit
|
commitdiff
|
tree
2021-07-16
Andrew Reynolds
Do not exhaustive instantiation when FMF is disabled...
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Fix context for proofs of instantiations (#6890)
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Distinguish quantifiers preprocess as its own proof...
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Connect the equality solver to theory arith (#6894)
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Arithmetic equality solver (#6876)
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Move master equality engine notification to own file...
commit
|
commitdiff
|
tree
2021-07-15
Andrew Reynolds
Add node converter utility (#6878)
commit
|
commitdiff
|
tree
2021-07-14
Andrew Reynolds
Fix for context on input proof generator (#6873)
commit
|
commitdiff
|
tree
2021-07-14
Andrew Reynolds
Move synthesis verification check to own file (#6882)
commit
|
commitdiff
|
tree
2021-07-14
Andrew Reynolds
Refactor setup of proof equality engine for central...
commit
|
commitdiff
|
tree
2021-07-14
Andrew Reynolds
Fix models for sequences of infinite element type ...
commit
|
commitdiff
|
tree
2021-07-13
Andrew Reynolds
Add branch and bound lemma if linear arithmetic generates...
commit
|
commitdiff
|
tree
2021-07-12
Andrew Reynolds
Add branch and bound (#6865)
commit
|
commitdiff
|
tree
2021-07-12
Andrew Reynolds
Fix for learned rewrite pass, add regression (#6850)
commit
|
commitdiff
|
tree
2021-07-12
Andrew Reynolds
Add arithmetic preprocess rewrite equality module ...
commit
|
commitdiff
|
tree
2021-07-12
Andrew Reynolds
Add trace for combination splits (#6862)
commit
|
commitdiff
|
tree
2021-07-12
Andrew Reynolds
Improvements to debug check model (#6861)
commit
|
commitdiff
|
tree
2021-07-09
Andrew Reynolds
Fix sets cardinality inference involving equivalent...
commit
|
commitdiff
|
tree
2021-07-09
Andrew Reynolds
Implement stop-only for new justification heuristic...
commit
|
commitdiff
|
tree
2021-07-08
Andrew Reynolds
Disable ordering heuristic for justification by default...
commit
|
commitdiff
|
tree
2021-07-07
Andrew Reynolds
Fix regressions for competition build (#6846)
commit
|
commitdiff
|
tree
2021-07-07
Andrew Reynolds
Standard output for trigger selection (#6841)
commit
|
commitdiff
|
tree
2021-07-06
Andrew Reynolds
Integrate learned rewrite preprocessing pass (#6840)
commit
|
commitdiff
|
tree
2021-07-06
Andrew Reynolds
Add implementation of learned rewrite pass (#6843)
commit
|
commitdiff
|
tree
2021-07-06
Andrew Reynolds
Add learned rewrite preprocessing pass (#6842)
commit
|
commitdiff
|
tree
2021-07-05
Andrew Reynolds
Make buffered inference manager more robust to backtracking...
commit
|
commitdiff
|
tree
2021-07-02
Andrew Reynolds
Fix rewriter for negative constant seq.nth (#6827)
commit
|
commitdiff
|
tree
2021-07-01
Andrew Reynolds
Add recursive function definitions to subsolver in...
commit
|
commitdiff
|
tree
2021-07-01
Andrew Reynolds
Add option to limit the number of instantiation rounds...
commit
|
commitdiff
|
tree
2021-06-30
Andrew Reynolds
Do not notify during equality engine initialization...
commit
|
commitdiff
|
tree
2021-06-30
Andrew Reynolds
Do not apply fmfBound to standard quantifiers when...
commit
|
commitdiff
|
tree
2021-06-30
Andrew Reynolds
Fix pre vs. post-rewrite in proofs for theory preprocessor...
commit
|
commitdiff
|
tree
2021-06-28
Andrew Reynolds
Rename internal string kinds to match API (#6797)
commit
|
commitdiff
|
tree
2021-06-24
Andrew Reynolds
Fix linear arithmetic for duplicate lemmas in incremental...
commit
|
commitdiff
|
tree
2021-06-22
Andrew Reynolds
Avoid full normalization of lambdas in getValue (#6787)
commit
|
commitdiff
|
tree
2021-06-22
Andrew Reynolds
Minor simplification to equality engine notifications...
commit
|
commitdiff
|
tree
2021-06-22
Andrew Reynolds
Always check legal eliminations in quantified logics...
commit
|
commitdiff
|
tree
2021-06-22
Andrew Reynolds
Fix type enumeration for non first-class sorts in FMF...
commit
|
commitdiff
|
tree
next