projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Refactor collection of debug and trace tags (#5996)
2021-02-26
Andrew Reynolds
Minor improvement and fix to smt2 printer (#6009)
commit
|
commitdiff
|
tree
2021-02-26
Andrew Reynolds
Optionally permit creation of non-flat function types...
commit
|
commitdiff
|
tree
2021-02-26
Andrew Reynolds
(proof-new) Fix regular expression unfolding under...
commit
|
commitdiff
|
tree
2021-02-25
Andrew Reynolds
Move slow regressions to regress1 (#5999)
commit
|
commitdiff
|
tree
2021-02-24
Andrew Reynolds
Add state and inference manager to inst match generator...
commit
|
commitdiff
|
tree
2021-02-24
Andrew Reynolds
Add interface to TheoryState for sort inference and...
commit
|
commitdiff
|
tree
2021-02-23
Andrew Reynolds
Explanation of failure for instantiate, use in enumerative...
commit
|
commitdiff
|
tree
2021-02-22
Andrew Reynolds
Eliminate raw use of output channel and valuation in...
commit
|
commitdiff
|
tree
2021-02-22
Andrew Reynolds
Move quantifiers attributes to quantifiers registry...
commit
|
commitdiff
|
tree
2021-02-22
Andrew Reynolds
(proof-new) Change proof-new option to proof (#5955)
commit
|
commitdiff
|
tree
2021-02-22
Andrew Reynolds
Require length-in-conclusion form for strings inferences...
commit
|
commitdiff
|
tree
2021-02-22
Andrew Reynolds
(proof-new) Option to automatically add SYMM steps...
commit
|
commitdiff
|
tree
2021-02-22
Andrew Reynolds
Fix datatypes inference manager when proofs are enabled...
commit
|
commitdiff
|
tree
2021-02-19
Andrew Reynolds
Simplify interface to instantiate (#5926)
commit
|
commitdiff
|
tree
2021-02-19
Andrew Reynolds
Fill in missing inference ids in datatypes theory ...
commit
|
commitdiff
|
tree
2021-02-19
Andrew Reynolds
Refactoring theory inference process (#5920)
commit
|
commitdiff
|
tree
2021-02-19
Andrew Reynolds
Fix rewrite for contains over replace (#5924)
commit
|
commitdiff
|
tree
2021-02-19
Andrew Reynolds
Remove string stat for inferences (#5932)
commit
|
commitdiff
|
tree
2021-02-18
Andrew Reynolds
Document UF inferences (#5917)
commit
|
commitdiff
|
tree
2021-02-18
Andrew Reynolds
Eliminate non-static members in term util (#5919)
commit
|
commitdiff
|
tree
2021-02-18
Andrew Reynolds
Move first order model for full model check to own...
commit
|
commitdiff
|
tree
2021-02-17
Andrew Reynolds
Move methods from term util to quantifiers registry...
commit
|
commitdiff
|
tree
2021-02-17
Andrew Reynolds
Compute fact or lemma in datatypes prior to buffering...
commit
|
commitdiff
|
tree
2021-02-13
Andrew Reynolds
Moving methods from quantifiers engine to quantifiers...
commit
|
commitdiff
|
tree
2021-02-12
Andrew Reynolds
Simplify and fix decision engine's handling of skolem...
commit
|
commitdiff
|
tree
2021-02-12
Andrew Reynolds
(proof-new) Option to not automatically consider symmetry...
commit
|
commitdiff
|
tree
2021-02-11
Andrew Reynolds
Fix spurious assertion failure in regexp normalization...
commit
|
commitdiff
|
tree
2021-02-11
Andrew Reynolds
Simplify interface for preprocessor (#5890)
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Refactor term registration visitors (#5875)
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Fix open proof for factoring lemma (#5885)
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Simplify method for inferring proxy lemmas in strings...
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Remove track instantiations infrastructure (#5883)
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Optimize get skolems method (#5876)
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Do not traverse quantifiers in term formula removal...
commit
|
commitdiff
|
tree
2021-02-09
Andrew Reynolds
Eliminating dependencies from inst utils (#5882)
commit
|
commitdiff
|
tree
2021-02-09
Andrew Reynolds
Make term database optionally SAT-context-dependent...
commit
|
commitdiff
|
tree
2021-02-08
Andrew Reynolds
Use quantifiers inference manager for lemma management...
commit
|
commitdiff
|
tree
2021-02-08
Andrew Reynolds
Fix disequality between seq.unit terms (#5880)
commit
|
commitdiff
|
tree
2021-02-08
Andrew Reynolds
Remove support for inst closure (#5874)
commit
|
commitdiff
|
tree
2021-02-08
Andrew Reynolds
Avoid spurious traversal of terms during preregistration...
commit
|
commitdiff
|
tree
2021-02-06
Andrew Reynolds
Do not combine theories if theory engine needs check...
commit
|
commitdiff
|
tree
2021-02-05
Andrew Reynolds
Minor cleaning of quantifiers engine (#5858)
commit
|
commitdiff
|
tree
2021-02-05
Andrew Reynolds
Miscellaneous cleaning in theory engine (#5854)
commit
|
commitdiff
|
tree
2021-02-04
Andrew Reynolds
Introduce quantifiers registry utility (#5829)
commit
|
commitdiff
|
tree
2021-02-04
Andrew Reynolds
Eliminate equality query dependence on quantifiers...
commit
|
commitdiff
|
tree
2021-02-02
Andrew Reynolds
(proof-new) Miscellaneous fixes and regressions (#5841)
commit
|
commitdiff
|
tree
2021-02-02
Andrew Reynolds
(proof-new) Refactor theory preprocessing (#5835)
commit
|
commitdiff
|
tree
2021-02-02
Andrew Reynolds
Remove quantifiers regression from decision folder...
commit
|
commitdiff
|
tree
2021-02-02
Andrew Reynolds
Cleanup some includes (#5847)
commit
|
commitdiff
|
tree
2021-02-02
Andrew Reynolds
Improvements for NL traces (#5846)
commit
|
commitdiff
|
tree
2021-02-01
Andrew Reynolds
Eliminate PREPROCESS lemma property (#5827)
commit
|
commitdiff
|
tree
2021-02-01
Andrew Reynolds
Simplify alpha equivalence module (#5839)
commit
|
commitdiff
|
tree
2021-01-30
Andrew Reynolds
Fix unguarded call to get representative (#5838)
commit
|
commitdiff
|
tree
2021-01-29
Andrew Reynolds
(proof-new) Distinguish pre vs post rewrites in term...
commit
|
commitdiff
|
tree
2021-01-28
Andrew Reynolds
Reorganize calls to quantifiers engine from SmtEngine...
commit
|
commitdiff
|
tree
2021-01-28
Andrew Reynolds
Simplify lemma interface (#5819)
commit
|
commitdiff
|
tree
2021-01-28
Andrew Reynolds
Use standard equality engine information in quantifiers...
commit
|
commitdiff
|
tree
2021-01-28
Andrew Reynolds
Always theory-preprocess lemmas (#5817)
commit
|
commitdiff
|
tree
2021-01-27
Andrew Reynolds
Add option for whether to filter candidate rewrite...
commit
|
commitdiff
|
tree
2021-01-27
Andrew Reynolds
Split pattern term selector from trigger (#5811)
commit
|
commitdiff
|
tree
2021-01-27
Andrew Reynolds
(proof-new) Improvements to quantifiers engine and...
commit
|
commitdiff
|
tree
2021-01-27
Andrew Reynolds
Use term canonizer utility locally in quantifiers ...
commit
|
commitdiff
|
tree
2021-01-27
Andrew Reynolds
Use standard conflict mechanism in quantifiers state...
commit
|
commitdiff
|
tree
2021-01-26
Andrew Reynolds
Introduce quantifiers inference manager (#5821)
commit
|
commitdiff
|
tree
2021-01-26
Andrew Reynolds
Remove deprecated quantifiers modules (#5820)
commit
|
commitdiff
|
tree
2021-01-26
Andrew Reynolds
Refactor quantifiers engine initialization (#5813)
commit
|
commitdiff
|
tree
2021-01-25
Andrew Reynolds
Ensure uses of ground terms in triggers are preprocessed...
commit
|
commitdiff
|
tree
2021-01-25
Andrew Reynolds
Split inst match generator into multiple files (#5805)
commit
|
commitdiff
|
tree
2021-01-25
Andrew Reynolds
Split E-matching strategies to own files (#5807)
commit
|
commitdiff
|
tree
2021-01-24
Andrew Reynolds
Initial cleaning of e-matching instantiation strategy...
commit
|
commitdiff
|
tree
2021-01-24
Andrew Reynolds
Initial cleaning of triggers (#5795)
commit
|
commitdiff
|
tree
2021-01-24
Andrew Reynolds
Initial cleaning of inst match generator (#5794)
commit
|
commitdiff
|
tree
2021-01-24
Andrew Reynolds
(proof-new) Instantiation list utility (#5768)
commit
|
commitdiff
|
tree
2021-01-24
Andrew Reynolds
Add interface for getting preprocessed term (#5798)
commit
|
commitdiff
|
tree
2021-01-21
Andrew Reynolds
Add div, mod, abs in non-strict parsing mode (#5793)
commit
|
commitdiff
|
tree
2021-01-20
Andrew Reynolds
Refactoring the single invocation solver (#5706)
commit
|
commitdiff
|
tree
2021-01-20
Andrew Reynolds
Fix type issues with relevant domain computation (...
commit
|
commitdiff
|
tree
2021-01-20
Andrew Reynolds
Fix corner case of wrongly applied selector as trigger...
commit
|
commitdiff
|
tree
2021-01-20
Andrew Reynolds
Do not track processed in remove term formulas loop...
commit
|
commitdiff
|
tree
2021-01-20
Andrew Reynolds
Use arbitrary ground term assignment for sorts where...
commit
|
commitdiff
|
tree
2021-01-15
Andrew Reynolds
Implement --no-strings-lazy-pp as a preprocessing pass...
commit
|
commitdiff
|
tree
2021-01-14
Andrew Reynolds
Updates to theory preprocess equality (#5776)
commit
|
commitdiff
|
tree
2021-01-13
Andrew Reynolds
Split eager solver from strings solver state (#5775)
commit
|
commitdiff
|
tree
2021-01-13
Andrew Reynolds
Do not call ppRewrite on Boolean equalities (#5762)
commit
|
commitdiff
|
tree
2021-01-11
Andrew Reynolds
Merge theory registrar and theory proxy (#5758)
commit
|
commitdiff
|
tree
2021-01-11
Andrew Reynolds
Further simplifications in preparation for removing...
commit
|
commitdiff
|
tree
2021-01-11
Andrew Reynolds
Remove extended rewrite for arithmetic (#5760)
commit
|
commitdiff
|
tree
2021-01-06
Andrew Reynolds
Add new interfaces to term formula removal and theory...
commit
|
commitdiff
|
tree
2021-01-05
Andrew Reynolds
Remove a few miscellaneous references to the expr layer...
commit
|
commitdiff
|
tree
2020-12-23
Andrew Reynolds
Add option to track and notify from CNF stream (#5708)
commit
|
commitdiff
|
tree
2020-12-23
Andrew Reynolds
Remove quant EPR option (#5716)
commit
|
commitdiff
|
tree
2020-12-23
Andrew Reynolds
(proof-new) Miscelleneous fixes from proof-new (#5714)
commit
|
commitdiff
|
tree
2020-12-23
Andrew Reynolds
Minor simplification to Theory::theoryOf (#5719)
commit
|
commitdiff
|
tree
2020-12-22
Andrew Reynolds
Move slow regression to regress3 (#5715)
commit
|
commitdiff
|
tree
2020-12-22
Andrew Reynolds
Make theory preprocess rewrite equalities a preprocessing...
commit
|
commitdiff
|
tree
2020-12-22
Andrew Reynolds
Remove preregister instantiation heuristic (#5713)
commit
|
commitdiff
|
tree
2020-12-21
Andrew Reynolds
Move ownership of theory preprocessor to TheoryProxy...
commit
|
commitdiff
|
tree
2020-12-21
Andrew Reynolds
Eliminate recursion from the internals of term formula...
commit
|
commitdiff
|
tree
2020-12-21
Andrew Reynolds
Fix issue with selector triggers (#5689)
commit
|
commitdiff
|
tree
2020-12-18
Andrew Reynolds
Simplify internal API for sygus (#5687)
commit
|
commitdiff
|
tree
next