projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
FloatingPoint: Separate out symFPU glue code. (#5492)
[cvc5.git]
/
src
/
theory
/
quantifiers_engine.cpp
2020-11-19
Andrew Reynolds
Enable new implementation of CEGQI based on nested...
blob
|
commitdiff
|
raw
2020-11-12
Andrew Reynolds
(proof-new) Proofs for skolemization (#5339)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-01
Mathias Preiner
Add additional ground terms to SyGuS instantiation...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-15
Andrew Reynolds
Move quantifiers engine private to own file (#5053)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-08
Andrew Reynolds
Eliminate a custom use of TheorySep in quantifiers...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-03
Andrew Reynolds
Minor cleanup of quantifiers engine (#4994)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-03
Andrew Reynolds
(proof-new) Support proofs of quantifier instantiation...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-01
FabianWolff
Fix spelling errors (#4977)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-26
Andrew Reynolds
Connect combination engine to theory engine (#4940)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-21
Andrew Reynolds
Connect the relevance manager to TheoryEngine and use...
blob
|
commitdiff
|
raw
|
diff to current
2020-08-18
Andrew Reynolds
Quantifiers engine stores a pointer to the master equal...
blob
|
commitdiff
|
raw
|
diff to current
2020-08-11
Andrew Reynolds
Remove instantiation model true option (#4861)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-28
Andrew Reynolds
Use lemma property enum for OutputChannel::lemma (...
blob
|
commitdiff
|
raw
|
diff to current
2020-07-14
Andrew Reynolds
Debug instantiations output (#4739)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-13
Andrew Reynolds
Statistics on instantiations per quantified formula...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-30
Andrew Reynolds
Simplify quantifiers strategy for when to apply last...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-16
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2020-04-21
Andrew Reynolds
Make option names related to CEGQI consistent (#4316)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-17
Mathias Preiner
SyGuS instantiation quantifiers module (#3910)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-15
Andrew Reynolds
Abort if in conflict in enumerative instantiation ...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-11
Andrew Reynolds
Remove partial instantiation for local theory extension...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Andrew Reynolds
Only register sygus terms to unfold if option is set...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Andrew Reynolds
Rename sygus option name (#3977)
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Andrew Reynolds
Remove instantiation propagator infrastructure (#3975)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-19
Andrew Reynolds
Delay enumerative instantiation if theory engine does...
blob
|
commitdiff
|
raw
|
diff to current
2020-02-14
Andrew Reynolds
Remove quantifiers rewrite rules infrastructure (#3754)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-27
Haniel Barbosa
Enable sygusRecFun by default and fixes SyGuS+RecFun...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-04
Andrew Reynolds
Make check synth solution robust to auxiliary assertion...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-04
Andrew Reynolds
Make getSynthSolution return a Bool (#3306)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-18
Andrew Reynolds
Decouple fmf-bound and finite-model-find (#3297)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-17
Andrew Reynolds
Encapsulate relevant domain (#3293)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-16
Andrew Reynolds
Remove equality inference option for quantifiers (...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-12
Andrew Reynolds
Encapsulate synth engine (#3271)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-12
Andrew Reynolds
Refactoring finite bounds in Quantifiers Engine (#3261)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-11
Andrew Reynolds
Infrastructure for instantiation rewriter (#3262)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-05
Andrew Reynolds
Refactoring CEGQI interface (#3239)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-17
Andrew Reynolds
Move quantifiers relevance module inside E-matching...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-12
Andrew Reynolds
Give rewrite engine pointer to conflict-based instanti...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-08
Andrew Reynolds
Reorganize includes for quantifiers engine (#3169)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-05
Andrew Reynolds
Remove forward declarations in quantifiers engine ...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-01
Andrew Reynolds
Move some generic utilities out of quantifiers (#3139)
blob
|
commitdiff
|
raw
|
diff to current
2019-03-26
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2018-12-11
Andrew Reynolds
Remove alternate versions of mbqi (#2742)
blob
|
commitdiff
|
raw
|
diff to current
2018-09-18
Andrew Reynolds
Move and rename sygus solver classes (#2488)
blob
|
commitdiff
|
raw
|
diff to current
2018-09-18
Andrew Reynolds
Clean remaining references to getNextDecisionRequest...
blob
|
commitdiff
|
raw
|
diff to current
2018-09-17
Andrew Reynolds
Move inst_strategy_cbqi to inst_strategy_cegqi (#2477)
blob
|
commitdiff
|
raw
|
diff to current
2018-09-10
Andrew Reynolds
Squash implementation of counterexample-guided instanti...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-28
Andrew Reynolds
Split term canonize utility to own file and document...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-25
Andrew Reynolds
Clean up quantifiers engine initialization. (#2371)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-22
Andrew Reynolds
More unused code elimination (#2358)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-21
Andrew Reynolds
More unused code elimination (#2339)
blob
|
commitdiff
|
raw
|
diff to current
2018-07-03
Andrew Reynolds
Remove miscellaneous dead and unused code from quantifi...
blob
|
commitdiff
|
raw
|
diff to current
2018-06-28
Andrew Reynolds
Split and document ceg theory instantiators (#2094)
blob
|
commitdiff
|
raw
|
diff to current
2018-06-26
Andrew Reynolds
Remove unnecessary code in register quantifier internal...
blob
|
commitdiff
|
raw
|
diff to current
2018-06-25
Aina Niemetz
Updated copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2018-06-01
Andrew Reynolds
Fix quantifiers conflict lemma handling (#2043)
blob
|
commitdiff
|
raw
|
diff to current
2018-06-01
Andrew Reynolds
Reduce before preregister. (#2025)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-30
Andrew Reynolds
Fixes for quantifiers + incremental (#2009)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-27
Andrew Reynolds
Fix cegqi assertions for quantified non-linear cases...
blob
|
commitdiff
|
raw
|
diff to current
2018-05-21
Andrew Reynolds
Refactor sygus eval unfold (#1946)
blob
|
commitdiff
|
raw
|
diff to current
2018-03-23
Andrew Reynolds
Remove unused code (#1700)
blob
|
commitdiff
|
raw
|
diff to current
2018-03-06
Andrew Reynolds
Simplify initialization of quantifiers engine (#1641)
blob
|
commitdiff
|
raw
|
diff to current
2018-02-14
Andrew Reynolds
Quantifiers subdirectories (#1608)
blob
|
commitdiff
|
raw
|
diff to current
2018-02-02
Haniel Barbosa
Option to check solutions produced by SyGuS solver...
blob
|
commitdiff
|
raw
|
diff to current
2017-12-08
Andrew Reynolds
Make collect model info return a Bool (#1421)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-25
Andrew Reynolds
(Refactor) Instantiate utility (#1387)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-15
Andrew Reynolds
Make QEffort an enum (#1366)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-09
Andrew Reynolds
Decouple sygus term database and term database. (...
blob
|
commitdiff
|
raw
|
diff to current
2017-11-02
Andrew Reynolds
(Move-only) Split quant util (#1306)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-01
Andrew Reynolds
(Refactor) Split term util (#1303)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-28
Andrew Reynolds
(Move only) Move enumerative instantiation strategy...
blob
|
commitdiff
|
raw
|
diff to current
2017-10-28
Andrew Reynolds
Document term db (#1220)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-27
Andrew Reynolds
Refactor theory model (#1236)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-10
Andres Noetzli
Fix memory leak in quantifiers engine (#1219)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-10
Andrew Reynolds
Split term database (#1206)
blob
|
commitdiff
|
raw
|
diff to current
2017-09-29
Andrew Reynolds
Simplify representation of inversion Skolems for bv...
blob
|
commitdiff
|
raw
|
diff to current
2017-09-27
Andrew Reynolds
Minor fixes for partial quantifier elimination. (#1147)
blob
|
commitdiff
|
raw
|
diff to current
2017-08-24
Andrew Reynolds
Merge pull request #191 from timothy-king/cleanup-regexp
blob
|
commitdiff
|
raw
|
diff to current
2017-08-17
ajreynol
Add mbqi interleave option, change option fs-inst to...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-21
Tim King
Merge branch 'master' into cleanup-regexp
blob
|
commitdiff
|
raw
|
diff to current
2017-07-21
Tim King
Moving from the gnu extensions for hash maps to the...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-07
Mathias Preiner
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2017-06-01
ajreynol
Minor optimizations related to cbqi.
blob
|
commitdiff
|
raw
|
diff to current
2017-05-17
Clark Barrett
Merge pull request #155 from makaimann/conditional_coverage
blob
|
commitdiff
|
raw
|
diff to current
2017-05-16
Andrew Reynolds
Merge pull request #156 from 4tXJ7f/fix_safe_print
blob
|
commitdiff
|
raw
|
diff to current
2017-05-15
Andrew Reynolds
Merge pull request #159 from 4tXJ7f/fix_set_types
blob
|
commitdiff
|
raw
|
diff to current
2017-05-15
Andrew Reynolds
Merge pull request #158 from 4tXJ7f/fix_sets_rewriter
blob
|
commitdiff
|
raw
|
diff to current
2017-05-15
Andrew Reynolds
Merge pull request #157 from 4tXJ7f/fix_iterator
blob
|
commitdiff
|
raw
|
diff to current
2017-05-15
ajreynol
Make conflict-based instantiation abort if a ground...
blob
|
commitdiff
|
raw
|
diff to current
2017-03-29
ajreynol
Add quantifiers options related to model and master...
blob
|
commitdiff
|
raw
|
diff to current
2017-03-27
Clark Barrett
Merge pull request #137 from 4tXJ7f/throw_quals
blob
|
commitdiff
|
raw
|
diff to current
2017-03-27
Tim King
Making ppNotifyAssertions take a const vector.
blob
|
commitdiff
|
raw
|
diff to current
2017-03-24
ajreynol
Refactor model building for quantifiers to be a single...
blob
|
commitdiff
|
raw
|
diff to current
2017-03-02
ajreynol
Eliminate Boolean term conversion. Generalizes removeIT...
blob
|
commitdiff
|
raw
|
diff to current
2017-02-16
ajreynol
Fixes for sets+rels check. Minor.
blob
|
commitdiff
|
raw
|
diff to current
2016-12-07
guykatzz
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
next