projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
(Refactor) Instantiate utility (#1387)
[cvc5.git]
/
src
/
theory
/
quantifiers
/
ce_guided_single_inv.h
2017-11-25
Andrew Reynolds
(Refactor) Instantiate utility (#1387)
blob
|
commitdiff
|
raw
2017-11-17
Andrew Reynolds
(Refactor) Document and clean single invocation partiti...
blob
|
commitdiff
|
raw
|
diff to current
2017-09-30
Andrew Reynolds
SyGuS streaming solution mode (#1131)
blob
|
commitdiff
|
raw
|
diff to current
2017-09-21
Andrew Reynolds
Sygus inv templ refactor (#1110)
blob
|
commitdiff
|
raw
|
diff to current
2017-07-10
ajreynol
Merge datatype shared selectors/sygus comp 2017 branch...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-07
Mathias Preiner
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2016-10-13
Tim King
Revert "Merge branch 'origin' of https://github.com...
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-26
Tim King
Adding a destructor to CegqiOutputSingleInv.
blob
|
commitdiff
|
raw
|
diff to current
2016-08-24
PaulMeng
Merge remote-tracking branch 'origin/master'
blob
|
commitdiff
|
raw
|
diff to current
2016-07-26
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2016-07-26
ajreynol
Add option to minimize sygus solutions based on using...
blob
|
commitdiff
|
raw
|
diff to current
2016-07-05
PaulMeng
Merge branch 'master' of https://github.com/CVC4/CVC4.git
blob
|
commitdiff
|
raw
|
diff to current
2016-04-20
PaulMeng
update from the master
blob
|
commitdiff
|
raw
|
diff to current
2016-04-10
ajreynol
More work on instantiation propagation. Enable external...
blob
|
commitdiff
|
raw
|
diff to current
2016-04-09
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2016-04-04
Tim King
Updating the copyright headers and scripts.
blob
|
commitdiff
|
raw
|
diff to current
2016-03-24
Tim King
Freeing CegConjecture::d_ceg_si. Also making d_ceg_si...
blob
|
commitdiff
|
raw
|
diff to current
2016-03-08
ajreynol
Extend synthesis solver to handle single invocation...
blob
|
commitdiff
|
raw
|
diff to current
2016-03-01
ajreynol
Shorter explanations for strings based on tracking...
blob
|
commitdiff
|
raw
|
diff to current
2015-12-02
ajreynol
Minor fixes for cegqi-si-partial.
blob
|
commitdiff
|
raw
|
diff to current
2015-12-02
Tim King
Merge pull request #79 from CVC4/fix-mac-build-script
blob
|
commitdiff
|
raw
|
diff to current
2015-12-01
ajreynol
More work on --cegqi-si-partial, incomplete.
blob
|
commitdiff
|
raw
|
diff to current
2015-11-28
ajreynol
Initial work on --cegqi-si-partial, refactoring.
blob
|
commitdiff
|
raw
|
diff to current
2015-11-26
ajreynol
Update to new implementation of single invocation parti...
blob
|
commitdiff
|
raw
|
diff to current
2015-11-26
ajreynol
Front-end support for get-value of sort cardinality...
blob
|
commitdiff
|
raw
|
diff to current
2015-11-25
ajreynol
Infrastructure for partially single invocation properti...
blob
|
commitdiff
|
raw
|
diff to current
2015-09-02
Kshitij Bansal
Merge remote-tracking branch 'origin/master'
blob
|
commitdiff
|
raw
|
diff to current
2015-08-28
ajreynol
Improvements to sygus, register equivalent terms based...
blob
|
commitdiff
|
raw
|
diff to current
2015-08-27
ajreynol
Do ITE term bookkeeping when solving Sygus inputs....
blob
|
commitdiff
|
raw
|
diff to current
2015-08-24
ajreynol
Improvements to vts in cbqi, bug fix vts for non-atomic...
blob
|
commitdiff
|
raw
|
diff to current
2015-08-19
ajreynol
Implementation of model-based projection in cbqi, clean...
blob
|
commitdiff
|
raw
|
diff to current
2015-07-30
ajreynol
Implement virtual term substitution for non-nested...
blob
|
commitdiff
|
raw
|
diff to current
2015-07-28
Tianyi Liang
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2015-07-25
ajreynol
Add option --sygus-inv-templ for synthesizing strengthe...
blob
|
commitdiff
|
raw
|
diff to current
2015-07-20
ajreynol
Squashed merge of SygusComp 2015 branch.
blob
|
commitdiff
|
raw
|
diff to current
2015-07-05
ajreynol
Add options --partial-triggers, --elim-taut-quant,...
blob
|
commitdiff
|
raw
|
diff to current
2015-07-02
ajreynol
On-demand upper bound lemmas for deltas in quantified...
blob
|
commitdiff
|
raw
|
diff to current
2015-05-29
ajreynol
Do not enforce dt fairness when single invocation sygus.
blob
|
commitdiff
|
raw
|
diff to current
2015-05-12
barrettcw
Merge pull request #74 from finnhaedicke/namespace_minisat
blob
|
commitdiff
|
raw
|
diff to current
2015-04-23
Clark Barrett
Merge branch 'master' into google
blob
|
commitdiff
|
raw
|
diff to current
2015-04-21
Clark Barrett
Changes needed to compile at Google, plus some bug...
blob
|
commitdiff
|
raw
|
diff to current
2015-04-17
Kshitij Bansal
Merge pull request #72 from kbansal/decision-requirephase
blob
|
commitdiff
|
raw
|
diff to current
2015-04-02
Kshitij Bansal
Merge pull request #71 from kbansal/const-are-triggers
blob
|
commitdiff
|
raw
|
diff to current
2015-04-01
ajreynol
Improvements and bug fixes related to cbqi/cegqi. ...
blob
|
commitdiff
|
raw
|
diff to current
2015-03-23
ajreynol
Decouple counter-example guided quantifier instantiatio...
blob
|
commitdiff
|
raw
|
diff to current
2015-03-11
ajreynol
Minor fixes and improvements to cegqi-si for linear...
blob
|
commitdiff
|
raw
|
diff to current
2015-03-05
ajreynol
Minor fixes. Extend cegqi-si to real arithmetic.
blob
|
commitdiff
|
raw
|
diff to current
2015-03-04
ajreynol
More work on arithmetic single invocation synthesis...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-26
ajreynol
Robust strategy for single invocation LIA synthesis...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-11
ajreynol
Better support for solving multiple functions with...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-11
ajreynol
Move si solution reconstruction to own file, make more...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-06
ajreynol
Handle missing cases for single inv solution reconstruc...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-06
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2015-02-05
ajreynol
Working version of sygus solution reconstruction from...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-04
ajreynol
Initial draft of solution reconstruction into syntax...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-04
ajreynol
Work on solution reconstruction for single inv. Fix...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-04
ajreynol
Refactor sygus_util to TermDb. Initial work on solutio...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-04
ajreynol
Start work on simplifying single inv solutions. Minor.
blob
|
commitdiff
|
raw
|
diff to current
2015-02-03
ajreynol
Simple variable elimination for single inv properties...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-02
ajreynol
Solutions for single invocation conjectures.
blob
|
commitdiff
|
raw
|
diff to current
2015-02-02
ajreynol
Single invocation module for counterexample guided...
blob
|
commitdiff
|
raw
|
diff to current