projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix combinations of cegqi and non-standard triggers (#4271)
[cvc5.git]
/
src
/
theory
/
quantifiers_engine.cpp
2020-03-11
Andrew Reynolds
Remove partial instantiation for local theory extension...
blob
|
commitdiff
|
raw
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
2016-12-07
ajreynol
Refactoring, generalization of bounded inference module...
blob
|
commitdiff
|
raw
|
diff to current
2016-12-02
Tim King
Merge pull request #95 from 4tXJ7f/fix_sierra_build
blob
|
commitdiff
|
raw
|
diff to current
2016-12-02
Clark Barrett
Merge pull request #113 from 4tXJ7f/remove_extract_rule
blob
|
commitdiff
|
raw
|
diff to current
2016-12-02
ajreynol
Refactor preprocessing of models in fmf. Fix options...
blob
|
commitdiff
|
raw
|
diff to current
2016-11-21
ajreynol
Refactoring related to track instantiation option.
blob
|
commitdiff
|
raw
|
diff to current
2016-11-03
ajreynol
Add priorities to getNextDecision. Properly handle...
blob
|
commitdiff
|
raw
|
diff to current
2016-10-28
ajreynol
Add get instantiations utilities to API.
blob
|
commitdiff
|
raw
|
diff to current
2016-10-11
Paul Meng
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
blob
|
commitdiff
|
raw
|
diff to current
2016-10-01
Tim King
Merge pull request #93 from timothy-king/clang-format
blob
|
commitdiff
|
raw
|
diff to current
2016-09-29
ajreynol
Address some coverity warnings, add another stat.
blob
|
commitdiff
|
raw
|
diff to current
2016-09-29
ajreynol
Minor cleanup and additions to quantifiers statistics.
blob
|
commitdiff
|
raw
|
diff to current
2016-09-15
ajreynol
Begin refactoring of cbqi, remove a few dead options...
blob
|
commitdiff
|
raw
|
diff to current
2016-09-15
ajreynol
Refactor setIncomplete in quantifiers.
blob
|
commitdiff
|
raw
|
diff to current
2016-09-14
ajreynol
Lemma cache in theory sep. Minor optimization for sets...
blob
|
commitdiff
|
raw
|
diff to current
2016-09-13
ajreynol
Minor changes to sep logic, epr, quantifier splitting.
blob
|
commitdiff
|
raw
|
diff to current
2016-09-12
ajreynol
Remove old implementation of cbqi
blob
|
commitdiff
|
raw
|
diff to current
2016-09-09
ajreynol
Support for separation logic + EPR. Refactor preprocess...
blob
|
commitdiff
|
raw
|
diff to current
2016-09-08
ajreynol
Refactor seplog preprocess. Handle case where sep data...
blob
|
commitdiff
|
raw
|
diff to current
2016-09-02
Tim King
Merge pull request #91 from timothy-king/no-throw
blob
|
commitdiff
|
raw
|
diff to current
2016-09-01
ajreynol
Cleanup quantifier elimination in smt engine.
blob
|
commitdiff
|
raw
|
diff to current
2016-09-01
ajreynol
Updates to cbqi. New strategy --cbqi-nested-qe to...
blob
|
commitdiff
|
raw
|
diff to current
2016-08-26
ajreynol
Basic support for EPR+CBQI. Minor cleanup.
blob
|
commitdiff
|
raw
|
diff to current
next